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.

1 files changed, 37 insertions, 71 deletions

diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index 6c36e67e8..d80d14c85 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -6,77 +6,43 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* This file implements:
+   - the [=>] tactical
+   - the [:] pseudo-tactical for move, case, elim and abstract
 
-open Ssrmatching_plugin
-open Ssrast
-open Ssrcommon
-
-type block_names = (int * EConstr.types array) option
-
-(* For case/elim with eq generation: args are elim_tac introeq_tac ipats
- * elim E : "=> ipats" where E give rise to introeq_tac *)
-val tclEQINTROS :
-           ?ind:block_names ref ->
-           ?ist:ist ->
-           v82tac ->
-           v82tac -> ssripats -> v82tac
-(* special case with no eq and tactic taking ist *)
-val tclINTROS :
-           ist ->
-           (ist -> v82tac) ->
-           ssripats -> v82tac
-
-(* move=> ipats *)
-val introstac : ?ist:ist -> ssripats -> v82tac
-
-val elim_intro_tac :
-  Ssrast.ssripats ->
-  ?ist:Tacinterp.interp_sign ->
-  [> `EConstr of 'a * 'b * EConstr.t ] ->
-  Ssrast.ssripat option ->
-  Tacmach.tactic ->
-  bool ->
-  Ssrast.ssrhyp list ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-(* "move=> top; tac top; clear top" respecting the speed *)
-val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a
+   Putting these two features in the same file lets one hide much of the
+   interaction between [tac E:] and [=>] ([E] has to be processed by [=>],
+   not by [:]
+*)
 
-val ssrmovetac :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    (Ssrast.ssripat option *
-       (((Ssrast.ssrdocc * Ssrmatching.cpattern) list
-        list * Ssrast.ssrclear) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
-
-val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-val with_dgens :
-  (Ssrast.ssrdocc * Ssrmatching.cpattern) list
-   list * Ssrast.ssrclear ->
-  ((Ssrast.ssrdocc * Ssrmatching.cpattern) list ->
-   Ssrast.ssrdocc * Ssrmatching.cpattern ->
-   Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) ->
-  Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic
-
-val ssrcasetac :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    (Ssrast.ssripat option *
-       (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
-
-val ssrapplytac :
-  Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    ('a *
-       ((((Ssrast.ssrhyps option * Ssrmatching_plugin.Ssrmatching.occ) *
-            (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr))
-           list list * Ssrast.ssrhyps) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
+open Ssrast
 
+(* The => tactical *)
+val tclIPAT : ssripats -> unit Proofview.tactic
+
+(* As above but with the SSR exception: first case is dispatch *)
+val tclIPATssr : ssripats -> unit Proofview.tactic
+
+(* Wrappers to deal with : and eqn generation/naming:
+     [tac E: gens => ipats]
+   where [E] is injected into [ipats] (at the right place) and [gens] are
+   generalized before calling [tac] *)
+val ssrmovetac : ssrmovearg -> unit Proofview.tactic
+val ssrsmovetac : unit Proofview.tactic
+val ssrelimtac : ssrmovearg -> unit Proofview.tactic
+val ssrselimtoptac : unit Proofview.tactic
+val ssrcasetac : ssrmovearg -> unit Proofview.tactic
+val ssrscasetoptac : unit Proofview.tactic
+
+(* The implementation of abstract: is half here, for the [[: var ]]
+ * ipat, and in ssrfwd for the integration with [have] *)
+val ssrabstract : ssrdgens -> unit Proofview.tactic
+
+(* Handling of [[:var]], needed in ssrfwd. Since ssrfwd is still outside the
+ * tactic monad we export code with the V82 interface *)
+module Internal : sig
+val examine_abstract :
+  EConstr.t -> Goal.goal Evd.sigma -> EConstr.types * EConstr.t array
+val pf_find_abstract_proof :
+  bool -> Goal.goal Evd.sigma -> Constr.constr -> Evar.t
+end