Reimplementing Genarg safely.

No more Obj.magic in Genarg. We leverage the expressivity of GADT
coupled with dynamic tags to get rid of unsafety. For now the API
did not change in order to port the legacy code more easily.

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"