Tentatively implementing apply.

12 files changed, 121 insertions, 6 deletions

diff --git a/_CoqProject b/_CoqProject
index 583639612b..f202e1aed2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -20,6 +20,8 @@ src/tac2core.mli
 src/tac2qexpr.mli
 src/tac2quote.ml
 src/tac2quote.mli
+src/tac2tactics.ml
+src/tac2tactics.mli
 src/tac2stdlib.ml
 src/tac2stdlib.mli
 src/g_ltac2.ml4
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index bb98ea3e5d..ca3631799b 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -291,7 +291,7 @@ open Tac2entries.Pltac
 let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 GEXTEND Gram
-  GLOBAL: q_ident q_bindings q_intropatterns;
+  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns;
   ident_or_anti:
     [ [ id = Prim.ident -> QExpr id
       | LEFTQMARK; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
@@ -375,6 +375,9 @@ GEXTEND Gram
   q_intropatterns:
     [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ~loc:!@loc ipat ] ]
   ;
+  q_intropattern:
+    [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ~loc:!@loc ipat ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 8d2d7dc0f4..4c4082ad65 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -6,5 +6,6 @@ Tac2entries
 Tac2ffi
 Tac2core
 Tac2quote
+Tac2tactics
 Tac2stdlib
 G_ltac2
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b45275210e..329c115be3 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -883,6 +883,14 @@ let () = add_scope "bindings" begin function
 | _ -> scope_fail ()
 end
 
+let () = add_scope "intropattern" begin function
+| [] ->
+  let scope = Extend.Aentry Tac2entries.Pltac.q_intropattern in
+  let act tac = tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_scope "intropatterns" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_intropatterns in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 0f32736096..52a5899d25 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -26,6 +26,7 @@ let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
 
 let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
 let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
+let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
 let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
 end
 
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index e5031fdba2..2e51a4fb2e 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -59,5 +59,6 @@ val tac2expr : raw_tacexpr Pcoq.Gram.entry
 
 val q_ident : raw_tacexpr Pcoq.Gram.entry
 val q_bindings : raw_tacexpr Pcoq.Gram.entry
+val q_intropattern : raw_tacexpr Pcoq.Gram.entry
 val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index f63252ec22..b678b65b82 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -12,6 +12,7 @@ open Misctypes
 open Genredexpr
 open Tac2expr
 open Tac2core
+open Tac2tactics
 open Proofview.Notations
 
 module Value = Tac2ffi
@@ -178,6 +179,17 @@ let () = define_prim2 "tac_intros" begin fun ev ipat ->
   Tactics.intros_patterns ev ipat
 end
 
+let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
+  let adv = Value.to_bool adv in
+  let ev = Value.to_bool ev in
+  let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  let cb = Value.to_list map_cb cb in
+  let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in
+  let map_ipat p = to_pair Value.to_ident map p in
+  let ipat = Value.to_option map_ipat ipat in
+  Tac2tactics.apply adv ev cb ipat
+end
+
 let () = define_prim3 "tac_elim" begin fun ev c copt ->
   let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
new file mode 100644
index 0000000000..2590d7daed
--- /dev/null
+++ b/src/tac2tactics.ml
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Tactics
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
+
+(** FIXME: export a better interface in Tactics *)
+let delayed_of_tactic tac env sigma =
+  let _, pv = Proofview.init sigma [] in
+  let c, pv, _, _ = Proofview.apply env tac pv in
+  (sigma, c)
+
+let apply adv ev cb cl =
+  let map c = None, Loc.tag (delayed_of_tactic c) in
+  let cb = List.map map cb in
+  match cl with
+  | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
+  | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
new file mode 100644
index 0000000000..86278f177e
--- /dev/null
+++ b/src/tac2tactics.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Misctypes
+open Tactypes
+open Proofview
+
+(** Local reimplementations of tactics variants from Coq *)
+
+val apply : advanced_flag -> evars_flag ->
+  EConstr.constr with_bindings tactic list ->
+  (Id.t * intro_pattern option) option -> unit tactic
diff --git a/tests/example2.v b/tests/example2.v
index ca9e3dcff5..fd5a9044e9 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -26,3 +26,18 @@ intros H.
 elim &H with 0.
 split.
 Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+Fail apply &H.
+apply &H with (m := 0).
+split.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+eapply &H.
+split.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 2d7b4c8a8b..1bc48d587a 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -37,11 +37,11 @@ Ltac2 Notation "econstructor" n(tactic) bnd(bindings) :=
   Std.constructor_n true n bnd.
 
 Ltac2 elim0 ev c bnd use :=
-    let use := match use with
-    | None => None
-    | Some u =>
-      let ((_, c, wth)) := u in Some (c, wth)
-    end in
+  let use := match use with
+  | None => None
+  | Some u =>
+    let ((_, c, wth)) := u in Some (c, wth)
+  end in
   Std.elim ev (c, bnd) use.
 
 Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
@@ -53,3 +53,28 @@ Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
 Ltac2 Notation "eelim" c(constr) bnd(bindings)
   use(opt(seq("using", constr, bindings))) :=
   elim0 true c bnd use.
+
+Ltac2 apply0 adv ev cb cl :=
+  let cl := match cl with
+  | None => None
+  | Some p =>
+    let ((_, id, ipat)) := p in
+    let p := match ipat with
+    | None => None
+    | Some p =>
+      let ((_, ipat)) := p in
+      Some ipat
+    end in
+    Some (id, p)
+  end in
+  Std.apply adv ev cb cl.
+
+Ltac2 Notation "eapply"
+  cb(list1(thunk(seq(constr, bindings)), ","))
+  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  apply0 true true cb cl.
+
+Ltac2 Notation "apply"
+  cb(list1(thunk(seq(constr, bindings)), ","))
+  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  apply0 true false cb cl.
diff --git a/theories/Std.v b/theories/Std.v
index 20504f1247..3d1e8f462d 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -74,11 +74,15 @@ with or_and_intro_pattern := [
 ].
 
 Ltac2 Type evar_flag := bool.
+Ltac2 Type advanced_flag := bool.
 
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
 Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "ltac2" "tac_intros".
 
+Ltac2 @ external apply : advanced_flag -> evar_flag ->
+  (unit -> constr_with_bindings) list -> (ident * (intro_pattern option)) option -> unit := "ltac2" "tac_apply".
+
 Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
 Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "tac_case".