Module `Ssrmatching_plugin.Ssrmatching`Source

******** Small Scale Reflection pattern matching facilities *************

Pattern parsing

Sourcetype ssrtermkind =

| InParens
| WithAt
| NoFlag
| Cpattern

Sourcetype cpattern = {

kind : ssrtermkind;
pattern : Genintern.glob_constr_and_expr;
interpretation : Geninterp.interp_sign option;

}

The type of context patterns, the patterns of the set tactic and : tactical. These are patterns that identify a precise subterm.

Sourceval pr_cpattern : cpattern -> Pp.t

Pattern interpretation and matching

Sourceexception NoMatch

Sourceexception NoProgress

Sourcetype ('ident, 'term) ssrpattern =

| T of 'term
| In_T of 'term
| X_In_T of 'ident * 'term
| In_X_In_T of 'ident * 'term
| E_In_X_In_T of 'term * 'ident * 'term
| E_As_X_In_T of 'term * 'ident * 'term

AST for rpattern (and consequently cpattern)

Sourcetype pattern = Evd.evar_map * (Constr.constr, Constr.constr) ssrpattern

Sourceval pp_pattern : Environ.env -> pattern -> Pp.t

Sourcetype rpattern = (cpattern, cpattern) ssrpattern

The type of rewrite patterns, the patterns of the rewrite tactic. These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix)

Sourceval pr_rpattern : rpattern -> Pp.t

Source

val redex_of_pattern : 
  ?resolve_typeclasses:bool ->
  Environ.env ->
  pattern ->
  Constr.constr Evd.in_evar_universe_context

Extracts the redex and applies to it the substitution part of the pattern.

raises Anomaly
if called on In_T or In_X_In_T

Sourceval interp_rpattern : Environ.env -> Evd.evar_map -> rpattern -> pattern

interp_rpattern ise gl rpat "internalizes" and "interprets" rpat in the current Ltac interpretation signature ise and tactic input gl

Source

val interp_cpattern : 
  Environ.env ->
  Evd.evar_map ->
  cpattern ->
  (Genintern.glob_constr_and_expr * Geninterp.interp_sign) option ->
  pattern

interp_cpattern ise gl cpat ty "internalizes" and "interprets" cpat in the current Ltac interpretation signature ise and tactic input gl. ty is an optional type for the redex of cpat

Sourcetype occ = (bool * int list) option

The set of occurrences to be matched. The boolean is set to true * to signal the complement of this set (i.e. {-1 3})

Source

type subst =
  Environ.env ->
  Constr.constr ->
  Constr.constr ->
  int ->
  Constr.constr

subst e p t i. i is the number of binders traversed so far, p the term from the pattern, t the matched one

Source

val eval_pattern : 
  ?raise_NoMatch:bool ->
  Environ.env ->
  Evd.evar_map ->
  Constr.constr ->
  pattern option ->
  occ ->
  subst ->
  Constr.constr

eval_pattern b env sigma t pat occ subst maps t calling subst on every occ occurrence of pat. The int argument is the number of binders traversed. If pat is None then then subst is called on t. t must live in env and sigma, pat must have been interpreted in (an extension of) sigma.

raises NoMatch
if pat has no occurrence and b is true (default false)

returns
t where all occ occurrences of pat have been mapped using subst

Source

val fill_occ_pattern : 
  ?raise_NoMatch:bool ->
  Environ.env ->
  Evd.evar_map ->
  Constr.constr ->
  pattern ->
  occ ->
  int ->
  Constr.constr Evd.in_evar_universe_context * Constr.constr

fill_occ_pattern b env sigma t pat occ h is a simplified version of eval_pattern. It replaces all occ occurrences of pat in t with Rel h. t must live in env and sigma, pat must have been interpreted in (an extension of) sigma.

raises NoMatch
if pat has no occurrence and b is true (default false)

returns
the instance of the redex of pat that was matched and t transformed as described above.

*************************** Low level APIs ******************************

Sourcetype ssrdir =

| L2R
| R2L

Sourceval pr_dir_side : ssrdir -> Pp.t

Sourcetype tpattern

a pattern for a term with wildcards

Source

val mk_tpattern : 
  ?p_origin:(ssrdir * Constr.constr) ->
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map * Constr.constr) ->
  (Constr.constr -> Evd.evar_map -> bool) ->
  ssrdir ->
  Constr.constr ->
  Evd.evar_map * tpattern

mk_tpattern env sigma0 sigma_p ok p_origin dir t compiles a term t living in env sigma (an extension of sigma0) intro a tpattern. The tpattern can hold a (proof) term p and a diction dir. The ok callback is used to filter occurrences.

returns
the compiled tpattern and its evar_map

raises UserEerror
is the pattern is a wildcard

Sourcetype find_P = Environ.env -> Constr.constr -> int -> k:subst -> Constr.constr

findP env t i k is a stateful function that finds the next occurrence of a tpattern and calls the callback k to map the subterm matched. The int argument passed to k is the number of binders traversed so far plus the initial value i.

returns
t where the subterms identified by the selected occurrences of the patter have been mapped using k

raises NoMatch
if the raise_NoMatch flag given to mk_tpattern_matcher is true and if the pattern did not match

raises UserEerror
if the raise_NoMatch flag given to mk_tpattern_matcher is false and if the pattern did not match

Source

type conclude =
  unit ->
  Constr.constr * ssrdir * (Evd.evar_map * UState.t * Constr.constr)

conclude () asserts that all mentioned occurrences have been visited.

returns
the instance of the pattern, the evarmap after the pattern instantiation, the proof term and the ssrdit stored in the tpattern

raises UserEerror
if too many occurrences were specified

Source

val mk_tpattern_matcher : 
  ?all_instances:bool ->
  ?raise_NoMatch:bool ->
  ?upats_origin:(ssrdir * Constr.constr) ->
  Evd.evar_map ->
  occ ->
  (Evd.evar_map * tpattern list) ->
  find_P * conclude

mk_tpattern_matcher b o sigma0 occ sigma_tplist creates a pair a function find_P and conclude with the behaviour explained above. The flag b (default false) changes the error reporting behaviour of find_P if none of the tpattern matches. The argument o can be passed to tune the UserError eventually raised (useful if the pattern is coming from the LHS/RHS of an equation)

Example of mk_tpattern_matcher to implement rewrite \{occ\}[in t]rules. It first matches "in t" (called pat), then in all matched subterms it matches the LHS of the rules using find_R. concl0 is the initial goal, concl will be the goal where some terms are replaced by a De Bruijn index. The rw_progress extra check selects only occurrences that are not rewritten to themselves (e.g. an occurrence "x + x" rewritten with the commutativity law of addition is skipped)

let find_R, conclude = match pat with
| Some (_, In_T _) ->
    let aux (sigma, pats) (d, r, lhs, rhs) =
      let sigma, pat =
        mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in
      sigma, pats @ [pat] in
    let rpats = List.fold_left aux (r_sigma, []) rules in
    let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in
    find_R ~k:(fun _ _ h -> mkRel h),
    fun cl -> let rdx, d, r = end_R () in (d,r),rdx
| _ -> ... in
let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in
let (d, r), rdx = conclude concl in

Source

val pf_fill_occ_term : 
  Goal.goal Evd.sigma ->
  occ ->
  (Evd.evar_map * EConstr.t) ->
  EConstr.t * EConstr.t

Source

val fill_occ_term : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  occ ->
  (Evd.evar_map * EConstr.t) ->
  EConstr.t * EConstr.t

Helpers to make stateful closures. Example: a find_P function may be called many times, but the pattern instantiation phase is performed only the first time. The corresponding conclude has to return the instantiated pattern redex. Since it is up to find_P to raise NoMatch if the pattern has no instance, conclude considers it an anomaly if the pattern did not match

Sourceval do_once : 'a option Stdlib.ref -> (unit -> 'a) -> unit

do_once r f calls f and updates the ref only once

Sourceval assert_done : 'a option Stdlib.ref -> 'a

assert_done r return the content of r.

raises Anomaly
is r is None

Very low level APIs. these are calls to evarconv's the_conv_x followed by solve_unif_constraints_with_heuristics. In case of failure they raise NoMatch

Source

val unify_HO : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map

Source

val pf_unify_HO : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr ->
  Goal.goal Evd.sigma

Sourceval tag_of_cpattern : cpattern -> ssrtermkind

Some more low level functions needed to implement the full SSR language on top of the former APIs

Sourceval loc_of_cpattern : cpattern -> Loc.t option

Sourceval id_of_pattern : pattern -> Names.Id.t option

Sourceval is_wildcard : cpattern -> bool

Sourceval cpattern_of_id : Names.Id.t -> cpattern

Sourceval pr_constr_pat : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t

Sourceval pr_econstr_pat : Environ.env -> Evd.evar_map -> Evd.econstr -> Pp.t

Sourceval pf_merge_uc : UState.t -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma

Sourceval pf_unsafe_merge_uc : UState.t -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma

Sourceval debug : bool -> unit

Sourceval ssrinstancesof : cpattern -> unit Proofview.tactic

Functions used for grammar extensions. Do not use.

Sourcemodule Internal : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssrmatching_plugin/Ssrmatching_plugin/Ssrmatching/index.html

Module `Ssrmatching_plugin.Ssrmatching`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssrmatching_plugin/Ssrmatching_plugin/Ssrmatching/index.html

Module Ssrmatching_plugin.SsrmatchingSource

Module `Ssrmatching_plugin.Ssrmatching`Source