From cf02db980ab6fc5e9dc8614400cbe4a0aaad48f4 Mon Sep 17 00:00:00 2001
From: Corentin Leruth <corentin.leruth@gmail.com>
Date: Thu, 24 Aug 2023 07:15:49 +0200
Subject: [PATCH] change meta_map impl to use Type module

---
 src/core/dune        |  27 ++++++++---
 src/core/gen/dune    |   3 +-
 src/core/gen/gen.ml  | 110 +++++++++++++++++++++++++++++++++++++++++++
 src/core/meta_map.ml |  84 ++++++++-------------------------
 4 files changed, 151 insertions(+), 73 deletions(-)

diff --git a/src/core/dune b/src/core/dune
index 2240246..95cc850 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -1,12 +1,25 @@
-
 (library
  (name trace_core)
  (public_name trace.core)
- (synopsis "Lightweight stub for tracing")
-)
+ (synopsis "Lightweight stub for tracing"))
 
 (rule
-  (targets atomic_.ml)
-  (action
-    (with-stdout-to %{targets}
-     (run ./gen/gen.exe --ocaml %{ocaml_version} --atomic))))
+ (targets atomic_.ml)
+ (action
+  (with-stdout-to
+   %{targets}
+   (run ./gen/gen.exe --ocaml %{ocaml_version} --atomic))))
+
+(rule
+ (targets type_.ml)
+ (action
+  (with-stdout-to
+   %{targets}
+   (run ./gen/gen.exe --ocaml %{ocaml_version} --type-ml))))
+
+(rule
+ (targets type_.mli)
+ (action
+  (with-stdout-to
+   %{targets}
+   (run ./gen/gen.exe --ocaml %{ocaml_version} --type-mli))))
diff --git a/src/core/gen/dune b/src/core/gen/dune
index cd463d8..9df6b51 100644
--- a/src/core/gen/dune
+++ b/src/core/gen/dune
@@ -1,3 +1,2 @@
-
 (executable
-  (name gen))
+ (name gen))
diff --git a/src/core/gen/gen.ml b/src/core/gen/gen.ml
index 4485bb6..fee3dfc 100644
--- a/src/core/gen/gen.ml
+++ b/src/core/gen/gen.ml
@@ -45,14 +45,108 @@ let atomic_post_412 = {|
 include Atomic
 |}
 
+let type_ml_pre_510 =
+  {|
+(* Type equality witness *)
+
+type (_, _) eq = Equal: ('a, 'a) eq
+
+(* Type identifiers *)
+
+module Id = struct
+  type _ id = ..
+  module type ID = sig
+    type t
+    type _ id += Id : t id
+  end
+
+  type 'a t = (module ID with type t = 'a)
+
+  let make (type a) () : a t =
+    (module struct type t = a type _ id += Id : t id end)
+
+  let[@inline] uid (type a) ((module A) : a t) =
+    Obj.Extension_constructor.id (Obj.Extension_constructor.of_val A.Id)
+
+  let provably_equal
+      (type a b) ((module A) : a t) ((module B) : b t) : (a, b) eq option
+    =
+    match A.Id with B.Id -> Some Equal | _ -> None
+end
+|}
+
+let type_mli_pre_510 =
+  {|
+type (_, _) eq = Equal: ('a, 'a) eq (** *)
+(** The purpose of [eq] is to represent type equalities that may not otherwise
+    be known by the type checker (e.g. because they may depend on dynamic data).
+
+    A value of type [(a, b) eq] represents the fact that types [a] and [b] are
+    equal.
+
+    If one has a value [eq : (a, b) eq] that proves types [a] and [b] are equal,
+    one can use it to convert a value of type [a] to a value of type [b] by
+    pattern matching on [Equal]:
+    {[
+      let cast (type a) (type b) (Equal : (a, b) Type.eq) (a : a) : b = a
+    ]}
+
+    At runtime, this function simply returns its second argument unchanged.
+*)
+
+(** {1:identifiers Type identifiers} *)
+
+(** Type identifiers.
+
+    A type identifier is a value that denotes a type. Given two type
+    identifiers, they can be tested for {{!Id.provably_equal}equality} to
+    prove they denote the same type. Note that:
+
+    - Unequal identifiers do not imply unequal types: a given type can be
+      denoted by more than one identifier.
+    - Type identifiers can be marshalled, but they get a new, distinct,
+      identity on unmarshalling, so the equalities are lost.
+
+    See an {{!Id.example}example} of use. *)
+module Id : sig
+
+  (** {1:ids Type identifiers} *)
+
+  type 'a t
+  (** The type for identifiers for type ['a]. *)
+
+  val make : unit -> 'a t
+  (** [make ()] is a new type identifier. *)
+
+  val uid : 'a t -> int
+  (** [uid id] is a runtime unique identifier for [id]. *)
+
+  val provably_equal : 'a t -> 'b t -> ('a, 'b) eq option
+  (** [provably_equal i0 i1] is [Some Equal] if identifier [i0] is equal
+      to [i1] and [None] otherwise. *)
+end
+|}
+
+let type_ml_post_510 = {|
+include Type
+|}
+
+let type_mli_post_510 = {|
+include module type of Type
+|}
+
 let p_version s = Scanf.sscanf s "%d.%d" (fun x y -> x, y)
 
 let () =
   let atomic = ref false in
+  let type_ml = ref false in
+  let type_mli = ref false in
   let ocaml = ref Sys.ocaml_version in
   Arg.parse
     [
       "--atomic", Arg.Set atomic, " atomic";
+      "--type-ml", Arg.Set type_ml, " type.ml";
+      "--type-mli", Arg.Set type_mli, " type.mli";
       "--ocaml", Arg.Set_string ocaml, " set ocaml version";
     ]
     ignore "";
@@ -67,4 +161,20 @@ let () =
         atomic_post_412
     in
     print_endline code
+  ) else if !type_ml then (
+    let code =
+      if (major, minor) < (5, 10) then
+        type_ml_pre_510
+      else
+        type_ml_post_510
+    in
+    print_endline code
+  ) else if !type_mli then (
+    let code =
+      if (major, minor) < (5, 10) then
+        type_mli_pre_510
+      else
+        type_mli_post_510
+    in
+    print_endline code
   )
diff --git a/src/core/meta_map.ml b/src/core/meta_map.ml
index b4564c0..9c732a7 100644
--- a/src/core/meta_map.ml
+++ b/src/core/meta_map.ml
@@ -1,83 +1,39 @@
-module type KEY_IMPL = sig
-  type t
-
-  exception Store of t
-
-  val id : int
-end
+module Type = Type_
 
 module Key = struct
-  type 'a t = (module KEY_IMPL with type t = 'a)
+  type 'a t = 'a Type.Id.t
 
-  let _n = ref 0
+  let create = Type.Id.make
+  let id = Type.Id.uid
 
-  let create (type k) () =
-    incr _n;
-    let id = !_n in
-    let module K = struct
-      type t = k
-
-      let id = id
-
-      exception Store of k
-    end in
-    (module K : KEY_IMPL with type t = k)
-
-  let id (type k) (module K : KEY_IMPL with type t = k) = K.id
-
-  let equal : type a b. a t -> b t -> bool =
-   fun (module K1) (module K2) -> K1.id = K2.id
+  let equal a b =
+    match Type.Id.provably_equal a b with
+    | None -> false
+    | Some Type.Equal -> true
 end
 
 type pair = Pair : 'a Key.t * 'a -> pair
-type exn_pair = E_pair : 'a Key.t * exn -> exn_pair
 
-let pair_of_e_pair (E_pair (k, e)) =
-  let module K = (val k) in
-  match e with
-  | K.Store v -> Pair (k, v)
-  | _ -> assert false
+module M = Map.Make (Int)
 
-module M = Map.Make (struct
-  type t = int
-
-  let compare (i : int) j = Stdlib.compare i j
-end)
-
-type t = exn_pair M.t
+type t = pair M.t
 
 let empty = M.empty
 let mem k t = M.mem (Key.id k) t
 
 let find_exn (type a) (k : a Key.t) t : a =
-  let module K = (val k) in
-  let (E_pair (_, e)) = M.find K.id t in
-  match e with
-  | K.Store v -> v
-  | _ -> assert false
+  let (Pair (k', v)) = M.find (Key.id k) t in
+  match Type.Id.provably_equal k k' with
+  | None -> assert false
+  | Some Type.Equal -> v
 
 let find k t = try Some (find_exn k t) with Not_found -> None
-
-let add_e_pair_ p t =
-  let (E_pair ((module K), _)) = p in
-  M.add K.id p t
-
-let add_pair_ p t =
-  let (Pair (((module K) as k), v)) = p in
-  let p = E_pair (k, K.Store v) in
-  M.add K.id p t
-
-let add (type a) (k : a Key.t) v t =
-  let module K = (val k) in
-  add_e_pair_ (E_pair (k, K.Store v)) t
-
-let remove (type a) (k : a Key.t) t =
-  let module K = (val k) in
-  M.remove K.id t
-
-let cardinal t = M.cardinal t
+let add k v t = M.add (Key.id k) (Pair (k, v)) t
+let remove k t = M.remove (Key.id k) t
+let cardinal = M.cardinal
 let length = cardinal
-let iter f t = M.iter (fun _ p -> f (pair_of_e_pair p)) t
-let to_list t = M.fold (fun _ p l -> pair_of_e_pair p :: l) t []
+let iter f t = M.iter (fun _ p -> f p) t
+let to_list t = M.fold (fun _ p l -> p :: l) t []
+let add_pair_ (Pair (k, v)) t = add k v t
 let add_list t l = List.fold_right add_pair_ l t
 let of_list l = add_list empty l