package term-indexing

  1. Overview
  2. Docs

Parameters

module P : Intf.Signature
module T : Intf.Term with type prim = P.t and type t = P.t Term.term

Signature

include Intf.Pattern with type prim = P.t and type path = Path.t and type term = P.t Term.term
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 = P.t Term.term

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.

val all_matches_with_hash_consing : t -> term -> path list
OCaml

Innovation. Community. Security.