EVAL_TAC
bossLib.EVAL_TAC : tactic
Evaluate a goal deductively.
Applying EVAL_TAC to a goal A ?- g results in EVAL being applied
to g to obtain |- g = g'. This theorem is used to transform the goal
to A ?- g'.
The notion of evaluation is based around rules for replacing constants
by their (equational) definitions. Thus EVAL_TAC is currently suited
to evaluation of expressions that look like functional programs.
Evaluation of inductive relations is not currently supported.
Failure
Shouldn't fail, but may diverge.
Example
EVAL_TAC reduces the goal
?- P (REVERSE (FLAT [[x; y]; [a; b; c; d]])) to the goal
?- P [d; c; b; a; y; x]
Comments
The main problem with EVAL_TAC is knowing when it will terminate. One
typical cause of non-termination is that a constant in the goal has not
been added to the_compset. Another is that a test in a conditional in
the expression may involve a variable.
Symbolic evaluation.