diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-31 12:40:56 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-02 11:19:07 +0100 |
commit | 351273dcebb47b66a4e5a1952f3009c5214e03ec (patch) | |
tree | 49ba3300a10640a37957c021dddd38c45cec34ba /lib | |
parent | fb57fefa5f46ba8ad7be98cff81354389d87d402 (diff) |
Naming the type of Dyn.Map for future reuse.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/dyn.ml | 41 | ||||
-rw-r--r-- | lib/dyn.mli | 39 |
2 files changed, 44 insertions, 36 deletions
diff --git a/lib/dyn.ml b/lib/dyn.ml index 6bd43455f..e9f9709cb 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,6 +11,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type PreS = sig type 'a tag @@ -24,24 +44,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list @@ -104,6 +107,8 @@ let dump () = Int.Map.bindings !dyntab module Map(M : TParam) = struct type t = Obj.t M.t Int.Map.t +type 'a obj = 'a M.t +type 'a key = 'a tag let cast : 'a M.t -> 'b M.t = Obj.magic let empty = Int.Map.empty let add tag v m = Int.Map.add tag (cast v) m diff --git a/lib/dyn.mli b/lib/dyn.mli index e43c8a9bc..a2bbd95a7 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -13,6 +13,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type S = sig type 'a tag @@ -26,24 +46,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list |