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