----------------------------------------------------------------------
EVAL_TAC                                                     (bossLib)
----------------------------------------------------------------------
EVAL_TAC : tactic

SYNOPSIS
Evaluate a goal deductively.

KEYWORDS
tactic, evaluation.

DESCRIBE
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.

USES
Symbolic evaluation.

SEEALSO
bossLib.EVAL.

----------------------------------------------------------------------