Rewrite Rule Definitions

©1998 Research Institute for Symbolic Computation (RISC-Linz)

Package Description

This package contains the implementation of command Def for defining rewrite rules.

Implementation

Begin

FormFunction

Syntax call
FormFunction[
params,lvars,term,cnd ]
Input
params,lvars : lists of Mathematica symbols
term : a term,
cnd : pair of the form { ppeqs, eqs } where ppeqs is a list of parameter passing equations and eqs is a list of initial equations.

These four terms are those involved in the encoding of a conditional rewrite rule R.
Output
the encoding corresponding to R.
Implementation

Def

Syntax call
Def[
vars, {, ... , }]
or
Def[
vars, {, ... , }, TypeCheck->b ]
Input

Effect
for every conditional rewrite rule of the form f[ , ... , ] → t ⇐ ∧"ï∧ perform the following steps
õ! type check only if the option TypeCheck ->True is specified, or no TypeCheck option is specified but
type-checking is switched on;
if is ill typed then give an error message and return "⊥",
õ! add to the list of conditional rewrite rules associated with f.
õ! Return "⊤" if all conditional rewrite rules were successfully inserted in the corresponding rewrite rule lists.
Remarks
The encoding of a CRR of the form f[ , ... , ] → t ⇐ ∧"ï∧ is
Function[{, ... , }, Module[{, ... , }, RewritesTo[t , {, ... , }, {, ... ,}]]] ,
where , ... , are the rule variables, and is added to the list RewriteRuleList[f] of conditional rewrite rules
associated with f.
Implementation

Uniform

Syntax call
Uniform[
term ]
Input
term : a term
Output
if term is a constant then return {{},{}}
if term is of the form ] then return a pair {vars,eqs} where vars is a
list of n fresh variables ,..., and eqs is the list of parameter passing equations
Example
Uniform[f[x,r[a],b]] returns the pair
{{w\$144,w\$145,w\$146},{w\$144≈x,w\$145≈r[a],w\$146≈b}}
Implementation