aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/genarg.ml')
-rw-r--r--lib/genarg.ml288
1 files changed, 196 insertions, 92 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 5efb07444..030797da9 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,12 +9,13 @@
open Pp
open Util
-module Dyn = Dyn.Make(struct end)
+module ValT = Dyn.Make(struct end)
+module ArgT = Dyn.Make(struct end)
module Val =
struct
- type 'a typ = 'a Dyn.tag
+ type 'a typ = 'a ValT.tag
type _ tag =
| Base : 'a typ -> 'a tag
@@ -26,7 +27,7 @@ struct
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 -> Dyn.eq t1 t2
+ | Base t1, Base t2 -> ValT.eq t1 t2
| List t1, List t2 ->
begin match eq t1 t2 with
| None -> None
@@ -48,7 +49,7 @@ struct
| _ -> None
let rec repr : type a. a tag -> std_ppcmds = function
- | Base t -> str (Dyn.repr t)
+ | Base t -> str (ValT.repr t)
| List t -> repr t ++ spc () ++ str "list"
| Opt t -> repr t ++ spc () ++ str "option"
| Pair (t1, t2) -> str "(" ++ repr t1 ++ str " * " ++ repr t2 ++ str ")"
@@ -78,58 +79,147 @@ let rec pr_argument_type = function
str "*" ++ spc () ++ pr_argument_type t2 ++ str ")"
| ExtraArgType s -> str s
-type ('raw, 'glob, 'top) genarg_type = argument_type
+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
+| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
+ ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
+
+let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2.
+ (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type ->
+ (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option =
+fun t1 t2 -> match t1, t2 with
+| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2
+| ListArg t1, ListArg t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| OptArg t1, OptArg t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| PairArg (t1, u1), PairArg (t2, u2) ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl ->
+ match genarg_type_eq u1 u2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| _ -> None
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision *)
(* Dynamics but tagged by a type expression *)
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
+
+type _ level =
+| Rlevel : rlevel level
+| Glevel : glevel level
+| Tlevel : tlevel level
+
+type (_, _) abstract_argument_type =
+| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
+| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
+| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
+
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
-type 'a generic_argument = argument_type * Obj.t
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
-let rawwit t = t
-let glbwit t = t
-let topwit t = t
+let rawwit t = Rawwit t
+let glbwit t = Glbwit t
+let topwit t = Topwit t
-let wit_list t = ListArgType t
+let wit_list t = ListArg t
-let wit_opt t = OptArgType t
+let wit_opt t = OptArg t
-let wit_pair t1 t2 = PairArgType (t1,t2)
+let wit_pair t1 t2 = PairArg (t1, t2)
-let in_gen t o = (t,Obj.repr o)
-let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
-let genarg_tag (s,_) = s
+let in_gen t o = GenArg (t, o)
-let has_type (t, v) u = argument_type_eq t u
+let abstract_argument_type_eq :
+ type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option =
+ fun t1 t2 -> match t1, t2 with
+ | Rawwit t1, Rawwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+ | Glbwit t1, Glbwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+ | Topwit t1, Topwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+
+let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a =
+ let GenArg (t', v) = o in
+ match abstract_argument_type_eq t t' with
+ | None -> failwith "out_gen"
+ | Some Refl -> v
+
+let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
+| None -> false
+| Some _ -> true
-let unquote x = x
+let rec untype : type a b c. (a, b, c) genarg_type -> argument_type = function
+| ExtraArg t -> ExtraArgType (ArgT.repr t)
+| ListArg t -> ListArgType (untype t)
+| OptArg t -> OptArgType (untype t)
+| PairArg (t1, t2) -> PairArgType (untype t1, untype t2)
+
+let unquote : type l. (_, l) abstract_argument_type -> _ = function
+| Rawwit t -> untype t
+| Glbwit t -> untype t
+| Topwit t -> untype t
+
+let genarg_tag (GenArg (t, _)) = unquote t
-type ('a,'b) abstract_argument_type = argument_type
type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
-let arg_list wit = ListArgType wit
-let arg_opt wit = OptArgType wit
+let arg_list : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function
+| Rawwit t -> Rawwit (ListArg t)
+| Glbwit t -> Glbwit (ListArg t)
+| Topwit t -> Topwit (ListArg t)
-type ('a, 'b, 'c, 'l) cast = Obj.t
+let arg_opt : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function
+| Rawwit t -> Rawwit (OptArg t)
+| Glbwit t -> Glbwit (OptArg t)
+| Topwit t -> Topwit (OptArg t)
-let raw = Obj.obj
-let glb = Obj.obj
-let top = Obj.obj
+type ('a, 'b, 'c, 'l) cast =
+| Rcast : 'a -> ('a, 'b, 'c, rlevel) cast
+| Gcast : 'b -> ('a, 'b, 'c, glevel) cast
+| Tcast : 'c -> ('a, 'b, 'c, tlevel) cast
+
+let raw : ('a, 'b, 'c, rlevel) cast -> _ = function Rcast x -> x
+let glb : ('a, 'b, 'c, glevel) cast -> _ = function Gcast x -> x
+let top : ('a, 'b, 'c, tlevel) cast -> _ = function Tcast x -> x
type ('r, 'l) unpacker =
{ unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj)
+let unpack (type l) (pack : (_, l) unpacker) (GenArg (t, obj) : l generic_argument) = match t with
+| Rawwit t -> pack.unpacker t (Rcast obj)
+| Glbwit t -> pack.unpacker t (Gcast obj)
+| Topwit t -> pack.unpacker t (Tcast obj)
(** Type transformers *)
@@ -137,16 +227,20 @@ type ('r, 'l) list_unpacker =
{ list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
('a list, 'b list, 'c list, 'l) cast -> 'r }
-let list_unpack pack (t, obj) = match t with
-| ListArgType t -> pack.list_unpacker t (Obj.obj obj)
+let list_unpack (type l) (pack : (_, l) list_unpacker) (GenArg (t, obj) : l generic_argument) = match t with
+| Rawwit (ListArg t) -> pack.list_unpacker t (Rcast obj)
+| Glbwit (ListArg t) -> pack.list_unpacker t (Gcast obj)
+| Topwit (ListArg t) -> pack.list_unpacker t (Tcast obj)
| _ -> failwith "out_gen"
type ('r, 'l) opt_unpacker =
{ opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
('a option, 'b option, 'c option, 'l) cast -> 'r }
-let opt_unpack pack (t, obj) = match t with
-| OptArgType t -> pack.opt_unpacker t (Obj.obj obj)
+let opt_unpack (type l) (pack : (_, l) opt_unpacker) (GenArg (t, obj) : l generic_argument) = match t with
+| Rawwit (OptArg t) -> pack.opt_unpacker t (Rcast obj)
+| Glbwit (OptArg t) -> pack.opt_unpacker t (Gcast obj)
+| Topwit (OptArg t) -> pack.opt_unpacker t (Tcast obj)
| _ -> failwith "out_gen"
type ('r, 'l) pair_unpacker =
@@ -154,52 +248,60 @@ type ('r, 'l) pair_unpacker =
('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
(('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r }
-let pair_unpack pack (t, obj) = match t with
-| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj)
+let pair_unpack (type l) (pack : (_, l) pair_unpacker) (GenArg (t, obj) : l generic_argument) = match t with
+| Rawwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Rcast obj)
+| Glbwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Gcast obj)
+| Topwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Tcast obj)
| _ -> failwith "out_gen"
(** Creating args *)
-type load = {
- nil : Obj.t option;
- dyn : Obj.t Val.tag;
+module type Param = sig type ('raw, 'glb, 'top) t end
+module ArgMap(M : Param) =
+struct
+ type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack
+ include ArgT.Map(struct type 'a t = 'a pack end)
+end
+
+type ('raw, 'glb, 'top) load = {
+ nil : 'raw option;
+ dyn : 'top Val.tag;
}
-let (arg0_map : load String.Map.t ref) = ref String.Map.empty
+module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
-let cast_tag : 'a Val.tag -> 'b Val.tag = Obj.magic
+let arg0_map = ref LoadMap.empty
let create_arg opt ?dyn name =
- if String.Map.mem name !arg0_map then
+ match ArgT.name name with
+ | Some _ ->
Errors.anomaly (str "generic argument already declared: " ++ str name)
- else
- let dyn = match dyn with None -> Val.Base (Dyn.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
+ | None ->
+ let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
+ let obj = LoadMap.Pack { nil = opt; 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 default_empty_value t =
- let rec aux = function
- | ListArgType _ -> Some (Obj.repr [])
- | OptArgType _ -> Some (Obj.repr None)
- | PairArgType(t1, t2) ->
- (match aux t1, aux t2 with
- | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
- | _ -> None)
- | ExtraArgType s ->
- (String.Map.find s !arg0_map).nil
- in
- match aux t with
- | Some v -> Some (Obj.obj v)
- | None -> None
+let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function
+| ListArg _ -> Some []
+| OptArg _ -> Some None
+| PairArg (t1, t2) ->
+ begin match default_empty_value t1, default_empty_value t2 with
+ | Some v1, Some v2 -> Some (v1, v2)
+ | _ -> None
+ end
+| ExtraArg s ->
+ match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil
-let rec val_tag = function
-| ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn
-| ListArgType t -> cast_tag (Val.List (val_tag t))
-| OptArgType t -> cast_tag (Val.Opt (val_tag t))
-| PairArgType (t1, t2) -> cast_tag (Val.Pair (val_tag t1, val_tag t2))
+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
exception CastError of argument_type * Val.t
@@ -210,39 +312,42 @@ let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
| Some Refl -> Some x
let try_prj wit v = match prj (val_tag wit) v with
-| None -> raise (CastError (wit, v))
+| None -> raise (CastError (untype wit, v))
| Some x -> x
-let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a =
-fun wit v -> match unquote wit with
-| ExtraArgType _ -> try_prj wit v
-| ListArgType t ->
+let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c =
+fun wit v -> match wit with
+| ExtraArg _ -> try_prj wit v
+| ListArg t ->
let Val.Dyn (tag, v) = v in
begin match tag with
| Val.List tag ->
let map x = val_cast t (Val.Dyn (tag, x)) in
- Obj.magic (List.map map v)
- | _ -> raise (CastError (wit, Val.Dyn (tag, v)))
+ List.map map v
+ | _ -> raise (CastError (untype wit, Val.Dyn (tag, v)))
end
-| OptArgType t ->
+| OptArg t ->
let Val.Dyn (tag, v) = v in
begin match tag with
| Val.Opt tag ->
let map x = val_cast t (Val.Dyn (tag, x)) in
- Obj.magic (Option.map map v)
- | _ -> raise (CastError (wit, Val.Dyn (tag, v)))
+ Option.map map v
+ | _ -> raise (CastError (untype wit, Val.Dyn (tag, v)))
end
-| PairArgType (t1, t2) ->
+| PairArg (t1, t2) ->
let Val.Dyn (tag, v) = v in
begin match tag with
| Val.Pair (tag1, tag2) ->
let (v1, v2) = v in
let v1 = Val.Dyn (tag1, v1) in
let v2 = Val.Dyn (tag2, v2) in
- Obj.magic (val_cast t1 v1, val_cast t2 v2)
- | _ -> raise (CastError (wit, Val.Dyn (tag, v)))
+ (val_cast t1 v1, val_cast t2 v2)
+ | _ -> raise (CastError (untype wit, Val.Dyn (tag, v)))
end
+let val_tag = function Topwit t -> val_tag t
+let val_cast = function Topwit t -> val_cast t
+
(** Registering genarg-manipulating functions *)
module type GenObj =
@@ -254,30 +359,31 @@ end
module Register (M : GenObj) =
struct
- let arg0_map =
- ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t)
+ module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
+ let arg0_map = ref GenMap.empty
let register0 arg f = match arg with
- | ExtraArgType s ->
- if String.Map.mem s !arg0_map then
- let msg = str M.name ++ str " function already registered: " ++ str s in
+ | ExtraArg s ->
+ if GenMap.mem s !arg0_map then
+ let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
Errors.anomaly msg
else
- arg0_map := String.Map.add s (Obj.magic f) !arg0_map
+ arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
| _ -> assert false
let get_obj0 name =
- try String.Map.find name !arg0_map
+ try
+ let GenMap.Pack obj = GenMap.find name !arg0_map in obj
with Not_found ->
- match M.default (ExtraArgType name) with
+ match M.default (ExtraArg name) with
| None ->
- Errors.anomaly (str M.name ++ str " function not found: " ++ str name)
+ Errors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
| Some obj -> obj
(** For now, the following function is quite dummy and should only be applied
to an extra argument type, otherwise, it will badly fail. *)
let obj t = match t with
- | ExtraArgType s -> Obj.magic (get_obj0 s)
+ | ExtraArg s -> get_obj0 s
| _ -> assert false
end
@@ -285,12 +391,10 @@ end
(** Hackish part *)
let arg0_names = ref (String.Map.empty : string String.Map.t)
-(** We use this table to associate a name to a given witness, to use it with
- the extension mechanism. This is REALLY ad-hoc, but I do not know how to
- do so nicely either. *)
-
+
let register_name0 t name = match t with
-| ExtraArgType s ->
+| ExtraArg s ->
+ let s = ArgT.repr s in
let () = assert (not (String.Map.mem s !arg0_names)) in
arg0_names := String.Map.add s name !arg0_names
| _ -> failwith "register_name0"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 10:45:38 +0000