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 consequentlycpattern
)
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
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 -> 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
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 -> 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 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 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 returnredex_of_pattern pat
ifpat
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 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 -> 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 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 -> 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 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 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
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 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