Allowing calls to Ltac2 inside Ltac1.

3 files changed, 96 insertions, 2 deletions

diff --git a/doc/ltac2.md b/doc/ltac2.md
index 5b1776b64f..d1c5c68494 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -698,11 +698,30 @@ errors after expansion.
 
 One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses
 a Ltac1 expression, and semantics of this quotation is the evaluation of the
-corresponding code for its side effects.
+corresponding code for its side effects. In particular, in cannot return values,
+and the quotation has type `unit`.
 
 Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
 to the use of standalone function calls.
 
+## Ltac2 from Ltac1
+
+Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
+instead.
+
+Note that the tactic expression is evaluated eagerly, if one wants to use it as
+an argument to a Ltac1 function, she has to resort to the good old
+`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately
+and won't print anything.
+
+```
+Ltac mytac tac := idtac "wow"; tac.
+
+Goal True.
+Proof.
+mytac ltac2:(fail).
+```
+
 # Transition from Ltac1
 
 Owing to the use of a bunch of notations, the transition shouldn't be
@@ -812,6 +831,5 @@ your duty to catch it and reraise it depending on your use.
 # TODO
 
 - Implement deep pattern-matching.
-- Implement compatibility layer with Ltac1
 - Craft an expressive set of primitive functions
 - Implement native compilation to OCaml
diff --git a/src/tac2core.ml b/src/tac2core.ml
index b95410f40e..118bea0f8e 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -765,6 +765,26 @@ let () =
   in
   Pretyping.register_constr_interp0 wit_ltac2 interp
 
+(** Ltac2 in Ltac1 *)
+
+let () =
+  (** FUCK YOU API *)
+  let e = (Obj.magic Tac2entries.Pltac.tac2expr : _ API.Pcoq.Gram.entry) in
+  let inject (loc, v) = Tacexpr.TacGeneric (in_gen (rawwit wit_ltac2) v) in
+  Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
+
+let () =
+  let open Ltac_plugin in
+  let open Tacinterp in
+  let idtac = Value.of_closure (default_ist ()) (Tacexpr.TacId []) in
+  (** FUCK YOU API *)
+  let idtac = (Obj.magic idtac : Geninterp.Val.t) in
+  let interp ist tac =
+    Tac2interp.interp Tac2interp.empty_environment tac >>= fun _ ->
+    Ftactic.return idtac
+  in
+  Geninterp.register_interp0 wit_ltac2 interp
+
 (** Patterns *)
 
 let () =
diff --git a/tests/compat.v b/tests/compat.v
new file mode 100644
index 0000000000..44421349da
--- /dev/null
+++ b/tests/compat.v
@@ -0,0 +1,56 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+(** Test calls to Ltac1 from Ltac2 *)
+
+Ltac2 foo () := ltac1:(discriminate).
+
+Goal true = false -> False.
+Proof.
+foo ().
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+(** FIXME when the non-strict mode is implemented. *)
+Fail intros H; ltac1:(rewrite H); reflexivity.
+Abort.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac2 bar nay := ltac1:(discriminate nay).
+
+(** Test calls to Ltac2 from Ltac1 *)
+
+Set Default Proof Mode "Classic".
+
+Ltac foo := ltac2:(foo ()).
+
+Goal true = false -> False.
+Proof.
+ltac2:(foo ()).
+Qed.
+
+Goal true = false -> False.
+Proof.
+foo.
+Qed.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac bar x := ltac2:(foo x).
+
+Ltac mytac tac := idtac "wow".
+
+Goal True.
+Proof.
+(** Fails because quotation is evaluated eagerly *)
+Fail mytac ltac2:(fail).
+(** One has to thunk thanks to the idtac trick *)
+let t := idtac; ltac2:(fail) in mytac t.
+constructor.
+Qed.