diff options
-rw-r--r-- | lib/genarg.ml | 288 |
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" |