Allowing complex types in ML objects.

4 files changed, 29 insertions, 23 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 81388af0ef..b8bec37d04 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -775,9 +775,11 @@ let to_lvar ist =
   let lfun = Tac2interp.set_env ist Id.Map.empty in
   { empty_lvar with Glob_term.ltac_genargs = lfun }
 
-let intern_constr ist c =
+let gtypref kn = GTypRef (Other kn, [])
+
+let intern_constr self ist c =
   let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in
-  c
+  (c, gtypref t_constr)
 
 let interp_constr flags ist c =
   let open Pretyping in
@@ -796,7 +798,6 @@ let () =
   let interp ist c = interp_constr (constr_flags ()) ist c in
   let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
   let obj = {
-    ml_type = t_constr;
     ml_intern = intern;
     ml_subst = Detyping.subst_glob_constr;
     ml_interp = interp;
@@ -809,7 +810,6 @@ let () =
   let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
   let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in
   let obj = {
-    ml_type = t_constr;
     ml_intern = intern;
     ml_subst = Detyping.subst_glob_constr;
     ml_interp = interp;
@@ -821,8 +821,7 @@ let () =
   let interp _ id = return (ValExt (Value.val_ident, id)) in
   let print _ id = str "ident:(" ++ Id.print id ++ str ")" in
   let obj = {
-    ml_type = t_ident;
-    ml_intern = (fun _ id -> id);
+    ml_intern = (fun _ _ id -> id, gtypref t_ident);
     ml_interp = interp;
     ml_subst = (fun _ id -> id);
     ml_print = print;
@@ -830,14 +829,13 @@ let () =
   define_ml_object Tac2env.wit_ident obj
 
 let () =
-  let intern ist c =
+  let intern self ist c =
     let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in
-    pat
+    pat, gtypref t_pattern
   in
   let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
   let interp _ c = return (ValExt (Value.val_pattern, c)) in
   let obj = {
-    ml_type = t_pattern;
     ml_intern = intern;
     ml_interp = interp;
     ml_subst = Patternops.subst_pattern;
@@ -846,15 +844,16 @@ let () =
   define_ml_object Tac2env.wit_pattern obj
 
 let () =
-  let intern ist qid = match qid with
-  | Libnames.Ident (_, id) -> Globnames.VarRef id
+  let intern self ist qid = match qid with
+  | Libnames.Ident (_, id) ->
+    Globnames.VarRef id, gtypref t_reference
   | Libnames.Qualid (loc, qid) ->
     let gr =
       try Nametab.locate qid
       with Not_found ->
         Nametab.error_global_not_found ?loc qid
     in
-    gr
+    gr, gtypref t_reference
   in
   let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
@@ -863,7 +862,6 @@ let () =
   | r -> str "reference:(" ++ Printer.pr_global r ++ str ")"
   in
   let obj = {
-    ml_type = t_reference;
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
@@ -872,12 +870,12 @@ let () =
   define_ml_object Tac2env.wit_reference obj
 
 let () =
-  let intern ist tac =
+  let intern self ist tac =
     (** Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ist = { ist with Genintern.extra } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    tac
+    tac, gtypref t_unit
   in
   let interp _ tac =
     (** FUCK YOU API *)
@@ -889,7 +887,6 @@ let () =
     str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic (Obj.magic env) tac ++ str ")"
   in
   let obj = {
-    ml_type = t_unit;
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 489113c031..56fd55ee84 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -251,9 +251,10 @@ let shortest_qualid_of_projection kn =
   let sp = KNmap.find kn tab.tab_proj_rev in
   KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
 
+type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
+
 type ('a, 'b) ml_object = {
-  ml_type : type_constant;
-  ml_intern : Genintern.glob_sign -> 'a -> 'b;
+  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> 'b -> Pp.t;
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 0ef62d67ed..15664db756 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -105,9 +105,10 @@ val interp_primitive : ml_tactic_name -> ml_tactic
 
 (** {5 ML primitive types} *)
 
+type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
+
 type ('a, 'b) ml_object = {
-  ml_type : type_constant;
-  ml_intern : Genintern.glob_sign -> 'a -> 'b;
+  ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> 'b -> Pp.t;
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 490436422d..5d2fc2b47b 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -775,14 +775,21 @@ let rec intern_rec env = function
   (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (Tuple 0, []))
 | CTacExt (loc, tag, arg) ->
   let open Genintern in
-  let tpe = interp_ml_object tag in
+  let self ist e =
+    let env = match Store.get ist.extra ltac2_env with
+    | None -> empty_env ()
+    | Some env -> env
+    in
+    intern_rec env e
+  in
+  let obj = interp_ml_object tag in
   (** External objects do not have access to the named context because this is
       not stable by dynamic semantics. *)
   let genv = Global.env_of_context Environ.empty_named_context_val in
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
-  let arg = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> tpe.ml_intern ist arg) () in
-  (GTacExt (tag, arg), GTypRef (Other tpe.ml_type, []))
+  let arg, tpe = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> obj.ml_intern self ist arg) () in
+  (GTacExt (tag, arg), tpe)
 
 and intern_rec_with_constraint env e exp =
   let loc = loc_of_tacexpr e in