[ssr] new syntax for the under tactic

5 files changed, 135 insertions, 91 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a4ab038314..cb529bd68e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3692,9 +3692,7 @@ complete terms, as shown by the simple example below.
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G by rewrite subnn.
-
-  ``(* FIXME: replace with do... *)``
+      under eq_G => n do rewrite subnn.
 
 .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
    :name: under
@@ -3762,7 +3760,7 @@ lemma ``eq_G``, but this time in interactive mode:
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G.
+      under eq_G => m.
         rewrite subnn.
         over.
 
@@ -3857,9 +3855,7 @@ shortened to: :n:`under @term => i do tac1.`
       Lemma test_big_nested (F G : nat -> nat) (m n : nat) :
         \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
         \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
-      under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC].
-
-   ``(* FIXME: replace with do... *)``
+      under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC].
 
 .. _locking_ssr:
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8bca62a4ff..349f0082e1 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -331,68 +331,53 @@ let is_app_evar sigma t =
       | _ -> false end
   | _ -> false
 
-let tmp = ref 0
-
-let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
- let c = Proofview.Goal.concl gl in
- let sigma = Proofview.Goal.sigma gl in
- let env = Proofview.Goal.env gl in
- let rec aux c =
-  match EConstr.kind_of_type sigma c with
-  | Term.SortType _ -> Proofview.tclUNIT ()
-  | ( Term.ProdType ({ Context.binder_name = name },_,t)
-    | Term.LetInType ({ Context.binder_name = name },_,_,t) ) ->
-      begin match names with
-      | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names
-      | [] ->
-          (* after quell intro patterns, use IpatTemp *)
-          let id =
-            match name with
-            | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp)
-            | Name.Name n -> n in
-          incr tmp;
-          Ssripats.tclIPAT [
-            Ssripats.IOpId id;
-            Ssripats.IOpEqGen (intro_lock names);
-            Ssripats.IOpEqGen (Tactics.revert [id])]
-      end
-  | Term.CastType (t,_) -> aux t
-  | Term.AtomicType _ ->
-      let t = Reductionops.whd_all env sigma c in
-      match EConstr.kind_of_type sigma t with
-      | Term.ProdType _ -> aux t
-      | Term.AtomicType(hd, args) when
-          Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
-          Array.length args = 3 && is_app_evar sigma args.(2) ->
-            Tactics.New.refine ~typecheck:true (fun sigma ->
-              let sigma, under =
-                Ssrcommon.mkSsrConst "Under" env sigma in
-              let sigma, under_from_eq =
-                Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
-              let ty = EConstr.mkApp (under,args) in
-              let sigma, t = Evarutil.new_evar env sigma ty in
-              sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
-      | _ -> Proofview.tclUNIT ()
+let intro_lock ipats =
+  let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
+    Proofview.tclORELSE
+      (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
+      (fun _exn -> Proofview.Goal.enter begin fun gl ->
+        let c = Proofview.Goal.concl gl in
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
+        let t = Reductionops.whd_all env sigma c in
+        match EConstr.kind_of_type sigma t with
+        | Term.AtomicType(hd, args) when
+            Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
+            Array.length args = 3 && is_app_evar sigma args.(2) ->
+              Tactics.New.refine ~typecheck:true (fun sigma ->
+                let sigma, under =
+                  Ssrcommon.mkSsrConst "Under" env sigma in
+                let sigma, under_from_eq =
+                  Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+                let ty = EConstr.mkApp (under,args) in
+                let sigma, t = Evarutil.new_evar env sigma ty in
+                sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+        | _ ->
+    ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
+
+            Proofview.tclUNIT ()
+       end)
+    end
   in
-    aux c
-
-end
-
-let rec pretty_rename evar_map term = function
-  | [] -> term
-  | varname :: varnames ->
-     try begin
-       match EConstr.destLambda evar_map term
-       with ({ Context.binder_relevance = r }, types, body) ->
-           let res = pretty_rename evar_map body varnames in
-           let name = Names.Name.mk_name varname in
-           (* Note: we don't explicitly check name \notin free_vars(res) here *)
-           EConstr.mkLambda (Context.make_annot name r, types, res)
-         end
-     with
-     | DestKO ->
-        ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
-        term
+  Ssripats.tclIPATssr ipats <*> lock_eq ()
+
+let pretty_rename evar_map term varnames =
+  let rec aux term vars =
+    try
+      match vars with
+      | [] -> term
+      | Names.Name.Anonymous :: varnames ->
+          let name, types, body = EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (name, types, res)
+      | Names.Name.Name _ as name :: varnames ->
+          let { Context.binder_relevance = r }, types, body =
+            EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (Context.make_annot name r, types, res)
+    with DestKO -> term
+  in
+    aux term varnames
 
 let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1)
 
@@ -408,19 +393,37 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let undertac ist varnames ((dir,mult),_ as rule) hint =
-  if mult <> Ssrequality.nomult then
-    Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
+let undertac ist ipats ((dir,_),_ as rule) hint =
+
+  let varnames =
+    let rec aux acc = function
+      | IPatId id :: rest -> aux (Names.Name.Name id :: acc) rest
+      | IPatClear _ :: rest -> aux acc rest
+      | IPatSimpl _ :: rest -> aux acc rest
+      | IPatAnon (One _ | Drop) :: rest ->
+          aux (Names.Name.Anonymous :: acc) rest
+      | _ -> List.rev acc in
+    aux [] (Option.default [] ipats) in
+
+  (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra
+   * goal (the one that is left once we run over) *)
+  let ipats =
+    match ipats with
+    | None -> [IPatNoop]
+    | Some (IPatCase(Regular []) :: _ as ipats) -> ipats
+    | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest
+    | Some (IPatCase(Block _) :: _ as l) -> l
+    | Some l -> [IPatCase(Regular [l;[]])] in
 
   let map_redex env evar_map ~before:_ ~after:t =
-    ppdebug(lazy Pp.(str("under vars: " ^
-      (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames ""))));
-    ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t));
+    ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
 
     let evar_map, ty = Typing.type_of env evar_map t in
     let new_t = (* pretty-rename the bound variables *)
       try begin match EConstr.destApp evar_map t with (f, ar) ->
             let lam = Array.last ar in
+            ppdebug(lazy Pp.(str"under: mapping:" ++
+                             pr_econstr_env env evar_map lam));
             let new_lam = pretty_rename evar_map lam varnames in
             let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
             new_ar.(len1) <- new_lam;
@@ -450,5 +453,8 @@ let undertac ist varnames ((dir,mult),_ as rule) hint =
               (if hint = nullhint then [None] else snd hint))
            @ [betaiota])
   in
-  (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
-     intro_lock varnames <*> undertacs)
+  let rew =
+    Proofview.V82.tactic
+      (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule])
+  in
+  rew <*> intro_lock ipats <*> undertacs
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 745560da03..6f7cc6d445 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -59,7 +59,7 @@ val sufftac :
 
 val undertac :
   Ltac_plugin.Tacinterp.interp_sign ->
-  Names.Id.t list -> Ssrequality.ssrrwarg ->
+  Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
 
 val overtac :
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 507cf8db70..2c46947658 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -741,15 +741,33 @@ let pushIPatNoop = function
   | pats :: orpat -> (IPatNoop :: pats) :: orpat
   | [] -> []
 
+let test_ident_no_do strm =
+  match Util.stream_nth 0 strm with
+  | Tok.IDENT s when s <> "do" -> ()
+  | _ -> raise Stream.Failure
+
+let test_ident_no_do =
+  Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do
+
 }
 
+ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
+| [ "YouShouldNotTypeThis" ident(id) ] -> { id }
+END
+
+
+GRAMMAR EXTEND Gram
+  GLOBAL: ident_no_do;
+  ident_no_do: [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ];
+END
+
 ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
   INTERPRETED BY { interp_ipats }
   GLOBALIZED BY { intern_ipats }
   | [ "_" ] -> { [IPatAnon Drop] }
   | [ "*" ] -> { [IPatAnon All] }
   | [ ">" ] -> { [IPatFastNondep] }
-  | [ ident(id) ] -> { [IPatId id] }
+  | [ ident_no_do(id) ] -> { [IPatId id] }
   | [ "?" ] -> { [IPatAnon (One None)] }
   | [ "+" ] -> { [IPatAnon Temporary] }
   | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
@@ -2650,9 +2668,32 @@ TACTIC EXTEND ssrgenhave2
     V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
 END
 
+{
+
+let check_under_arg ((_dir,mult),((_occ,_rpattern),_rule)) =
+  if mult <> nomult then
+    CErrors.user_err Pp.(str"under does not support multipliers")
+
+}
+
+
 TACTIC EXTEND under
-  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] ->
-    { Ssrfwd.undertac ist names r hint }
+  | [ "under" ssrrwarg(arg) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist None arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg h
+    }
+  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *)
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some [IPatAnon All]) arg h
+    }
 END
 
 {
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 9ce249124d..5f27858d17 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -86,12 +86,13 @@ Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) :
   \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
 Proof.
 (* in interactive mode *)
-under i Hi: eq_bigr.
-  under j Hj: eq_big.
+under eq_bigr => i Hi.
+  under eq_big => [j|j Hj].
   { rewrite muln1. over. }
   { rewrite addnC. over. }
+(* MISSING BETA *)
   over.
-done.
+by [].
 Qed.
 
 Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) :
@@ -99,14 +100,14 @@ Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) :
   \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
 Proof.
 (* in one-liner mode *)
-under i Hi: eq_bigr by under j Hj: eq_big by [rewrite muln1 | rewrite addnC].
+under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ].
 done.
 Qed.
 
 Lemma test_big_patt1 (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0.
 Proof.
-under i Hi: [in RHS]eq_bigr.
+under [in RHS]eq_bigr => i Hi.
   by rewrite addnC over.
 done.
 Qed.
@@ -115,14 +116,14 @@ Lemma test_big_patt2 (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (F i + F i) =
   \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2).
 Proof.
-under i Hi: [X in _ = _ + X]eq_bigr by rewrite mulnS muln1.
+under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1.
 by rewrite big_const_nat iter_addn_0.
 Qed.
 
 Lemma test_big_occs (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
 Proof.
-under i Hi: {2}[in RHS]eq_bigr by rewrite muln0.
+under {2}[in RHS]eq_bigr => i Hi do rewrite muln0.
 by rewrite big_const_nat iter_addn_0.
 Qed.
 
@@ -131,15 +132,15 @@ Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) :
   \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
   \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
 Proof.
-under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *)
+under [RHS]eq_bigr => a A do under eq_bigr => b B do []. (* renaming bound vars *)
 myadmit.
 Qed.
 
 Lemma test_big_andb (F : nat -> nat) (m n : nat) :
   \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1.
 Proof.
-under i: eq_bigl by rewrite andb_idl; first by move/eqP->.
-under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *)
+under eq_bigl => i do rewrite andb_idl; first by move/eqP->.
+under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *)
 myadmit.
 Qed.
 
@@ -158,6 +159,6 @@ under x: Lem.
 - rewrite f_eq; over.
 - done.
  *)
-under x: Lem by [done|rewrite f_eq|done].
+under Lem => [|x|] do [done|rewrite f_eq|done].
 done.
 Qed.