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

diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 6514b186e..63d79198e 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -45,7 +45,7 @@ let rot_hyps dir i hyps =
 
 let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
   let i = get_index ivar in
-  let evtac = ssrevaltac ist in
+  let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in
   let tac1 = evtac atac1 in
   if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1  else
   let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in
@@ -91,10 +91,11 @@ let hidetacs clseq idhide cl0 =
 
 let endclausestac id_map clseq gl_id cl0 gl =
   let not_hyp' id = not (List.mem_assoc id id_map) in
-  let orig_id id = try List.assoc id id_map with _ -> id in
+  let orig_id id = try List.assoc id id_map with Not_found -> id in
   let dc, c = EConstr.decompose_prod_assum (project gl) (pf_concl gl) in
   let hide_goal = hidden_clseq clseq in
-  let c_hidden = hide_goal && EConstr.eq_constr (project gl) c (EConstr.mkVar gl_id) in
+  let c_hidden =
+    hide_goal && EConstr.eq_constr (project gl) c (EConstr.mkVar gl_id) in
   let rec fits forced = function
   | (id, _) :: ids, decl :: dc' when RelDecl.get_name decl = Name id ->
     fits true (ids, dc')
@@ -114,26 +115,28 @@ let endclausestac id_map clseq gl_id cl0 gl =
   let ugtac gl' =
     Proofview.V82.of_tactic
       (convert_concl_no_check (unmark (pf_concl gl'))) gl' in
-  let ctacs = if hide_goal then [Proofview.V82.of_tactic (Tactics.clear [gl_id])] else [] in
+  let ctacs =
+    if hide_goal then [Proofview.V82.of_tactic (Tactics.clear [gl_id])]
+    else [] in
   let mktac itacs = Tacticals.tclTHENLIST (itacs @ utacs @ ugtac :: ctacs) in
   let itac (_, id) = Proofview.V82.of_tactic (Tactics.introduction id) in
   if fits false (id_map, List.rev dc) then mktac (List.map itac id_map) gl else
   let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
-  CErrors.user_err (Pp.str "tampering with discharged assumptions of \"in\" tactical")
+  errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
 
 let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
-let tclCLAUSES ist tac (gens, clseq) gl =
+let tclCLAUSES tac (gens, clseq) gl =
   if clseq = InGoal || clseq = InSeqGoal then tac gl else
   let clr_gens = pf_clauseids gl gens clseq in
   let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
-  let gl_id = mk_anon_id hidden_goal_tag gl in
+  let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in
   let cl0 = pf_concl gl in
   let dtac gl =
     let c = pf_concl gl in
     let gl, args, c =
-      List.fold_right (abs_wgen true ist mk_discharged_id) gens (gl,[], c) in
+      List.fold_right (abs_wgen true mk_discharged_id) gens (gl,[], c) in
     apply_type c args gl in
   let endtac =
     let id_map = CList.map_filter (function
@@ -147,7 +150,7 @@ let tclCLAUSES ist tac (gens, clseq) gl =
 let hinttac ist is_by (is_or, atacs) =
   let dtac = if is_by then donetac ~-1 else Tacticals.tclIDTAC in
   let mktac = function
-  | Some atac -> Tacticals.tclTHEN (ssrevaltac ist atac) dtac
+  | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac
   | _ -> dtac in
   match List.map mktac atacs with
   | [] -> if is_or then dtac else Tacticals.tclIDTAC
@@ -156,4 +159,7 @@ let hinttac ist is_by (is_or, atacs) =
 
 let ssrdotac ist (((n, m), tac), clauses) =
   let mul = get_index n, m in
-  tclCLAUSES ist (tclMULT mul (hinttac ist false tac)) clauses
+  tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses
+
+let tclCLAUSES tac g_c =
+  Proofview.V82.(tactic (tclCLAUSES (of_tactic tac) g_c))