Leveraging GADTs to provide a better Dyn API.

5 files changed, 22 insertions, 24 deletions

diff --git a/lib/cSig.mli b/lib/cSig.mli
index 4463e8d9c6..796e58cbfb 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b
 type 'a until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
+type (_, _) eq = Refl : ('a, 'a) eq
+
 module type SetS =
 sig
     type elt
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 60167ef1ba..0571f3b5d6 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -11,12 +11,12 @@ open Pp
 
 module type S =
 sig
-type t
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
 
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
 val dump : unit -> (int * string) list
 end
 
@@ -24,7 +24,9 @@ module Make(M : CSig.EmptyS) =
 struct
 (* Dynamics, programmed with DANGER !!! *)
 
-type t = int * Obj.t
+type 'a tag = int
+
+type t = Dyn : 'a tag * 'a -> t
 
 let dyntab = ref (Int.Map.empty : string Int.Map.t)
 (** Instead of working with tags as strings, which are costly, we use their
@@ -41,25 +43,16 @@ let create (s : string) =
       anomaly ~label:"Dyn.create" msg
   in
   let () = dyntab := Int.Map.add hash s !dyntab in
-  let infun v = (hash, Obj.repr v) in
-  let outfun (nh, rv) =
-    if Int.equal hash nh then Obj.magic rv
-    else
-      anomaly (str "dyn_out: expected " ++ str s)
-  in
-  (infun, outfun)
+  hash
 
-let has_tag (s, _) tag =
-  let hash = Hashtbl.hash (tag : string) in
-  Int.equal s hash
+let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+  fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
 
-let tag (s,_) =
+let repr s =
   try Int.Map.find s !dyntab
   with Not_found ->
     anomaly (str "Unknown dynamic tag " ++ int s)
 
-let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
-
 let dump () = Int.Map.bindings !dyntab
 
 end
\ No newline at end of file
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 55c4f0ce8f..28587859e1 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -10,12 +10,12 @@
 
 module type S =
 sig
-type t
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
 
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
 val dump : unit -> (int * string) list
 end
 
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc4..b67539918d 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -124,6 +124,7 @@ let delayed_force f = f ()
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
 
 let map_union f g = function
   | Inl a -> Inl (f a)
diff --git a/lib/util.mli b/lib/util.mli
index 1dc405fcbe..0ce6cc6603 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
 val open_utf8_file_in : string -> in_channel
 (** Open an utf-8 encoded file and skip the byte-order mark if any. *)