Pattern#

Ltac2.Pattern

A context is a constr with a hole that can be instantiated through the instantiate function.

val empty_context : context

A trivial context only made of the hole.

type substitution = constr Names.Id.Map.t

A substitution is a mapping from pattern variables to terms.

val matches : Environ.env -> Evd.evar_map -> pattern -> constr -> substitution option

matches env sigma pattern t tries matching t against pattern, and returns the assignment of pattern variables, or None if pattern-matching failed.

val matches_subterm : pattern -> constr -> (context * substitution) Proofview.tactic

matches_subterm pattern t returns a stream of results corresponding to all of the subterms of t that match pattern as in matches, in the current goal. The stream is encoded as a backtracking value whose last exception is Constr_matching.PatternMatchingFailure. The additional value compared to matches is the context of the match, to be filled with the instantiate function.

type match_pattern = private ..

Patterns used in goal-matching.

type match_pattern +=
  1. | Pattern of pattern
    (*

    Matches the whole term.

    *)
  2. | Context of pattern
    (*

    Matches a subterm.

    *)
type hyp_match_pattern

Patterns used to match over a hypothesis.

val match_hyp : ?body:match_pattern -> match_pattern -> hyp_match_pattern

match_hyp ?body t matches the type of a hypothesis with t, and the body of the hypothesis with body, if specified.

type hyp_match_result = private {
  1. name : ident;
    (*

    Name of the hypothesis matched.

    *)
  2. body_context : context option;
    (*

    Context where the body matched, if any.

    *)
  3. type_context : context option;
    (*

    Context in which the type of the hypothesis matched.

    *)
}

Result of matching over a hypothesis.

type goal_match_result = private {
  1. hyps : hyp_match_result list;
    (*

    List of hypothesis match results.

    *)
  2. context : context option;
    (*

    Context where the conclusion matched, if any.

    *)
  3. substitution : substitution;
    (*

    Substitution of pattern matching.

    *)
}

Result of matching over goals.

val matches_goal : ?reverse:bool -> hyp_match_pattern list -> match_pattern -> goal_match_result Proofview.tactic

Given a list of patterns hpats for hypotheses and one pattern cpat for the conclusion, matches_goal ?reverse hpats cpat produces (a stream of):

  • A list, with one element per pattern in hpats, containing the name of the matched hypothesis, the context of the body pattern (or None if the body pattern was match_pattern.Pattern), and the context of the hypothesis pattern.
  • A context corresponding to the conclusion.
  • A substitution from pattern variables to terms.

This produces a backtracking stream of results containing all the possible result combinations. The order of considered hypotheses is reversed if reverse is true.

val instantiate : context -> constr -> constr

instantiate context t fills the hole of context with t.