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