#### lambdapi

Library

Module

Module type

Parameter

Class

Class type

`val head : Term.term Lplib.Base.pp`

`head ppf t`

prints head of term `t`

.

`type arg = {`

`arg_path : int list;` | (* Reversed path to the subterm. *) |

`arg_rank : int;` | (* Number of binders along the path. *) |

`}`

Representation of a subterm in argument position in a pattern.

`val arg_path : int list Lplib.Base.pp`

`arg_path ppf pth`

prints path `pth`

as a dotted list of integers to formatter `ppf`

.

**NOTE** the `arg_path`

describes a path to the represented term. The idea is that each index of the list tells under which argument to go next (counting from `0`

), starting from the end of the list. For example let us consider the term `f x (g a b)`

. The subterm `a`

is accessed with the path `[0 ; 1]`

(go under the second argument `g a b`

first, and then take its first argument). Similarly, `b`

is encoded as `[1 ; 1]`

and `x`

as `[0]`

. Note that a value `[]`

does not describe a valid path. Also, a `0`

index is used when going under abstractions. In that case, the field `arg_rank`

is incremented.

`type clause = {`

`c_lhs : Term.term array;` | (* Left hand side of a rule. *) |

`c_rhs : Term.rhs * int;` | (* Right hand side of a rule. *) |

`c_subst : Tree_type.rhs_substit;` | (* Substitution of RHS variables. *) |

`xvars_nb : int;` | (* Number of extra variables in the rule RHS. *) |

`cond_pool : CP.t;` | (* Condition pool with convertibility and free variable constraints. *) |

`}`

A clause matrix row (schematically *c_lhs ↪ c_rhs if cond_pool*).

`val clause : clause Lplib.Base.pp`

`clause ppf c`

pretty prints clause `c`

to formatter `ppf`

.

`type t = {`

`clauses : clause list;` | (* The rules. *) |

`slot : int;` | (* Index of next slot to use in |

`positions : arg list;` | (* Positions of the elements of the matrix in the initial term. We must have |

`}`

Type of clause matrices.

`val pp : t Lplib.Base.pp`

`pp ppf cm`

pretty prints clause matrix `cm`

to formatter `ppf`

.

`type decision = `

`| Yield of clause` | (* Rewrite to a RHS when a LHS filters the input. *) |

`| Check_stack` | (* Check whether the stack is empty (used to handle multiple arities with the sequential strategy set). *) |

`| Specialise of int` | (* Specialise the matrix against constructors on a given column. *) |

`| Condition of Tree_type.tree_cond` | (* Binary decision on the result of the test of a condition. A condition |

Available operations on clause matrices. Every operation corresponds to decision made during evaluation. This type is not used outside of the compilation process.

`val is_treecons : Term.term -> bool`

`is_treecons t`

tells whether term `t`

corresponds to a constructor (see `Tree_type.TC.t`

) that is a candidate for a specialization.

`val is_empty : t -> bool`

`is_empty m`

returns whether matrix `m`

is empty. Note that a matrix is empty when it has *no* row; not when it has empty rows.

`val score : Term.term list -> float`

`score c`

returns the score heuristic for column `c`

. This score is the number of tree constructors divided by the number of conditions.

`val discard_cons_free : clause list -> int array`

`discard_cons_free r`

returns the indexes of columns on which a specialisation can be performed. They are the columns with at least one symbol as head term.

`val choose : t -> int option`

`choose m`

returns the index of column to switch on.

`is_exhausted p c`

tells whether clause `r`

whose terms are at positions in `p`

can be applied or not.

`val yield : Term.match_strat -> t -> decision`

`yield m`

returns the next operation to carry out on matrix `m`

, that is, either specialising, solving a constraint or rewriting to a rule.

```
val get_cons :
int Term.VarMap.t ->
Term.term list ->
(Tree_type.TC.t * Term.term) list
```

`get_cons id l`

returns a list of unique (and sorted) tuples containing tree construcors from `l`

and the original term. Variables are assigned id `id`

.

`val store : t -> int -> bool`

`store m c`

is true iff a term of column `c`

of matrix `m`

contains a pattern variable. In that case, the term needs to be stored into the `vars`

array (in order to build the substitution).

`val index_var : int Term.VarMap.t -> Term.term -> int`

`val mk_wildcard : Term.VarSet.t -> Term.term`

`mk_wildcard vs`

creates a pattern variable that accepts anything and in which variables `vs`

can appear free. There is no order on `vs`

because such created wildcard are not bound anywhere, so terms filtered by such wildcards are not kept.

```
val update_aux :
int ->
int ->
arg list ->
int Term.VarMap.t ->
clause ->
clause
```

`update_aux col mem clause`

the condition pool and the substitution of clause `clause`

assuming that column `col`

is inspected and `mem`

subterms have to be memorised.

```
val specialize :
Term.VarSet.t ->
Term.term ->
int ->
arg list ->
clause list ->
arg list * clause list
```

`specialize free_vars pat col pos cls`

filters and transforms LHS of clauses `cls`

whose column `col`

contain a pattern that can filter elements filtered by pattern `pat`

, with `pos`

being the position of arguments in clauses and `free_vars`

is the set of variables that can appear free in patterns.

`default col pos cls`

selects and transforms clauses `cls`

assuming that terms on column `col`

does not match any symbol being the head structure of another term in column `col`

; `pos`

is the positions of terms in clauses.

```
val binder :
( Term.term -> Term.term * Term.tbinder ) ->
Term.VarSet.t ->
int ->
Term.tvar ->
arg list ->
clause list ->
arg list * clause list
```

`binder get free_vars col v pos cls`

selects and transforms clauses `cls`

assuming that each term `t`

in column `col`

is a binder such that `get t`

returns `Some(a, b)`

. The term `b`

under the binder has its bound variable substituted by `v`

; `pos`

is the position of terms in clause `cls`

. The domain `a`

of the binder and `b[v/x]`

are put back into the stack (in that order), with `a`

with argument position 0 and `b[v/x]`

as argument 1.

```
val abstract :
Term.VarSet.t ->
int ->
Term.tvar ->
arg list ->
clause list ->
arg list * clause list
```

`abstract free_vars col v pos cls`

selects and transforms clauses `cls`

keeping lines whose column `col`

is able to filter an abstraction. The body of the abstraction has its bound variable substituted by `v`

; `pos`

is the position of terms in clauses `cls`

and `free_vars`

is the set of *free* variables introduced by other binders that may appear in patterns.

```
val product :
Term.VarSet.t ->
int ->
Term.tvar ->
arg list ->
clause list ->
arg list * clause list
```

`product free_vars col v pos cls`

is like ```
abstract free_vars col v pos
cls
```

for products.

`val cond_ok : Tree_type.tree_cond -> clause list -> clause list`

`cond_ok cond cls`

updates the clause list `cls`

assuming that condition `cond`

is satisfied.

`val cond_fail : Tree_type.tree_cond -> clause list -> clause list`

`cond_fail cond cls`

updates the clause list `cls`

with the information that the condition `cond`

is not satisfied.

`empty_stack c`

keeps the empty clauses from `c`

.