diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-07 10:59:00 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-04 18:01:24 +0100 |
commit | f35069aec1847068ecb501244507cb5aa9fa9b81 (patch) | |
tree | 7a47940f36cec47c35d9e73812361f12e22c2202 /plugins/ssr/ssrast.mli | |
parent | 9efd7ac0311f2b55756d7aa2790b0adb75c69579 (diff) |
ssr: rewrite Ssripats and Ssrview in the tactic monad
Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.
The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time). Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.
The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
with a state). Ssrcommon.MakeState provides an easy way for a tactic
to enrich the goal with with data of interest, such as the set of
hyps to be cleared. This cleans up the old implementation that, in
order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
tactic monad. Most of them are the rewriting of already existing
utilities. When possible the old version was removed.
Diffstat (limited to 'plugins/ssr/ssrast.mli')
-rw-r--r-- | plugins/ssr/ssrast.mli | 46 |
1 files changed, 34 insertions, 12 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index cdd4ee645..c53e74406 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -43,12 +43,24 @@ type ssrclear = ssrhyps (* Discharge occ switch (combined occurrence / clear switch) *) type ssrdocc = ssrclear option * ssrocc -(* FIXME, make algebraic *) -type ssrtermkind = char - +(* OLD ssr terms *) +type ssrtermkind = char (* FIXME, make algebraic *) type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr -type ssrview = ssrterm list +(* NEW ssr term *) + +(* These terms are raw but closed with the intenalization/interpretation + * context. It is up to the tactic receiving it to decide if such contexts + * are useful or not, and eventually manipulate the term before turning it + * into a constr *) +type ast_closure_term = { + body : Constrexpr.constr_expr; + glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *) + interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *) + annotation : [ `None | `Parens | `DoubleParens | `At ]; +} + +type ssrview = ast_closure_term list (* TODO type id_mod = Hat | HatTilde | Sharp @@ -59,7 +71,6 @@ type anon_iter = | One | Drop | All - (* TODO | Dependent (* fast mode *) | UntilMark @@ -71,15 +82,15 @@ type ssripat = | IPatId of (*TODO id_mod option * *) Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) -(* TODO | IPatDispatch of ssripatss (* /[..|..] *) *) + | IPatDispatch of ssripatss (* /[..|..] *) | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of ssrterm list (* /view *) + | IPatView of ssrview (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl - | IPatNewHidden of Id.t list -(* | IPatVarsForAbstract of Id.t list *) + | IPatAbstractVars of Id.t list + | IPatTac of unit Proofview.tactic and ssripats = ssripat list and ssripatss = ssripats list @@ -127,12 +138,12 @@ type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint)) -type clause = +type clause = (ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) type clauses = clause list * ssrclseq -type wgen = +type wgen = (ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) @@ -141,9 +152,20 @@ type wgen = type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) + +open Ssrmatching_plugin +open Ssrmatching +type ssrdgens = { dgens : (ssrdocc * cpattern) list; + gens : (ssrdocc * cpattern) list; + clr : ssrclear } +type ssrcasearg = ssripat option * (ssrdgens * ssripats) +type ssrmovearg = ssrview * ssrcasearg +type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear +type ssrapplyarg = ssrterm list * (ssragens * ssripats) + (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign type ist = Tacinterp.interp_sign -type goal = Goal.goal +type goal = Goal.goal type 'a sigma = 'a Evd.sigma type v82tac = Tacmach.tactic |