Module Ssrmatching_plugin.Ssrmatching
type cpattern
The type of context patterns, the patterns of the
set
tactic and:
tactical. These are patterns that identify a precise subterm.
type rpattern
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)
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 consequentlycpattern
)
type pattern
= Evd.evar_map * (Constr.constr, Constr.constr) ssrpattern
val pp_pattern : Environ.env -> pattern -> Pp.t
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
orIn_X_In_T
val interp_rpattern : Environ.env -> Evd.evar_map -> rpattern -> pattern
interp_rpattern ise gl rpat
"internalizes" and "interprets"rpat
in the currentLtac
interpretation signatureise
and tactic inputgl
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 currentLtac
interpretation signatureise
and tactic inputgl
.ty
is an optional type for the redex ofcpat
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 -> 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
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
mapst
callingsubst
on everyocc
occurrence ofpat
. Theint
argument is the number of binders traversed. Ifpat
isNone
then then subst is called ont
.t
must live inenv
andsigma
,pat
must have been interpreted in (an extension of)sigma
.- raises NoMatch
if
pat
has no occurrence andb
istrue
(defaultfalse
)
- returns
t
where allocc
occurrences ofpat
have been mapped usingsubst
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 ofeval_pattern
. It replaces allocc
occurrences ofpat
int
with Relh
.t
must live inenv
andsigma
,pat
must have been interpreted in (an extension of)sigma
.- raises NoMatch
if
pat
has no occurrence andb
istrue
(defaultfalse
)
- returns
the instance of the redex of
pat
that was matched andt
transformed as described above.
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 termt
living inenv
sigma
(an extension ofsigma0
) intro atpattern
. Thetpattern
can hold a (proof) termp
and a dictiondir
. Theok
callback is used to filter occurrences.- returns
the compiled
tpattern
and itsevar_map
- raises UserEerror
is the pattern is a wildcard
type 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 callbackk
to map the subterm matched. Theint
argument passed tok
is the number of binders traversed so far plus the initial valuei
.- returns
t
where the subterms identified by the selected occurrences of the patter have been mapped usingk
- raises NoMatch
if the raise_NoMatch flag given to
mk_tpattern_matcher
istrue
and if the pattern did not match
- raises UserEerror
if the raise_NoMatch flag given to
mk_tpattern_matcher
isfalse
and if the pattern did not match
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
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 functionfind_P
andconclude
with the behaviour explained above. The flagb
(defaultfalse
) changes the error reporting behaviour offind_P
if none of thetpattern
matches. The argumento
can be passed to tune theUserError
eventually raised (useful if the pattern is coming from the LHS/RHS of an equation)
val pf_fill_occ_term : Goal.goal Evd.sigma -> occ -> (Evd.evar_map * EConstr.t) -> EConstr.t * EConstr.t
val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> (Evd.evar_map * EConstr.t) -> EConstr.t * EConstr.t
val cpattern_of_term : (char * Genintern.glob_constr_and_expr) -> Geninterp.interp_sign -> cpattern
val do_once : 'a option Stdlib.ref -> (unit -> 'a) -> unit
do_once r f
callsf
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 pf_unify_HO : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> Goal.goal Evd.sigma
val tag_of_cpattern : cpattern -> char
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 : 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 pf_merge_uc : UState.t -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
val pf_unsafe_merge_uc : UState.t -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
val debug : bool -> unit
val ssrinstancesof : cpattern -> unit Proofview.tactic
module Internal : sig ... end