RESTR_EVAL_CONV
computeLib.RESTR_EVAL_CONV : term list -> conv
Symbolically evaluate a term, except for specified constants.
An application RESTR_EVAL_CONV [c1, ..., cn] M evaluates the term M
in the call-by-value style of EVAL. When a type instance c of any
element in c1,...,cn is encountered, c is not expanded by
RESTR_EVAL_CONV. The effect is that evaluation stops at c (even
though any arguments to c may be evaluated). This facility can be used
to control EVAL_CONV to some extent.
Failure
Never fails, but may diverge.
Example
In the following, we first attempt to map the factorial function FACT
over a list of variables. This attempt goes into a loop, because the
conditional statement in the evaluation rule for FACT is never
determine when the argument is equal to zero. However, if we suppress
the evaluation of FACT, then we can return a useful answer.
- EVAL (Term `MAP FACT [x; y; z]`); (* loops! *)
> Interrupted.
- val [FACT] = decls "FACT"; (* find FACT constant *)
> val FACT = `FACT` : term
- RESTR_EVAL_CONV [FACT] (Term `MAP FACT [x; y; z]`);
> val it = |- MAP FACT [x; y; z] = [FACT x; FACT y; FACT z] : thm
Controlling symbolic evaluation when it loops or becomes exponential.
See also
bossLib.EVAL,
computeLib.RESTR_EVAL_TAC,
computeLib.RESTR_EVAL_RULE,
Term.decls