----------------------------------------------------------------------
CBV_CONV                                                  (computeLib)
----------------------------------------------------------------------
CBV_CONV : compset -> conv

SYNOPSIS
Call by value rewriting.

LIBRARY
compute

DESCRIBE
The conversion {CBV_CONV} expects a simplification set and a
term. Its term argument is rewritten using the equations added in the
simplification set. The strategy used is somewhat similar to ML’s,
that is call-by-value (arguments of constants are completely reduced
before the rewrites associated to the constant are applied) with weak
reduction (no reduction of the function body before the function is
applied). The main differences are that beta-redexes are reduced with
a call-by-name strategy (the argument is not reduced), and reduction
under binders is done when it occurs in a position where it cannot be
substituted.

The simplification sets are mutable objects, this means they are
extended by side-effect. The function {new_compset} will create
a new set containing reflexivity ({REFL_CLAUSE}), plus the supplied rewrites.
Theorems can be added to an existing compset with the function {add_thms}.

It is also possible to add conversions to a simplification set with
{add_conv}. The only restriction is that a constant ({c}) and an arity
({n}) must be provided. The conversion will be called only on terms in
which {c} is applied to {n} arguments.

Two theorem “preprocessors” are provided to control the strictness
of the arguments of a constant. {lazyfy_thm} has pattern variables on
the left hand side turned into abstractions on the right hand
side. This transformation is applied on every conjunct, and removes
prenex universal quantifications. A typical example is {COND_CLAUSES}:

  (COND T a b = a) /\ (COND F a b = b)

Using these equations is very inefficient because both {a}
and {b} are evaluated, regardless of the value of the boolean
expression. It is better to use {COND_CLAUSES} with the form above

  (COND T = \a b. a) /\ (COND F = \a b. b)

The call-by-name evaluation of beta redexes avoids computing
the unused branch of the conditional.

Conversely, {strictify_thm} does the reverse transformation. This is
particularly relevant for {LET_DEF}:

  LET = \f x. f x   -->   LET f x = f x

This forces the evaluation of the argument before reducing the
beta-redex. Hence the usual behaviour of {LET}.

It is necessary to provide rules for all the constants appearing in the
expression to reduce (all also for those that appear in the right hand
side of a rule), unless the given constant is considered as a
constructor of the representation chosen. As an example,
{reduceLib.num_compset} creates a new simplification set with all the
rules needed for basic boolean and arithmetical calculations built in.

EXAMPLE

   - val rws = computeLib.new_compset [computeLib.lazyfy_thm COND_CLAUSES];
   > val rws = <compset> : compset

   - computeLib.CBV_CONV rws ``(\x.x) ((\x.x) if T then 0+0 else 10)``;
   > val it = |- (\x. x) ((\x. x) (if T then 0 + 0 else 10)) = 0 + 0 : thm

   - computeLib.CBV_CONV (reduceLib.num_compset())
              ``if 100 - 5 * 5 < 80  then 2 EXP 16 else 3``;
   > val it = |- (if 100 - 5 * 5 < 80 then 2 ** 16 else 3) = 65536 : thm


Failing to give enough rules may make {CBV_CONV} build a
huge result, or even loop. The same may occur if the initial term to
reduce contains free variables.

   val eqn = bossLib.Define `exp n p = if p=0 then 1 else n * (exp n (p-1))`;
   val _ = computeLib.add_thms [eqn] rws;

   - computeLib.CBV_CONV rws ``exp 2 n``;
   > Interrupted.

   - computeLib.set_skip rws ``COND`` (SOME 1);
   > val it = () : unit

   - computeLib.CBV_CONV rws ``exp 2 n``;
   > val it = |- exp 2 n = if n = 0 then 1 else 2 * exp 2 (n - 1) : thm

The first invocation of {CBV_CONV} loops since the exponent
never reduces to 0.  Below the first steps are computed:

    exp 2 n
    if n = 0 then 1 else 2 * exp 2 (n-1)
    if n = 0 then 1 else 2 * if (n-1) = 0 then 1 else 2 * exp 2 (n-1-1)
    ...

The call to {set_skip} means that if the constants {COND}
appears applied to one argument and does not create a redex (in the
example, if the condition does not reduce to {T} or {F}), then the
forthcoming arguments (the two branches of the conditional) are not
reduced at all.

FAILURE
Should never fail. Nonetheless, using rewrites with assumptions may
cause problems when rewriting under abstractions. The following
example illustrates that issue.

   - val th = ASSUME “0 = x”;
   - val tm = Term`\(x:num). x = 0`;
   - val rws = from_list [th];
   - CBV_CONV rws tm;

This fails because the 0 is replaced by {x}, making the assumption
{0 = x}. Then, the abstraction cannot be rebuilt since {x} appears
free in the assumptions.

SEEALSO
numLib.REDUCE_CONV, computeLib.bool_compset, bossLib.EVAL.

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