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, 23 insertions, 22 deletions

diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index 6fd906ff4..986b5fbf5 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -6,31 +6,32 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-
 open Ssrast
-open Ssrcommon
 
-val viewtab : Glob_term.glob_constr list array
-val add_view_hints : Glob_term.glob_constr list -> int -> unit
-val glob_view_hints : Constrexpr.constr_expr list -> Glob_term.glob_constr list
+(* Adaptor DB (Hint View) *)
+module AdaptorDb : sig
+
+  type kind = Forward | Backward | Equivalence
 
-val pfa_with_view :
-           ist ->
-           ?next:ssripats ref ->
-           bool * ssrterm list ->
-           EConstr.t ->
-           EConstr.t ->
-           (EConstr.t -> EConstr.t -> tac_ctx tac_a) ->
-           ssrhyps ->
-   (goal * tac_ctx) sigma -> EConstr.types * EConstr.t * (goal * tac_ctx) list sigma
+  val get : kind -> Glob_term.glob_constr list
+  val declare : kind -> Glob_term.glob_constr list -> unit
 
-val pf_with_view_linear :
-           ist ->
-           goal sigma ->
-           bool * ssrterm list ->
-           EConstr.t ->
-           EConstr.t ->
-           EConstr.types * EConstr.t * goal sigma
+end
 
+(* Apply views to the top of the stack (intro pattern) *)
+val tclIPAT_VIEWS :
+    views:ast_closure_term list ->
+    conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
+  unit Proofview.tactic
 
+(* Apply views to a given subject (as if was the top of the stack), then
+   call conclusion on the obtained term (something like [v2 (v1 subject)]).
+   The term being passed to conclusion is abstracted over non-resolved evars:
+   if [simple_types] then all unnecessary dependencies among the abstracted
+   evars are pruned *)
+val tclWITH_FWD_VIEWS :
+  simple_types:bool ->
+    subject:EConstr.t ->
+    views:ast_closure_term list ->
+    conclusion:(EConstr.t -> unit Proofview.tactic) ->
+  unit Proofview.tactic