# Rewrite Rule Definitions

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

##### NO WARRANTY

## 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