diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/genarg.ml | 73 | ||||
| -rw-r--r-- | lib/genarg.mli | 32 |
2 files changed, 4 insertions, 101 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index ef0de89af..69408fb1a 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,52 +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 tag * 'a -> t - - let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option = - fun t1 t2 -> match t1, t2 with - | Base t1, Base t2 -> ValT.eq t1 t2 - | List t1, List t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Opt t1, Opt t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Pair (t1, u1), Pair (t2, u2) -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> - match eq u1 u2 with - | None -> None - | Some Refl -> Some Refl - end - | _ -> None - - let repr = ValT.repr - - let rec pr : type a. a tag -> std_ppcmds = function - | Base t -> str (repr t) - | List t -> pr t ++ spc () ++ str "list" - | Opt t -> pr t ++ spc () ++ str "option" - | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")" - -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 @@ -202,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 93665fd45..b8bb6af04 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -86,36 +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 tag * 'a -> t - - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option - val repr : 'a typ -> string - val pr : 'a tag -> Pp.std_ppcmds - -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} *) @@ -180,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 |