Module Constr_matching

This module implements pattern-matching on terms

type instantiated_pattern
type binding_bound_vars = Names.Id.Set.t
exception PatternMatchingFailure

PatternMatchingFailure is the exception raised when pattern matching fails

val special_meta : Constr.metavariable

special_meta is the default name of the meta holding the surrounding context in subterm matching

type bound_ident_map = Names.Id.t Names.Id.Map.t

bound_ident_map represents the result of matching binding identifiers of the pattern with the binding identifiers of the term matched

matches pat c matches c against pat and returns the resulting assignment of metavariables; it raises PatternMatchingFailure if not matchable; bindings are given in increasing order based on the numbers given in the pattern

matches_head pat c does the same as matches pat c but accepts pat to match an applicative prefix of c

extended_matches pat c also returns the names of bound variables in c that matches the bound variables in pat; if several bound variables or metavariables have the same name, the metavariable, or else the rightmost bound variable, takes precedence

is_matching pat c just tells if c matches against pat

val is_matching_head : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool

is_matching_head pat c just tells if c or an applicative prefix of it matches against pat

type context
val empty_context : context
val repr_context : context -> EConstr.t
val instantiate_context : context -> EConstr.t -> EConstr.t
type matching_result = {
m_sub : bound_ident_map * Ltac_pretype.patvar_map;
m_ctx : context;
}

The type of subterm matching results: a substitution + a context (whose hole is denoted here with special_meta)

match_subterm pat c returns the substitution and the context corresponding to each **closed** subterm of c matching pat, considering application contexts as well.

val is_matching_appsubterm : ?closed:bool -> Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool

is_matching_appsubterm pat c tells if a subterm of c matches against pat taking partial subterms into consideration