[ssr] implement {}/v as a short hand for {v}/v when v is an id

6 files changed, 81 insertions, 46 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 5571c5420..6ba937a2f 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -88,7 +88,7 @@ type ssripat =
   | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
   | IPatInj of ssripatss
   | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
-  | IPatView of ssrview (* /view *)
+  | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
   | IPatClear of ssrclear (* {H1 H2} *)
   | IPatSimpl of ssrsimpl
   | IPatAbstractVars of Id.t list
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 09f3899ec..46fde4115 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -212,8 +212,8 @@ let tclLOG p t =
 
 let rec ipat_tac1 ipat : unit tactic =
   match ipat with
-  | IPatView l ->
-      Ssrview.tclIPAT_VIEWS ~views:l
+  | IPatView (clear_if_id,l) ->
+      Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id
         ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
   | IPatDispatch ipatss ->
       tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
@@ -588,7 +588,7 @@ let ssrmovetac = function
        (tacVIEW_THEN_GRAB view ~conclusion) <*>
      tclIPAT (IPatClear clr :: ipats)
   | _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
-     tclIPAT (IPatView view :: IPatClear clr :: ipats)
+     tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats)
   | _, (Some pat, (dgens, ipats)) ->
     let dgentac = with_dgens dgens eqmovetac in
     dgentac <*> tclIPAT (eqmoveipats pat ipats)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7a1d06fdc..347a1e4e2 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -412,8 +412,8 @@ let pr_docc = function
 let pr_ssrdocc _ _ _ = pr_docc
 
 ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc
-| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
 | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ]
+| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
 END
 
 (* Old kinds of terms *)
@@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
   | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
-  | IPatView v -> IPatView (List.map map_ast_closure_term v)
+  | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
   | IPatTac _ -> assert false (*internal usage only *)
 
 let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
@@ -646,7 +646,7 @@ let interp_ipat ist gl =
   | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
   | IPatAbstractVars l ->
      IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l))
-  | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist
+  | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist
      gl x)) l)
   | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
   | IPatTac _ -> assert false (*internal usage only *)
@@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
 (* TODO  | [ "+" ] -> [ [IPatAnon Temporary] ] *)
   | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ]
   | [ ssrdocc(occ) "->" ] -> [ match occ with
+      | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
       | None, occ -> [IPatRewrite (occ, L2R)]
       | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]]
   | [ ssrdocc(occ) "<-" ] -> [ match occ with
+      | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
       | None, occ ->  [IPatRewrite (occ, R2L)]
       | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]]
+  | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with
+      | Some [], _ -> [IPatView (true,v)]
+      | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)]
+      | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ]
   | [ ssrdocc(occ) ] -> [ match occ with
       | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
       | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")]
@@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
   | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ]
   | [ "-/" integer(n) "/" integer (m) "=" ] ->
       [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ]
-  | [ ssrfwdview(v) ] -> [ [IPatView v] ]
+  | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ]
   | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
   | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
 END
@@ -1678,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt
 let pr_ssrgen _ _ _ = pr_gen
 
 ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen
-| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ]
+| [ ssrdocc(docc) cpattern(dt) ] -> [
+     match docc with
+     | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here")
+     | _ -> docc, dt ]
 | [ cpattern(dt) ] -> [ nodocc, dt ]
 END
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 11369228c..8f4b2179e 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -107,7 +107,8 @@ let rec pr_ipat p =
   | IPatAnon All -> str "*"
   | IPatAnon Drop -> str "_"
   | IPatAnon One -> str "?"
-  | IPatView v -> pr_view2 v
+  | IPatView (false,v) -> pr_view2 v
+  | IPatView (true,v) -> str"{}" ++ pr_view2 v
   | IPatNoop -> str "-"
   | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
   | IPatTac _ -> str "<tac>"
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index faebe3179..3f974ea06 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -67,9 +67,9 @@ end
 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 vsINIT    : EConstr.t * 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 vsASSERT_EMPTY : unit tactic
 
 end = struct (* {{{ *)
@@ -78,6 +78,7 @@ type vstate = {
   subject_name : Id.t option;   (* top *)
     (* None if views are being applied to a term *)
   view : EConstr.t;  (* v2 (v1 top) *)
+  to_clear : Id.t list;
 }
 
 include Ssrcommon.MakeState(struct
@@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct
   let init = None
 end)
 
-let vsINIT view = tclSET (Some { subject_name = None; view })
+let vsINIT (view, to_clear) =
+  tclSET (Some { subject_name = None; view; to_clear })
 
 let vsPUSH k =
   tacUPDATE (fun s -> match s with
-  | Some { subject_name; view } ->
-      k view >>= fun view ->
-      tclUNIT (Some { subject_name; view })
+  | 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
@@ -102,15 +104,15 @@ let vsPUSH k =
           | _ -> 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 })
+        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
-  | Some { subject_name; view } ->
+  | Some { subject_name; view; to_clear } ->
         tclSET None <*>
-        k subject_name view
+        k ~name:subject_name view ~to_clear
   | None -> anomaly "vsCONSUME: empty storage")
 
 let vsASSERT_EMPTY =
@@ -187,6 +189,16 @@ end
  * modular, see the 2 functions below that would need to "uncommit" *)
 let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
 
+let tclADD_CLEAR_IF_ID (env, ist, t) x =
+  Ssrprinters.ppdebug (lazy
+    Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
+  let hd, _ = EConstr.decompose_app ist t in
+  match EConstr.kind ist hd with
+  | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
+  | _ -> tclUNIT (x,[])
+
+let tclPAIR p x = tclUNIT (x, p)
+
 (* 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         *)
@@ -203,14 +215,15 @@ let guess_max_implicits ist glob =
   (fun _ -> tclUNIT 5)
 
 let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
-  interp_glob ist glob >>= fun (env, sigma, term) ->
+  interp_glob ist glob >>= fun (env, sigma, term as ot) ->
   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")
+  if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i)
+  then Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+  else tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
+       >>= tclADD_CLEAR_IF_ID ot
 end
 
 (* There are two ways of "applying" a view to term:            *)
@@ -221,7 +234,7 @@ end
 (* 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 interp_view ~clear_if_id 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 *)
@@ -230,25 +243,31 @@ let interp_view ist v p =
   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
+     interp_glob ist (mkGApp p_id rargs)
+     >>= tclKeepOpenConstr >>= tclPAIR []
   | _ ->
      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 ->
+       (pad_to_inductive ist v >>= fun (vpad,clr) ->
         Ssrcommon.tclFIRSTa (List.map
-          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)
+        >>= tclPAIR clr)
        (fun _ ->
         guess_max_implicits ist v >>= fun n ->
         Ssrcommon.tclFIRSTi (fun n ->
-           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
-     >>= tclKeepOpenConstr
+           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n
+        >>= fun x -> tclADD_CLEAR_IF_ID x x)
+     >>= fun (ot,clr) ->
+       if clear_if_id
+       then tclKeepOpenConstr ot >>= tclPAIR clr
+       else tclKeepOpenConstr ot >>= tclPAIR []
 
 (* we store in the state (v top), then (v1 (v2 top))... *)
-let pile_up_view (ist, v) =
+let pile_up_view ~clear_if_id (ist, v) =
   let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
-  State.vsPUSH (fun p -> interp_view ist v p)
+  State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
 
 let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
@@ -292,7 +311,7 @@ let pose_proof subject_name p =
   <*>
   Tactics.New.reduce_after_refine
 
-let rec apply_all_views ending vs s0 =
+let rec apply_all_views ~clear_if_id ending vs s0 =
   match vs with
   | [] -> ending s0
   | v :: vs ->
@@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 =
       | `Tac tac ->
            Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
            ending s0 <*> Tacinterp.eval_tactic tac <*>
-           Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+           Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs
       | `Term v ->
            Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
-           pile_up_view v <*> apply_all_views ending vs s0
+           pile_up_view ~clear_if_id v <*>
+           apply_all_views ~clear_if_id ending vs s0
 
 (* Entry points *********************************************************)
 
-let tclIPAT_VIEWS ~views:vs ~conclusion:tac =
+let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~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
+    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
     State.vsASSERT_EMPTY <*>
-    Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*>
+    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 _ t -> finalize_view s0 ~simple_types t >>= tac) in
+    State.vsCONSUME (fun ~name:_ t ~to_clear:_ ->
+      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.vsINIT (subject,[]) <*>
+    Ssrcommon.tacSIGMA >>=
+      apply_all_views ~clear_if_id:false ending_tac vs <*>
     State.vsASSERT_EMPTY
   end
 
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index be51fe7f9..b128a95da 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -20,9 +20,11 @@ module AdaptorDb : sig
 
 end
 
-(* Apply views to the top of the stack (intro pattern) *)
+(* Apply views to the top of the stack (intro pattern). If clear_if_id is
+ * true (default false) then views that happen to be a variable are considered
+ * as to be cleared (see the to_clear argument to the continuation) *)
 val tclIPAT_VIEWS :
-    views:ast_closure_term list ->
+    views:ast_closure_term list -> ?clear_if_id:bool ->
     conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
   unit Proofview.tactic