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