package term-indexing

The type of primitives, i.e. the symbols. Each value of type prim has a definite arity.

The type of paths in terms.

The type of patterns.

The type of matchings. A matching is a disjunction of patterns.

The type of patterns on lists of terms.

The type of terms.

pattern_matches patt t checks whether the pattern patt matches the term t

all_matches t matching returns all paths at which there is a subterm satisfying matching

first_match t matching returns the first paths, if any, where there is a subterm satisfying matching.

If the matched pattern does not specify focused subterms, the result is at most a singleton list. If the matched pattern specifies focused subterms, the result is a list of paths, one for each focused subterm.

refine_focused patt paths returns the refinements of path that correspond to focused subterms of patt. If patt is does not specify focii, the result is the empty list.

prim p plist is a pattern matching a term with head bearing a primitive p and subterms matching the list pattern plist.

prim_pred pred plist is a pattern matching a term with primitive p such that pred p is true, and subterms matching the list pattern plist.

var i is a pattern matching a variable i.

any is a pattern matching any term.

focus patt returns a pattern equivalent to patt except that a focus mark is added on all terms matched by patt.

Raises Invalid_pattern if t is already a focus.

list_any is a list pattern matching any list of terms.

list_empty is a list pattern matching the empty list of terms.

list_cons hd tl is a list pattern matching a list with head matching the pattern hd and tail matching the list pattern tl.

An alias for list_cons

Pattern pretty-printing

uid p returns a unique integer attached to p. It is guaranteed that if two patterns have the same uid, they are equal.