Library

Module

Module type

Parameter

Class

Class type

#### Atomic pattern constructor representation

`module TC : sig ... end`

Representation of an atomic pattern constructor.

`module TCMap : sig ... end`

A mapping with atomic pattern constructors as keys.

#### Decision trees for rewriting

`type tree_cond = `

Representation of a branching conditions.

**NOTE** that when performing a `tree_cond.CondFV`

check, we are concerned about variables that were bound in the term being reduced and that may appear free while deconstructing it. If the term being reduced contains free variables, those can appear in a subterm even if not in the array.

`val tree_cond : tree_cond Lplib.Base.pp`

Substitution of variables in a RHS. During the filtering process, some subterms of the filtered term may be stored in an array. Let `v`

be that array. When a leaf is reached, variables of the LHS that are bound in the RHS must be substitued. An element `(p, (v, xs))`

of the substitution substitutes variable `v`

of the RHS by term `p`

of array `v`

. In the case of higher order patterns, `p`

may need to be itself subsituted with *bound* variables `xs`

collected when traversing binders.

`type 'rhs tree = `

`| Fail` | (* Empty decision tree, used when there are no rewriting rules. *) | ||||||||||||

`| Leaf of rhs_substit * 'rhs` | (* The value | ||||||||||||

`| Cond of {`
`}` | (* Conditional branching according to a condition. *) | ||||||||||||

`| Eos of 'rhs tree * 'rhs tree` | (* End of stack node, branches on left tree if the stack is finished, on the right if it isn't. Required when there are rules with a lower arity than some other rule above and when | ||||||||||||

`| Node of {`
`}` | (* Arbitrarily branching node allowing to perform switches (a switch is the matching of a pattern). The node contains one subtree per switch, plus a possible default case as well as an abstraction case. *) |

Representation of a tree. The definition relies on parameters since module `Term`

depends on the current module, and that would thus produce a dependency cycle. However it should be understood that parameter ``rhs`

will only be instantiated with `(Term.term_env, Term.term) Bindlib.mbinder`

(i.e., the representation of a RHS).

`val tree_capacity : 'r tree -> int`

`tree_capacity t`

computes the capacity of tree `t`

. During evaluation the terms that are being filtered by the patterns have to be saved in order to be bound in the right hand side of the rule, or because they must verify a constraint. The capacity is the maximum number of such terms that may need to be saved. More precisely, let `P`

be the set of all paths from the root to leaves in the tree `t`

, and let `nb_store`

be a function mapping a path to the number of nodes that have the `store`

tag to `true`

. We then define the capacity `c`

of `t`

is `c = max{nb_store(p) | p ∈ P}`

.

A tree with its capacity and as lazy structures. For the definition of the capacity, see `Tree_type.tree_capacity`

. Laziness allows to (sometimes) avoid creating several times the same trees when the rules are not given in one go.

`val empty_dtree : 'rhs dtree`

`empty_dtree`

is the empty decision tree.