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, 312 insertions, 108 deletions

diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index f2990070b..cb67f538e 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -6,121 +6,325 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-
 open Util
 open Names
-open Term
+
 open Ltac_plugin
-open Tacinterp
-open Glob_term
-open Tacmach
-open Tacticals
+
+open Proofview
+open Notations
 
 open Ssrcommon
+open Ssrast
+
+module AdaptorDb = struct
+
+  type kind = Forward | Backward | Equivalence
+
+  module AdaptorKind = struct
+    type t = kind
+    let compare = Pervasives.compare
+  end
+  module AdaptorMap = Map.Make(AdaptorKind)
+
+  let term_view_adaptor_db =
+    Summary.ref ~name:"view_adaptor_db" AdaptorMap.empty
+
+  let get k =
+    try AdaptorMap.find k !term_view_adaptor_db
+    with Not_found -> []
+
+  let cache_adaptor (_, (k, t)) =
+    let lk = get k in
+    if not (List.exists (Glob_ops.glob_constr_eq t) lk) then
+      term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
+
+  let subst_adaptor ( subst, (k, t as a)) =
+    let t' = Detyping.subst_glob_constr subst t in
+    if t' == t then a else k, t'
+
+  let classify_adaptor x = Libobject.Substitute x
+
+  let in_db =
+    Libobject.declare_object {
+       (Libobject.default_object "VIEW_ADAPTOR_DB")
+    with
+       Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o);
+       Libobject.cache_function = cache_adaptor;
+       Libobject.subst_function = subst_adaptor;
+       Libobject.classify_function = classify_adaptor }
+
+  let declare kind terms =
+    List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term)))
+      (List.rev terms)
+
+end
+
+(* Forward View application code *****************************************)
+
+module State : sig
+
+  (* View storage API *)
+  val vsINIT    : EConstr.t -> unit tactic
+  val vsPUSH    : (EConstr.t -> EConstr.t tactic) -> unit tactic
+  val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic
+  val vsASSERT_EMPTY : unit tactic
+
+end = struct (* {{{ *)
+
+type vstate = {
+  subject_name : Id.t option;   (* top *)
+    (* None if views are being applied to a term *)
+  view : EConstr.t;  (* v2 (v1 top) *)
+}
+
+include Ssrcommon.MakeState(struct
+  type state = vstate option
+  let init = None
+end)
 
-(* The table and its display command *)
-
-(* FIXME this looks hackish *)
-
-let viewtab : glob_constr list array = Array.make 3 []
-
-let _ =
-  let init () = Array.fill viewtab 0 3 [] in
-  let freeze _ = Array.copy viewtab in
-  let unfreeze vt = Array.blit vt 0 viewtab 0 3 in
-  Summary.declare_summary "ssrview"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
-
-(* Populating the table *)
-
-let cache_viewhint (_, (i, lvh)) =
-  let mem_raw h = List.exists (Glob_ops.glob_constr_eq h) in
-  let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in
-  viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i)
-
-let subst_viewhint ( subst, (i, lvh as ilvh)) =
-  let lvh' = List.smartmap (Detyping.subst_glob_constr subst) lvh in
-  if lvh' == lvh then ilvh else i, lvh'
-      
-let classify_viewhint x = Libobject.Substitute x
-
-let in_viewhint =
-  Libobject.declare_object {(Libobject.default_object "VIEW_HINTS") with
-       Libobject.open_function = (fun i o -> if i = 1 then cache_viewhint o);
-       Libobject.cache_function = cache_viewhint;
-       Libobject.subst_function = subst_viewhint;
-       Libobject.classify_function = classify_viewhint }
-
-let glob_view_hints lvh =
-  let env = Global.env () in
-  List.map (Constrintern.intern_constr env Evd.(from_env env)) lvh
-
-let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
-
-let interp_view ist si env sigma gv rv rid =
-  match DAst.get rv with
-  | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) ->
-    let loc = rv.CAst.loc in
-    let rv = DAst.make ?loc @@ GApp (rid, rargs) in
-    snd (interp_open_constr ist (re_sig si sigma) (rv, None))
+let vsINIT view = tclSET (Some { subject_name = None; view })
+
+let vsPUSH k =
+  tacUPDATE (fun s -> match s with
+  | Some { subject_name; view } ->
+      k view >>= fun view ->
+      tclUNIT (Some { subject_name; view })
+  | None ->
+      Goal.enter_one ~__LOC__ begin fun gl ->
+        let concl = Goal.concl gl in
+        let id = (* We keep the orig name for checks in "in" tcl *)
+          match EConstr.kind_of_type (Goal.sigma gl) concl with
+          | Term.ProdType(Name.Name id, _, _)
+            when Ssrcommon.is_discharged_id id -> id
+          | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
+        let view = EConstr.mkVar id in
+        Ssrcommon.tclINTRO_ID id <*>
+        k view >>= fun view ->
+        tclUNIT (Some { subject_name = Some id; view })
+      end)
+
+let vsCONSUME k =
+  tclGET (fun s -> match s with
+  | Some { subject_name; view } ->
+        tclSET None <*>
+        k subject_name view
+  | None -> anomaly "vsCONSUME: empty storage")
+
+let vsASSERT_EMPTY =
+  tclGET (function
+  | Some _ -> anomaly ("vsASSERT_EMPTY: not empty")
+  | _ -> tclUNIT ())
+
+end (* }}} *)
+
+let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce =
+  let ltacvars = {
+    Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint ~ltacvars genv sigma ce
+
+(* Disambiguation of /t
+    - t is ltac:(tactic args)
+    - t is a term
+   To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we
+   need to internalize t.
+*)
+let is_tac_in_term { body; glob_env; interp_env } =
+  Goal.(enter_one ~__LOC__ begin fun goal ->
+    let genv = env goal in
+    let sigma = sigma goal in
+    let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
+    (* We use the env of the goal, not the global one *)
+    let ist = { ist with Genintern.genv } in
+    (* We unravel notations *)
+    let g = intern_constr_expr ist sigma body in
+    match DAst.get g with
+    | Glob_term.GHole (_,_, Some x)
+      when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic)
+        -> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x))
+    | _ -> tclUNIT (`Term (interp_env, g))
+end)
+
+(* To inject a constr into a glob_constr we use an Ltac variable *)
+let tclINJ_CONSTR_IST ist p =
+  let fresh_id = Ssrcommon.mk_internal_id "ssr_inj_constr_in_glob" in
+  let ist = {
+    ist with Geninterp.lfun =
+      Id.Map.add fresh_id (Taccoerce.Value.of_constr p) ist.Geninterp.lfun} in
+  tclUNIT (ist,Glob_term.GVar fresh_id)
+
+let mkGHole =
+  DAst.make
+    (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
+let mkGApp f args =
+  if args = [] then f
+  else DAst.make (Glob_term.GApp (f, args))
+
+(* From glob_constr to open_constr === (env,sigma,constr) *)
+let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
+  let env = Goal.env goal in
+  let sigma = Goal.sigma goal in
+  Ssrprinters.ppdebug (lazy
+    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob));
+  try
+    let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
+    Ssrprinters.ppdebug (lazy
+      Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
+    tclUNIT (env,sigma,term)
+  with e ->
+    Ssrprinters.ppdebug (lazy
+    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
+     tclZERO e
+end
+
+(* Commits the term to the monad *)
+(* I think we should make the API safe by storing here the original evar map,
+ * so that one cannot commit it wrongly.
+ * We could also commit the term automatically, but this makes the code less
+ * modular, see the 2 functions below that would need to "uncommit" *)
+let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
+
+(* The ssr heuristic : *)
+(* Estimate a bound on the number of arguments of a raw constr. *)
+(* This is not perfect, because the unifier may fail to         *)
+(* typecheck the partial application, so we use a minimum of 5. *)
+(* Also, we don't handle delayed or iterated coercions to       *)
+(* FUNCLASS, which is probably just as well since these can     *)
+(* lead to infinite arities.                                    *)
+let guess_max_implicits ist glob =
+  Proofview.tclORELSE
+    (interp_glob ist (mkGApp glob (mkGHoles 6)) >>= fun (env,sigma,term) ->
+     let term_ty = Retyping.get_type_of env sigma term in
+     let ctx, _ = Reductionops.splay_prod env sigma term_ty in
+     tclUNIT (List.length ctx + 6))
+  (fun _ -> tclUNIT 5)
+
+let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
+  interp_glob ist glob >>= fun (env, sigma, term) ->
+  let term_ty = Retyping.get_type_of env sigma term in
+  let ctx, i = Reductionops.splay_prod env sigma term_ty in
+  let rel_ctx =
+    List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in
+  if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i
+  then tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
+  else Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+end
+
+(* There are two ways of "applying" a view to term:            *)
+(*  1- using a view hint if the view is an instance of some    *)
+(*     (reflection) inductive predicate.                       *)
+(*  2- applying the view if it coerces to a function, adding   *)
+(*     implicit arguments.                                     *)
+(* They require guessing the view hints and the number of      *)
+(* implicits, respectively, which we do by brute force.        *)
+(* Builds v p *)
+let interp_view ist v p =
+  let is_specialize hd =
+    match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in
+  (* We cast the pile of views p into a term p_id *)
+  tclINJ_CONSTR_IST ist p >>= fun (ist, p_id) ->
+  let p_id = DAst.make p_id in
+  match DAst.get v with
+  | Glob_term.GApp (hd, rargs) when is_specialize hd ->
+     Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
+     interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr
   | _ ->
-  let interp rc rargs =
-    interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in
-  let rec simple_view rargs n =
-    if n < 0 then view_error "use" gv else
-    try interp rv rargs with _ -> simple_view (mkRHole :: rargs) (n - 1) in
-  let view_nbimps = interp_view_nbimps ist (re_sig si sigma) rv in
-  let view_args = [mkRApp rv (mkRHoles view_nbimps); rid] in
-  let rec view_with = function
-  | [] -> simple_view [rid] (interp_nbargs ist (re_sig si sigma) rv)
-  | hint :: hints -> try interp hint view_args with _ -> view_with hints in
-  snd (view_with (if view_nbimps < 0 then [] else viewtab.(0)))
-
-
-let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr =
-  let c2r ist x = { ist with lfun =
-    Id.Map.add top_id (Value.of_constr x) ist.lfun } in
-  let terminate (sigma, c') =
-    let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
-    let c' = Reductionops.nf_evar sigma c' in
-    let n, c', _, ucst = without_ctx pf_abs_evars gl0 (sigma, c') in
-    let c' = if not prune then c' else without_ctx pf_abs_cterm gl0 n c' in
-    let gl0 = pf_merge_uc ucst gl0 in
-    let gl0, ap =
-      let gl0, ctx = pull_ctx gl0 in
-      let gl0, ap = pf_abs_prod name gl0 c' (Termops.prod_applist sigma cl [c]) in
-      push_ctx ctx gl0, ap in
-    let gl0 = pf_merge_uc_of sigma gl0 in
-    ap, c', gl0 in
-  let rec loop (sigma, c') = function
-  | [] ->
-      let ap, c', gl = terminate (sigma, c') in
-      ap, c', conclude ap c' gl
-  | f :: view ->
-      let ist, rid =
-        match EConstr.kind sigma c' with
-        | Var id -> ist,mkRVar id
-        | _ -> c2r ist c',mkRltacVar top_id in
-      let v = intern_term ist env f in
-      loop (interp_view ist si env sigma f v rid) view
-  in loop
-
-let pfa_with_view ist ?(next=ref []) (prune, view) cl c conclude clr gl =
-  let env, sigma, si =
-    without_ctx pf_env gl, Refiner.project gl, without_ctx sig_it gl in
-  with_view
-    ist ~next si env gl c (constr_name sigma c) cl prune conclude clr (sigma, c) view 
-
-let pf_with_view_linear ist gl v cl c =
-  let x,y,gl =
-    pfa_with_view ist v cl c (fun _ _ -> tac_ctx tclIDTAC) []
-      (push_ctx (new_ctx ()) gl) in
-  let gl, _ = pull_ctxs gl in
-  assert(List.length (sig_it gl) = 1);
-  x,y,re_sig (List.hd (sig_it gl)) (Refiner.project gl)
+     Ssrprinters.ppdebug (lazy Pp.(str "view"));
+     (* We find out how to build (v p) eventually using an adaptor *)
+     let adaptors = AdaptorDb.(get Forward) in
+     Proofview.tclORELSE
+       (pad_to_inductive ist v >>= fun vpad ->
+        Ssrcommon.tclFIRSTa (List.map
+          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+       (fun _ ->
+        guess_max_implicits ist v >>= fun n ->
+        Ssrcommon.tclFIRSTi (fun n ->
+           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
+     >>= tclKeepOpenConstr
+
+(* we store in the state (v top), then (v1 (v2 top))... *)
+let pile_up_view (ist, v) =
+  let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
+  State.vsPUSH (fun p -> interp_view ist v p)
+
+let finalize_view s0 ?(simple_types=true) p =
+Goal.enter_one ~__LOC__ begin fun g ->
+  let env = Goal.env g in
+  let sigma = Goal.sigma g in
+  let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
+  let filter x _ = Evar.Set.mem x evars_of_p in
+  let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
+  let p = Reductionops.nf_evar sigma p in
+  let get_body = function Evd.Evar_defined x -> x | _ -> assert false in
+  let evars_of_econstr sigma t =
+    Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in
+  let rigid_of s =
+    List.fold_left (fun l k ->
+      if Evd.is_defined sigma k then
+        let bo = get_body Evd.(evar_body (find sigma k)) in
+          k :: l @ Evar.Set.elements (evars_of_econstr sigma bo)
+      else l
+    ) [] s in
+  let und0 = (* Unassigned evars in the initial goal *)
+    let sigma0 = Tacmach.project s0 in
+    let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in
+    let g0 = Evd.evars_of_filtered_evar_info g0info in
+    List.filter (fun k -> Evar.Set.mem k g0)
+      (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
+  let rigid = rigid_of und0 in
+  let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in
+  let p = if simple_types then pf_abs_cterm s0 n p else p in
+  Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++
+    Printer.pr_econstr_env env sigma p));
+  let sigma = List.fold_left Evd.remove sigma to_prune in
+  Unsafe.tclEVARS sigma <*>
+  tclUNIT p
+end
+
+let pose_proof subject_name p =
+  Tactics.generalize [p] <*>
+  Option.cata
+    (fun id -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)) (tclUNIT())
+    subject_name
+  <*>
+  Tactics.New.reduce_after_refine
+
+let rec apply_all_views ending vs s0 =
+  match vs with
+  | [] -> ending s0
+  | v :: vs ->
+      Ssrprinters.ppdebug (lazy Pp.(str"piling..."));
+      is_tac_in_term v >>= function
+      | `Tac tac ->
+           Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
+           ending s0 <*> Tacinterp.eval_tactic tac <*>
+           Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+      | `Term v ->
+           Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
+           pile_up_view v <*> apply_all_views ending vs s0
+
+(* Entry points *********************************************************)
+
+let tclIPAT_VIEWS ~views:vs ~conclusion:tac =
+  let end_view_application s0 =
+    State.vsCONSUME (fun name t ->
+      finalize_view s0 t >>= pose_proof name <*>
+      tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in
+  tclINDEPENDENT begin
+    State.vsASSERT_EMPTY <*>
+    Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*>
+    State.vsASSERT_EMPTY
+  end
 
+let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac =
+  let ending_tac s0 =
+    State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in
+  tclINDEPENDENT begin
+    State.vsASSERT_EMPTY <*>
+    State.vsINIT subject <*>
+    Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*>
+    State.vsASSERT_EMPTY
+  end
 
 (* vim: set filetype=ocaml foldmethod=marker: *)