package term-indexing

  1. Overview
  2. Docs

Patterns over first-order terms and pattern matching.

type prim = P.t

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

type path = Path.t

The type of paths in terms.

type t

The type of patterns.

type matching = t list

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

type plist

The type of patterns on lists of terms.

type term = Term.t

The type of terms.

val pattern_matches : t -> term -> bool

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

val all_matches : matching -> term -> path list

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

val first_match : matching -> term -> path list

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.

val refine_focused : t -> path -> path list

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.

val prim : prim -> plist -> t

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

val prim_pred : (prim -> bool) -> plist -> t

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.

val var : int -> t

var i is a pattern matching a variable i.

val any : t

any is a pattern matching any term.

val focus : t -> t

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.

val list_any : plist

list_any is a list pattern matching any list of terms.

val list_empty : plist

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

val list_cons : t -> plist -> plist

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

val (@.) : t -> plist -> plist

An alias for list_cons

val pp : Format.formatter -> t -> unit

Pattern pretty-printing

val uid : t -> int

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

OCaml

Innovation. Community. Security.