lambdapi 2.4.1 · OCaml Package

Clause matrices encode pattern matching problems. The clause matrix C can be denoted C = P ↪ A where P is a pattern matrix and A is a column of RHS. Each line of a matrix is a pattern to which a RHS is attached. When reducing a term, if a line filters the term (i.e., the term matches the pattern) then term is rewritten to the RHS.

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 vars array to store variables.
*)
positions : arg list;
(*
Positions of the elements of the matrix in the initial term. We must have length positions = max {length cl | cl ∈ clauses}.
*)

}

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 CondNL(c, s) indicates a non-linearity constraint on column c with respect to slot s. A condition CondFV(vs, i) corresponds to a free variable condition: only variables of vs are in the matched term.
*)

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 of_rules : Term.rule list -> t

of_rules rs transforms rewriting rules rs into a clause matrix.

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 get_col : int -> t -> Term.term list

get_col n m retrieves column n of matrix m.

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.

val is_exhausted : arg list -> clause -> bool

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 Core.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 Core.Term.VarMap.t -> Term.term -> int

val mk_wildcard : Core.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 Core.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 : 
  Core.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.

val default : int -> arg list -> clause list -> arg list * clause list

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) ->
  Core.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 : 
  Core.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 : 
  Core.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.

val empty_stack : clause list -> arg list * clause list

empty_stack c keeps the empty clauses from c.

val not_empty_stack : clause list -> clause list

not_empty_stack c keeps the not empty clauses from c.

package lambdapi