Module Constr_matching

This module implements pattern-matching on terms

type instantiated_pattern
val instantiate_pattern : Environ.env -> Evd.evar_map -> Ltac_pretype.extended_patvar_map -> Pattern.constr_pattern -> 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

val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map

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

val matches_head : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map

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

val extended_matches : Environ.env -> Evd.evar_map -> (binding_bound_vars * instantiated_pattern) -> EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map

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

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

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)

val match_subterm : Environ.env -> Evd.evar_map -> (binding_bound_vars * instantiated_pattern) -> EConstr.constr -> matching_result IStream.t

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