From 2a0feed32c79c06610e69f9c4dcc9aa3e65863db Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 27 Aug 2022 20:48:32 -0400 Subject: [PATCH] format --- src/smt/registry.ml | 55 ++++++++++++++++++++++---------------------- src/smt/registry.mli | 16 ++++++------- 2 files changed, 35 insertions(+), 36 deletions(-) diff --git a/src/smt/registry.ml b/src/smt/registry.ml index f2450d1b..1a66b948 100644 --- a/src/smt/registry.ml +++ b/src/smt/registry.ml @@ -1,37 +1,38 @@ +(* registry keys *) +module type KEY = sig + type elt - (* registry keys *) - module type KEY = sig - type elt + val id : int - val id : int + exception E of elt +end - exception E of elt - end +type 'a key = (module KEY with type elt = 'a) +type t = { tbl: exn Util.Int_tbl.t } [@@unboxed] - type 'a key = (module KEY with type elt = 'a) - type t = { tbl: exn Util.Int_tbl.t } [@@unboxed] +let create () : t = { tbl = Util.Int_tbl.create 8 } - let create () : t = { tbl = Util.Int_tbl.create 8 } - let n_ = ref 0 +(* TODO: use atomic *) +let n_ = ref 0 - let create_key (type a) () : a key = - let id = !n_ in - incr n_; - let module K = struct - type elt = a +let create_key (type a) () : a key = + let id = !n_ in + incr n_; + let module K = struct + type elt = a - exception E of a + exception E of a - let id = id - end in - (module K) + let id = id + end in + (module K) - let get (type a) (self : t) (k : a key) : _ option = - let (module K : KEY with type elt = a) = k in - match Util.Int_tbl.get self.tbl K.id with - | Some (K.E x) -> Some x - | _ -> None +let get (type a) (self : t) (k : a key) : _ option = + let (module K : KEY with type elt = a) = k in + match Util.Int_tbl.get self.tbl K.id with + | Some (K.E x) -> Some x + | _ -> None - let set (type a) (self : t) (k : a key) (v : a) : unit = - let (module K) = k in - Util.Int_tbl.replace self.tbl K.id (K.E v) +let set (type a) (self : t) (k : a key) (v : a) : unit = + let (module K) = k in + Util.Int_tbl.replace self.tbl K.id (K.E v) diff --git a/src/smt/registry.mli b/src/smt/registry.mli index 0e41bcac..5e41d5bb 100644 --- a/src/smt/registry.mli +++ b/src/smt/registry.mli @@ -1,14 +1,12 @@ - - (** Registry to extract values *) - type t - type 'a key +type t +type 'a key - val create_key : unit -> 'a key - (** Call this statically, typically at program initialization, for +val create_key : unit -> 'a key +(** Call this statically, typically at program initialization, for each distinct key. *) - val create : unit -> t - val get : t -> 'a key -> 'a option - val set : t -> 'a key -> 'a -> unit +val create : unit -> t +val get : t -> 'a key -> 'a option +val set : t -> 'a key -> 'a -> unit