Ok-if
Conditional exit from break-rewrite
Recall that one way to exit from a break-rewrite interactive
break is to type the command :ok. See brr-commands. The
:ok command exits silently, without printing the result of attempting to
apply the rule that caused the break. The :ok-if command takes a term
as an argument and is like :ok but exits only if the term evaluates to
non-nil.
Example Form:
:ok-if (null (brr@ :wonp))
General Form:
:ok-if expr
where expr is a term involving no free variables other than state
and returning one non-state result which is treated as Boolean. This
form is intended to be executed from within break-rewrite (see break-rewrite).
Consider first the simple situation that the (ok-if term) is a command
read by break-rewrite. Then, if the term is non-nil,
break-rewrite exits and otherwise it does not.
More generally, ok-if returns an ACL2 error triple (mv erp val
state). (See ld or see programming-with-state for more on
error triples.) If any form being evaluated as a command by
break-rewrite returns the triple returned by (ok-if term) then the
effect of that form is to exit break-rewrite if term is non-nil.
Thus, one might define a function or macro that returns the value of
ok-if expressions on all outputs and thus create a convenient new way to
exit break-rewrite.
The exit test, term, generally uses brr@ to access context
sensitive information about the attempted rule application. See brr@.
Ok-if is useful inside of command sequences produced by break conditions.
See monitor. :ok-if is most useful after an :eval command
has caused break-rewrite to try to apply the rule because in the
resulting break environment expr can access such things as whether the
rule succeeded, if so, what term it produced, and if not, why. There is no
need to use :ok-if before :evaling the rule since the same effects
could be achieved with the break condition on the rule itself. Perhaps we
should replace this concept with :eval-and-break-if? Time will
tell.
