module P : Intf.Signaturemodule Z : Intf.Zipper with type term = T.tinclude Intf.Pattern
with type prim = P.t
and type term = P.t Term.term
and type 'a with_state = 'a Z.with_state
and type zipper = Z.ttype prim = P.tThe type of primitives, i.e. the symbols. Each value of type prim has a definite arity.
type 'a with_state = 'a Z.with_statetype zipper = Z.tThe type of zippers over terms.
type matching = t listThe type of matchings. A matching is a disjunction of patterns.
pattern_matches patt t checks whether the pattern patt matches the term t
val all_matches : matching -> term with_state -> zipper listall_matches t matching returns all zippers at which there is a subterm satisfying matching
val first_match : matching -> term with_state -> zipper listfirst_match t matching returns the first zippers, 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 zippers, one for each focused subterm.
refine_focused patt zippers returns the refinements of zippers 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.
val any_var : tany_var is a pattern matching any variable.
val var : int -> tvar i is a pattern matching a variable i.
val any : tany 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.
val list_any : plistlist_any is a list pattern matching any list of terms.
val list_empty : plistlist_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.
val pp : Format.formatter -> t -> unitPattern pretty-printing
val uid : t -> intuid 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 Z.with_state -> zipper list