----------------------------------------------------------------------
monitoring                                                (computeLib)
----------------------------------------------------------------------
monitoring : (term -> bool) option ref

SYNOPSIS
Monitoring support for evaluation.

KEYWORDS
evaluation, monitoring.

DESCRIBE
The reference variable {monitoring} provides a simple way to view the
operation of {EVAL}, {EVAL_RULE}, and {EVAL_TAC}. The initial value of
{monitoring} is {NONE}. If one wants to monitor the expansion of a function,
defined with constant {c}, then setting {monitoring} to {SOME (same_const c)}
will tell the system to print out the expansion of {c} by the evaluation
entrypoints. To monitor the expansions of a collection of functions, defined
with {c1},...,{cn}, then {monitoring} can be set to

   SOME (fn x => same_const c1 x orelse ... orelse same_const cn x)


FAILURE
Never fails.

EXAMPLE

- val [FACT] = decls "FACT";
> val FACT = `FACT` : term

- computeLib.monitoring := SOME (same_const FACT);

- EVAL (Term `FACT 4`);
FACT 4 = (if 4 = 0 then 1 else 4 * FACT (PRE 4))
FACT 3 = (if 3 = 0 then 1 else 3 * FACT (PRE 3))
FACT 2 = (if 2 = 0 then 1 else 2 * FACT (PRE 2))
FACT 1 = (if 1 = 0 then 1 else 1 * FACT (PRE 1))
FACT 0 = (if 0 = 0 then 1 else 0 * FACT (PRE 0))
> val it = |- FACT 4 = 24 : thm


SEEALSO
computeLib.RESTR_EVAL_CONV, Term.decls.

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