package lambdapi
Legend:
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 =
| CondNL of int * int(*

Are the terms at the given indices convertible? We enforce the invariant that the first element is a point of reference, which appears in all the convertibility conditions involving a given non-linear variable.

*)
| CondFV of int * int array(*

Are the (indexed) bound variables (which are free at the time of the checking) of the term at the given index in the array?

*)

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
type rhs_substit = (int * (int * int array)) list

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 Leaf(m, rhs) stores the RHS rhs of the rewriting rule that can be applied upon reaching the leaf. The association list m is used to construct the environment of the RHS. Note that we do not need to use a map here since we only need to insert at the head, and iterate over the elements of the structure.

*)
| Cond of {
ok : 'rhs tree;(*

Branch to follow if the condition is verified.

*)
cond : tree_cond;(*

The condition to test.

*)
fail : 'rhs tree;(*

Branch to follow if the condition is not verified.

*)
}		(*

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 Term.sym.sym_mstrat is Term.match_strat.Sequen.

*)
| Node of {
swap : int;(*

Indicates on which term of the input stack (counting from the head), the next switch is to be done.

*)
store : bool;(*

Whether to store the current term. Stored terms might be used in the right hand side, are for constraint checks.

*)
children : 'rhs tree TCMap.t;(*

Subtrees representing the matching of available constructors.

*)
abstraction : (int * 'rhs tree) option;(*

Specialisation by an abstraction with the involved free variable.

*)
product : (int * 'rhs tree) option;(*

Specialisation by product with the involved free variable.

*)
default : 'rhs tree option;(*

When the available patterns contain a wildcard, this subtree is used as a last resort (if none of the children match).

*)
}		(*

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}.

type 'rhs dtree = int Lazy.t * 'rhs tree Lazy.t

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.