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, 43 insertions, 0 deletions

diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 4b2fab6d1..4b0bd703a 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -64,12 +64,55 @@ let pr_glob_constr_and_expr = function
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
 let pr_hyp (SsrHyp (_, id)) = Id.print id
+let pr_hyps = pr_list pr_spc pr_hyp
 
 let pr_occ = function
   | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}"
   | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}"
   | None -> str "{}"
 
+let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}"
+let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr
+
+let pr_dir = function L2R -> str "->" | R2L -> str "<-"
+
+let pr_simpl = function
+  | Simpl -1 -> str "/="
+  | Cut -1 -> str "//"
+  | Simpl n -> str "/" ++ int n ++ str "="
+  | Cut n -> str "/" ++ int n ++ str"/"
+  | SimplCut (-1,-1) -> str "//="
+  | SimplCut (n,-1) -> str "/" ++ int n ++ str "/="
+  | SimplCut (-1,n) -> str "//" ++ int n ++ str "="
+  | SimplCut (n,m) -> str "/" ++ int n ++ str "/" ++ int m ++ str "="
+  | Nop -> mt ()
+
+(* New terms *)
+
+let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body
+
+let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
+
+let rec pr_ipat p =
+  match p with
+  | IPatId id -> Id.print id
+  | IPatSimpl sim -> pr_simpl sim
+  | IPatClear clr -> pr_clear mt clr
+  | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]")
+  | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir
+  | IPatAnon All -> str "*"
+  | IPatAnon Drop -> str "_"
+  | IPatAnon One -> str "?"
+  | IPatView v -> pr_view2 v
+  | IPatNoop -> str "-"
+  | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
+  | IPatTac _ -> str "<tac>"
+(* TODO  | IPatAnon Temporary -> str "+" *)
+and pr_ipats ipats = pr_list spc pr_ipat ipats
+and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
+
 (* 0 cost pp function. Active only if Debug Ssreflect is Set *)
 let ppdebug_ref = ref (fun _ -> ())
 let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)