1\DOC EVAL_TAC
2
3\TYPE {EVAL_TAC : tactic}
4
5\SYNOPSIS
6Evaluate a goal deductively.
7
8\KEYWORDS
9tactic, evaluation.
10
11\DESCRIBE
12Applying {EVAL_TAC} to a goal {A ?- g} results in {EVAL} being applied
13to {g} to obtain {|- g = g'}. This theorem is used to transform the goal
14to {A ?- g'}.
15
16The notion of evaluation is based around rules for replacing constants
17by their (equational) definitions. Thus {EVAL_TAC} is currently
18suited to evaluation of expressions that look like functional programs.
19Evaluation of inductive relations is not currently supported.
20
21\FAILURE
22Shouldn't fail, but may diverge.
23
24\EXAMPLE
25{EVAL_TAC} reduces the goal {?-  P (REVERSE (FLAT [[x; y]; [a; b; c; d]]))}
26to the goal
27{
28   ?- P [d; c; b; a; y; x]
29}
30
31\COMMENTS
32The main problem with {EVAL_TAC} is knowing when it will terminate. One
33typical cause of non-termination is that a constant in the goal has not
34been added to {the_compset}. Another is that a test in a conditional in
35the expression may involve a variable.
36
37\USES
38Symbolic evaluation.
39
40\SEEALSO
41bossLib.EVAL.
42
43\ENDDOC
44