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, 31 insertions, 17 deletions

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 96ded5abf..2dfcb8572 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -501,21 +501,19 @@ END
 (* View purpose *)
 
 let pr_viewpos = function
-  | 0 -> str " for move/"
-  | 1 -> str " for apply/"
-  | 2 -> str " for apply//"
-  | _ -> mt ()
+  | Some Ssrview.AdaptorDb.Forward -> str " for move/"
+  | Some Ssrview.AdaptorDb.Backward -> str " for apply/"
+  | Some Ssrview.AdaptorDb.Equivalence -> str " for apply//"
+  | None -> mt ()
 
 let pr_ssrviewpos _ _ _ = pr_viewpos
 
-let mapviewpos f n k = if n < 3 then f n else for i = 0 to k - 1 do f i done
-
-ARGUMENT EXTEND ssrviewpos TYPED AS int PRINTED BY pr_ssrviewpos
-  | [ "for" "move" "/" ] -> [ 0 ]
-  | [ "for" "apply" "/" ] -> [ 1 ]
-  | [ "for" "apply" "/" "/" ] -> [ 2 ]
-  | [ "for" "apply" "//" ] -> [ 2 ]
-  | [ ] -> [ 3 ]
+ARGUMENT EXTEND ssrviewpos PRINTED BY pr_ssrviewpos
+  | [ "for" "move" "/" ] -> [ Some Ssrview.AdaptorDb.Forward ]
+  | [ "for" "apply" "/" ] -> [ Some Ssrview.AdaptorDb.Backward ]
+  | [ "for" "apply" "/" "/" ] -> [ Some Ssrview.AdaptorDb.Equivalence ]
+  | [ "for" "apply" "//" ] -> [ Some Ssrview.AdaptorDb.Equivalence ]
+  | [ ] -> [ None ]
 END
 
 let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc ()
@@ -524,19 +522,35 @@ ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY pr_ssrviewposspc
   | [ ssrviewpos(i) ] -> [ i ]
 END
 
-let print_view_hints i =
-  let pp_viewname = str "Hint View" ++ pr_viewpos i ++ str " " in
-  let pp_hints = pr_list spc pr_rawhintref Ssrview.viewtab.(i) in
+let print_view_hints kind l =
+  let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
+  let pp_hints = pr_list spc pr_rawhintref l in
   Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
-| [ "Print" "Hint" "View" ssrviewpos(i) ] -> [ mapviewpos print_view_hints i 3 ]
+| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
+  [ match i with
+    | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k)
+    | None ->
+        List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k))
+          [ Ssrview.AdaptorDb.Forward;
+            Ssrview.AdaptorDb.Backward;
+            Ssrview.AdaptorDb.Equivalence ]
+  ]
 END
 
+let glob_view_hints lvh =
+  List.map (Constrintern.intern_constr (Global.env ()) (Evd.from_env (Global.env ()))) lvh
 
 VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
   |  [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] ->
-     [ mapviewpos (Ssrview.add_view_hints (Ssrview.glob_view_hints lvh)) n 2 ]
+     [ let hints = glob_view_hints lvh in
+       match n with
+       | None ->
+          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Forward hints;
+          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Backward hints
+       | Some k ->
+          Ssrview.AdaptorDb.declare k hints ]
 END
 
 (* }}} *)