[ssr] compile "=> {x..} y" as "=> {x..y} y"

This is for consistency with "rewrite {x..} y"

7 files changed, 52 insertions, 20 deletions

diff --git a/CHANGES.md b/CHANGES.md
index bcccd34774..57a0381250 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -163,6 +163,15 @@ SSReflect
   - replace hypothesis: => {}H
   See the reference manual for the actual documentation.
 
+- Clear discipline made consistent: when a clear switch {x..} comes
+  immediately before an existing identifier (used as a view, as a rewrite rule
+  or as name for a new context entry) then such identifier is cleared too.
+  Eg. The following sentences are elaborated as follows:
+  - "=> {x..} H" -> "=> H {x..H}" if H can be cleared
+  - "=> {x..} /v" -> "=> /v {x..v}" if v can be cleared
+  - "rewrite {x..} E" -> "rewrite E {x..E}" if E can be cleared
+
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 59d64feece..c058279207 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1592,9 +1592,13 @@ of the remaining subgoals.
 The first entry in the :token:`i_view` grammar rule, :n:`/@term`,
 represents a view (see section :ref:`views_and_reflection_ssr`).
 It interprets the top of the stack with the view :token:`term`.
-It is equivalent to ``move/term``. The optional flag ``{}`` can
-be used to signal that the :token:`term`, when it is a context entry,
-has to be cleared.
+It is equivalent to ``move/term``.
+
+A :token:`clear_switch` that immediately precedes an :token:`i_view`
+that happen to be a :token:`ident` is extended with that
+:token:`ident` and the :token:`clear_switch` is executed after the view.
+Eg ``{}/v`` is equivalent to ``/v{v}``.
+
 If the next :token:`i_item` is a view, then the view is
 applied to the assumption in top position once all the
 previous :token:`i_item` have been performed.
@@ -1615,8 +1619,9 @@ annotation: views are interpreted opening the ``ssripat`` scope.
   a new constant, fact, or defined constant :token:`ident`, respectively.
   Note that defined constants cannot be introduced when δ-expansion is
   required to expose the top variable or assumption.
-  An empty occurrence switch ``{}`` has the effect of clearing
-  the :token:`ident` before performing the introduction of :token:`ident`.
+  A :token:`clear_switch` (even an empty one) immediately preceding a
+  :token:`ident` is extended with that :token:`ident` if the identifier
+  points to an existing context entry.
   In other words by prefixing the :token:`ident` with ``{}`` one can
   *replace* the context entry.
 ``>``
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 311d912efd..c3b9bde9b8 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -66,7 +66,7 @@ let check_hyp_exists hyps (SsrHyp(_, id)) =
   try ignore(Context.Named.lookup id hyps)
   with Not_found -> errorstrm Pp.(str"No assumption is named " ++ Id.print id)
 
-let test_hypname_exists hyps id =
+let test_hyp_exists hyps (SsrHyp(_, id)) =
   try ignore(Context.Named.lookup id hyps); true
   with Not_found -> false
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 51116ccd75..e642b5e788 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -29,7 +29,7 @@ val allocc : ssrocc
 val hyp_id : ssrhyp -> Id.t
 val hyps_ids : ssrhyps -> Id.t list
 val check_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> unit
-val test_hypname_exists : ('a, 'b) Context.Named.pt -> Id.t -> bool
+val test_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> bool
 val check_hyps_uniq : Id.t list -> ssrhyps -> unit
 val not_section_id : Id.t -> bool
 val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index f10a25dac8..a8dfd69240 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -39,7 +39,7 @@ type ssriop =
   | IOpRewrite of ssrocc * ssrdir
   | IOpView of ssrclear option * ssrview (* extra clears to be performed *)
 
-  | IOpClear of ssrclear
+  | IOpClear of ssrclear * ssrhyp option (* must clear, may clear *)
   | IOpSimpl of ssrsimpl
 
   | IOpEqGen of unit Proofview.tactic (* generation of eqn *)
@@ -70,7 +70,11 @@ let rec pr_ipatop = function
   | IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
   | IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
 
-  | IOpClear cl -> Ssrprinters.pr_clear Pp.spc cl
+  | IOpClear (clmust,clmay) ->
+      Pp.(Ssrprinters.pr_clear spc clmust ++
+            match clmay with
+            | Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")"
+            | None -> mt ())
   | IOpSimpl s -> Ssrprinters.pr_simpl s
 
   | IOpEqGen _ -> Pp.str "E:"
@@ -298,6 +302,13 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
   tclUNIT ()
 end
 
+let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl ->
+  let ctx = Goal.hyps gl in
+  k (Option.bind hyps (fun h ->
+      if Ssrcommon.test_hyp_exists ctx h &&
+         Ssrcommon.(not_section_id (hyp_id h)) then Some h else None))
+end
+
 (** [=> []] *****************************************************************)
 
 (* calls t1 then t2 on each subgoal passing to t2 the index of the current
@@ -467,9 +478,16 @@ let rec ipat_tac1 ipat : bool tactic =
        ipatss
      <*> notTAC
 
-  | IOpClear ids ->
-      tacCHECK_HYPS_EXIST ids <*>
-      intro_clear (List.map Ssrcommon.hyp_id ids) <*>
+  | IOpClear (must,may) ->
+      tacCHECK_HYPS_EXIST must <*>
+      tacFILTER_HYP_EXIST may (fun may ->
+        let must = List.map Ssrcommon.hyp_id must in
+        let cl = Option.fold_left (fun cls (SsrHyp(_,id)) ->
+          if CList.mem_f Id.equal id cls then begin
+            duplicate_clear id;
+            cls
+          end else id :: cls) must may in
+        intro_clear cl) <*>
       notTAC
 
   | IOpSimpl x ->
@@ -528,8 +546,8 @@ let tclCompileIPats l =
 
   | (IPatClear cl) :: (IPatView v) :: rest ->
       (IOpView(Some cl,v)) :: elab rest
-  | (IPatClear []) :: (IPatId id) :: rest ->
-      (IOpClear [SsrHyp(None,id)]) :: IOpId id :: elab rest
+  | (IPatClear cl) :: (IPatId id) :: rest ->
+      (IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest
 
   (* boring code *)
   | [] -> []
@@ -546,7 +564,7 @@ let tclCompileIPats l =
   | IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest
   | IPatView vs :: rest -> IOpView (None,vs) :: elab rest
   | IPatSimpl s :: rest -> IOpSimpl s :: elab rest
-  | IPatClear cl :: rest -> IOpClear cl :: elab rest
+  | IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest
 
   | IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest
   | IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest
@@ -853,9 +871,9 @@ let ssrmovetac = function
      gentac <*>
      tclLAST_GEN ~to_ind:false lastgen
        (tacVIEW_THEN_GRAB view ~conclusion) <*>
-     tclIPAT (IOpClear clr :: IpatMachine.tclCompileIPats ipats)
+     tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
   | _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
-     tclIPAT (IOpView (None,view) :: IOpClear clr :: IpatMachine.tclCompileIPats ipats)
+      tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
   | _, (Some pat, (dgens, ipats)) ->
     let dgentac = with_dgens dgens eqmovetac in
     dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats))
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index 0d71a24aa1..a04c3f4c46 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -44,7 +44,7 @@ type ssriop =
   | IOpRewrite of ssrocc * ssrdir
   | IOpView of ssrclear option * ssrview (* extra clears to be performed *)
 
-  | IOpClear of ssrclear
+  | IOpClear of ssrclear * ssrhyp option
   | IOpSimpl of ssrsimpl
 
   | IOpEqGen of unit Proofview.tactic (* generation of eqn *)
diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v
index 70e1d5bcf1..528f33f30d 100644
--- a/test-suite/ssr/ipat_replace.v
+++ b/test-suite/ssr/ipat_replace.v
@@ -9,9 +9,9 @@ have {}H : True.
 by apply: H.
 Qed.
 
-Lemma test2 (H : True) : False -> False.
+Lemma test2 (H : True) : False -> False -> False.
 Proof.
-Fail move=> {}W.
+move=> {}W.
 move=> {}H.
 by apply: H.
 Qed.