Conditional Rewrite Rules
-------------------------

A rewrite rule can also be "conditional", written in the form
`OLD := NEW :: COND'.  (There is also the obsolete
form `[OLD, NEW, COND]'.)  If a COND part
is present in the
rule, this is an additional condition that must be satisfied before
the rule is accepted.  Once OLD has been successfully matched
to the target expression, COND is evaluated (with all the
meta-variables substituted for the values they matched) and simplified
with `a s' (`calc-simplify').  If the result is a nonzero
number or any other object known to be nonzero (See Declarations),
the rule is accepted.  If the result is zero or if it is a symbolic
formula that is not known to be nonzero, the rule is rejected.
See Logical Operations, for a number of functions that return
1 or 0 according to the results of various tests.

For example, the formula `n > 0' simplifies to 1 or 0 if `n' is
replaced by a positive or nonpositive number, respectively (or if `n'
has been declared to be positive or nonpositive).  Thus, the rule
`f(x,y) := g(y+x,x) :: x+y > 0' would apply to `f(0, 4)' but not to
`f(-3, 2)' or `f(12, a+1)' (assuming no outstanding declarations for
`a').  In the case of `f(-3, 2)', the condition can be shown not to be
satisfied; in the case of `f(12, a+1)', the condition merely cannot be
shown to be satisfied, but that is enough to reject the rule.

While Calc will use declarations to reason about variables in the
formula being rewritten, declarations do not apply to meta-variables.
For example, the rule `f(a) := g(a+1)' will match for any values of
`a', such as complex numbers, vectors, or formulas, even if `a' has
been declared to be real or scalar.  If you want the meta-variable `a'
to match only literal real numbers, use `f(a) := g(a+1) :: real(a)'.
If you want `a' to match only reals and formulas which are provably
real, use `dreal(a)' as the condition.

The `::' operator is a shorthand for the `condition' function; `OLD :=
NEW :: COND' is equivalent to the formula `condition(assign(OLD, NEW),
COND)'.

If you have several conditions, you can use `... :: c1 :: c2 :: c3' or
`... :: c1 && c2 && c3'.  The two are entirely equivalent.

It is also possible to embed conditions inside the pattern: `f(x ::
x>0, y) := g(y+x, x)'.  This is purely a notational convenience,
though; where a condition appears in a rule has no effect on when it
is tested.  The rewrite-rule compiler automatically decides when it is
best to test each condition while a rule is being matched.

Certain conditions are handled as special cases by the rewrite rule
system and are tested very efficiently: Where `x' is any
meta-variable, these conditions are `integer(x)', `real(x)',
`constant(x)', `negative(x)', `x >= y' where `y' is either a constant
or another meta-variable and `>=' may be replaced by any of the six
relational operators, and `x % a = b' where `a' and `b' are constants.
Other conditions, like `x >= y+1' or `dreal(x)', will be less
efficient to check since Calc must bring the whole evaluator and
simplifier into play.

An interesting property of `::' is that neither of its arguments will
be touched by Calc's default simplifications.  This is important
because conditions often are expressions that cannot safely be
evaluated early.  For example, the `typeof' function never remains in
symbolic form; entering `typeof(a)' will put the number 100 (the type
code for variables like `a') on the stack.  But putting the condition
`... :: typeof(a) = 6' on the stack is safe since `::' prevents the
`typeof' from being evaluated until the condition is actually used by
the rewrite system.

Since `::' protects its lefthand side, too, you can use a dummy
condition to protect a rule that must itself not evaluate early.  For
example, it's not safe to put `a(f,x) := apply(f, [x])' on the stack
because it will immediately evaluate to `a(f,x) := f(x)', where the
meta-variable-ness of `f' on the righthand side has been lost.  But
`a(f,x) := apply(f, [x]) :: 1' is safe, and of course the condition
`1' is always true (nonzero) so it has no effect on the functioning of
the rule.  (The rewrite compiler will ensure that it doesn't even
impact the speed of matching the rule.)