package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 = {
  1. m_sub : bound_ident_map * Ltac_pretype.patvar_map;
  2. 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct