|
|
|---|
|
|
|
|---|
Log showing combinations of defun-modes and guard-checking
See guard-evaluation-examples-script for a script that shows the interaction of defun-modes with the value set by set-guard-checking. Here, we present a log resulting from running this script. It may also be helpful to see evaluation.
See set-guard-checking for discussion of the interaction between defun-modes and guard-checking that is illustrated by this script. Also see guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the interactions illustrated here.
ACL2 !>(defun fact (x) (declare (xargs :guard (integerp x) :mode :program)) (if (posp x) (* x (fact (1- x))) 1)) Summary Form: ( DEFUN FACT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 !>(trace$ fact) ((FACT)) ACL2 !>:set-guard-checking t Guard-checking-on already has value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the :program function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the :program function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard t :mode :program)) (if (posp x) (* x (fact (1- x))) 1)) Summary Form: ( DEFUN FACT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) ((FACT)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard (integerp x) :verify-guards nil :mode :logic)) (if (posp x) (* x (fact (1- x))) 1)) For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is [[output omitted here]] Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) ((FACT)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) [[Comment added to the log: Normally you would get a message about guard-checking being inhibited on recursive calls. However, when a function is traced the guard-checking is done on recursive calls unless the guards have been verified (see :DOC verify-guards). ]] 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) [[Comment added to the log: In spite of the warning above, guards are checked here on self-recursive calls, because the function is traced. ]] 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >(verify-guards fact) Computing the guard conjecture for FACT.... The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FACT. FACT is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FACT) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FACT ACL2 >(trace$ fact) ((FACT)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u L 1:x(DEFUN FACT (X) ...) ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard (integerp x) :mode :logic)) (if (posp x) (* x (fact (1- x))) 1)) For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is [[output omitted here]] Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) ((FACT)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC trace for a useful debugging utility. See :DOC set-guard- checking for information about suppressing this check with (set-guard- checking :none), as recommended for new users. ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard t :verify-guards nil :mode :logic)) (if (posp x) (* x (fact (1- x))) 1)) For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is [[output omitted here]] Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) ((FACT)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >(verify-guards fact) Computing the guard conjecture for FACT.... The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription rule FACT. FACT is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FACT) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT [[Note added to log: No need to trace fact again after verify-guards.]] ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all Leaving guard checking on, but changing value to :ALL. ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >