From d54eacd7b48b9cb0212d5a7cef2ea428469df74a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Dec 2016 14:44:05 +0100
Subject: Allow the embedding of Ltac2 terms in constrs via the ltac2:(...)
 syntax.

---
 g_ltac2.ml4   | 10 ++++++++++
 tac2core.ml   | 14 ++++++++++++++
 tac2env.ml    |  4 ++++
 tac2env.mli   |  4 ++++
 tac2intern.ml | 17 +++++++++++++++++
 5 files changed, 49 insertions(+)

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index ff3d79bbae..1dbd223b22 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -11,6 +11,8 @@ open Util
 open Genarg
 open Names
 open Pcoq
+open Constrexpr
+open Misctypes
 open Tac2expr
 open Ltac_plugin
 
@@ -190,6 +192,14 @@ GEXTEND Gram
   ;
 END
 
+GEXTEND Gram
+  Pcoq.Constr.operconstr: LEVEL "0"
+    [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
+          let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+          CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+  ;
+END
+
 let pr_ltac2entry _ = mt () (** FIXME *)
 let pr_ltac2expr _ = mt () (** FIXME *)
 
diff --git a/tac2core.ml b/tac2core.ml
index fd998151fd..c18b6032a6 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -473,3 +473,17 @@ let () =
     ml_interp = interp;
   } in
   define_ml_object Stdarg.wit_ident obj
+
+let () =
+  let interp ist env sigma concl tac =
+    let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
+      match Val.eq tag val_valexpr with
+      | None -> accu
+      | Some Refl -> Id.Map.add id v accu
+    in
+    let ist = Id.Map.fold fold ist Id.Map.empty in
+    let tac = Proofview.tclIGNORE (interp ist tac) in
+    let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
+    (EConstr.of_constr c, sigma)
+  in
+  Pretyping.register_constr_interp0 wit_ltac2 interp
diff --git a/tac2env.ml b/tac2env.ml
index 17c70d2e44..a058d764e7 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -208,3 +208,7 @@ let interp_ml_object t = MLType.obj t
 
 let coq_prefix =
   MPfile (DirPath.make (List.map Id.of_string ["Init"; "ltac2"; "Coq"]))
+
+(** Generic arguments *)
+
+let wit_ltac2 = Genarg.make0 "ltac2"
diff --git a/tac2env.mli b/tac2env.mli
index 96174e8c92..4d2a1645ea 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -100,3 +100,7 @@ val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
 
 val coq_prefix : ModPath.t
 (** Path where primitive datatypes are defined in Ltac2 plugin. *)
+
+(** {5 Generic arguments} *)
+
+val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
diff --git a/tac2intern.ml b/tac2intern.ml
index 23f8325da8..bc15b567d4 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -1054,3 +1054,20 @@ let subst_quant_typedef subst (prm, def as qdef) =
 let subst_type_scheme subst (prm, t as sch) =
   let t' = subst_type subst t in
   if t' == t then sch else (prm, t')
+
+(** Registering *)
+
+let () =
+  let open Genintern in
+  let intern ist tac =
+    let env = match Genintern.Store.get ist.extra ltac2_env with
+    | None -> empty_env ()
+    | Some env -> env
+    in
+    let loc = loc_of_tacexpr tac in
+    let (tac, t) = intern_rec env tac in
+    let () = check_elt_unit loc env t in
+    (ist, tac)
+  in
+  Genintern.register_intern0 wit_ltac2 intern
+let () = Genintern.register_subst0 wit_ltac2 subst_expr
-- 
cgit v1.2.3