From 93771ae6715bdc6acde9b0b7b8e4947a635defe9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 7 Jul 2020 16:18:13 +0200 Subject: [PATCH] [server] Data: fixes the signature of functors for indexed values. These functors only require a 'kind' string. --- src/plugins/server/data.ml | 18 +++++++++++------- src/plugins/server/data.mli | 15 +++++++++------ 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml index f1a17dc67cf..c75c1b63d7c 100644 --- a/src/plugins/server/data.ml +++ b/src/plugins/server/data.ml @@ -565,6 +565,11 @@ end (* --- Index --- *) (* -------------------------------------------------------------------------- *) +module type Info = +sig + val kind: string +end + (** Simplified [Map.S] *) module type Map = sig @@ -584,7 +589,7 @@ sig val clear : unit -> unit end -module INDEXER(M : Map)(D : S)(I : Index with type t = D.t) : +module INDEXER(M : Map)(I : Info) : sig type index val create : unit -> index @@ -634,10 +639,10 @@ struct end -module Static(M : Map)(S : S)(I : Index with type t = S.t) +module Static(M : Map)(I : Info) : Index with type t = M.key = struct - module INDEX = INDEXER(M)(S)(I) + module INDEX = INDEXER(M)(I) let kind = I.kind let index = INDEX.create () let clear () = INDEX.clear index @@ -652,10 +657,10 @@ struct end) end -module Index(M : Map)(S : S)(I : Index with type t = S.t) +module Index(M : Map)(I : Info) : Index with type t = M.key = struct - module INDEX = INDEXER(M)(S)(I) + module INDEX = INDEXER(M)(I) module TYPE : Datatype.S with type t = INDEX.index = Datatype.Make (struct @@ -695,8 +700,7 @@ sig val id : t -> int end -module Identified(A : IdentifiedType)(S : S) - (I : Index with type t = S.t) : Index with type t = A.t = +module Identified(A : IdentifiedType)(I : Info) : Index with type t = A.t = struct type index = (int,A.t) Hashtbl.t diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli index 6ba578402a2..a86c1f14888 100644 --- a/src/plugins/server/data.mli +++ b/src/plugins/server/data.mli @@ -323,6 +323,12 @@ end *) (* -------------------------------------------------------------------------- *) +(** Datatype information. *) +module type Info = +sig + val kind: string +end + (** Simplified [Map.S]. *) module type Map = sig @@ -345,12 +351,10 @@ sig end (** Builds an indexer that {i does not} depend on current project. *) -module Static(M : Map)(S : S) - (I : Index with type t = S.t) : Index with type t = M.key +module Static(M : Map)(I : Info) : Index with type t = M.key (** Builds a {i projectified} index. *) -module Index(M : Map)(S : S) - (I : Index with type t = S.t) : Index with type t = M.key +module Index(M : Map)(I : Info) : Index with type t = M.key (** Datatype already identified by unique integers. *) module type IdentifiedType = @@ -360,8 +364,7 @@ sig end (** Builds a {i projectified} index on types with {i unique} identifiers. *) -module Identified(A : IdentifiedType)(S : S) - (I : Index with type t = S.t) : Index with type t = A.t +module Identified(A : IdentifiedType)(I : Info) : Index with type t = A.t (* -------------------------------------------------------------------------- *) (** {2 Error handling} -- GitLab