Attaching a dynamic argument to the toplevel type of generic arguments.

2 files changed, 60 insertions, 6 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 8712eda8e..b6a2849ad 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,6 +9,8 @@
 open Pp
 open Util
 
+module Val = Dyn.Make(struct end)
+
 type argument_type =
   (* Basic types *)
   | IntOrVarArgType
@@ -133,13 +135,22 @@ let pair_unpack pack (t, obj) = match t with
 
 (** Creating args *)
 
-let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
+type load = {
+  nil : Obj.t option;
+  dyn : Obj.t Val.tag;
+}
+
+let (arg0_map : load String.Map.t ref) = ref String.Map.empty
 
-let create_arg opt name =
+let cast_tag : 'a Val.tag -> 'b Val.tag = Obj.magic
+
+let create_arg opt ?dyn name =
   if String.Map.mem name !arg0_map then
     Errors.anomaly (str "generic argument already declared: " ++ str name)
   else
-    let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in
+    let dyn = match dyn with None -> Val.create name | Some dyn -> cast_tag dyn in
+    let obj = { nil = Option.map Obj.repr opt; dyn; } in
+    let () = arg0_map := String.Map.add name obj !arg0_map in
     ExtraArgType name
 
 let make0 = create_arg
@@ -153,12 +164,39 @@ let default_empty_value t =
       | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
       | _ -> None)
   | ExtraArgType s ->
-    String.Map.find s !arg0_map
+    (String.Map.find s !arg0_map).nil
   | _ -> None in
   match aux t with
   | Some v -> Some (Obj.obj v)
   | None -> None
 
+(** Beware: keep in sync with the corresponding types *)
+let int_or_var_T = Val.create "int_or_var"
+let ident_T = Val.create "ident"
+let var_T = Val.create "var"
+let genarg_T = Val.create "genarg"
+let constr_T = Val.create "constr"
+let constr_may_eval_T = Val.create "constr_may_eval"
+let open_constr_T = Val.create "open_constr"
+
+let option_val = Val.create "option"
+let list_val = Val.create "list"
+let pair_val = Val.create "pair"
+
+let val_tag = function
+| IntOrVarArgType -> cast_tag int_or_var_T
+| IdentArgType -> cast_tag ident_T
+| VarArgType -> cast_tag var_T
+| GenArgType -> cast_tag genarg_T
+| ConstrArgType -> cast_tag constr_T
+| ConstrMayEvalArgType -> cast_tag constr_may_eval_T
+| OpenConstrArgType -> cast_tag open_constr_T
+| ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn
+(** Recursive types have no associated dynamic tag *)
+| ListArgType t -> assert false
+| OptArgType t -> assert false
+| PairArgType (t1, t2) -> assert false
+
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 2dcaa789f..d52a24610 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -72,14 +72,20 @@ type ('raw, 'glob, 'top) genarg_type
 (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
     one, and ['top] the internalized one. *)
 
+module Val : Dyn.S
+(** Dynamic types for toplevel values. While the generic types permit to relate
+    objects at various levels of interpretation, toplevel values are wearing
+    their own type regardless of where they came from. This allows to use the
+    same runtime representation for several generic types. *)
+
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -179,6 +185,16 @@ type ('r, 'l) pair_unpacker =
 
 val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
 
+(** {6 Dynamic toplevel values} *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. Only works for
+    ground generic arguments. *)
+
+val option_val : Val.t option Val.tag
+val list_val : Val.t list Val.tag
+val pair_val : (Val.t * Val.t) Val.tag
+
 (** {6 Type reification} *)
 
 type argument_type =