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, 49 insertions, 16 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index c29a1fe7c..daad730ff 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -51,6 +51,24 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
 
 let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
 
+let interp_nbargs ist gl rc =
+  try
+    let rc6 = mkRApp rc (mkRHoles 6) in
+    let sigma, t = interp_open_constr ist gl (rc6, None) in
+    let si = sig_it gl in
+    let gl = re_sig si sigma in
+    6 + Ssrcommon.nbargs_open_constr gl t
+  with _ -> 5
+
+let interp_view_nbimps ist gl rc =
+  try
+    let sigma, t = interp_open_constr ist gl (rc, None) in
+    let si = sig_it gl in
+    let gl = re_sig si sigma in
+    let pl, c = splay_open_constr gl t in
+    if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
+  with _ -> 0
+
 let interp_agens ist gl gagens =
   match List.fold_right (interp_agen ist gl) gagens ([], []) with
   | clr, rlemma :: args ->
@@ -86,40 +104,55 @@ let mkRAppView ist gl rv gv =
 
 let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;
 
-let refine_interp_apply_view i ist gl gv =
+let refine_interp_apply_view dbl ist gl gv =
   let pair i = List.map (fun x -> i, x) in
   let rv = pf_intern_term ist gl gv in
   let v = mkRAppView ist gl rv gv in
-  let interp_with (i, hint) =
+  let interp_with (dbl, hint) =
+    let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
   let interp_with x = prof_apply_interp_with.profile interp_with x in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
   | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
-  loop (pair i Ssrview.viewtab.(i) @
-        if i = 2 then pair 1 Ssrview.viewtab.(1) else [])
-
-let apply_top_tac gl =
-  Tacticals.tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); Proofview.V82.of_tactic (Tactics.clear [top_id])] gl
-
-let inner_ssrapplytac gviews ggenl gclr ist gl =
+  loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
+        if dbl = Ssrview.AdaptorDb.Equivalence
+        then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
+        else [])
+
+let apply_top_tac =
+  Tacticals.New.tclTHENLIST [
+    Proofview.V82.tactic (introid top_id);
+    Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
+    Tactics.clear [top_id]
+  ]
+
+let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl ->
  let _, clr = interp_hyps ist gl gclr in
  let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
  let ggenl, tclGENTAC =
    if gviews <> [] && ggenl <> [] then
-     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g) (List.hd ggenl) in
-     [], Tacticals.tclTHEN (genstac (ggenl,[]) ist)
+     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
+     [], Tacticals.tclTHEN (genstac (ggenl,[]))
    else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
  tclGENTAC (fun gl ->
   match gviews, ggenl with
   | v :: tl, [] ->
-    let dbl = if List.length tl = 1 then 2 else 1 in
+    let dbl =
+      if List.length tl = 1
+      then Ssrview.AdaptorDb.Equivalence
+      else Ssrview.AdaptorDb.Backward in
     Tacticals.tclTHEN
-      (List.fold_left (fun acc v -> Tacticals.tclTHENLAST acc (vtac v dbl)) (vtac v 1) tl)
-      (cleartac clr) gl
+      (List.fold_left (fun acc v ->
+         Tacticals.tclTHENLAST acc (vtac v dbl))
+        (vtac v Ssrview.AdaptorDb.Backward) tl)
+      (old_cleartac clr) gl
   | [], [agens] ->
     let clr', (sigma, lemma) = interp_agens ist gl agens in
     let gl = pf_merge_uc_of sigma gl in
-    Tacticals.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr'] gl
-  | _, _ -> Tacticals.tclTHEN apply_top_tac (cleartac clr) gl) gl
+    Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
+  | _, _ ->
+     let open Proofview.Notations in
+     Proofview.V82.of_tactic (apply_top_tac <*> cleartac clr) gl) gl
+)