OK-IF
conditional exit from break-rewrite
Major Section: BREAK-REWRITE
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 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.
