Embedding generic arguments in Ltac2 AST.

5 files changed, 56 insertions, 3 deletions

diff --git a/tac2env.ml b/tac2env.ml
index d17e657516..3500b2ef3d 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -52,7 +52,7 @@ let rec eval_pure = function
 | GTacCst (_, n, []) -> ValInt n
 | GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
 | GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _
-| GTacApp _ | GTacCse _ | GTacPrm _ ->
+| GTacApp _ | GTacCse _ | GTacPrm _ | GTacExt _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 
 let define_global kn e =
@@ -137,3 +137,20 @@ let locate_type qid =
 let locate_extended_all_type qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_type
+
+type 'a ml_object = {
+  ml_type : type_constant;
+  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+}
+
+module MLTypeObj =
+struct
+  type ('a, 'b, 'c) obj = 'b ml_object
+  let name = "ltac2_ml_type"
+  let default _ = None
+end
+
+module MLType = Genarg.Register(MLTypeObj)
+
+let define_ml_object t tpe = MLType.register0 t tpe
+let interp_ml_object t = MLType.obj t
diff --git a/tac2env.mli b/tac2env.mli
index efabdb5466..eb471b9abf 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -56,3 +56,13 @@ val locate_extended_all_type : qualid -> type_constant list
 
 val define_primitive : ml_tactic_name -> ml_tactic -> unit
 val interp_primitive : ml_tactic_name -> ml_tactic
+
+(** {5 ML primitive types} *)
+
+type 'a ml_object = {
+  ml_type : type_constant;
+  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+}
+
+val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit
+val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
diff --git a/tac2expr.mli b/tac2expr.mli
index 445c69aa23..15c630ca87 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -76,6 +76,7 @@ type raw_tacexpr =
 | CTacCnv of Loc.t * raw_tacexpr * raw_typexpr
 | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
 | CTacCse of Loc.t * raw_tacexpr * raw_taccase list
+| CTacExt of Loc.t * raw_generic_argument
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
@@ -94,6 +95,7 @@ type glb_tacexpr =
 | GTacArr of glb_tacexpr list
 | GTacCst of KerName.t * int * glb_tacexpr list
 | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
+| GTacExt of glob_generic_argument
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
 (** Toplevel statements *)
@@ -134,3 +136,5 @@ and closure = {
 }
 
 type ml_tactic = valexpr list -> valexpr Proofview.tactic
+
+type environment = valexpr Id.Map.t
diff --git a/tac2intern.ml b/tac2intern.ml
index b1b35b0787..516690dfd3 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -144,6 +144,9 @@ let empty_env () = {
   env_rec = Id.Map.empty;
 }
 
+let ltac2_env : environment Genintern.Store.field =
+  Genintern.Store.field ()
+
 let fresh_id env = UF.fresh env.env_cst
 
 let get_alias (loc, id) env =
@@ -171,6 +174,7 @@ let loc_of_tacexpr = function
 | CTacCnv (loc, _, _) -> loc
 | CTacSeq (loc, _, _) -> loc
 | CTacCse (loc, _, _) -> loc
+| CTacExt (loc, _) -> loc
 
 let loc_of_patexpr = function
 | CPatAny loc -> loc
@@ -324,12 +328,12 @@ let rec is_value = function
 | GTacCst (kn, n, el) ->
   (** To be a value, a constructor must be immutable *)
   assert false (** TODO *)
-| GTacArr _ | GTacCse _ | GTacPrm _ -> false
+| GTacArr _ | GTacCse _ | GTacExt _ | GTacPrm _ -> false
 
 let is_rec_rhs = function
 | GTacFun _ -> true
 | GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ -> false
-| GTacTup _ | GTacArr _ | GTacPrm _ | GTacCst _ | GTacCse _ -> false
+| GTacTup _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _ | GTacCse _ -> false
 
 let rec fv_type f t accu = match t with
 | GTypVar id -> f id accu
@@ -600,6 +604,17 @@ let rec intern_rec env = function
   (GTacLet (false, [Anonymous, e1], e2), t2)
 | CTacCse (loc, e, pl) ->
   intern_case env loc e pl
+| CTacExt (loc, ext) ->
+  let open Genintern in
+  let GenArg (Rawwit tag, _) = ext in
+  let tpe = 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 (_, ext) = generic_intern ist ext in
+  (GTacExt ext, GTypRef (tpe.ml_type, []))
 
 and intern_let_rec env loc el e =
   let fold accu ((loc, na), _, _) = match na with
@@ -892,6 +907,9 @@ let rec subst_expr subst e = match e with
   let cse1' = Array.map (fun (ids, e) -> (ids, subst_expr subst e)) cse1 in
   let ci' = subst_case_info subst ci in
   GTacCse (subst_expr subst e, ci', cse0', cse1')
+| GTacExt ext ->
+  let ext' = Genintern.generic_substitute subst ext in
+  if ext' == ext then e else GTacExt ext'
 
 let subst_typedef subst e = match e with
 | GTydDef t ->
diff --git a/tac2interp.ml b/tac2interp.ml
index 221f107dc8..b868caf963 100644
--- a/tac2interp.ml
+++ b/tac2interp.ml
@@ -83,6 +83,10 @@ let rec interp ist = function
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   Tac2env.interp_primitive ml el
+| GTacExt e ->
+  let GenArg (Glbwit tag, e) = e in
+  let tpe = Tac2env.interp_ml_object tag in
+  tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e)
 
 and interp_app ist f args = match f with
 | ValCls { clos_env = ist; clos_var = ids; clos_exp = e } ->