Module Ssrmatching_plugin.Ssrmatching

type ssrtermkind =
| InParens
| WithAt
| NoFlag
| Cpattern
type 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.

val pr_cpattern : cpattern -> Pp.t
exception NoMatch
exception NoProgress
type ('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)

type pattern = {
pat_sigma : Evd.evar_map;
pat_pat : (EConstr.existentialEConstr.t) ssrpattern;
}
val pp_pattern : Environ.env -> pattern -> Pp.t
type rpattern = (cpatterncpattern) 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)

val pr_rpattern : rpattern -> Pp.t
val redex_of_pattern : pattern -> (Evd.evar_map * EConstr.t) option

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

val 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

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

type 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})

type subst = Environ.env -> EConstr.t -> EConstr.t -> int -> EConstr.t

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

val eval_pattern : ?⁠raise_NoMatch:bool -> Environ.env -> Evd.evar_map -> EConstr.t -> pattern option -> occ -> subst -> EConstr.t

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

val fill_occ_pattern : ?⁠raise_NoMatch:bool -> Environ.env -> Evd.evar_map -> EConstr.t -> pattern -> occ -> int -> EConstr.t Evd.in_evar_universe_context * EConstr.t

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.

val fill_rel_occ_pattern : Environ.env -> Evd.evar_map -> EConstr.t -> pattern -> occ -> Evd.evar_map * EConstr.t * EConstr.t

Variant of the above function where we fix h := 1 and return redex_of_pattern pat if pat has no occurrence.

type ssrdir =
| L2R
| R2L
val pr_dir_side : ssrdir -> Pp.t
type tpatterns

patterns for a term with wildcards

val empty_tpatterns : Evd.evar_map -> tpatterns
val mk_tpattern : ?⁠p_origin:(ssrdir * EConstr.t) -> ?⁠ok:(EConstr.t -> Evd.evar_map -> bool) -> rigid:(Evar.t -> bool) -> Environ.env -> EConstr.t -> ssrdir -> EConstr.t -> tpatterns -> tpatterns

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

type find_P = Environ.env -> EConstr.t -> int -> k:subst -> EConstr.t

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

type conclude = unit -> EConstr.t * ssrdir * (bool * Evd.evar_map * UState.t * EConstr.t)

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

val mk_tpattern_matcher : ?⁠all_instances:bool -> ?⁠raise_NoMatch:bool -> ?⁠upats_origin:(ssrdir * EConstr.t) -> Evd.evar_map -> occ -> tpatterns -> 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)

val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> (Evd.evar_map * EConstr.t) -> EConstr.t * EConstr.t
val do_once : 'a option Stdlib.ref -> (unit -> 'a) -> unit

do_once r f calls f and updates the ref only once

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

assert_done r return the content of r.

raises Anomaly

is r is None

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

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

val loc_of_cpattern : cpattern -> Loc.t option
val id_of_pattern : Evd.evar_map -> pattern -> Names.Id.t option
val is_wildcard : cpattern -> bool
val cpattern_of_id : Names.Id.t -> cpattern
val pr_constr_pat : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_econstr_pat : Environ.env -> Evd.evar_map -> Evd.econstr -> Pp.t
val debug : bool -> unit
val ssrinstancesof : cpattern -> unit Proofview.tactic
module Internal : sig ... end