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 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.