move to containers 3.0

sidekick.opam

@@ -12,7 +12,7 @@ build: [
 ]
 depends: [
   "dune" {build}
-  "containers" { >= "2.8" & < "3.0" }
+  "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
   "msat" { >= "0.8.2" < "0.9" }
   "ocaml" { >= "4.03" }

src/base-term/Base_types.ml

@@ -811,7 +811,7 @@ end = struct
     match view t with
     | Bool b -> C.Bool b
     | App_fun (f,_) when not (Fun.do_cc f) -> C.Opaque t (* skip *)
-    | App_fun (f,args) -> C.App_fun (f, IArray.to_seq args)
+    | App_fun (f,args) -> C.App_fun (f, IArray.to_iter args)
     | Eq (a,b) -> C.Eq (a, b)
     | Not u -> C.Not u
     | Ite (a,b,c) -> C.If (a,b,c)

src/base-term/CCHet.ml

@@ -0,0 +1,199 @@
+
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Associative containers with Heterogenerous Values} *)
+
+(*$R
+  let k1 : int Key.t = Key.create() in
+  let k2 : int Key.t = Key.create() in
+  let k3 : string Key.t = Key.create() in
+  let k4 : float Key.t = Key.create() in
+
+  let tbl = Tbl.create () in
+
+  Tbl.add tbl k1 1;
+  Tbl.add tbl k2 2;
+  Tbl.add tbl k3 "k3";
+
+  assert_equal (Some 1) (Tbl.find tbl k1);
+  assert_equal (Some 2) (Tbl.find tbl k2);
+  assert_equal (Some "k3") (Tbl.find tbl k3);
+  assert_equal None (Tbl.find tbl k4);
+  assert_equal 3 (Tbl.length tbl);
+
+  Tbl.add tbl k1 10;
+  assert_equal (Some 10) (Tbl.find tbl k1);
+  assert_equal 3 (Tbl.length tbl);
+  assert_equal None (Tbl.find tbl k4);
+
+  Tbl.add tbl k4 0.0;
+  assert_equal (Some 0.0) (Tbl.find tbl k4);
+
+  ()
+
+
+*)
+
+type 'a iter = ('a -> unit) -> unit
+type 'a gen = unit -> 'a option
+
+module type KEY_IMPL = sig
+  type t
+  exception Store of t
+  val id : int
+end
+
+module Key = struct
+  type 'a t = (module KEY_IMPL with type t = 'a)
+
+  let _n = ref 0
+
+  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
+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 Tbl = struct
+  module M = Hashtbl.Make(struct
+      type t = int
+      let equal (i:int) j = i=j
+      let hash (i:int) = Hashtbl.hash i
+    end)
+
+  type t = exn_pair M.t
+
+  let create ?(size=16) () = M.create size
+
+  let mem t k = M.mem t (Key.id k)
+
+  let find_exn (type a) t (k : a Key.t) : a =
+    let module K = (val k) in
+    let E_pair (_, v) = M.find t K.id in
+    match v with
+      | K.Store v -> v
+      | _ -> assert false
+
+  let find t k =
+    try Some (find_exn t k)
+    with Not_found -> None
+
+  let add_pair_ t p =
+    let Pair (k,v) = p in
+    let module K = (val k) in
+    let p = E_pair (k, K.Store v) in
+    M.replace t K.id p
+
+  let add t k v = add_pair_ t (Pair (k,v))
+
+  let remove (type a) t (k:a Key.t) =
+    let module K = (val k) in
+    M.remove t K.id
+
+  let length t = M.length t
+
+  let iter f t = M.iter (fun _ pair -> f (pair_of_e_pair pair)) t
+
+  let to_iter t yield = iter yield t
+
+  let to_list t = M.fold (fun _ p l -> pair_of_e_pair p::l) t []
+
+  let add_list t l = List.iter (add_pair_ t) l
+
+  let add_iter t seq = seq (add_pair_ t)
+
+  let of_list l =
+    let t = create() in
+    add_list t l;
+    t
+
+  let of_iter seq =
+    let t = create() in
+    add_iter t seq;
+    t
+end
+
+module Map = struct
+  module M = Map.Make(struct
+      type t = int
+      let compare (i:int) j = Stdlib.compare i j
+    end)
+
+  type t = exn_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 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 length = cardinal
+
+  let iter f t = M.iter (fun _ p -> f (pair_of_e_pair p)) t
+
+  let to_iter t yield = iter yield t
+
+  let to_list t = M.fold (fun _ p l -> pair_of_e_pair p::l) t []
+
+  let add_list t l = List.fold_right add_pair_ l t
+
+  let add_iter t seq =
+    let t = ref t in
+    seq (fun pair -> t := add_pair_ pair !t);
+    !t
+
+  let of_list l = add_list empty l
+
+  let of_iter seq = add_iter empty seq
+end

src/base-term/CCHet.mli

@@ -0,0 +1,94 @@
+
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Associative containers with Heterogeneous Values}
+
+    This is similar to {!CCMixtbl}, but the injection is directly used as
+    a key.
+
+    @since 0.17 *)
+
+type 'a iter = ('a -> unit) -> unit
+type 'a gen = unit -> 'a option
+
+module Key : sig
+  type 'a t
+
+  val create : unit -> 'a t
+
+  val equal : 'a t -> 'a t -> bool
+  (** Compare two keys that have compatible types. *)
+end
+
+type pair =
+  | Pair : 'a Key.t * 'a -> pair
+
+(** {2 Imperative table indexed by [Key]} *)
+module Tbl : sig
+  type t
+
+  val create : ?size:int -> unit -> t
+
+  val mem : t -> _ Key.t -> bool
+
+  val add : t -> 'a Key.t -> 'a -> unit
+
+  val remove : t -> _ Key.t -> unit
+
+  val length : t -> int
+
+  val find : t -> 'a Key.t -> 'a option
+
+  val find_exn : t -> 'a Key.t -> 'a
+  (** @raise Not_found if the key is not in the table. *)
+
+  val iter : (pair -> unit) -> t -> unit
+
+  val to_iter : t -> pair iter
+
+  val of_iter : pair iter -> t
+
+  val add_iter : t -> pair iter -> unit
+
+  val add_list : t -> pair list -> unit
+
+  val of_list : pair list -> t
+
+  val to_list : t -> pair list
+end
+
+(** {2 Immutable map} *)
+module Map : sig
+  type t
+
+  val empty : t
+
+  val mem : _ Key.t -> t -> bool
+
+  val add : 'a Key.t -> 'a -> t -> t
+
+  val remove : _ Key.t -> t -> t
+
+  val length : t -> int
+
+  val cardinal : t -> int
+
+  val find : 'a Key.t -> t -> 'a option
+
+  val find_exn : 'a Key.t -> t -> 'a
+  (** @raise Not_found if the key is not in the table. *)
+
+  val iter : (pair -> unit) -> t -> unit
+
+  val to_iter : t -> pair iter
+
+  val of_iter : pair iter -> t
+
+  val add_iter : t -> pair iter -> t
+
+  val add_list : t -> pair list -> t
+
+  val of_list : pair list -> t
+
+  val to_list : t -> pair list
+end

src/base-term/Config.mli

@@ -34,11 +34,11 @@ type pair =
 
 val iter : (pair -> unit) -> t -> unit
 
-val to_seq : t -> pair sequence
+val to_iter : t -> pair sequence
 
-val of_seq : pair sequence -> t
+val of_iter : pair sequence -> t
 
-val add_seq : t -> pair sequence -> t
+val add_iter : t -> pair sequence -> t
 
 val add_list : t -> pair list -> t
 

src/base-term/Model.ml

@@ -5,7 +5,7 @@
 open Base_types
 
 module Val_map = struct
-  module M = CCIntMap
+  module M = CCMap.Make(CCInt)
   module Key = struct
     type t = Value.t list
     let equal = CCList.equal Value.equal
@@ -21,16 +21,16 @@ module Val_map = struct
   let cardinal = M.cardinal
 
   let find k m =
-    try Some (CCList.assoc ~eq:Key.equal k @@ M.find_exn (Key.hash k) m)
+    try Some (CCList.assoc ~eq:Key.equal k @@ M.find (Key.hash k) m)
     with Not_found -> None
 
   let add k v m =
     let h = Key.hash k in
-    let l = M.find h m |> CCOpt.get_or ~default:[] in
+    let l = M.get_or ~default:[] h m in
     let l = CCList.Assoc.set ~eq:Key.equal k v l in
     M.add h l m
 
-  let to_seq m yield = M.iter (fun _ l -> List.iter yield l) m
+  let to_iter m yield = M.iter (fun _ l -> List.iter yield l) m
 end
 
 module Fun_interpretation = struct
@@ -40,7 +40,7 @@ module Fun_interpretation = struct
   }
 
   let default fi = fi.default
-  let cases_list fi = Val_map.to_seq fi.cases |> Iter.to_rev_list
+  let cases_list fi = Val_map.to_iter fi.cases |> Iter.to_rev_list
 
   let make ~default l : t =
     let m = List.fold_left (fun m (k,v) -> Val_map.add k v m) Val_map.empty l in
@@ -129,8 +129,8 @@ let pp out {values; funs} =
       (Fmt.list ~sep:(Fmt.return "@ ") pp_fun_entry) (FI.cases_list fi) 
   in
   Fmt.fprintf out "(@[model@ @[:terms (@[<hv>%a@])@]@ @[:funs (@[<hv>%a@])@]@])"
-    (Fmt.seq ~sep:Fmt.(return "@ ") pp_tv) (Term.Map.to_seq values)
-    (Fmt.seq ~sep:Fmt.(return "@ ") pp_fun) (Fun.Map.to_seq funs)
+    (Fmt.iter ~sep:Fmt.(return "@ ") pp_tv) (Term.Map.to_iter values)
+    (Fmt.iter ~sep:Fmt.(return "@ ") pp_fun) (Fun.Map.to_iter funs)
 
 exception No_value
 

src/base-term/dune

@@ -2,5 +2,5 @@
  (name sidekick_base_term)
  (public_name sidekick.base-term)
  (synopsis "Basic term definitions for the standalone SMT solver")
- (libraries containers containers.data sidekick.core sidekick.util)
+ (libraries containers sidekick.core sidekick.util)
  (flags :standard -w -32 -open Sidekick_util))

src/cc/Sidekick_cc.ml

@@ -138,7 +138,7 @@ module Make (A: CC_ARG)
 
     let[@inline] iter_parents (n:node) : node Iter.t =
       assert (is_root n);
-      Bag.to_seq n.n_parents
+      Bag.to_iter n.n_parents
 
     type bitfield = Bits.field
     let[@inline] get_field f t = Bits.get f t.n_bits
@@ -324,8 +324,8 @@ module Make (A: CC_ARG)
     in
     Fmt.fprintf out
       "(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig-tbl@ %a@])@])"
-      (Util.pp_seq ~sep:" " pp_n) (T_tbl.values cc.tbl)
-      (Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)
+      (Util.pp_iter ~sep:" " pp_n) (T_tbl.values cc.tbl)
+      (Util.pp_iter ~sep:" " pp_sig_e) (Sig_tbl.to_iter cc.signatures_tbl)
 
   (* compute up-to-date signature *)
   let update_sig (s:signature) : Signature.t =

src/cc/dune

@@ -3,5 +3,5 @@
 (library
   (name Sidekick_cc)
   (public_name sidekick.cc)
-  (libraries containers containers.data iter sidekick.core sidekick.util)
+  (libraries containers iter sidekick.core sidekick.util)
   (flags :standard -open Sidekick_util))

src/core/Sidekick_core.ml

@@ -243,7 +243,7 @@ module type CC_S = sig
   (* TODO: remove? this is managed by the solver anyway? *)
   val on_pre_merge : t -> ev_on_pre_merge -> unit
   (** Add a function to be called when two classes are merged *)
-  
+
   val on_post_merge : t -> ev_on_post_merge -> unit
   (** Add a function to be called when two classes are merged *)
 
@@ -272,7 +272,7 @@ module type CC_S = sig
   val assert_lit : t -> lit -> unit
   (** Given a literal, assume it in the congruence closure and propagate
       its consequences. Will be backtracked.
-  
+
       Useful for the theory combination or the SAT solver's functor *)
 
   val assert_lits : t -> lit Iter.t -> unit
@@ -790,7 +790,7 @@ end = struct
         Log.debugf 5
           (fun k->k
               "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ :val2 %a@])@])"
-              M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); 
+              M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2);
         begin match M.merge cc n1 v1 n2 v2 e_n1_n2 with
           | Ok v' ->
             N_tbl.remove self.values n2; (* only keep repr *)
@@ -807,7 +807,7 @@ end = struct
 
   let pp out (self:t) : unit =
     let pp_e out (t,v) = Fmt.fprintf out "(@[%a@ :has %a@])" N.pp t M.pp v in
-    Fmt.fprintf out "(@[%a@])" (Fmt.seq pp_e) (iter_all self)
+    Fmt.fprintf out "(@[%a@])" (Fmt.iter pp_e) (iter_all self)
 
   let create_and_setup ?size (solver:SI.t) : t =
     let field_has_value =

src/msat-solver/Sidekick_msat_solver.ml

@@ -305,7 +305,7 @@ module Make(A : ARG)
     let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
       Msat.Log.debugf 2
         (fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])"
-            (if final then "[final]" else "") self.level (Util.pp_seq ~sep:"; " Lit.pp) lits);
+            (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
       (* transmit to CC *)
       let cc = cc self in
       if not final then (
@@ -553,7 +553,7 @@ module Make(A : ARG)
           Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Value.pp v
             in
         Fmt.fprintf out "(@[<hv>model@ %a@])"
-          (Util.pp_seq pp_pair) (Term.Tbl.to_seq tbl)
+          (Util.pp_iter pp_pair) (Term.Tbl.to_iter tbl)
   end
 
   type res =

src/msat-solver/dune

@@ -1,6 +1,6 @@
 (library
  (name Sidekick_msat_solver)
  (public_name sidekick.msat-solver)
- (libraries containers containers.data iter sidekick.core sidekick.util
+ (libraries containers iter sidekick.core sidekick.util
    sidekick.cc msat msat.backend)
  (flags :standard -open Sidekick_util))

src/th-data/Sidekick_th_data.ml

@@ -390,7 +390,7 @@ module Make(A : ARG) : S with module A = A = struct
       let pp_entry out (n,node) =
         Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node
       in
-      Fmt.fprintf out "(@[graph@ %a@])" (Fmt.seq pp_entry) (N_tbl.to_iter g)
+      Fmt.fprintf out "(@[graph@ %a@])" (Fmt.iter pp_entry) (N_tbl.to_iter g)
 
     let mk_graph (self:t) cc : graph =
       let g: graph = N_tbl.create ~size:32 () in

src/util/Bag.ml

@@ -34,12 +34,12 @@ let rec fold f acc = function
   | L x -> f acc x
   | N (a,b) -> fold f (fold f acc a) b
 
-let[@unroll 2] rec to_seq t yield = match t with
+let[@unroll 2] rec to_iter t yield = match t with
   | E -> ()
   | L x -> yield x
-  | N (a,b) -> to_seq a yield; to_seq b yield
+  | N (a,b) -> to_iter a yield; to_iter b yield
 
-let[@inline] iter f t = to_seq t f
+let[@inline] iter f t = to_iter t f
 
 let equal f a b =
   let rec push x l = match x with

src/util/Bag.mli

@@ -21,7 +21,7 @@ val cons : 'a -> 'a t -> 'a t
 
 val append : 'a t -> 'a t -> 'a t
 
-val to_seq : 'a t -> 'a Iter.t
+val to_iter : 'a t -> 'a Iter.t
 
 val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
 

src/util/IArray.ml

@@ -68,7 +68,7 @@ let exists p a =
 
 (** {2 Conversions} *)
 
-type 'a sequence = ('a -> unit) -> unit
+type 'a iter = ('a -> unit) -> unit
 type 'a gen = unit -> 'a option
 
 let of_list = Array.of_list
@@ -91,9 +91,9 @@ let to_array_map = Array.map
 
 let of_array_unsafe a = a (* careful with that axe, Eugene *)
 
-let to_seq a k = iter k a
+let to_iter a k = iter k a
 
-let of_seq s =
+let of_iter s =
   let l = ref [] in
   s (fun x -> l := x :: !l);
   Array.of_list (List.rev !l)
@@ -101,7 +101,7 @@ let of_seq s =
 (*$Q
   Q.(list int) (fun l -> \
     let g = Iter.of_list l in \
-    of_seq g |> to_seq |> Iter.to_list = l)
+    of_iter g |> to_iter |> Iter.to_list = l)
 *)
 
 let rec gen_to_list_ acc g = match g() with

src/util/IArray.mli

@@ -55,7 +55,7 @@ val exists : ('a -> bool) -> 'a t -> bool
 
 (** {2 Conversions} *)
 
-type 'a sequence = ('a -> unit) -> unit
+type 'a iter = ('a -> unit) -> unit
 type 'a gen = unit -> 'a option
 
 val of_list : 'a list -> 'a t
@@ -74,9 +74,9 @@ val of_array_unsafe : 'a array -> 'a t
 (** Take ownership of the given array. Careful, the array must {b NOT}
     be modified afterwards! *)
 
-val to_seq : 'a t -> 'a sequence
+val to_iter : 'a t -> 'a iter
 
-val of_seq : 'a sequence -> 'a t
+val of_iter : 'a iter -> 'a t
 
 val of_gen : 'a gen -> 'a t
 

src/util/Stat.ml

@@ -45,6 +45,6 @@ let pp_all out l =
     | C_int {name; count} -> Fmt.fprintf out "@[:%s %d@]" name count
     | C_float {name; count} -> Fmt.fprintf out "@[:%s %.4f@]" name count
   in
-  Fmt.fprintf out "(@[stats@ %a@])" Fmt.(seq ~sep:(return "@ ") pp_w) l
+  Fmt.fprintf out "(@[stats@ %a@])" Fmt.(iter ~sep:(return "@ ") pp_w) l
 
 let global = create()

src/util/Util.ml

@@ -11,8 +11,8 @@ let pp_sep sep out () = Format.fprintf out "%s@," sep
 let pp_list ?(sep=" ") pp out l =
   Fmt.list ~sep:(pp_sep sep) pp out l
 
-let pp_seq ?(sep=" ") pp out l =
-  Fmt.seq ~sep:(pp_sep sep) pp out l
+let pp_iter ?(sep=" ") pp out l =
+  Fmt.iter ~sep:(pp_sep sep) pp out l
 
 let pp_pair ?(sep=" ") pp1 pp2 out t =
   Fmt.pair ~sep:(pp_sep sep) pp1 pp2 out t
@@ -21,17 +21,19 @@ let pp_array ?(sep=" ") pp out l =
   Fmt.array ~sep:(pp_sep sep) pp out l
 
 let pp_iarray ?(sep=" ") pp out a =
-  Fmt.seq ~sep:(pp_sep sep) pp out (IArray.to_seq a)
+  Fmt.iter ~sep:(pp_sep sep) pp out (IArray.to_iter a)
 
 let flat_map_l_ia f l =
   CCList.flat_map (fun x -> IArray.to_list @@ f x) l
 
 let setup_gc () =
   let g = Gc.get () in
-  g.Gc.space_overhead <- 3_000; (* major gc *)
-  g.Gc.max_overhead <- 10_000; (* compaction *)
-  g.Gc.minor_heap_size <- 500_000; (* ×8 to obtain bytes on 64 bits -->  *)
-  Gc.set g
+  Gc.set {
+    g with Gc.
+    space_overhead = 3_000; (* major gc *)
+    max_overhead = 10_000; (* compaction *)
+    minor_heap_size = 500_000; (* ×8 to obtain bytes on 64 bits -->  *)
+  }
 
 module Int_set = CCSet.Make(CCInt)
 module Int_map = CCMap.Make(CCInt)

src/util/Util.mli

@@ -6,7 +6,7 @@ type 'a printer = 'a CCFormat.printer
 
 val pp_list : ?sep:string -> 'a printer -> 'a list printer
 
-val pp_seq : ?sep:string -> 'a printer -> 'a Iter.t printer
+val pp_iter : ?sep:string -> 'a printer -> 'a Iter.t printer
 
 val pp_array : ?sep:string -> 'a printer -> 'a array printer