# 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.

`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.existential, EConstr.t) ssrpattern;`

`}`

`val pp_pattern : Environ.env -> pattern -> Pp.t`

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

`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.

`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`