Moving the Val module to Geninterp.

2 files changed, 4 insertions, 92 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3ff9afa601..69408fb1a5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,7 +9,6 @@
 open Pp
 open Util
 
-module ValT = Dyn.Make(struct end)
 module ArgT =
 struct
   module DYN = Dyn.Make(struct end)
@@ -25,37 +24,6 @@ struct
     Some (Any (Obj.magic t)) (** All created tags are made of triples *)
 end
 
-module Val =
-struct
-
-  type 'a typ = 'a ValT.tag
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a typ * 'a -> t
-
-  let eq = ValT.eq
-  let repr = ValT.repr
-
-  let rec pr : type a. a typ -> std_ppcmds = fun t -> str (repr t)
-
-  let list_tag = ValT.create "list"
-  let opt_tag = ValT.create "option"
-  let pair_tag = ValT.create "pair"
-
-  let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
-  | Base t -> Dyn (t, x)
-  | List tag -> Dyn (list_tag, List.map (fun x -> inject tag x) x)
-  | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x)
-  | Pair (tag1, tag2) ->
-    Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x)))
-
-end
-
 type (_, _, _) genarg_type =
 | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
 | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
@@ -187,36 +155,14 @@ struct
   include ArgT.Map(struct type 'a t = 'a pack end)
 end
 
-type ('raw, 'glb, 'top) load = {
-  dyn : 'top Val.tag;
-}
-
-module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
-
-let arg0_map = ref LoadMap.empty
-
-let create_arg ?dyn name =
+let create_arg name =
   match ArgT.name name with
+  | None -> ExtraArg (ArgT.create name)
   | Some _ ->
     Errors.anomaly (str "generic argument already declared: " ++ str name)
-  | None ->
-    let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
-    let obj = LoadMap.Pack { dyn; } in
-    let name = ArgT.create name in
-    let () = arg0_map := LoadMap.add name obj !arg0_map in
-    ExtraArg name
 
 let make0 = create_arg
 
-let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
-| ListArg t -> Val.List (val_tag t)
-| OptArg t -> Val.Opt (val_tag t)
-| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
-| ExtraArg s ->
-  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn
-
-let val_tag = function Topwit t -> val_tag t
-
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 04113ae289..b8bb6af04a 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -86,42 +86,14 @@ type (_, _, _) genarg_type =
 (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
     one, and ['top] the internalized one. *)
 
-module Val :
-sig
-  type 'a typ
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a typ * 'a -> t
-
-  val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
-  val repr : 'a typ -> string
-  val pr : 'a typ -> Pp.std_ppcmds
-
-  val list_tag : t list typ
-  val opt_tag : t option typ
-  val pair_tag : (t * t) typ
-
-  val inject : 'a tag -> 'a -> t
-
-end
-(** 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 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : 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 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -186,12 +158,6 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
-(** {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. *)
-
 (** {6 Type reification} *)
 
 type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type