From 43c20fa2dc549b33746473215bc7641ea3a0bce3 Mon Sep 17 00:00:00 2001 From: Corentin Leruth Date: Thu, 24 Aug 2023 07:52:25 +0200 Subject: [PATCH] inline module Type instead of generating --- src/core/dune | 14 ------ src/core/gen/gen.ml | 110 ------------------------------------------- src/core/meta_map.ml | 31 +++++++++++- 3 files changed, 30 insertions(+), 125 deletions(-) diff --git a/src/core/dune b/src/core/dune index 95cc850..6966d12 100644 --- a/src/core/dune +++ b/src/core/dune @@ -9,17 +9,3 @@ (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/gen.ml b/src/core/gen/gen.ml index fee3dfc..4485bb6 100644 --- a/src/core/gen/gen.ml +++ b/src/core/gen/gen.ml @@ -45,108 +45,14 @@ 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 ""; @@ -161,20 +67,4 @@ 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 9c732a7..11ceb15 100644 --- a/src/core/meta_map.ml +++ b/src/core/meta_map.ml @@ -1,4 +1,33 @@ -module Type = Type_ +(* Type identifiers, can be deleted once OCaml >= 5.1 is required *) +module Type = struct + type (_, _) eq = Equal : ('a, 'a) eq + + 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 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 + + let uid (type a) ((module A) : a t) = + Obj.Extension_constructor.id (Obj.Extension_constructor.of_val A.Id) + end +end module Key = struct type 'a t = 'a Type.Id.t