1\DOC RESTR_EVAL_CONV 2 3\TYPE {RESTR_EVAL_CONV : term list -> conv} 4 5\SYNOPSIS 6Symbolically evaluate a term, except for specified constants. 7 8\KEYWORDS 9evaluation. 10 11\DESCRIBE 12An application {RESTR_EVAL_CONV [c1, ..., cn] M} evaluates the term {M} 13in the call-by-value style of {EVAL}. When a type instance {c} of any 14element in {c1},...,{cn} is encountered, {c} is not expanded by 15{RESTR_EVAL_CONV}. The effect is that evaluation stops at {c} (even 16though any arguments to {c} may be evaluated). This facility can be used 17to control {EVAL_CONV} to some extent. 18 19\FAILURE 20Never fails, but may diverge. 21 22\EXAMPLE 23In the following, we first attempt to map the factorial function {FACT} 24over a list of variables. This attempt goes into a loop, because the 25conditional statement in the evaluation rule for {FACT} is never 26determine when the argument is equal to zero. However, if we suppress 27the evaluation of {FACT}, then we can return a useful answer. 28{ 29 - EVAL (Term `MAP FACT [x; y; z]`); (* loops! *) 30 > Interrupted. 31 32 - val [FACT] = decls "FACT"; (* find FACT constant *) 33 > val FACT = `FACT` : term 34 35 - RESTR_EVAL_CONV [FACT] (Term `MAP FACT [x; y; z]`); 36 37 > val it = |- MAP FACT [x; y; z] = [FACT x; FACT y; FACT z] : thm 38} 39 40\USES 41Controlling symbolic evaluation when it loops or becomes exponential. 42 43\SEEALSO 44bossLib.EVAL, computeLib.RESTR_EVAL_TAC,computeLib.RESTR_EVAL_RULE, 45Term.decls. 46 47\ENDDOC 48