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.

Usage

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

Flattening

PrintVarDecl

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

End