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