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.

See also

bossLib.EVAL