[ssr] new syntax for the under tactic

3 files changed, 120 insertions, 73 deletions

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
 
 {