[ssr] extended intro patterns: + > [^] /ltac:

This commit implements the following intro patterns:

Temporary "=> +"
 "move=> + stuff" ==== "move=> tmp stuff; move: tmp"
 It preserves the original name.
 "=>" can be chained to force generalization as in
 "move=> + y + => x z"

Tactics as views "=> /ltac:(tactic)"
 Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
 Limited to views on the right of "=>", views that decorate a tactic
 as move or case are not supported to be tactics.

Dependent "=> >H"
 move=> >H  ===== move=> ???? H, with enough ? to
 name H the first non-dependent assumption (LHS of the first arrow).
 TC isntances are skipped.

Block intro "=> [^ H] [^~ H]"
 after "case" or "elim" or "elim/v" it introduces in one go
 all new assumptions coming from the eliminations. The names are
 picked from the inductive type declaration or the elimination principle
 "v" in "elim/v" and are appended/prepended the seed "H"

The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).

1 files changed, 111 insertions, 59 deletions

diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 1aa64d7141..4816027296 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -59,18 +59,23 @@ end
 
 (* Forward View application code *****************************************)
 
+let reduce_or l = tclUNIT (List.fold_left (||) false l)
+
 module State : sig
 
   (* View storage API *)
-  val vsINIT    : EConstr.t * Id.t list -> unit tactic
+  val vsINIT    : view:EConstr.t -> subject_name:Id.t list -> to_clear:Id.t list -> unit tactic
   val vsPUSH    : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic
-  val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic
+  val vsCONSUME : (names:Id.t list -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic
+
+  (* The bool is the || of the bool returned by the continuations *)
+  val vsCONSUME_IF_PRESENT : (names:Id.t list -> EConstr.t option -> to_clear:Id.t list -> bool tactic) -> bool tactic
   val vsASSERT_EMPTY : unit tactic
 
 end = struct (* {{{ *)
 
 type vstate = {
-  subject_name : Id.t option;   (* top *)
+  subject_name : Id.t list;   (* top *)
     (* None if views are being applied to a term *)
   view : EConstr.t;  (* v2 (v1 top) *)
   to_clear : Id.t list;
@@ -81,34 +86,43 @@ include Ssrcommon.MakeState(struct
   let init = None
 end)
 
-let vsINIT (view, to_clear) =
-  tclSET (Some { subject_name = None; view; to_clear })
+let vsINIT ~view ~subject_name ~to_clear =
+  tclSET (Some { subject_name; view; to_clear })
+
+(** Initializes the state in which view data is accumulated when views are
+applied to the first assumption in the goal *)
+let vsBOOTSTRAP = 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 <*>
+  tclSET (Some { subject_name = [id]; view; to_clear = [] })
+end
 
-let vsPUSH k =
-  tacUPDATE (fun s -> match s with
+let rec vsPUSH k =
+ tclINDEPENDENT (tclGET (function
   | Some { subject_name; view; to_clear } ->
       k view >>= fun (view, clr) ->
-      tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr })
-  | 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, to_clear) ->
-        tclUNIT (Some { subject_name = Some id; view; to_clear })
-      end)
-
-let vsCONSUME k =
-  tclGET (fun s -> match s with
+      tclSET (Some { subject_name; view; to_clear = to_clear @ clr })
+  | None -> vsBOOTSTRAP <*> vsPUSH k))
+
+let rec vsCONSUME k =
+ tclINDEPENDENT (tclGET (function
   | Some { subject_name; view; to_clear } ->
         tclSET None <*>
-        k ~name:subject_name view ~to_clear
-  | None -> anomaly "vsCONSUME: empty storage")
+        k ~names:subject_name view ~to_clear
+  | None -> vsBOOTSTRAP <*> vsCONSUME k))
+
+let vsCONSUME_IF_PRESENT k =
+ tclINDEPENDENTL (tclGET1 (function
+  | Some { subject_name; view; to_clear } ->
+        tclSET None <*>
+        k ~names:subject_name (Some view) ~to_clear
+  | None -> k ~names:[] None ~to_clear:[])) >>= reduce_or
 
 let vsASSERT_EMPTY =
   tclGET (function
@@ -128,13 +142,19 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce =
    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 } =
+let is_tac_in_term ?extra_scope { 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 open extra_scope *)
+    let body =
+      match extra_scope with
+      | None -> body
+      | Some s -> CAst.make (Constrexpr.CDelimiters(s,body))
+    in
     (* We unravel notations *)
     let g = intern_constr_expr ist sigma body in
     match DAst.get g with
@@ -300,51 +320,83 @@ end
 
 let pose_proof subject_name p =
   Tactics.generalize [p] <*>
-  Option.cata
-    (fun id -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)) (tclUNIT())
-    subject_name
+  begin match subject_name with
+  | id :: _ -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)
+  | _ -> tclUNIT() end
   <*>
   Tactics.New.reduce_after_refine
 
-let rec apply_all_views ~clear_if_id ending vs s0 =
+(* returns true if the last item was a tactic *)
+let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 =
   match vs with
-  | [] -> ending s0
+  | [] -> finalization s0 (fun name p ->
+            (match p with
+            | None -> conclusion ~to_clear:[]
+            | Some p ->
+                pose_proof name p <*> conclusion ~to_clear:name) <*>
+            tclUNIT false)
   | 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 ~clear_if_id ending vs
+      is_tac_in_term ~extra_scope:"ssripat" v >>= function
       | `Term v ->
            Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
            pile_up_view ~clear_if_id v <*>
-           apply_all_views ~clear_if_id ending vs s0
+           apply_all_views_aux ~clear_if_id vs finalization conclusion s0
+      | `Tac tac ->
+           Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
+           finalization s0 (fun name p ->
+            (match p with
+            | None -> tclUNIT ()
+            | Some p -> pose_proof name p) <*>
+           Tacinterp.eval_tactic tac <*>
+           if vs = [] then begin
+             Ssrprinters.ppdebug (lazy Pp.(str"..was the last view"));
+             conclusion ~to_clear:name <*> tclUNIT true
+           end else
+             Tactics.clear name <*>
+             tclINDEPENDENTL begin
+               Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view"));
+               Ssrcommon.tacSIGMA >>=
+                 apply_all_views_aux ~clear_if_id vs finalization conclusion
+             end >>= reduce_or)
+
+let apply_all_views vs ~conclusion ~clear_if_id =
+  let finalization s0 k =
+    State.vsCONSUME_IF_PRESENT (fun ~names t ~to_clear ->
+      match t with
+      | None -> k [] None
+      | Some t ->
+          finalize_view s0 t >>= fun p -> k (names @ to_clear) (Some p)) in
+  Ssrcommon.tacSIGMA >>=
+    apply_all_views_aux ~clear_if_id vs finalization conclusion
+
+(* We apply a view to a term given by the user, e.g. `case/V: x`. `x` is
+   `subject` *)
+let apply_all_views_to subject ~simple_types vs ~conclusion = begin
+  let rec process_all_vs = function
+    | [] -> tclUNIT ()
+    | v :: vs -> is_tac_in_term v >>= function
+      | `Tac _ -> Ssrcommon.errorstrm Pp.(str"tactic view not supported")
+      | `Term v -> pile_up_view ~clear_if_id:false v <*> process_all_vs vs in
+  State.vsASSERT_EMPTY <*>
+  State.vsINIT ~subject_name:[] ~to_clear:[] ~view:subject <*>
+  Ssrcommon.tacSIGMA >>= fun s0 ->
+  process_all_vs vs <*>
+  State.vsCONSUME (fun ~names:_ t ~to_clear:_ ->
+    finalize_view s0 ~simple_types t >>= conclusion)
+end
 
 (* Entry points *********************************************************)
 
-let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac =
-  let end_view_application s0 =
-    State.vsCONSUME (fun ~name t ~to_clear ->
-      let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in
-      finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in
-  tclINDEPENDENT begin
+let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion =
+  tclINDEPENDENTL begin
     State.vsASSERT_EMPTY <*>
-    Ssrcommon.tacSIGMA >>=
-      apply_all_views ~clear_if_id 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 ~name:_ t ~to_clear:_ ->
-      finalize_view s0 ~simple_types t >>= tac) in
-  tclINDEPENDENT begin
+    apply_all_views vs ~conclusion ~clear_if_id >>= fun was_tac ->
     State.vsASSERT_EMPTY <*>
-    State.vsINIT (subject,[]) <*>
-    Ssrcommon.tacSIGMA >>=
-      apply_all_views ~clear_if_id:false ending_tac vs <*>
-    State.vsASSERT_EMPTY
-  end
+    tclUNIT was_tac
+  end >>= reduce_or
+
+let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion =
+  tclINDEPENDENT (apply_all_views_to subject ~simple_types vs ~conclusion)
 
 (* vim: set filetype=ocaml foldmethod=marker: *)