From 5e41515d75f198cc378a2a71cd02cd1c014ae5ff Mon Sep 17 00:00:00 2001
From: Alessandro Coglio
- An untranslated term is a term as entered by the user.
+ An untranslated @(see term) is a term as entered by the user.
This function checks @('x') by attempting to translate it.
- If the translation succeeds, the translated term is returned.
- Otherwise, a structured error message is returned (printable with @('~@')).
+ If the translation succeeds, the translated term is returned,
+ along with the output @(see stobj)s of the term (see below for details).
+ Otherwise, a structured error message is returned (printable with @('~@')),
+ along with @('nil') as output stobjs.
These two possible outcomes can be distinguished by the fact that
the former is a
+ The ‘output stobjs’ of a term are the analogous
+ of the @(tsee stobjs-out) property of a function,
+ namely a list of symbols that is like a “mask’ for the result.
+ A @('nil') in the list means that
+ the corresponding result is a non-stobj value,
+ while the name of a stobj in the list means that
+ the corresponding result is the named stobj.
+ The list is a singleton, unless the term returns
+
The @(':stobjs-out') and @('((:stobjs-out . :stobjs-out))') arguments
- passed to @('translate1-cmp')
+ passed to @('translate1-cmp') as bindings
mean that the term is checked to be valid for evaluation.
This is stricter than checking the term to be valid for use in a theorem,
and weaker than checking the term to be valid
@@ -288,7 +302,12 @@
should coincide.
- This function does not terminate
+ If @('translate1-cmp') is successful,
+ it should return updated bindings that associate @(':stobjs-out')
+ to the output stobjs of the term.
+
+ The @(tsee check-user-term) function does not terminate
if the translation expands an ill-behaved macro that does not terminate.
- An untranslated lambda expression is
+ An untranslated @(see lambda) expression is
a lambda expression as entered by the user.
This function checks whether @('x')is
a @('nil')-terminated list of exactly three elements,
@@ -320,25 +343,33 @@
and whose third element is an untranslated term that is valid for evaluation.
- If the check succeeds, the translated lambda expression is returned.
+ If the check succeeds, the translated lambda expression is returned,
+ along with the output @(see stobj)s of the body of the lambda expression
+ (see @(tsee check-user-term) for an explanation
+ of the output stobjs of a term).
Otherwise, a possibly structured error message is returned
- (printable with @('~@')).
+ (printable with @('~@')),
+ along with @('nil') as output stobjs.
- This function does not terminate
+ The @(tsee check-user-lambda-expr) function does not terminate
if @(tsee check-user-term) does not terminate.
The ‘output stobjs’ of a term are the analogous of the @(tsee stobjs-out) property of a function, - namely a list of symbols that is like a “mask’ for the result. + namely a list of symbols that is like a “mask” for the result. A @('nil') in the list means that the corresponding result is a non-stobj value, while the name of a stobj in the list means that @@ -303,7 +303,7 @@
If @('translate1-cmp') is successful, - it should return updated bindings that associate @(':stobjs-out') + it returns updated bindings that associate @(':stobjs-out') to the output stobjs of the term.
From ea7137ee5766cd03eab5786bfe2a25822fb7aee2 Mon Sep 17 00:00:00 2001
From: Alessandro Coglio
If successful, return @('t').
If unsuccessful or if an error occurs during the proof attempt,
- stop with an error message.
+ return a structured error message (printable with @('~@')).
If the @('verbose') argument is @('t'),
also print a progress message to indicate that
the proof of the applicability condition is being attempted,
- and then that it has been proved.
+ and then to indicate the outcome of the attempt.
Parentheses are printed around the progress message
@@ -92,30 +82,32 @@
(hints (applicability-condition->hints app-cond))
((run-when verbose)
(cw "(Proving applicability condition ~x0:~%~x1~|" name formula))
- ((mv erp yes/no state) (prove$ formula :hints hints))
- ((when erp)
- (applicability-condition-fail
- ctx
- "Prover error ~x0 when attempting to prove ~
- applicability condition ~x1:~%~x2~|."
- erp name formula)
- (mv nil state))
- ((unless yes/no)
- (applicability-condition-fail
- ctx
- "The applicability condition ~x0 fails:~%~x1~|"
- name formula)
- (mv nil state))
- ((run-when verbose)
- (cw "Done.)~%~%")))
- (mv t state)))
+ ((mv erp yes/no state) (prove$ formula :hints hints)))
+ (cond (erp (b* (((run-when verbose)
+ (cw "Prover error.)~%~%")))
+ (mv `("Prover error ~x0 ~
+ when attempting to prove ~
+ the applicability condition ~x1:~%~x2~|"
+ (#\0 . ,erp)
+ (#\1 . ,name)
+ (#\2 . ,formula))
+ state)))
+ (yes/no (b* (((run-when verbose)
+ (cw "Done.)~%~%")))
+ (mv t state)))
+ (t (b* (((run-when verbose)
+ (cw "Failed.)~%~%")))
+ (mv `("The applicability condition ~x0 fails:~%~x1~|"
+ (#\0 . ,name)
+ (#\1 . ,formula))
+ state))))))
(define prove-applicability-conditions
((app-conds applicability-condition-listp)
(verbose booleanp)
- (ctx "Context for errors.")
state)
- :returns (mv (yes/no booleanp)
+ :returns (mv (t/msg (or (eq t/msg t)
+ (msgp t/msg)))
state)
:prepwork ((program))
:short "Try to prove a list of applicability conditions, one after the other."
@@ -123,7 +115,7 @@
"
If successful, return @('t').
If unsuccessful or if an error occurs during a proof attempt,
- stop with an error message.
+ return a structured error message (printable with @('~@')).
If the @('verbose') argument is @('t'),
@@ -131,10 +123,12 @@
See also @(see must-fail).
@@ -98,9 +98,8 @@ theories, etc. to your books. Basic examples: ) }) -The @('form') should typically be a form that returns an @(see -error-triple), which is true for most top-level ACL2 events and other high -level commands.
+The @('form') should evaluate to an @(see error-triple), which is true for +most top-level ACL2 events and other high level commands.
The @('form') is submitted in a @(see make-event), which has a number of consequences. Most importantly, when @('form') is an event like a @(see diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp index f4a4ec145c1..1e62db0d87d 100644 --- a/books/system/doc/acl2-doc.lisp +++ b/books/system/doc/acl2-doc.lisp @@ -81820,6 +81820,14 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.
") commands that can be given inside the interactive @(see proof-builder) loop that is entered using @(tsee verify).") +(defxdoc proof-checker + :parents (proof-builder) + :short "Old name for @(see proof-builder)" + :long "See @(see proof-builder). Historically, this tool was misnamed the + ``proof-checker'', but since the tool is used for building and exploring (what + could be called) proofs rather than for checking them, its name was changed to + ``proof-builder'' in 2016.
") + (defxdoc proof-of-well-foundedness :parents (ordinals) :short "A proof that @(tsee o<) is well-founded on @(tsee o-p)s" @@ -109251,41 +109259,6 @@ introduction-to-the-tau-system) for more information about Tau. out of the wormhole and to do @(':')@(tsee brr) @('nil') in the external state when the next opportunity arises.") -(defxdoc with-brr-ens - :parents (break-rewrite brr-commands) - :short "Inside @(see break-rewrite), evaluate with respect to the theory - currently installed in the prover" - :long "@({ - Example Forms: - - (with-brr-ens (pe 'nth)) - (with-brr-ens (pl 'nth)) - (with-brr-ens (disabledp 'nth)) - - General Form: - - (with-brr-ens form) - }) - -where @('form') is any form that evaluates either to a single value, - @('val'), or to an @(see error-triple), @('(mv erp val state)'). The return - value — which might be irrelevant if the form is evaluated for - side-effect, such as a call of a @(see history) command such as @(tsee pe) or - @(tsee pl) — is @('(mv nil val state)') in the first case and also, if - @('erp') is @('nil'), in the second case.
- -At the @(':')@(see brr) prompt, evaluation of utilities such as - @(':')@(tsee pe) display whether or not a rule is globally @(see disable)d. - However, inside the @(see break-rewrite) loop one might wish to know instead - whether or not the rule is disabled at the current stage of the proof attempt - that is underway. The wrapper @('with-brr-ens') binds the so-called ``global - enabled structure'' to the corresponding structure that is currently installed - during the proof in progress, which will thus be used for @(see history) - queries such as @(tsee pe). In order to take advantage of this feature, you - must state the query as an ordinary expression, not as a keyword command (see - @(see keyword-commands)), for example as @('(with-brr-ens (pe 'nth))'), not as - @('(with-brr-ens :pe 'nth)').
") - (defxdoc with-fast-alist :parents (fast-alists acl2-built-ins) :short "@('(with-fast-alist name form)') causes @('name') to be a fast alist diff --git a/doc.lisp b/doc.lisp index aba74ca2d2e..cd51b0cfa62 100644 --- a/doc.lisp +++ b/doc.lisp @@ -12573,11 +12573,7 @@ Subtopics To stop monitoring a rule name [Why-brr] - An explanation of why ACL2 has an explicit [brr] mode - - [With-brr-ens] - Inside [break-rewrite], evaluate with respect to the theory - currently installed in the prover") + An explanation of why ACL2 has an explicit [brr] mode") (BREAKS (ERRORS) "Common Lisp breaks @@ -12853,14 +12849,7 @@ Subtopics does not apply, but instead, :poly-list shows the result of applying the linear lemma as a list of polynomials, implicitly conjoined. The leading term of each polynomial is enclosed in an - extra set of parentheses. - - -Subtopics - - [With-brr-ens] - Inside [break-rewrite], evaluate with respect to the theory - currently installed in the prover") + extra set of parentheses.") (BRR@ (BREAK-REWRITE) "To access context sensitive information within [break-rewrite] @@ -82202,6 +82191,9 @@ Subtopics [Proof-builder-commands] List of commands for the interactive proof-builder + [Proof-checker] + Old name for [proof-builder] + [Retrieve] Re-enter a (specified) [proof-builder] state @@ -82577,6 +82569,14 @@ Subtopics [ACL2-pc::x-dumb] (atomic macro) expand function call at the current subterm, without simplifying") + (PROOF-CHECKER + (PROOF-BUILDER) + "Old name for [proof-builder] + + See [proof-builder]. Historically, this tool was misnamed the + ``proof-checker'', but since the tool is used for building and + exploring (what could be called) proofs rather than for checking + them, its name was changed to ``proof-builder'' in 2016.") (PROOF-OF-WELL-FOUNDEDNESS (ORDINALS) "A proof that [o<] is well-founded on [o-p]s @@ -110132,40 +110132,6 @@ Subtopics user who has finally unmonitored all runes is therefore strongly advised to carry this information out of the wormhole and to do :[brr] nil in the external state when the next opportunity arises.") - (WITH-BRR-ENS - (BREAK-REWRITE BRR-COMMANDS) - "Inside [break-rewrite], evaluate with respect to the theory currently - installed in the prover - - Example Forms: - - (with-brr-ens (pe 'nth)) - (with-brr-ens (pl 'nth)) - (with-brr-ens (disabledp 'nth)) - - General Form: - - (with-brr-ens form) - - where form is any form that evaluates either to a single value, val, - or to an [error-triple], (mv erp val state). The return value --- - which might be irrelevant if the form is evaluated for side-effect, - such as a call of a [history] command such as [pe] or [pl] --- is - (mv nil val state) in the first case and also, if erp is nil, in - the second case. - - At the :[brr] prompt, evaluation of utilities such as :[pe] display - whether or not a rule is globally [disable]d. However, inside the - [break-rewrite] loop one might wish to know instead whether or not - the rule is disabled at the current stage of the proof attempt that - is underway. The wrapper with-brr-ens binds the so-called ``global - enabled structure'' to the corresponding structure that is - currently installed during the proof in progress, which will thus - be used for [history] queries such as [pe]. In order to take - advantage of this feature, you must state the query as an ordinary - expression, not as a keyword command (see [keyword-commands]), for - example as (with-brr-ens (pe 'nth)), not as (with-brr-ens :pe - 'nth).") (WITH-FAST-ALIST (FAST-ALISTS ACL2-BUILT-INS) "(with-fast-alist name form) causes name to be a fast alist for the From 8112a686337c6158cf8f8768b49fa118b09d11bb Mon Sep 17 00:00:00 2001 From: Alessandro Coglio+ This is 1, unless the function uses @(tsee mv) + (directly, or indirectly by calling another function that does) + to return multiple values. +
++ The number of results of the function + is the length of its output @(see stobj) list. + But the function must not be in @('*stobjs-out-invalid*'), + because in that case the number of its results depends on how it is called. +
" + (len (stobjs-out fn wrld)) + :guard-hints (("Goal" :in-theory (enable function-namep)))) + (define no-stobjs-p ((fn (function-namep fn wrld)) (wrld plist-worldp)) :guard (not (member-eq fn *stobjs-out-invalid*)) :returns (yes/no booleanp) From f5b999c07e6a2d02868d9f3f84f8fb613927bb9e Mon Sep 17 00:00:00 2001 From: Shilpi GoelFor example:
@({ diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp index 1e62db0d87d..a94cad2e17d 100644 --- a/books/system/doc/acl2-doc.lisp +++ b/books/system/doc/acl2-doc.lisp @@ -97803,6 +97803,13 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") (list (car pair) (cdr pair))))) }) +- If successful, return @('t'). - If unsuccessful or if an error occurs during the proof attempt, - return a structured error message (printable with @('~@')). + Besides returning an indication of success, + return a structured message (printable with @('~@')). + When the proof fails, the message is an error message. + When the proof succeeds, currently the message is empty, + but future versions of this code could return an informative message instead. +
++ If an error occurs during the proof attempt, + the proof is regarded as having failed.
If the @('verbose') argument is @('t'), @@ -85,7 +91,8 @@ ((mv erp yes/no state) (prove$ formula :hints hints))) (cond (erp (b* (((run-when verbose) (cw "Prover error.)~%~%"))) - (mv `("Prover error ~x0 ~ + (mv nil + `("Prover error ~x0 ~ when attempting to prove ~ the applicability condition ~x1:~%~x2~|" (#\0 . ,erp) @@ -94,10 +101,11 @@ state))) (yes/no (b* (((run-when verbose) (cw "Done.)~%~%"))) - (mv t state))) + (mv t "" state))) (t (b* (((run-when verbose) (cw "Failed.)~%~%"))) - (mv `("The applicability condition ~x0 fails:~%~x1~|" + (mv nil + `("The applicability condition ~x0 fails:~%~x1~|" (#\0 . ,name) (#\1 . ,formula)) state)))))) @@ -106,29 +114,33 @@ ((app-conds applicability-condition-listp) (verbose booleanp) state) - :returns (mv (t/msg (or (eq t/msg t) - (msgp t/msg))) + :returns (mv (success booleanp) + (msg msgp) state) :prepwork ((program)) :short "Try to prove a list of applicability conditions, one after the other." :long "
- If successful, return @('t'). - If unsuccessful or if an error occurs during a proof attempt, - return a structured error message (printable with @('~@')). + Besides returning an indication of success, + return a structured message (printable with @('~@')). + When the proof of an applicability condition fails, + the message is the error message generated by that proof attempt. + When all the proofs of the applicability conditions succeed, + currently the message is empty, + but future versions of this code could return an informative message instead.
If the @('verbose') argument is @('t'), also print progress messages for the applicability conditions.
" - (cond ((endp app-conds) (mv t state)) + (cond ((endp app-conds) (mv t "" state)) (t (b* ((app-cond (car app-conds)) - ((mv t/msg state) + ((mv success msg state) (prove-applicability-condition app-cond verbose state))) - (if (eq t/msg t) + (if success (prove-applicability-conditions (cdr app-conds) verbose state) - (mv t/msg state)))))) + (mv nil msg state)))))) (define applicability-condition-event ((app-cond applicability-condition-p) From 9fe1bde126070d144182fa9e673f556b49d340bf Mon Sep 17 00:00:00 2001 From: Alessandro CoglioNOTE! New users can ignore these release notes, because the @(see @@ -73830,6 +73852,16 @@ it." (verify-termination foo) ; formerly failed }) +
To evaluate a form @('(set-iprint t :hard-bound N)'), ACL2 will first + replace @('t') by @(':reset-enable'). This behavior has been expanded to + apply to @('(set-iprint nil :hard-bound N)') and @('(set-iprint :same + :hard-bound N)') as well: the first argument will be converted to @(':reset') + or @(':reset-enable'). See @(see set-iprint). This change fixes a bug in the + interaction between hard-bounds and rollovers. For an example that formerly + exhibited this bug, see a comment about ``hard-bounds and rollovers'' in + @('(defxdoc note-7-3 ...)') in community book + @('books/system/doc/acl2-doc.lisp').
+New optional arguments allow the @(tsee pso) utility to restrict output to @@ -73866,6 +73898,10 @@ it." which behaves like @('~s') except that margins are ignored. Thanks to Jared Davis for requesting this feature.
+The iprinting utility has a new keyword option, @(':share'), which causes + iprint indices to be re-used. See @(see set-iprint). Thanks to David Rager + for suggesting such an enhancement.
+The raw-Lisp definition of @(tsee defpkg) has been modified in a way that @@ -91253,6 +91289,48 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.
") ACL2 !> }) +You might wish to know which elided expressions are equal. You may specify + keyword argument @(':share t') for that purpose to turn on ``iprint sharing'', + which causes behavior as shown below: the value printed shows the iprint index + 2 being used twice for the list @('(C D E F)').
+ + @({ + ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) + ((A B . #@2#) (A B . #@2#) . #@3#) + ACL2 !> + }) + +Remark (feel free to skip this paragraph). To understand more fully how + iprint sharing works, consider the following log. The Warning below is + pointing out that previous iprint indices are no longer valid; we are starting + over. The first Observation points out that iprint sharing is on, and gives + the name @(':IPRINT-FAL') to look for in @('(fast-alist-summary)') in case you + want information on the @(see fast-alist) that associates values with + corresponding iprint indices. To see the relevance of a fast-alist, note that + the two elided occurrences of the list @('(C D E F)') were originally not the + identical list in memory; to make them identical, @(tsee hons-copy) is applied + to each to get the same list in memory, which is the one associated with + iprint index 2 in a fast-alist named @(':IPRINT-FAL').
+ + @({ + ACL2 !>(set-iprint t :share t) + + ACL2 Warning [Iprint] in SET-IPRINT: Converting SET-IPRINT action + from T to :RESET-ENABLE, as required by use of keyword :SHARE or :HARD- + BOUND. See :DOC set-iprint. + + + ACL2 Observation in SET-IPRINT: Iprinting is enabled with sharing, + with a fast-alist whose name is :IPRINT-FAL. + + ACL2 Observation in SET-IPRINT: Iprinting has been reset and enabled. + ACL2 !>(set-evisc-tuple (evisc-tuple 2 2 nil nil) :sites :all) + (:TERM :LD . #@1#) + ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) + ((A B . #@2#) (A B . #@2#) . #@3#) + ACL2 !> + }) +The documentation above probably suffices for most users. For those who want more details, below we detail all the ways to use the @('set-iprint') utility.
@@ -91263,21 +91341,26 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") (set-iprint nil) ; disable iprinting General Form: - (set-iprint action ; t, nil, :reset, :reset-enable, or :same - :soft-bound s ; initially 1000 - :hard-bound h ; initially 10000) + (set-iprint action ; t, nil, :reset, :reset-enable, or :same + :share sym ; initially nil + :soft-bound s ; initially 1000 + :hard-bound h ; initially 10000) })where all arguments are optional, but ACL2 queries for @('action') if it is - omitted. We defer the explanations of @(':soft-bound') and @(':hard-bound'). - The values for @('action') are as follows:
+ omitted. All arguments are evaluated. When a keyword argument is omitted, + there is no change in the behavior that it controls. For now we defer further + explanations of the keyword arguments. The values for @('action') are as + follows.-+@('t') — Enable iprinting. If keyword @(':hard-bound') is supplied, - then @('t') is converted to @(':reset-enable').
+@('t') — Enable iprinting. If either keyword @(':share') or + @(':hard-bound') is supplied, then @('t') is converted to + @(':reset-enable').
-@('nil') — Disable iprinting.
+@('nil') — Disable iprinting. If either keyword @(':share') or + @(':hard-bound') is supplied, then @('nil') is converted to @(':reset').
@(':reset') — Reset iprinting to its initial disabled state, so that when enabled, the first index @('i') for which `@('#@i#') is printed will be @@ -91287,32 +91370,55 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.
")@(':reset-enable') — Reset iprinting as with @(':reset'), and then enable iprinting.
-@(':same') — Make no change to the iprinting state (other than - setting the @(':soft-bound') and/or @(':hard-bound') if specified, as - explained below).
@(':same') — If either keyword @(':share') or @(':hard-bound') is + supplied, then @(':same') is converted to @(':reset') or @(':reset-enable') + according to whether iprinting is currently disabled or enabled, respectively. + Otherwise, make no change to the iprinting state other than setting the + @('soft-bound') if specified, as explained below.
+ + + +The value of @(':share') must be a symbol, with default @('nil'). If the + value is @('nil'), then an elided value will be printed using the next + available iprint index. The value @(':same') is treated as though @(':share') + had not been supplied. Otherwise, iprint sharing is on, which provides the + following behavior. Suppose that a value @('V') is to be elided that would be + assigned the next available iprint index, @('N'). If an iprint index @('I < + N') is already associated with a value equal to @('V'), then ACL2 will print + @('#@I') for @('V') instead of @('#@N'). Thus, @('N') will remain the next + available iprint index. This behavior is implementing using a @(see + fast-alist) that associates values with indices; in our example, the @(tsee + hons-copy) of @('V') is associated with @('I'). If the value of @(':share') + is @('t') then the name of this fast-alist — that is, its initial value + — is @(':iprint-fal'); otherwise, the value of @(':share') (other than + @('nil') or @(':same') is its name. This name is useful when viewing the + output of @(tsee fast-alist-summary).
Immediately after a top-level form is read, hence before it is evaluated, a check is made for whether the latest iprint index exceeds a certain bound, @('(iprint-soft-bound state)') — 1000, by default. If so, then the - @('(iprint-last-index state)') is set back to 0. This soft bound can be - changed to any positive integer @('k') by calling @('set-iprint') with - @(':soft-bound k'), typically @('(set-iprint :same :soft-bound k'))].
+ @('(iprint-last-index state)') is set back to 0 so that the next iprint index + that is generated will be 1. This soft bound can be changed to any positive + integer @('k') by calling @('set-iprint') with @(':soft-bound k'), for + example: @('(set-iprint :same :soft-bound k'))].The above ``soft bound'' is applied once for each top-level form, but you may want finer control by applying a bound after the pretty-printing of each individual form (since many forms may be pretty-printed between successive evaluations of top-level forms). That bound is @('(iprint-hard-bound state)'), and can be set with the @(':hard-bound') argument in analogy to how - @(':soft-bound') is set, as described above.
+ @(':soft-bound') is set, as described above, but with the effect of resetting + iprinting, with @('(iprint-last-index state)') set back to 0.A ``rollover'' is the detection that the soft or hard bound has been - exceeded, along with a state update so that the next iprint index will be 1. - When a rollover occurs, any index beyond the latest iprint index is no longer - available for reading. At the top level of the ACL2 read-eval-print loop, - this works as follows: ACL2 reads the next top-level form according to the - current iprint state, then handles a rollover if the latest iprint index - exceeded the current soft bound. The following log illustrates a rollover, - which follows the description above.
+ exceeded, along with a state update setting @('(iprint-last-index state)') to + 0 so that the next iprint index will be 1. Immediately before a rollover, any + index beyond the last iprint index used (which must be from before an earlier + rollover) is no longer available for reading. At the top level of the ACL2 + read-eval-print loop, this works as follows: ACL2 reads the next top-level + form according to the current iprint state, then handles a rollover if the + latest iprint index exceeded the current soft bound. The following log + illustrates a rollover, which follows the description above. @({ ACL2 !>(set-iprint t :soft-bound 3) @@ -91346,7 +91452,8 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") Error: Out-of-bounds index in #@5#. See :DOC set-iprint. *********************************************** - If you didn't cause an explicit interrupt (Control-C), + The message above might explain the error. If not, and + if you didn't cause an explicit interrupt (Control-C), then the root cause may be call of a :program mode function that has the wrong guard specified, or even no guard specified (i.e., an implicit guard of t). @@ -91357,6 +91464,58 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") ACL2 !> }) +Rollover has the following additional effect when iprint sharing is on: it + is illegal to read a form that has both an index from before the rollover and + an index from after the rollover. The following log illustrates this + requirement. Note that if the last input form below were read without error, + the result would likely be highly confusing, since iprint index 1 no longer + refers to the value it was originally given at the time the other iprint + indices in the input (2, 3, and 4) were given their values.
+ + @({ + ACL2 !>(set-iprint t :soft-bound 3 :share t) + + ACL2 Warning [Iprint] in SET-IPRINT: Converting SET-IPRINT action + from T to :RESET-ENABLE, as required by use of keyword :SHARE or :HARD- + BOUND. See :DOC set-iprint. + + + ACL2 Observation in SET-IPRINT: The soft-bound for iprinting has been + set to 3. + + ACL2 Observation in SET-IPRINT: Iprinting is enabled with sharing, + with a fast-alist whose name is :IPRINT-FAL. + + ACL2 Observation in SET-IPRINT: Iprinting has been reset and enabled. + ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld) + (:LD) + ACL2 !>'((a b c d) (x y z w)) + ((A B C . #@1#) (X Y Z . #@2#)) + ACL2 !>'((e f g h) (k l m n)) + ((E F G . #@3#) (K L M . #@4#)) + ACL2 !>'(#@1# #@2# #@3# #@4#) ; OK, since rollover occurs after the read + ((D) (W) (H) . #@1#) + ACL2 !>'(#@1# #@2# #@3# #@4#) + + *********************************************** + ************ ABORTING from raw Lisp *********** + Error: Attempt to read a form containing both an index + created before the most recent rollover (#@2#) and + an index created after that rollover (#@1#). See :DOC set-iprint. + *********************************************** + + The message above might explain the error. If not, and + if you didn't cause an explicit interrupt (Control-C), + then the root cause may be call of a :program mode + function that has the wrong guard specified, or even no + guard specified (i.e., an implicit guard of t). + See :DOC guards. + + To enable breaks into the debugger (also see :DOC acl2-customization): + (SET-DEBUGGER-ENABLE T) + ACL2 !> + }) +We conclude by mentioning two cases where iprinting and evisc-tuples are
ignored. (1) This is typically the case when printing results in raw Lisp
outside the ACL2 loop. To use iprinting and evisc-tuples in raw Lisp, use
diff --git a/history-management.lisp b/history-management.lisp
index 7f914a44d1c..b94989d019e 100644
--- a/history-management.lisp
+++ b/history-management.lisp
@@ -3700,6 +3700,7 @@
gag-mode-evisc-tuple ;;; see just above
slow-array-action ;;; see just above
iprint-ar ;;; see just above
+ iprint-fal ;;; see just above
iprint-soft-bound ;;; see just above
iprint-hard-bound ;;; see just above
show-custom-keyword-hint-expansion
diff --git a/hons-raw.lisp b/hons-raw.lisp
index 20a201681ef..4babdde36d5 100644
--- a/hons-raw.lisp
+++ b/hons-raw.lisp
@@ -1138,7 +1138,7 @@
(18cdrs (cddr 16cdrs)))
(consp 18cdrs)))))))))
-(defabbrev hl-flex-assoc (key al)
+(defmacro hl-flex-assoc (key al)
; (hl-flex-assoc key al) returns the entry associated with key, or returns nil
; if key is not bound. Note that the comparisons performed by flex-assoc are
@@ -1172,9 +1172,11 @@
; NIL
; ?
- (if (listp al)
- (assoc key al)
- (gethash key (the hash-table al))))
+ `(let ((key ,key)
+ (al ,al))
+ (if (listp al)
+ (assoc key al)
+ (gethash key (the hash-table al)))))
(defmacro hl-flex-acons (elem al &optional shared)
@@ -1245,7 +1247,7 @@
(= 1 (the fixnum (aref sbits (the fixnum idx)))))))))
#-static-hons
-(defabbrev hl-hspace-find-flex-alist-for-cdr (b ctables)
+(defmacro hl-hspace-find-flex-alist-for-cdr (b ctables)
; (HL-HSPACE-FIND-FLEX-ALIST-FOR-CDR B CTABLES) --> FLEX ALIST
;
@@ -1255,14 +1257,16 @@
; though the NIL-HT starts out as a hash table, we can still regard it as a
; flex alist.
- (cond ((null b)
- (hl-ctables-nil-ht ctables))
- ((or (consp b)
- (symbolp b)
- (stringp b))
- (gethash b (hl-ctables-cdr-ht ctables)))
- (t
- (gethash b (hl-ctables-cdr-ht-eql ctables)))))
+ `(let ((b ,b)
+ (ctables ,ctables))
+ (cond ((null b)
+ (hl-ctables-nil-ht ctables))
+ ((or (consp b)
+ (symbolp b)
+ (stringp b))
+ (gethash b (hl-ctables-cdr-ht ctables)))
+ (t
+ (gethash b (hl-ctables-cdr-ht-eql ctables))))))
(declaim (inline hl-hspace-honsp))
(defun hl-hspace-honsp (x hs)
@@ -1495,7 +1499,7 @@
'hl-with-lock-grabbed))
#+static-hons
-(defabbrev hl-symbol-addr (s)
+(defmacro hl-symbol-addr (s)
; (HL-SYMBOL-ADDR S) --> NAT
;
@@ -1519,28 +1523,29 @@
; without-interrupts because installing the new 'hl-static-address cons is a
; single setf.
- (let ((addr-cons (get (the symbol s) 'hl-static-address)))
- (if addr-cons
- ;; Already have an address. ADDR-CONS = (S . TRUE-ADDR), where
- ;; TRUE-ADDR is Index(ADDR-CONS) + BASE. So, we just need to
- ;; return the TRUE-ADDR.
- (cdr addr-cons)
- ;; We need to assign an address. Must lock!
- (hl-with-lock-grabbed
- (*hl-symbol-addr-lock*)
- ;; Some other thread might have assigned S an address before we
- ;; got the lock. So, double-check and make sure that there still
- ;; isn't an address.
- (setq addr-cons (get (the symbol s) 'hl-static-address))
+ `(let ((s ,s))
+ (let ((addr-cons (get (the symbol s) 'hl-static-address)))
(if addr-cons
+ ;; Already have an address. ADDR-CONS = (S . TRUE-ADDR), where
+ ;; TRUE-ADDR is Index(ADDR-CONS) + BASE. So, we just need to
+ ;; return the TRUE-ADDR.
(cdr addr-cons)
- ;; Okay, safe to generate a new address.
- (let* ((new-addr-cons (hl-static-cons s nil))
- (true-addr (+ hl-dynamic-base-addr
- (hl-staticp new-addr-cons))))
- (rplacd (the cons new-addr-cons) true-addr)
- (setf (get (the symbol s) 'hl-static-address) new-addr-cons)
- true-addr))))))
+ ;; We need to assign an address. Must lock!
+ (hl-with-lock-grabbed
+ (*hl-symbol-addr-lock*)
+ ;; Some other thread might have assigned S an address before we
+ ;; got the lock. So, double-check and make sure that there still
+ ;; isn't an address.
+ (setq addr-cons (get (the symbol s) 'hl-static-address))
+ (if addr-cons
+ (cdr addr-cons)
+ ;; Okay, safe to generate a new address.
+ (let* ((new-addr-cons (hl-static-cons s nil))
+ (true-addr (+ hl-dynamic-base-addr
+ (hl-staticp new-addr-cons))))
+ (rplacd (the cons new-addr-cons) true-addr)
+ (setf (get (the symbol s) 'hl-static-address) new-addr-cons)
+ true-addr)))))))
#+static-hons
(defun hl-addr-of-unusual-atom (x str-ht other-ht)
@@ -1632,25 +1637,27 @@
b))
#+static-hons
-(defabbrev hl-addr-combine* (a b)
+(defmacro hl-addr-combine* (a b)
;; Inlined version of hl-addr-combine, defined in community book
;; books/system/hl-addr-combine.lisp. See that book for all documentation
;; and a proof that this function is one-to-one. The only change we make
;; here is to use typep to see if the arguments are fixnums in the
;; comparisons, which speeds up our test loop by about 1/3.
- (if (and (typep a 'fixnum)
- (typep b 'fixnum)
- (< (the fixnum a) 1073741824) ; (expt 2 30)
- (< (the fixnum b) 1073741824))
- ;; Optimized version of the small case
- (the (signed-byte 61)
- (- (the (signed-byte 61)
- (logior (the (signed-byte 61)
- (ash (the (signed-byte 31) a) 30))
- (the (signed-byte 31) b)))))
- ;; Large case.
- (- (hl-nat-combine* a b)
- 576460752840294399))) ; (+ (expt 2 59) (expt 2 29) -1)
+ `(let ((a ,a)
+ (b ,b))
+ (if (and (typep a 'fixnum)
+ (typep b 'fixnum)
+ (< (the fixnum a) 1073741824) ; (expt 2 30)
+ (< (the fixnum b) 1073741824))
+ ;; Optimized version of the small case
+ (the (signed-byte 61)
+ (- (the (signed-byte 61)
+ (logior (the (signed-byte 61)
+ (ash (the (signed-byte 31) a) 30))
+ (the (signed-byte 31) b)))))
+ ;; Large case.
+ (- (hl-nat-combine* a b)
+ 576460752840294399)))) ; (+ (expt 2 59) (expt 2 29) -1)
; ----------------------------------------------------------------------
@@ -2161,7 +2168,7 @@
(setf (gethash x persist-ht) t)))
x))
-(defabbrev hl-hspace-hons (x y hs)
+(defmacro hl-hspace-hons (x y hs)
; (HL-HSPACE-HONS X Y HS) --> (X . Y) which is normed, and destructively
; updates HS.
@@ -2173,9 +2180,12 @@
; new cons is considered normed, and return it.
(declare (type hl-hspace hs))
- (hl-hspace-hons-normed (hl-hspace-norm x hs)
- (hl-hspace-norm y hs)
- nil hs))
+ `(let ((x ,x)
+ (y ,y)
+ (hs ,hs))
+ (hl-hspace-hons-normed (hl-hspace-norm x hs)
+ (hl-hspace-norm y hs)
+ nil hs)))
; ----------------------------------------------------------------------
@@ -3906,7 +3916,7 @@ To avoid the following break and get only the above warning:~% ~a~%"
(hl-maybe-initialize-default-hs))
(defun hons (x y)
- ;; hl-hspace-hons is inlined via defabbrev
+ ;; hl-hspace-hons is inlined via defmacro
(hl-maybe-initialize-default-hs)
(hl-hspace-hons x y *default-hs*))
diff --git a/hons.lisp b/hons.lisp
index eadf29f2d0c..16243c40bd8 100644
--- a/hons.lisp
+++ b/hons.lisp
@@ -32,6 +32,55 @@
(in-package "ACL2")
+(defmacro defn (f a &rest r)
+ `(defun ,f ,a (declare (xargs :guard t)) ,@r))
+
+(defmacro defnd (f a &rest r)
+ `(defund ,f ,a (declare (xargs :guard t)) ,@r))
+
+#+(or acl2-loop-only (not hons))
+(defn hons-equal (x y)
+ (declare (xargs :mode :logic))
+ ;; Has an under-the-hood implementation
+ (equal x y))
+
+(defn hons-assoc-equal (key alist)
+ (declare (xargs :mode :logic))
+ (cond ((atom alist)
+ nil)
+ ((and (consp (car alist))
+ (hons-equal key (caar alist)))
+ (car alist))
+ (t
+ (hons-assoc-equal key (cdr alist)))))
+
+#+(or acl2-loop-only (not hons))
+(defn hons-get (key alist)
+ (declare (xargs :mode :logic))
+ ;; Has an under-the-hood implementation
+ (hons-assoc-equal key alist))
+
+#+(or acl2-loop-only (not hons))
+(defn hons-acons (key val alist)
+ (declare (xargs :mode :logic))
+ ;; Has an under-the-hood implementation
+ (cons (cons key val) alist))
+
+#+(or acl2-loop-only (not hons))
+(defmacro fast-alist-free-on-exit-raw (alist form)
+ ;; Has an under-the-hood implementation
+ (declare (ignore alist))
+ form)
+
+#+(or acl2-loop-only (not hons))
+(defn fast-alist-free (alist)
+ (declare (xargs :mode :logic))
+ ;; Has an under-the-hood implementation
+ alist)
+
+(defmacro fast-alist-free-on-exit (alist form)
+ `(return-last 'fast-alist-free-on-exit-raw ,alist ,form))
+
#+(or acl2-loop-only (not hons))
(defn hons-copy (x)
;; Has an under-the-hood implementation
@@ -48,9 +97,6 @@
;; Has an under-the-hood implementation
(cons x y))
-; See basis-a.lisp for hons-equal, which supports hons-assoc-equal, which
-; supports eviscerate1.
-
#+(or acl2-loop-only (not hons))
(defn hons-equal-lite (x y)
;; Has an under-the-hood implementation
@@ -115,16 +161,6 @@
(and (consp warning)
(cdr warning))))
-#+(or acl2-loop-only (not hons))
-(defn hons-get (key alist)
- ;; Has an under-the-hood implementation
- (hons-assoc-equal key alist))
-
-#+(or acl2-loop-only (not hons))
-(defn hons-acons (key val alist)
- ;; Has an under-the-hood implementation
- (cons (cons key val) alist))
-
#+(or acl2-loop-only (not hons))
(defn hons-acons! (key val alist)
;; Has an under-the-hood implementation
@@ -179,11 +215,6 @@
;; Has an under-the-hood implementation
(len (fast-alist-fork alist nil)))
-#+(or acl2-loop-only (not hons))
-(defn fast-alist-free (alist)
- ;; Has an under-the-hood implementation
- alist)
-
#+(or acl2-loop-only (not hons))
(defn fast-alist-summary ()
;; Has an under-the-hood implementation
@@ -207,15 +238,6 @@
(defmacro with-stolen-alist (alist form)
`(return-last 'with-stolen-alist-raw ,alist ,form))
-#+(or acl2-loop-only (not hons))
-(defmacro fast-alist-free-on-exit-raw (alist form)
- ;; Has an under-the-hood implementation
- (declare (ignore alist))
- form)
-
-(defmacro fast-alist-free-on-exit (alist form)
- `(return-last 'fast-alist-free-on-exit-raw ,alist ,form))
-
(defn cons-subtrees (x al)
(cond ((atom x)
al)
diff --git a/interface-raw.lisp b/interface-raw.lisp
index fba26a5b8f0..f439c252bef 100644
--- a/interface-raw.lisp
+++ b/interface-raw.lisp
@@ -24,6 +24,104 @@
; cannot code in ACL2 because they require constructs not in ACL2, such
; as calling the compiler.
+; We start with a section that was originally in acl2-fns.lisp, but was moved
+; here when sharp-atsign-read started using several functions defined in the
+; sources, to avoid compiler warnings.
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; SUPPORT FOR #@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmacro sharp-atsign-read-er (str &rest format-args)
+ `(progn (loop (when (null (read-char-no-hang stream nil nil t))
+ (return)))
+ (error (concatenate 'string ,str ". See :DOC set-iprint.")
+ ,@format-args)))
+
+(defun sharp-atsign-read (stream char n &aux (state *the-live-state*))
+ (declare (ignore char n))
+ (let (ch
+ bad-ch
+ (zero-code (char-code #\0))
+ (index 0)
+ (iprint-last-index (iprint-last-index state)))
+ (loop
+ (when (eql (setq ch (read-char stream t nil t))
+ #\#)
+ (return))
+ (let ((digit (- (char-code ch) zero-code)))
+ (cond ((or (< digit 0)
+ (> digit 9))
+ (when (not bad-ch)
+ (setq bad-ch ch))
+ (return))
+ (t
+ (setq index (+ digit (* 10 index)))))))
+ (cond
+ (bad-ch
+ (sharp-atsign-read-er
+ "Non-digit character ~s following #@~s"
+ bad-ch index))
+ ((symbol-value (f-get-global 'certify-book-info state))
+ (sharp-atsign-read-er
+ "Illegal reader macro during certify-book, #@~s#"
+ index))
+ ((iprint-ar-illegal-index index state)
+ (sharp-atsign-read-er
+ "Out-of-bounds index in #@~s#"
+ index))
+ (t
+ (let ((old-read-state ; bind special
+ *iprint-read-state*))
+ (cond
+ ((eq old-read-state nil)
+ (iprint-ar-aref1 index state))
+ (t
+ (let ((new-read-state-order (if (<= index iprint-last-index)
+ '<=
+ '>)))
+ (cond
+ ((eq old-read-state t)
+ (setq *iprint-read-state*
+ (cons index new-read-state-order))
+ (iprint-ar-aref1 index state))
+ ((eq (cdr old-read-state)
+ new-read-state-order) ; both > or both <=
+ (iprint-ar-aref1 index state))
+ (t
+ (multiple-value-bind
+ (index-before index-after)
+ (cond
+ ((eq (cdr old-read-state) '<=)
+ (values index (car old-read-state)))
+ (t ; (eq (cdr old-read-state) '>)
+ (values (car old-read-state) index)))
+ (sharp-atsign-read-er
+ "Attempt to read a form containing both an index~%~
+ created before the most recent rollover (#@~s#) and~%~
+ an index created after that rollover (#@~s#)"
+ index-before index-after))))))))))))
+
+(defun define-sharp-atsign ()
+ (set-new-dispatch-macro-character
+ #\#
+ #\@
+ #'sharp-atsign-read))
+
+(eval-when
+
+; Note: CMUCL build breaks without the check below for a compiled function.
+
+ #-cltl2
+ (load eval)
+ #+cltl2
+ (:load-toplevel :execute)
+ (when (compiled-function-p! 'sharp-atsign-read)
+ (let ((*readtable* *acl2-readtable*))
+ (define-sharp-atsign))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
; EVALUATION
; Essay on Evaluation in ACL2
diff --git a/ld.lisp b/ld.lisp
index d56bfc1c691..e3df5e27fae 100644
--- a/ld.lisp
+++ b/ld.lisp
@@ -743,38 +743,59 @@
(declare (ignore erp val))
(mv t nil nil state)))))))))
-(defun restore-iprint-ar-from-wormhole (state)
- (declare (xargs :stobjs state))
+#-acl2-loop-only
+(defvar *iprint-read-state*
+
+; Possible values are:
+
+; nil - no requirement on current iprint index
+; t - either all indices must exceed iprint-last-index, or none does
+; (n . <=) - n, already read, is <= iprint-last-index; index must be too
+; (n . >) - n, already read, is > iprint-last-index; index must be too
+
+; The value is initially nil. At a top-level read, it is set to nil if
+; iprint-fal is nil, else to t. For the first index i that is read when the
+; value is t, we set the value to <= if (<= i iprint-last-index) and to >
+; otherwise.
+
+ nil)
+
+(defun iprint-oracle-updates (state)
#+acl2-loop-only
(mv-let (erp val state)
- (read-acl2-oracle state)
- (declare (ignore erp))
+ (read-acl2-oracle state)
+ (declare (ignore erp))
; If we intend to reason about this function, then we might want to check that
; val is a reasonable value. But that seems not important, since very little
; reasoning would be possible anyhow for this function.
- (pprogn (f-put-global 'iprint-ar
- (and (consp val) (car val))
- state)
- (f-put-global 'iprint-hard-bound
- (nfix (and (consp val)
- (consp (cdr val))
- (cadr val)))
- state)
- (f-put-global 'iprint-soft-bound
- (nfix (and (consp val)
- (consp (cdr val))
- (cddr val)))
- state)
- state))
+ (let ((val (fix-true-list val)))
+ (pprogn (f-put-global 'iprint-ar
+ (nth 0 val)
+ state)
+ (f-put-global 'iprint-hard-bound
+ (nfix (nth 1 val))
+ state)
+ (f-put-global 'iprint-soft-bound
+ (nfix (nth 2 val))
+ state)
+ (f-put-global 'iprint-fal
+ (nth 3 val)
+ state)
+ state)))
#-acl2-loop-only
(let* ((ar *wormhole-iprint-ar*))
(when ar
- (f-put-global 'iprint-ar (compress1 'iprint-ar ar) state)
+ (f-put-global 'iprint-ar ar state)
+ (f-put-global 'iprint-fal *wormhole-iprint-fal* state)
(f-put-global 'iprint-hard-bound *wormhole-iprint-hard-bound* state)
(f-put-global 'iprint-soft-bound *wormhole-iprint-soft-bound* state)
(setq *wormhole-iprint-ar* nil))
+ (setq *iprint-read-state*
+ (if (f-get-global 'iprint-fal state)
+ t
+ nil))
state))
(defun ld-fix-command (form)
@@ -812,7 +833,7 @@
; be (:kons x y).
(pprogn
- (restore-iprint-ar-from-wormhole state) ; even before the read
+ (iprint-oracle-updates state) ; even before the read
(mv-let (eofp val state)
(read-standard-oi state)
(pprogn
@@ -2532,10 +2553,10 @@
#-acl2-loop-only
(defun-one-output compiled-function-p! (fn)
-; In CMU Lisp, compiled-function-p is braindead. It seems that the
-; symbol-function of every defun'd function is a ``compiled'' object.
-; Some are #
- Pair each call in @('calls') with the tests @('tests'). -
" - (if (endp calls) - nil - (cons (make tests-and-call - :tests tests - :call (car calls)) - (recursive-calls-aux1 tests (cdr calls))))) - - (define recursive-calls-aux2 - ((tests-and-calls-list pseudo-tests-and-calls-listp)) - ;; :returns (calls-with-tests pseudo-tests-and-call-listp) - :verify-guards nil - :parents (recursive-calls) - :short "Second auxiliary function of @(tsee recursive-calls)." - :long - "- Collect all the calls, with tests, from the induction machine. -
" - (if (endp tests-and-calls-list) - nil - (let* ((tests-and-calls (car tests-and-calls-list)) - (tests (access tests-and-calls tests-and-calls :tests)) - (calls (access tests-and-calls tests-and-calls :calls))) - (append (recursive-calls-aux1 tests calls) - (recursive-calls-aux2 (cdr tests-and-calls-list)))))))) + (termination-machine + (list fn) (body fn nil wrld) nil nil (ruler-extenders fn wrld))) (std::deflist pseudo-event-landmark-listp (x) (pseudo-event-landmarkp x) From 000711cbf7ab7bf25a347ef7107be411cb14f4ef Mon Sep 17 00:00:00 2001 From: Alessandro Coglio
The @('N') forms must be
The forms may be followed by @(':with-output-off') and/or @(':check-expansion'), as in @(tsee must-succeed).
+ @(def must-succeed*)" (defmacro must-succeed* (&rest args) @@ -80,17 +89,19 @@ (defsection must-be-redundant - :parents (kestrel-general-utilities errors) + :parents (testing-utilities errors) :short "A top-level @(tsee assert$)-like command to ensure that given forms are redundant." :long + "The forms are put into an @(tsee encapsulate), along with a @(tsee set-enforce-redundancy) command that precedes them.
+ @(def must-be-redundant)" (defmacro must-be-redundant (&rest forms) @@ -103,15 +114,17 @@ (defsection must-fail-local - :parents (kestrel-general-utilities errors) + :parents (testing-utilities errors) :short "A @(see local) variant of @(tsee must-fail)." :long + "This is useful to overcome the problem discussed in the caveat in the documentation of @(tsee must-fail).
+ @(def must-fail-local)" (defmacro must-fail-local (&rest args) From 7e9eddb1880c6044d22a1f8ff9f473d968ba83ee Mon Sep 17 00:00:00 2001 From: Alessandro CoglioWe thank David Rager for providing the following - instructions, which we include verbatim and expect apply to +
We thank David Rager for providing + instructions, which we include verbatim below and expect apply to future versions. Note: We recommend using CCL for Windows - builds, in part so that interrupts (Control-C) will work. If - you are using Windows, please note that there have been stalls - using CCL 1.5 on Windows, though not with CCL 1.4. We have - been told by a CCL implementor that this bug has been fixed, - and people running CCL 1.5 under Windows at a revision less - than 13900 should update. + builds, in part so that interrupts (Control-C) will work. But + first, a remark:
+ +At least one user has built ACL2 on Windows 10 in July, 2016 by +following the instructions below, using the "bleeding edge" versions +of CCL, mingw, and ACL2. This user said the the bleeding edge +versions might not be necessary, but with older versions there were +too many times that the ACL2 build was hanging. Even with the +bleeding edge versions there were some hangs, but it wasn't clear if +that was the fault of CCL, Mingw, MSys, or something else. This user +explained further:
+ ++ +The problem with hangs: It seems that while compiling ACL2 there were +a few times when it simply hung. But apparently this is +non-deterministic. Simply cleaning and retrying several times managed +to get me out of the problem. + +- +
Here are David Rager's instructions.
I was able to get ACL2 3.6.1 to install and build the regression suite on Windows 7 with the following steps. I did not have to install cygwin.
- - + +Install MinGW. At the time of this writing, the following direct link works
-
+
MinGW-5.1.6.exe
If that direct link doesn't work, click on "MSYS Base System" on the more general MinWG project files page.
- +Realize that using "\" to indicate paths in windows confuses some linux programs and that you might need to use "/" sometimes.
After expanding the ACL2 sources, cd to that directory and type
something similar to the following (modify it to set LISP to your LISP
executable1)
-
+
make LISP=c:/ccl/wx86cl64.exe
-
+
The "make.exe" that will be used is intentionally the MSys version,
not the MinGW version.
rename saved_acl2 saved_acl2.bat
You can now make the regression suite by typing
make regression ACL2=c:/acl2-3.6.1/acl2-sources/saved_acl2.bat
The iprinting utility has a new keyword option, @(':share'), which causes - iprint indices to be re-used. See @(see set-iprint). Thanks to David Rager - for suggesting such an enhancement.
+ iprint indices to be re-used (using so-called ``iprint sharing'' and ``iprint + eager sharing''. See @(see set-iprint). Thanks to David Rager for suggesting + a notion of iprint sharing.You might wish to know which elided expressions are equal. You may specify - keyword argument @(':share t') for that purpose to turn on ``iprint sharing'', - which causes behavior as shown below: the value printed shows the iprint index - 2 being used twice for the list @('(C D E F)').
+If you wish to know which elided expressions are equal, you may call + @('set-iprint') with non-@('nil') value for keyword argument @(':share'). + That will turn on iprint sharing, which causes behavior as shown below: + the value printed shows the iprint index 2 being used twice for the list @('(C + D E F)').
@({ ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) @@ -91300,17 +91302,17 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") ACL2 !> }) -Remark (feel free to skip this paragraph). To understand more fully how - iprint sharing works, consider the following log. The Warning below is - pointing out that previous iprint indices are no longer valid; we are starting - over. The first Observation points out that iprint sharing is on, and gives - the name @(':IPRINT-FAL') to look for in @('(fast-alist-summary)') in case you - want information on the @(see fast-alist) that associates values with - corresponding iprint indices. To see the relevance of a fast-alist, note that - the two elided occurrences of the list @('(C D E F)') were originally not the - identical list in memory; to make them identical, @(tsee hons-copy) is applied - to each to get the same list in memory, which is the one associated with - iprint index 2 in a fast-alist named @(':IPRINT-FAL').
+We use the log displayed below to explain iprint sharing a bit more. The + Warning below is pointing out that previous iprint indices are no longer + valid; we are starting over. The first Observation points out that iprint + sharing is on, and gives the name @(':IPRINT-FAL') to look for in + @('(fast-alist-summary)') in case you want information on the @(see + fast-alist) that associates values with corresponding iprint indices. To see + the relevance of a fast-alist, note that the two elided occurrences of the + list @('(C D E F)') were originally not the identical list in memory; to make + them identical, @(tsee hons-copy) is applied to each to get the same list in + memory, which is the one associated with iprint index 2 in a fast-alist named + @(':IPRINT-FAL').
@({ ACL2 !>(set-iprint t :share t) @@ -91328,6 +91330,30 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") (:TERM :LD . #@1#) ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) ((A B . #@2#) (A B . #@2#) . #@3#) + ACL2 !>'(b c d e f) + (B C . #@4#) + ACL2 !> + }) + +One might have expected the last form printed above to take advantage of + the fact that the tail @('(C D E F)') of the input's value is already + associated with iprint index 2. If you want that sort of behavior — + that is, where we use an existing iprint index even when we have not yet + reached the print-level or print-depth specified by our most recent call of + @(tsee set-evisc-tuple) — then we can use the special value @(':eager') + for keyword @(':share'), which gives us eager iprinting:
+ + @({ + (set-iprint t :share :eager) + }) + +If we use that call of @('set-iprint') instead of our earlier one above + (that is, with @(':share t')), then the tail @('(C D E F)') is indeed + abbreviated using iprint index 2:
+ + @({ + ACL2 !>'(b c d e f) + (B . #@2#) ACL2 !> }) @@ -91386,13 +91412,18 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.") assigned the next available iprint index, @('N'). If an iprint index @('I < N') is already associated with a value equal to @('V'), then ACL2 will print @('#@I') for @('V') instead of @('#@N'). Thus, @('N') will remain the next - available iprint index. This behavior is implementing using a @(see + available iprint index. This behavior is implemented using a @(see fast-alist) that associates values with indices; in our example, the @(tsee hons-copy) of @('V') is associated with @('I'). If the value of @(':share') is @('t') then the name of this fast-alist — that is, its initial value — is @(':iprint-fal'); otherwise, the value of @(':share') (other than - @('nil') or @(':same') is its name. This name is useful when viewing the - output of @(tsee fast-alist-summary). + @('nil') or @(':same')) is its name. This name is useful when viewing the + output of @(tsee fast-alist-summary). Finally, a special case, called ``eager + sharing'', is installed if the value of @(':share') is @(':eager'). In that + case, the behavior described above — where @('#@I') is printed for + @('V') — will occur even if the value @('V') would otherwise not be + elided, provided the most recent call of @(tsee set-evisc-tuple) specified a + non-@('nil') print-level or print-length.Immediately after a top-level form is read, hence before it is evaluated, a check is made for whether the latest iprint index exceeds a certain bound, @@ -97803,7 +97834,7 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.
") :short "Developing ACL2 system code" :long "ACL2 is maintained solely by Matt Kaufmann and J Moore. However, we anticipate that a few others will eventually contribute as well. The - subtopics of this topic provide information that are intended to help future + subtopics of this topic provide information that is intended to help future developers.
") (defxdoc system-development-hints diff --git a/doc.lisp b/doc.lisp index ce6c122a5a7..0d5703e2917 100644 --- a/doc.lisp +++ b/doc.lisp @@ -72637,8 +72637,9 @@ New Features Davis for requesting this feature. The iprinting utility has a new keyword option, :share, which causes - iprint indices to be re-used. See [set-iprint]. Thanks to David - Rager for suggesting such an enhancement. + iprint indices to be re-used (using so-called ``iprint sharing'' + and ``iprint eager sharing''. See [set-iprint]. Thanks to David + Rager for suggesting a notion of iprint sharing. Heuristic and Efficiency Improvements @@ -92260,23 +92261,22 @@ Example ACL2 !> - You might wish to know which elided expressions are equal. You may - specify keyword argument :share t for that purpose to turn on - ``iprint sharing'', which causes behavior as shown below: the value - printed shows the iprint index 2 being used twice for the list (C D - E F). + If you wish to know which elided expressions are equal, you may call + set-iprint with non-nil value for keyword argument :share. That + will turn on iprint sharing, which causes behavior as shown below: + the value printed shows the iprint index 2 being used twice for the + list (C D E F). ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) ((A B . #@2#) (A B . #@2#) . #@3#) ACL2 !> - Remark (feel free to skip this paragraph). To understand more fully - how iprint sharing works, consider the following log. The Warning - below is pointing out that previous iprint indices are no longer - valid; we are starting over. The first Observation points out that - iprint sharing is on, and gives the name :IPRINT-FAL to look for in - (fast-alist-summary) in case you want information on the - [fast-alist] that associates values with corresponding iprint + We use the log displayed below to explain iprint sharing a bit more. + The Warning below is pointing out that previous iprint indices are + no longer valid; we are starting over. The first Observation points + out that iprint sharing is on, and gives the name :IPRINT-FAL to + look for in (fast-alist-summary) in case you want information on + the [fast-alist] that associates values with corresponding iprint indices. To see the relevance of a fast-alist, note that the two elided occurrences of the list (C D E F) were originally not the identical list in memory; to make them identical, [hons-copy] is @@ -92298,6 +92298,27 @@ Example (:TERM :LD . #@1#) ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) ((A B . #@2#) (A B . #@2#) . #@3#) + ACL2 !>'(b c d e f) + (B C . #@4#) + ACL2 !> + + One might have expected the last form printed above to take advantage + of the fact that the tail (C D E F) of the input's value is already + associated with iprint index 2. If you want that sort of behavior + --- that is, where we use an existing iprint index even when we + have not yet reached the print-level or print-depth specified by + our most recent call of [set-evisc-tuple] --- then we can use the + special value :eager for keyword :share, which gives us eager + iprinting: + + (set-iprint t :share :eager) + + If we use that call of set-iprint instead of our earlier one above + (that is, with :share t), then the tail (C D E F) is indeed + abbreviated using iprint index 2: + + ACL2 !>'(b c d e f) + (B . #@2#) ACL2 !> The documentation above probably suffices for most users. For those @@ -92350,12 +92371,17 @@ Example If an iprint index I < N is already associated with a value equal to V, then ACL2 will print #@I for V instead of #@N. Thus, N will remain the next available iprint index. This behavior is - implementing using a [fast-alist] that associates values with + implemented using a [fast-alist] that associates values with indices; in our example, the [hons-copy] of V is associated with I. If the value of :share is t then the name of this fast-alist --- that is, its initial value --- is :iprint-fal; otherwise, the value - of :share (other than nil or :same is its name. This name is useful - when viewing the output of [fast-alist-summary]. + of :share (other than nil or :same) is its name. This name is + useful when viewing the output of [fast-alist-summary]. Finally, a + special case, called ``eager sharing'', is installed if the value + of :share is :eager. In that case, the behavior described above --- + where #@I is printed for V --- will occur even if the value V would + otherwise not be elided, provided the most recent call of + [set-evisc-tuple] specified a non-nil print-level or print-length. Immediately after a top-level form is read, hence before it is evaluated, a check is made for whether the latest iprint index @@ -98880,8 +98906,8 @@ Subtopics ACL2 is maintained solely by Matt Kaufmann and J Moore. However, we anticipate that a few others will eventually contribute as well. - The subtopics of this topic provide information that are intended - to help future developers. + The subtopics of this topic provide information that is intended to + help future developers. Subtopics diff --git a/translate.lisp b/translate.lisp index ad50f3a3c42..a076aeae5f8 100644 --- a/translate.lisp +++ b/translate.lisp @@ -7700,13 +7700,15 @@ ; Warning: Keep this in sync with macroexpand1*-cmp. -; Bindings is an alist binding symbols either to their corresponding -; STOBJS-OUT or to symbols. The only symbols used are (about-to-be -; introduced) function symbols or the keyword :STOBJS-OUT. When fn is -; bound to gn it means we have determined that the STOBJS-OUT of fn is -; that of gn. We allow fn to be bound to itself -- indeed, it is -; required initially! (This allows bindings to double as a recording -; of all the names currently being introduced.) +; Bindings is an alist binding symbols either to their corresponding STOBJS-OUT +; or to symbols. The only symbols used are (about-to-be introduced) function +; symbols or the keyword :STOBJS-OUT. When fn is bound to gn it means we have +; determined that the STOBJS-OUT of fn is that of gn. We allow fn to be bound +; to itself -- indeed, it is required initially! (This allows bindings to +; double as a recording of all the names currently being introduced.) A +; special case is when :STOBJS-OUT is bound in bindings: initially it is bound +; to itself, but in the returned bindings it will be bound to the stobjs-out of +; the expression being translated. ; Stobjs-out is one of: @@ -9195,8 +9197,11 @@ ; one does not have state available, and then (default-state-vars nil). ; We return (mv erp transx bindings), where transx is the translation and -; bindings has been modified to bind every fn (ultimately) to a proper stobjs -; out setting. Use translate-deref to recover the bindings. +; bindings has been modified to bind every fn (ultimately) to a proper +; stobjs-out setting. A special case is when the initial stobjs-out is +; :stobjs-out; in that case, :stobjs-out is bound in the returned bindings to +; the stobjs-out of the expression being translated. Use translate-deref to +; recover the bindings. (trans-er-let* ((result @@ -9227,6 +9232,7 @@ (default-state-vars t)))) (defun collect-programs (names wrld) + ; Names is a list of function symbols. Collect the :program ones. (cond ((null names) nil) From af5bf03a102b73221bd17847296c33ae69758cec Mon Sep 17 00:00:00 2001 From: Matt KaufmannIf we use that call of @('set-iprint') instead of our earlier one above - (that is, with @(':share t')), then the tail @('(C D E F)') is indeed - abbreviated using iprint index 2:
+ (that is, with @(':share t')), then the first of the two last results from the + log above is unchanged, but in the second result, the tail @('(C D E F)') is + indeed abbreviated using iprint index 2. @({ + ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) + ((A B . #@2#) (A B . #@2#) . #@3#) ACL2 !>'(b c d e f) (B . #@2#) ACL2 !> diff --git a/doc.lisp b/doc.lisp index 0d5703e2917..90ae710d28b 100644 --- a/doc.lisp +++ b/doc.lisp @@ -92314,9 +92314,12 @@ Example (set-iprint t :share :eager) If we use that call of set-iprint instead of our earlier one above - (that is, with :share t), then the tail (C D E F) is indeed - abbreviated using iprint index 2: + (that is, with :share t), then the first of the two last results + from the log above is unchanged, but in the second result, the tail + (C D E F) is indeed abbreviated using iprint index 2. + ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f)) + ((A B . #@2#) (A B . #@2#) . #@3#) ACL2 !>'(b c d e f) (B . #@2#) ACL2 !> From f90b07604b9da3704fd97e70a2f97e34d51e7ecc Mon Sep 17 00:00:00 2001 From: Alessandro CoglioThe following (admittedly, contrived) example shows how to use this utility. First define:
diff --git a/books/kestrel/general/define-sk.lisp b/books/kestrel/general/define-sk.lisp index 47294e48030..4310696a479 100644 --- a/books/kestrel/general/define-sk.lisp +++ b/books/kestrel/general/define-sk.lisp @@ -20,7 +20,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defxdoc define-sk - :parents (std/util defun-sk acl2::kestrel-general-utilities) + :parents (std/util defun-sk acl2::kestrel-utilities) :short "A very fine alternative to @(see defun-sk)." :long "The following example explains how @(':ubi') works. We start up diff --git a/books/kestrel/system/applicability-conditions.lisp b/books/kestrel/system/applicability-conditions.lisp index 6f3d9729448..595dafb695c 100644 --- a/books/kestrel/system/applicability-conditions.lisp +++ b/books/kestrel/system/applicability-conditions.lisp @@ -26,7 +26,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defsection applicability-conditions - :parents (kestrel-system-utilities system-utilities) + :parents (kestrel-utilities system-utilities) :short "Utilities to manage logical formulas that must hold for certain processes to apply." diff --git a/books/kestrel/system/defchoose-queries.lisp b/books/kestrel/system/defchoose-queries.lisp index e3347b3e232..fad9d32be22 100644 --- a/books/kestrel/system/defchoose-queries.lisp +++ b/books/kestrel/system/defchoose-queries.lisp @@ -24,7 +24,7 @@ (defxdoc defchoose-queries - :parents (kestrel-system-utilities system-utilities defchoose) + :parents (kestrel-utilities system-utilities defchoose) :short "Utilities to query @(tsee defchoose) functions." diff --git a/books/kestrel/system/defun-sk-queries.lisp b/books/kestrel/system/defun-sk-queries.lisp index 8529693c586..7bb2be9b757 100644 --- a/books/kestrel/system/defun-sk-queries.lisp +++ b/books/kestrel/system/defun-sk-queries.lisp @@ -26,7 +26,7 @@ (defxdoc defun-sk-queries - :parents (kestrel-system-utilities system-utilities defun-sk) + :parents (kestrel-utilities system-utilities defun-sk) :short "Utilities to query @(tsee defun-sk) functions." diff --git a/books/kestrel/system/directed-untranslate.lisp b/books/kestrel/system/directed-untranslate.lisp index 90e4c7115b3..e14be77034c 100644 --- a/books/kestrel/system/directed-untranslate.lisp +++ b/books/kestrel/system/directed-untranslate.lisp @@ -7,7 +7,7 @@ (include-book "xdoc/top" :dir :system) (defxdoc directed-untranslate - :parents (kestrel-system-utilities system-utilities) + :parents (kestrel-utilities system-utilities) :short "Create a user-level form that reflects a given user-level form's structure." :long "
See @(see term) for relevant background about user-level ``terms''
diff --git a/books/kestrel/system/event-forms.lisp b/books/kestrel/system/event-forms.lisp
index 640df554e20..47d1c5b3184 100644
--- a/books/kestrel/system/event-forms.lisp
+++ b/books/kestrel/system/event-forms.lisp
@@ -21,7 +21,7 @@
(define pseudo-event-formp (x)
:returns (yes/no booleanp)
- :parents (kestrel-system-utilities system-utilities)
+ :parents (kestrel-utilities system-utilities)
:short
"True iff @('x') has the basic structure of an event form."
:long
diff --git a/books/kestrel/system/fresh-names.lisp b/books/kestrel/system/fresh-names.lisp
index 5a7c54ed2bf..9faa7f2dcc5 100644
--- a/books/kestrel/system/fresh-names.lisp
+++ b/books/kestrel/system/fresh-names.lisp
@@ -23,7 +23,7 @@
(wrld plist-worldp))
:returns (fresh-name symbolp)
:prepwork ((program))
- :parents (kestrel-system-utilities system-utilities)
+ :parents (kestrel-utilities system-utilities)
:short
"Append as many @('$') signs to @('name')
as needed to make the name new in the world, i.e. not already in use,
diff --git a/books/kestrel/system/install-not-norm-event.lisp b/books/kestrel/system/install-not-norm-event.lisp
index 00cee73ae6e..43baa880c1e 100644
--- a/books/kestrel/system/install-not-norm-event.lisp
+++ b/books/kestrel/system/install-not-norm-event.lisp
@@ -25,7 +25,7 @@
(local booleanp "Make the event form local or not."))
:returns (mv (fn$not-normalized symbolp)
(event-form pseudo-event-formp))
- :parents (kestrel-system-utilities system-utilities install-not-normalized)
+ :parents (kestrel-utilities system-utilities install-not-normalized)
:short
"Generate event form for
diff --git a/books/kestrel/system/prove-interface.lisp b/books/kestrel/system/prove-interface.lisp
index df1f7befb2c..4b26aa708f3 100644
--- a/books/kestrel/system/prove-interface.lisp
+++ b/books/kestrel/system/prove-interface.lisp
@@ -77,7 +77,7 @@
`(convert-soft-error-to-value ,form nil)))
(defxdoc prove$
- :parents (kestrel-system-utilities system-utilities)
+ :parents (kestrel-utilities system-utilities)
:short "A way to call the prover from a program."
:long " For examples, see community book
@('books/kestrel/system/prove-interface-tests.lisp').
From 9265370898b1e2e6c3605ede3a2dfb808aea7b51 Mon Sep 17 00:00:00 2001
From: Alessandro Coglio See community book @('kestrel/system/auto-termination-tests.lisp') for more
+ See community book @('kestrel/utilities/auto-termination-tests.lisp') for more
examples. For examples, see community book
- @('books/kestrel/system/prove-interface-tests.lisp').
@('(Getenv$ str state)'), where @('str') is a string, reads the value of environment variable @('str'), returning a value of @('nil') if none - is found or if the read fails. The logical story is that @('getenv$') reads - its value from the @('oracle') field of the ACL2 @(tsee state). The return - value is thus a triple of the form @('(mv erp val state)'), where @('erp') - will always be @('nil') in practice, and logically, @('val') is the top of the - acl2-oracle field of the state (see @(tsee read-acl2-oracle)) and the returned - state has the updated (popped) acl2-oracle.
+ is found or if the read fails. (Exception: if the value is not a legal ACL2 + string, say because it contains a character with @(tsee char-code) exceeding + 255, then an error is signalled.) The logical story is that @('getenv$') + reads its value from the @('oracle') field of the ACL2 @(tsee state). The + return value is thus a triple of the form @('(mv erp val state)'), where + @('erp') will always be @('nil') in practice, and logically, @('val') is the + top of the acl2-oracle field of the state (see @(tsee read-acl2-oracle)) and + the returned state has the updated (popped) acl2-oracle. @({ Example: @@ -42686,8 +42688,8 @@ tables in the current Hons Space."Note that @('open-output-channel') and @('open-output-channel!') will attempt to create directories as needed (but this is not the case for - @('open-input-channel'). For example, the following can succeed in writing to - the indicated file by creating subdirectory @('\"dir4\"') if that directory + @('open-input-channel')). For example, the following can succeed in writing + to the indicated file by creating subdirectory @('\"dir4\"') if that directory does not already exist.
@({ @@ -74037,6 +74039,13 @@ it." :use ((:instance char-code-linear (x *c*)))))) }) +The utility @(tsee getenv$) now causes an error if the value it would + otherwise return is not an ACL2 string, for example because it contains a + character whose @(tsee char-code) exceeds 255. Many other changes, less + visible to the user, have been made in how ACL2 deals with strings that come + from outside ACL2, in particular, file names (see the related item just + above).
+The handling of @(see meta)functions allowed an invariant to be violated, that conjectures in the prover are always 100% @(see logic) mode. An example is in a comment in the ACL2 source code under @('(deflabel note-7-3 ...)'). @@ -97979,7 +97988,7 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.
") submit the command @('meta-x tags-apropos') and reply @('pwd') at the prompt, you'll find a raw Lisp function @('our-pwd') that ACL2 defines as an analogue to the Linux @('pwd') command; and, with @('meta-x tags-search') applied to - @('(pwd'), you can see how ACL2 source code uses this utility. + @('(our-pwd'), you can see how ACL2 source code uses this utility.See @(see xargs) for discussion of how to use the @(':measure') keyword to specify a measure for a definition. A related utility, @('measure'), may be found in the @(see community-books), file - @('kestrel/system/world-queries.lisp').
") + @('kestrel/utilities/world-queries.lisp').") (defxdoc measure-debug :parents (measure debugging) @@ -73477,7 +73477,7 @@ it." ; Renamed :doc topic well-founded-relation to well-founded-relation-rule, to ; accommodate the form (define well-founded-relation ...) in -; books/kestrel/system/world-queries.lisp. +; books/kestrel/utilities/world-queries.lisp. ; We added to :doc redundant-encapsulate to add discussion of redefinition. ; Also, we tweaked a redundancy message for encapsulate so that it says "might @@ -87882,7 +87882,7 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.")To see the ruler-extenders of an existing function symbol, @('fn'), in a logical @(see world), @('wrld'), evaluate @('(ruler-extenders 'fn wrld)') - after @('(include-book \"kestrel/system/world-queries\" :dir :system)'). For + after @('(include-book \"kestrel/utilities/world-queries\" :dir :system)'). For example, evaluation of @('(ruler-extenders 'fn (w state))') provides the ruler-extenders of @('fn') in the current logical world.
@@ -109042,14 +109042,14 @@ introduction-to-the-tau-system) for more information about Tau. (defxdoc well-founded-relation ; This topic is appropriately redefined by (define well-founded-relation ...) -; in books/kestrel/system/world-queries.lisp. +; in books/kestrel/utilities/world-queries.lisp. :parents (rule-classes) :short "Show that a relation is well-founded on a set" :long "See @(see well-founded-relation-rule) for discussion of well-founded relations in ACL2. A related utility, @('well-founded-relation'), may be found in the @(see community-books), file - @('kestrel/system/world-queries.lisp').
") + @('kestrel/utilities/world-queries.lisp').") (defxdoc well-founded-relation-rule :parents (rule-classes) From 9e5de11e6b999dc8f601bd5bb264f8c9772cc549 Mon Sep 17 00:00:00 2001 From: Matt KaufmannWhen @(tsee defun-sk) was supplied with keyword argument @(':strengthen + t'), the name of the generated theorem was always in the @('\"ACL2\"') + package. Now it is in the same package as the function symbol being defined. + Thanks to Alessandro Coglio for suggesting this change.
+New optional arguments allow the @(tsee pso) utility to restrict output to
diff --git a/doc.lisp b/doc.lisp
index 90ae710d28b..22ca9728fe1 100644
--- a/doc.lisp
+++ b/doc.lisp
@@ -12701,7 +12701,7 @@ Subtopics
(str::pretty-printing \"[books]/std/strings/pretty.lisp\")
(quicklisp \"[books]/centaur/quicklisp/top.lisp\")
(removable-runes \"[books]/tools/removable-runes.lisp\")
- (ruler-extenders \"[books]/kestrel/system/world-queries.lisp\")
+ (ruler-extenders \"[books]/kestrel/utilities/world-queries.lisp\")
(satlink::sat-solver-options \"[books]/centaur/satlink/top.lisp\")
(satlink \"[books]/centaur/satlink/top.lisp\")
(xdoc::save \"[books]/xdoc/topics.lisp\")
@@ -24255,9 +24255,11 @@ Subtopics
only be executed in [defun-mode] :[logic]; see [defun-mode] and see
[defchoose]. Advanced feature: If argument :strengthen t is passed
to defun-sk, then :strengthen t will generate the extra constraint
- that that is generated for the corresponding defchoose event; see
- [defchoose]. You can use the command :[pcb!] to see the event
- generated by a call of the defun-sk macro.
+ that is generated for the corresponding defchoose event; see
+ [defchoose]. (The name of that generated theorem will be obtained
+ by adding the suffix \"-STRENGTHEN\" to the function symbol being
+ defined, in the same package). You can use the command :[pcb!] to
+ see the event generated by a call of the defun-sk macro.
If you find that the rewrite rules introduced with a particular use
of defun-sk are not ideal, even when using the :rewrite keyword
@@ -30534,8 +30536,8 @@ Subtopics
(defun file-write-date$ (file state)
(declare (xargs :guard (stringp file)
- :stobjs state))
- (declare (ignore file))
+ :stobjs state)
+ (ignorable file))
(mv-let (erp val state)
(read-acl2-oracle state)
(mv (and (null erp) (posp val) val)
@@ -35130,12 +35132,15 @@ Subtopics
(Getenv$ str state), where str is a string, reads the value of
environment variable str, returning a value of nil if none is found
- or if the read fails. The logical story is that getenv$ reads its
- value from the oracle field of the ACL2 [state]. The return value
- is thus a triple of the form (mv erp val state), where erp will
- always be nil in practice, and logically, val is the top of the
- acl2-oracle field of the state (see [read-ACL2-oracle]) and the
- returned state has the updated (popped) acl2-oracle.
+ or if the read fails. (Exception: if the value is not a legal ACL2
+ string, say because it contains a character with [char-code]
+ exceeding 255, then an error is signalled.) The logical story is
+ that getenv$ reads its value from the oracle field of the ACL2
+ [state]. The return value is thus a triple of the form (mv erp val
+ state), where erp will always be nil in practice, and logically,
+ val is the top of the acl2-oracle field of the state (see
+ [read-ACL2-oracle]) and the returned state has the updated (popped)
+ acl2-oracle.
Example:
(getenv$ \"PWD\" state) ==> (mv nil \"/u/joe/work\" state)
@@ -45953,7 +45958,7 @@ Subtopics
Note that open-output-channel and open-output-channel! will attempt
to create directories as needed (but this is not the case for
- open-input-channel. For example, the following can succeed in
+ open-input-channel). For example, the following can succeed in
writing to the indicated file by creating subdirectory \"dir4\" if
that directory does not already exist.
@@ -52864,7 +52869,7 @@ Subtopics
See [xargs] for discussion of how to use the :measure keyword to
specify a measure for a definition. A related utility, measure, may
be found in the [community-books], file
- kestrel/system/world-queries.lisp.
+ kestrel/utilities/world-queries.lisp.
Subtopics
@@ -72598,6 +72603,11 @@ Changes to Existing Features
``hard-bounds and rollovers'' in (defxdoc note-7-3 ...) in
community book books/system/doc/acl2-doc.lisp.
+ When [defun-sk] was supplied with keyword argument :strengthen t, the
+ name of the generated theorem was always in the \"ACL2\" package. Now
+ it is in the same package as the function symbol being defined.
+ Thanks to Alessandro Coglio for suggesting this change.
+
New Features
@@ -72772,6 +72782,13 @@ Bug Fixes
:in-theory (theory 'minimal-theory)
:use ((:instance char-code-linear (x *c*))))))
+ The utility [getenv$] now causes an error if the value it would
+ otherwise return is not an ACL2 string, for example because it
+ contains a character whose [char-code] exceeds 255. Many other
+ changes, less visible to the user, have been made in how ACL2 deals
+ with strings that come from outside ACL2, in particular, file names
+ (see the related item just above).
+
The handling of [meta]functions allowed an invariant to be violated,
that conjectures in the prover are always 100% [logic] mode. An
example is in a comment in the ACL2 source code under (deflabel
@@ -89020,7 +89037,7 @@ Subtopics
To see the ruler-extenders of an existing function symbol, fn, in a
logical [world], wrld, evaluate (ruler-extenders 'fn wrld) after
- (include-book \"kestrel/system/world-queries\" :dir :system). For
+ (include-book \"kestrel/utilities/world-queries\" :dir :system). For
example, evaluation of (ruler-extenders 'fn (w state)) provides the
ruler-extenders of fn in the current logical world.
@@ -99056,7 +99073,7 @@ Subtopics
example, if in Emacs you submit the command meta-x tags-apropos and
reply pwd at the prompt, you'll find a raw Lisp function our-pwd
that ACL2 defines as an analogue to the Linux pwd command; and,
- with meta-x tags-search applied to (pwd, you can see how ACL2
+ with meta-x tags-search applied to (our-pwd, you can see how ACL2
source code uses this utility.
@@ -99084,7 +99101,7 @@ List of a few ACL2 system utilities:
[world] w, return the number of its formal parameters.
* (body fn normalp w): For a function symbol or lambda expression fn of
[world] w, return its body ([normalize]d iff normalp is true).
- NOTE: If normalp is true, then fn should be a :tsee logic-mode
+ NOTE: If normalp is true, then fn should be a :[logic]-mode
function symbol of w.
* (conjoin lst): The conjunction of the given list of terms.
* (conjoin2 term1 term2): The conjunction of the given two terms.
@@ -109812,7 +109829,7 @@ Subtopics
See [well-founded-relation-rule] for discussion of well-founded
relations in ACL2. A related utility, well-founded-relation, may be
found in the [community-books], file
- kestrel/system/world-queries.lisp.")
+ kestrel/utilities/world-queries.lisp.")
(WELL-FOUNDED-RELATION-RULE
(RULE-CLASSES)
"Show that a relation is well-founded on a set
diff --git a/other-events.lisp b/other-events.lisp
index 4b8a549acb4..ab073c7543f 100644
--- a/other-events.lisp
+++ b/other-events.lisp
@@ -17069,7 +17069,7 @@
,@(and strengthen
'(:strengthen t))))
,@(and strengthen
- `((defthm ,(packn (list skolem-name '-strengthen))
+ `((defthm ,(add-suffix skolem-name "-STRENGTHEN")
,(defchoose-constraint-extra skolem-name bound-vars args
defchoose-body)
:hints (("Goal"
From bdfd5534d4b8bf337f409a2fb8df846060353563 Mon Sep 17 00:00:00 2001
From: Alessandro Coglio
Check whether @('x') is a symbol or a
-
@@ -183,28 +183,28 @@
" (or (variablep term) (fquotep term) - (and (terms-fns-guard-verified-p (fargs term) wrld) + (and (guard-verified-fns-listp (fargs term) wrld) (let ((fn (ffn-symb term))) (if (symbolp fn) (guard-verified-p fn wrld) - (term-fns-guard-verified-p (lambda-body fn) wrld)))))) + (guard-verified-fnsp (lambda-body fn) wrld)))))) - (define terms-fns-guard-verified-p ((terms pseudo-term-listp) - (wrld plist-worldp)) + (define guard-verified-fns-listp ((terms pseudo-term-listp) + (wrld plist-worldp)) :returns (yes/no booleanp) - :parents (term/terms-fns-guard-verified-p) + :parents (term/terms-guard-verified-fns) :short "True iff all the functions in the terms are guard-verified." (or (endp terms) - (and (term-fns-guard-verified-p (car terms) wrld) - (terms-fns-guard-verified-p (cdr terms) wrld))))) + (and (guard-verified-fnsp (car terms) wrld) + (guard-verified-fns-listp (cdr terms) wrld))))) -(define lambda-expr-fns-guard-verified-p ((lambd pseudo-lambda-expr-p) - (wrld plist-worldp)) +(define lambda-guard-verified-fnsp ((lambd pseudo-lambdap) + (wrld plist-worldp)) :returns (yes/no booleanp) :verify-guards nil :short "True iff all the functions in the lambda expression is guard-verified." - (term-fns-guard-verified-p (lambda-body lambd) wrld)) + (guard-verified-fnsp (lambda-body lambd) wrld)) (define lambda-expr-p (x (wrld plist-worldp)) :returns (yes/no booleanp) @@ -294,8 +294,8 @@ (cdr (assoc :stobjs-out bindings))) (mv term/message nil)))) -(define check-user-lambda-expr (x (wrld plist-worldp)) - :returns (mv (lambd/message (or (pseudo-lambda-expr-p lambd/message) +(define check-user-lambda (x (wrld plist-worldp)) + :returns (mv (lambd/message (or (pseudo-lambdap lambd/message) (msgp lambd/message))) (stobjs-out symbol-listp)) :prepwork ((program)) @@ -322,7 +322,7 @@ along with @('nil') as output stobjs.- The @(tsee check-user-lambda-expr) function does not terminate + The @(tsee check-user-lambda) function does not terminate if @(tsee check-user-term) does not terminate.
" (b* (((unless (true-listp x)) From 68ca8c22f6a4be811dbae22acb728b3b8b0dbd74 Mon Sep 17 00:00:00 2001 From: Eric Smith- Note that built-in @(see program)-mode functions - do not have an @('unnormalized-body') property, - even though they have definitions. - Since their translated bodies are not stored, - they are not considered to be “defined” - from the perspective of the @(tsee definedp) system utility. -
" (not (eq t (getpropc fn 'unnormalized-body t wrld)))) (define guard-verified-p ((fn/thm (or (function-namep fn/thm wrld) @@ -104,11 +97,13 @@ (eq (symbol-class fn/thm wrld) :common-lisp-compliant)) (define non-executablep ((fn (and (function-namep fn wrld) + (logicp fn wrld) (definedp fn wrld))) (wrld plist-worldp)) - ;; :returns (result (member result '(t nil :program))) + ;; :returns (result (member result '(t nil))) :guard-hints (("Goal" :in-theory (enable function-namep))) - :short "The @(tsee non-executable) status of the defined function @('fn')." + :short + "The @(tsee non-executable) status of the logic-mode, defined function @('fn')." (getpropc fn 'non-executablep nil wrld)) (define unwrapped-nonexec-body ((fn (and (function-namep fn wrld) From 49bc801f5cc85a0be04d6a0be8b917ec22354905 Mon Sep 17 00:00:00 2001 From: Alessandro CoglioThe application of a rule to a term may cause a goal to simplify to - more than one subgoal. A rule with such an application is called a - ``splitter''. Here, we explain the output produced for splitters when proof - output is enabled - (see @(see set-inhibit-output-lst)) and such reporting is turned on (as it is - by default) — that is, when the value of @('(')@(tsee - splitter-output)@(')') is true.
+ :long "When the ACL2 rewriter applies a rule to a term, a goal might + simplify to more than one subgoal. A rule with such an application is called + a ``splitter''. Here, we explain the output produced for splitters when proof + output is enabled (see @(see set-inhibit-output-lst)) and such reporting is + turned on (as it is by default) — that is, when the value of + @('(')@(tsee splitter-output)@(')') is true.
See @(see set-splitter-output) for how to turn off, or on, the reporting of
splitters. Also see @(see set-case-split-limitations) for information on how
diff --git a/defuns.lisp b/defuns.lisp
index b6b2a71f9e9..60e2db3abd8 100644
--- a/defuns.lisp
+++ b/defuns.lisp
@@ -4368,8 +4368,8 @@
(case symbol-class
(:program
(er-cmp ctx
- "~x0 is :program. Only :logic functions can have their ~
- guards verified. See :DOC verify-guards."
+ "~x0 is in :program mode. Only :logic mode functions can ~
+ have their guards verified. See :DOC verify-guards."
name))
((:ideal :common-lisp-compliant)
(let* ((recp (getpropc name 'recursivep nil wrld))
From 19c8e87eb12a4845475ae352a7b936eb58241b70 Mon Sep 17 00:00:00 2001
From: Matt Kaufmann
- Check whether @('x') is
- a @('nil')-terminated list of exactly three elements,
- whose first element is the symbol @('lambda'),
- whose second element is a list of symbols, and
- whose third element is a pseudo-term.
-
- Check whether @('x') is a symbol or a
-
- If the pseudo-function is a lambda expression, - a beta reduction is performed. -
" + If the pseudo-function is a lambda expression, + a beta reduction is performed. + " (cond ((symbolp fn) (cons-term fn terms)) (t (subcor-var (lambda-formals fn) terms (lambda-body fn))))) (defsection apply-term* - :short - "Apply- If the pseudo-function is a lambda expression, - a beta reduction is performed. -
- @(def apply-term*)" + If the pseudo-function is a lambda expression, + a beta reduction is performed. + + @(def apply-term*)" (defmacro apply-term* (fn &rest terms) `(apply-term ,fn (list ,@terms)))) -(define apply-unary-to-terms ((fn (and (pseudo-functionp fn) - (if (consp fn) - (eql 1 (len (cadr fn))) - t))) +(define apply-unary-to-terms ((fn (and (pseudo-functionp fn))) (terms pseudo-term-listp)) - :guard-hints (("Goal" :in-theory (enable PSEUDO-FUNCTIONP pseudo-lambdap))) + :guard (or (symbolp fn) + (eql 1 (len (lambda-formals fn)))) ;; :returns (applied-terms pseudo-term-listp) - :short - "Apply @('fn'), as a unary function, to each of @('terms'), - obtaining a list of corresponding terms." + :short "Apply @('fn'), as a unary function, to each of @('terms'), + obtaining a list of corresponding terms." (if (endp terms) nil (cons (apply-term* fn (car terms)) - (apply-unary-to-terms fn (cdr terms))))) + (apply-unary-to-terms fn (cdr terms)))) + :guard-hints (("Goal" :in-theory (enable pseudo-functionp pseudo-lambdap)))) (define lambda-logic-fnsp ((lambd pseudo-lambdap) (wrld plist-worldp)) :returns (yes/no booleanp) :guard-hints (("Goal" :in-theory (enable pseudo-lambdap))) - :short - "True iff the lambda expression is in logic mode, - i.e. its body is in logic mode." + :short "True iff the lambda expression is in logic mode, + i.e. its body is in logic mode." (logic-fnsp (lambda-body lambd) wrld)) (defines term/terms-no-stobjs-p @@ -135,16 +131,15 @@ (define term-no-stobjs-p ((term pseudo-termp) (wrld plist-worldp)) :returns (yes/no booleanp) :parents (term/terms-no-stobjs-p) - :short - "True iff the term has no stobjs, - i.e. all its functions have no stobjs." + :short "True iff the term has no stobjs, + i.e. all its functions have no stobjs." :long "- A term containing functions in @('*stobjs-out-invalid*') - (on which @(tsee no-stobjs-p) would cause a guard violation), - is regarded as having no stobjs, - if all its other functions have no stobjs. -
" + A term containing functions in @('*stobjs-out-invalid*') + (on which @(tsee no-stobjs-p) would cause a guard violation), + is regarded as having no stobjs, + if all its other functions have no stobjs. + " (or (variablep term) (fquotep term) (and (terms-no-stobjs-p (fargs term) wrld) @@ -166,9 +161,8 @@ ((lambd pseudo-lambdap) (wrld plist-worldp)) :returns (yes/no booleanp) :prepwork ((program)) - :short - "True iff the lambda expression has no stobjs, - i.e. its body has no stobjs." + :short "True iff the lambda expression has no stobjs, + i.e. its body has no stobjs." (term-no-stobjs-p (lambda-body lambd) wrld)) (defines term/terms-guard-verified-fns @@ -181,12 +175,12 @@ :short "True iff all the functions in the term are guard-verified." :long "- Note that if @('term') includes @(tsee mbe), - @('nil') is returned - if any function inside the @(':logic') component of @(tsee mbe) - is not guard-verified, - even when @('term') could otherwise be fully guard-verified. -
" + Note that if @('term') includes @(tsee mbe), + @('nil') is returned + if any function inside the @(':logic') component of @(tsee mbe) + is not guard-verified, + even when @('term') could otherwise be fully guard-verified. + " (or (variablep term) (fquotep term) (and (guard-verified-fns-listp (fargs term) wrld) @@ -206,16 +200,15 @@ (define lambda-expr-p (x (wrld plist-worldp-with-formals)) :returns (yes/no booleanp) - :short - "True iff @('x') is a valid translated lambda expression." + :short "True iff @('x') is a valid translated lambda expression." :long "- Check whether @('x') is a @('nil')-terminated list of exactly three elements, - whose first element is the symbol @('lambda'), - whose second element is a list of legal variable symbols without duplicates, - and whose third element is a valid translated term - whose free variables are all among the ones in the second element. -
" + Check whether @('x') is a @('nil')-terminated list of exactly three elements, + whose first element is the symbol @('lambda'), + whose second element is a list of legal variable symbols without duplicates, + and whose third element is a valid translated term + whose free variables are all among the ones in the second element. + " (and (true-listp x) (eql (len x) 3) (eq (first x) 'lambda) @@ -228,8 +221,8 @@ (wrld plist-worldp-with-formals)) :returns (yes/no booleanp) :guard-hints (("Goal" :in-theory (enable LAMBDA-EXPR-P))) - :short - "True iff all the functions in the lambda expression is guard-verified." + :short "True iff all the functions in the lambda expression + are guard-verified." (guard-verified-fnsp (lambda-body lambd) wrld)) (define check-user-term (x (wrld plist-worldp)) @@ -237,54 +230,54 @@ (msgp term/message))) (stobjs-out symbol-listp)) :prepwork ((program)) - :short - "Check whether @('x') is an untranslated term that is valid for evaluation." + :short "Check whether @('x') is an untranslated term + that is valid for evaluation." :long "
- An untranslated @(see term) is a term as entered by the user.
- This function checks @('x') by attempting to translate it.
- If the translation succeeds, the translated term is returned,
- along with the output @(see stobj)s of the term (see below for details).
- Otherwise, a structured error message is returned (printable with @('~@')),
- along with @('nil') as output stobjs.
- These two possible outcomes can be distinguished by the fact that
- the former yields a
- The ‘output stobjs’ of a term are the analogous
- of the @(tsee stobjs-out) property of a function,
- namely a list of symbols that is like a “mask” for the result.
- A @('nil') in the list means that
- the corresponding result is a non-stobj value,
- while the name of a stobj in the list means that
- the corresponding result is the named stobj.
- The list is a singleton, unless the term returns
-
- The @(':stobjs-out') and @('((:stobjs-out . :stobjs-out))') arguments - passed to @('translate1-cmp') as bindings - mean that the term is checked to be valid for evaluation. - This is stricter than checking the term to be valid for use in a theorem, - and weaker than checking the term to be valid - for use in the body of an executable function; - these different checks are performed by passing different values - to the second and third arguments of @('translate1-cmp') - (see the ACL2 source code for details). - However, for terms whose functions are all in logic mode, - validity for evaluation and validity for executable function bodies - should coincide. -
-- If @('translate1-cmp') is successful, - it returns updated bindings that associate @(':stobjs-out') - to the output stobjs of the term. -
-- The @(tsee check-user-term) function does not terminate - if the translation expands an ill-behaved macro that does not terminate. -
" + An untranslated @(see term) is a term as entered by the user. + This function checks @('x') by attempting to translate it. + If the translation succeeds, the translated term is returned, + along with the output @(see stobj)s of the term (see below for details). + Otherwise, a structured error message is returned (printable with @('~@')), + along with @('nil') as output stobjs. + These two possible outcomes can be distinguished by the fact that + the former yields a
+ The ‘output stobjs’ of a term are the analogous
+ of the @(tsee stobjs-out) property of a function,
+ namely a list of symbols that is like a “mask” for the result.
+ A @('nil') in the list means that
+ the corresponding result is a non-stobj value,
+ while the name of a stobj in the list means that
+ the corresponding result is the named stobj.
+ The list is a singleton, unless the term returns
+
+ The @(':stobjs-out') and @('((:stobjs-out . :stobjs-out))') arguments + passed to @('translate1-cmp') as bindings + mean that the term is checked to be valid for evaluation. + This is stricter than checking the term to be valid for use in a theorem, + and weaker than checking the term to be valid + for use in the body of an executable function; + these different checks are performed by passing different values + to the second and third arguments of @('translate1-cmp') + (see the ACL2 source code for details). + However, for terms whose functions are all in logic mode, + validity for evaluation and validity for executable function bodies + should coincide. +
++ If @('translate1-cmp') is successful, + it returns updated bindings that associate @(':stobjs-out') + to the output stobjs of the term. +
++ The @(tsee check-user-term) function does not terminate + if the translation expands an ill-behaved macro that does not terminate. +
" (mv-let (ctx term/message bindings) (translate1-cmp x :stobjs-out @@ -304,32 +297,31 @@ (msgp lambd/message))) (stobjs-out symbol-listp)) :prepwork ((program)) - :short - "Check whether @('x') is - an untranslated lambda expression that is valid for evaluation." + :short "Check whether @('x') is + an untranslated lambda expression that is valid for evaluation." :long "- An untranslated @(see lambda) expression is - a lambda expression as entered by the user. - This function checks whether @('x')is - a @('nil')-terminated list of exactly three elements, - whose first element is the symbol @('lambda'), - whose second element is a list of legal variable symbols without duplicates, - and whose third element is an untranslated term that is valid for evaluation. -
-- If the check succeeds, the translated lambda expression is returned, - along with the output @(see stobj)s of the body of the lambda expression - (see @(tsee check-user-term) for an explanation - of the output stobjs of a term). - Otherwise, a possibly structured error message is returned - (printable with @('~@')), - along with @('nil') as output stobjs. -
-- The @(tsee check-user-lambda) function does not terminate - if @(tsee check-user-term) does not terminate. -
" + An untranslated @(see lambda) expression is + a lambda expression as entered by the user. + This function checks whether @('x')is + a @('nil')-terminated list of exactly three elements, + whose first element is the symbol @('lambda'), + whose second element is a list of legal variable symbols without duplicates, + and whose third element is an untranslated term that is valid for evaluation. + ++ If the check succeeds, the translated lambda expression is returned, + along with the output @(see stobj)s of the body of the lambda expression + (see @(tsee check-user-term) for an explanation + of the output stobjs of a term). + Otherwise, a possibly structured error message is returned + (printable with @('~@')), + along with @('nil') as output stobjs. +
++ The @(tsee check-user-lambda) function does not terminate + if @(tsee check-user-term) does not terminate. +
" (b* (((unless (true-listp x)) (mv `("~x0 is not a NIL-terminated list." (#\0 . ,x)) nil)) @@ -352,26 +344,26 @@ :short "Translated term that a call to the macro translates to." :long "- This function translates a call to the macro - that only includes its required formal arguments, - returning the resulting translated term. -
-- Note that since the macro is in the ACL2 world - (because of the @(tsee macro-namep) guard), - the translation of the macro call should not fail. - However, the translation may not terminate, - as mentioned in @(tsee check-user-term). -
-- Note also that if the macro has optional arguments, - its translation with non-default values for these arguments - may yield different terms. - Furthermore, if the macro is sensitive - to the “shape” of its arguments, - calls with argument that are not the required formal arguments - may yield different terms. -
" + This function translates a call to the macro + that only includes its required formal arguments, + returning the resulting translated term. + ++ Note that since the macro is in the ACL2 world + (because of the @(tsee macro-namep) guard), + the translation of the macro call should not fail. + However, the translation may not terminate, + as mentioned in @(tsee check-user-term). +
++ Note also that if the macro has optional arguments, + its translation with non-default values for these arguments + may yield different terms. + Furthermore, if the macro is sensitive + to the “shape” of its arguments, + calls with argument that are not the required formal arguments + may yield different terms. +
" (mv-let (term stobjs-out) (check-user-term (cons mac (macro-required-args mac wrld)) wrld) (declare (ignore stobjs-out)) @@ -383,10 +375,10 @@ :short "Formula expressing the guard obligation of the term." :long "- The case in which @('term') is a symbol is dealt with separately - because @(tsee guard-obligation) - interprets a symbol as a function or theorem name, not as a variable. -
" + The case in which @('term') is a symbol is dealt with separately + because @(tsee guard-obligation) + interprets a symbol as a function or theorem name, not as a variable. + " (b* (((when (symbolp term)) *t*) ((mv erp val) (guard-obligation term nil nil __function__ state)) ((when erp) From 0d9e4c79931254ac6bd7a6db8b49ac5a9bd06b20 Mon Sep 17 00:00:00 2001 From: Alessandro Coglio