		Search-engine friendly clone of the ACL2 documentation.

Break-rewrite

Brr-commands

Below is a list of commonly used break-rewrite keyword commands. These are only defined within the breaks caused by monitors on runes in the process of being considered by the ACL2 rewriter. These breaks interact with you from within a wormhole and are handled by ld (the same function that manages ACL2's top-level interactive read-eval-print loop). So within certain limitations imposed by wormholes, you can evaluate any command you would at the top-level of ACL2 in addition to the special commands below.

Many break commands display terms, e.g., the target being rewritten, and “large” terms are “eviscerated” (i.e., abbreviated) before printing. These commands have corresponding commands suffixed with a ``+'' that avoid evisceration so that the terms in question are printed in full. See brr-evisc-tuple. The notation ``:ancestors[+]'' below indicates that the :ancestors command may print abbreviate terms but the :ancestors+ command does not.

:a!                abort to ACL2 top-level
:ancestors[+]      negations of backchaining hypotheses being pursued
:btm[+]            bottom-most frame in :path
:eval              try the rule (i.e., recursively try to relieve
                     the hypotheses and other conditions, possibly
                     producing other breaks) and return to this
                     break afterwards so you can query results
:eval!             :eval but remove all monitors first (see below)
:eval$ runes       :eval but first add monitors for runes (see below)
:explain-near-miss[+]
                   print an explanation of why the rule's pattern failed
                     to match the :target; only relevant in a break caused
                     by a near miss
:failure-reason[+] reason rule failed (after :eval)
:final-ttree[+]    ttree after :eval (see :DOC ttree)
:frame[+] i        ith frame in :path
:geneqv[+]         generated equivalence relation to be maintained
:go                :eval but don't return to this break, just
                     print the result of the try
:go!               :go but first remove all monitors (see below)
:go$ runes         :go but first add monitors for runes (see below)
:help              this message
:hyp i             ith hypothesis of the rule
:hyps              hypotheses of the rule
:initial-ttree[+]  ttree before :eval (see :DOC ttree)
:lhs[+]            left-hand side of rule's conclusion (or, in the case
                     of :rewrite-quoted-constant rules of form [2], the
                     right-hand side!); this is the pattern that the
                     target must match for this :rewrite rule to fire
:max-term[+]       maximal term of a :linear lemma; this is the pattern
                     that the target must match for this :linear rule to
                     fire
:ok                like :go, but don't print the result of the try
:ok!               :ok but first remove all monitors (see below)
:ok$ runes         :ok but first add monitors for runes (see below)
:path[+]           rewriter's path from top clause to :target
:poly-list[+]      list of polynomials (after :eval) of a linear rule,
                     where the leading term of each is enclosed in an
                     extra set of parentheses
:pot-list[+]       set of polynomials governing :target,
                     organized by maximal term
:rewritten-rhs[+]  rewritten :rhs (after :eval) of a rewrite rule
:rhs               right-hand side of rule's conclusion (or, in the case
                     of :rewrite-quoted-constant rules of form [2], the
                     left-hand side!)
:standard-help     :help message from ACL2 top-level
:target[+]         term being rewritten
:top[+]            top-most frame in :path
:type-alist[+]     type assumptions governing :target
:unify-subst[+]    substitution making :lhs equal :target
:wonp              indicates whether application succeeded (after :eval)

The form (brr@ :cmd), when evaluated within a break, will return the value that is only printed by certain of the keyword commands above. This is particularly useful when programming break conditions. See monitor.

Since you're actually in a general read-eval-print loop when interacting with break-rewrite you may type the usual ACL2 commands like :pbt or :pe or even defun and defthm. You cannot modify stobjs or files from within the break. However, all state changes you cause from within break-rewrite are lost when you exit or :eval the rule.

Note that if you are breaking on a monitored linear rule, several of the commands listed above do not apply: :lhs, :rhs, :initial-ttree, and :final-ttree. The pattern used to fire a linear rule is found with the command :max-term. In addition, :rewritten-rhs also does not apply to linear rules, 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.

See the discussion of form [2] :rewrite-quoted-constant rules for an explanation of the swapped meanings of ``:lhs'' and ``:rhs.''

The commands :eval$, :go$, and :ok$ take an argument, called runes, which may be a list of runes and/or runic designators (see rune) or a single rune or runic designator. For each rune in runes, these commands execute :monitor rune t, and then execute :eval, :go or :ok as appropriate.

This is useful if you want to monitor the use of a “secondary” rune only during the attempt to apply a “primary” rune: install the monitor on the secondary rune inside the break caused by the primary rune. In the case of :eval$, when the attempt to apply the primary rune is finished you will be back in the interactive break and can inspect the results. You will notice that the secondary rune is still on the list of monitored-runes. However, when you exit that break monitored-runes will be restored to its earlier value. In the case of go$ and ok$, no interactive break occurs after the primary rune has been applied.

Similar remarks apply to :eval!, :go!, and :ok! except they first :unmonitor :all, before proceeding with the appropriate :eval, :go, or :ok. These commands are useful if you want no breaks to occur while attempting to apply the rune that caused the current break.

Recall (from the discussion of monitors) that break conditions terms installed as part of break criteria do not just determine whether a break occurs but can compute the initial break commands fed to the interactive loop. Thus, for example, you can install a monitor that causes the rewriter to not only break when a certain rune is used, but then automatically print information, proceed from the break, inspect the result, and then either exit the break or prompt for user input. See the discussion in monitor.

Note: If you use commands that change the monitored runes during a break, e.g., monitor, unmonitor, or :eval!, :eval$, etc., then abort during the recursion, the list of monitored runes will not necessarily be restored to its original top-level setting.