diff --git a/src/base/Proof.ml b/src/base/Proof.ml index acea15fb..25e2821d 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -51,8 +51,24 @@ type proof_rule = t -> proof_step module Step_vec = struct type elt = proof_step + type t = elt Vec.t - include VecI32 + let get = Vec.get + let size = Vec.size + let iter = Vec.iter + let iteri = Vec.iteri + let create ?cap:_ () = Vec.create () + let clear = Vec.clear + let copy = Vec.copy + let is_empty = Vec.is_empty + let push = Vec.push + let fast_remove = Vec.fast_remove + let filter_in_place = Vec.filter_in_place + let ensure_size v len = Vec.ensure_size v ~elt:0l len + let pop = Vec.pop_exn + let set = Vec.set + let shrink = Vec.shrink + let to_iter = Vec.to_iter end let disable (self : t) : unit = diff --git a/src/checker/drup_check.ml b/src/checker/drup_check.ml index f0a02542..ed9b4664 100644 --- a/src/checker/drup_check.ml +++ b/src/checker/drup_check.ml @@ -30,8 +30,8 @@ end = struct let del_clause self c = Vec.push self.ops (Delete c) let get self i = Vec.get self.ops i let size self = Vec.size self.ops - let ops self = Vec.to_seq self.ops - let iteri self ~f = Vec.iteri f self.ops + let ops self = Vec.to_iter self.ops + let iteri self ~f = Vec.iteri ~f self.ops let pp_op out = function | Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c @@ -43,19 +43,17 @@ end = struct let pp_c out c = Clause.iter c ~f:(fun a -> fpf out "%d " (a : atom :> int)) in - Vec.iter - (function - | Input c -> fpf oc "i %a0\n" pp_c c - | Redundant c -> fpf oc "%a0\n" pp_c c - | Delete c -> fpf oc "d %a0\n" pp_c c) - self.ops + Vec.iter self.ops ~f:(function + | Input c -> fpf oc "i %a0\n" pp_c c + | Redundant c -> fpf oc "%a0\n" pp_c c + | Delete c -> fpf oc "d %a0\n" pp_c c) end (** Forward checking. Each event is checked by reverse-unit propagation on previous events. *) module Fwd_check : sig - type error = [ `Bad_steps of VecSmallInt.t | `No_empty_clause ] + type error = [ `Bad_steps of Veci.t | `No_empty_clause ] val pp_error : Trace.t -> error Fmt.printer @@ -64,10 +62,10 @@ module Fwd_check : sig success. In case of error it returns [Error idxs] where [idxs] are the indexes in the trace of the steps that failed. *) end = struct - type t = { checker: Checker.t; errors: VecSmallInt.t } + type t = { checker: Checker.t; errors: Veci.t } let create cstore : t = - { checker = Checker.create cstore; errors = VecSmallInt.create () } + { checker = Checker.create cstore; errors = Veci.create () } (* check event, return [true] if it's valid *) let check_op (self : t) i (op : Trace.op) : bool = @@ -87,15 +85,15 @@ end = struct Checker.del_clause self.checker c; true - type error = [ `Bad_steps of VecSmallInt.t | `No_empty_clause ] + type error = [ `Bad_steps of Veci.t | `No_empty_clause ] let pp_error trace out = function | `No_empty_clause -> Fmt.string out "no empty clause found" | `Bad_steps bad -> - let n0 = VecSmallInt.get bad 0 in + let n0 = Veci.get bad 0 in Fmt.fprintf out "@[checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]" - (VecSmallInt.size bad) n0 Trace.pp_op (Trace.get trace n0) + (Veci.size bad) n0 Trace.pp_op (Trace.get trace n0) let check trace : _ result = let self = create (Trace.cstore trace) in @@ -116,13 +114,13 @@ end = struct ) else ( Log.debugf 10 (fun k -> k "(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op); - VecSmallInt.push self.errors i + Veci.push self.errors i )); - Log.debugf 10 (fun k -> k "found %d errors" (VecSmallInt.size self.errors)); + Log.debugf 10 (fun k -> k "found %d errors" (Veci.size self.errors)); if not !has_false then Error `No_empty_clause - else if VecSmallInt.size self.errors > 0 then + else if Veci.size self.errors > 0 then Error (`Bad_steps self.errors) else Ok () diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 5965a048..504931cd 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -169,7 +169,7 @@ module type SAT_PROOF = sig type proof_step (** identifier for a proof *) - module Step_vec : Vec_sig.S with type elt = proof_step + module Step_vec : Vec_sig.BASE with type elt = proof_step (** A vector of steps *) type lit diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml index b3a525ba..895bf1d5 100644 --- a/src/drup/sidekick_drup.ml +++ b/src/drup/sidekick_drup.ml @@ -5,7 +5,7 @@ *) module Fmt = CCFormat -module VecSmallInt = VecSmallInt +module Veci = Veci (* TODO: resolution proof construction, optionally *) @@ -130,7 +130,7 @@ module Make () : S = struct end module Stack = struct - include VecSmallInt + include Veci let create () = create () end diff --git a/src/sat/Heap.ml b/src/sat/Heap.ml index 78e60e38..468cb99a 100644 --- a/src/sat/Heap.ml +++ b/src/sat/Heap.ml @@ -4,10 +4,10 @@ module type S = Heap_intf.S module Make (Elt : RANKED) = struct type elt_store = Elt.store type elt = Elt.t - type t = { store: elt_store; heap: VecSmallInt.t (* vec of elements *) } + type t = { store: elt_store; heap: Veci.t (* vec of elements *) } let _absent_index = -1 - let create store : t = { store; heap = VecSmallInt.create () } + let create store : t = { store; heap = Veci.create () } let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *) @@ -16,17 +16,17 @@ module Make (Elt : RANKED) = struct (* let rec heap_property cmp ({heap=heap} as s) i = - i >= (VecSmallInt.size heap) || + i >= (Veci.size heap) || ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) && heap_property cmp s (left i) && heap_property cmp s (right i)) let heap_property cmp s = heap_property cmp s 1 *) - let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecSmallInt.get self.heap i) + let[@inline] get_elt_ self i = Elt.of_int_unsafe (Veci.get self.heap i) let[@inline] set_elt_ self i elt = - VecSmallInt.set self.heap i (elt : Elt.t :> int) + Veci.set self.heap i (elt : Elt.t :> int) (* [elt] is above or at its expected position. Move it up the heap (towards high indices) to restore the heap property *) @@ -43,7 +43,7 @@ module Make (Elt : RANKED) = struct Elt.set_heap_idx self.store elt !i let percolate_down (self : t) (elt : Elt.t) : unit = - let sz = VecSmallInt.size self.heap in + let sz = Veci.size self.heap in let li = ref (left (Elt.heap_idx self.store elt)) in let ri = ref (right (Elt.heap_idx self.store elt)) in let i = ref (Elt.heap_idx self.store elt) in @@ -83,7 +83,7 @@ module Make (Elt : RANKED) = struct let filter (self : t) filt : unit = let j = ref 0 in - let lim = VecSmallInt.size self.heap in + let lim = Veci.size self.heap in for i = 0 to lim - 1 do if filt (get_elt_ self i) then ( set_elt_ self !j (get_elt_ self i); @@ -92,24 +92,24 @@ module Make (Elt : RANKED) = struct ) else Elt.set_heap_idx self.store (get_elt_ self i) _absent_index done; - VecSmallInt.shrink self.heap (lim - !j); + Veci.shrink self.heap (lim - !j); for i = (lim / 2) - 1 downto 0 do percolate_down self (get_elt_ self i) done - let[@inline] size s = VecSmallInt.size s.heap - let[@inline] is_empty s = VecSmallInt.is_empty s.heap + let[@inline] size s = Veci.size s.heap + let[@inline] is_empty s = Veci.is_empty s.heap let clear self : unit = - VecSmallInt.iter self.heap ~f:(fun e -> + Veci.iter self.heap ~f:(fun e -> Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index); - VecSmallInt.clear self.heap; + Veci.clear self.heap; () let insert self elt = if not (in_heap self elt) then ( - Elt.set_heap_idx self.store elt (VecSmallInt.size self.heap); - VecSmallInt.push self.heap (elt : Elt.t :> int); + Elt.set_heap_idx self.store elt (Veci.size self.heap); + Veci.push self.heap (elt : Elt.t :> int); percolate_up self elt ) @@ -128,21 +128,21 @@ module Make (Elt : RANKED) = struct *) let remove_min self = - match VecSmallInt.size self.heap with + match Veci.size self.heap with | 0 -> raise Not_found | 1 -> - let x = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in + let x = Elt.of_int_unsafe (Veci.pop self.heap) in Elt.set_heap_idx self.store x _absent_index; x | _ -> let x = get_elt_ self 0 in - let new_hd = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in + let new_hd = Elt.of_int_unsafe (Veci.pop self.heap) in (* heap.last() *) set_elt_ self 0 new_hd; Elt.set_heap_idx self.store x _absent_index; Elt.set_heap_idx self.store new_hd 0; (* enforce heap property again *) - if VecSmallInt.size self.heap > 1 then percolate_down self new_hd; + if Veci.size self.heap > 1 then percolate_down self new_hd; x end [@@inline] diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index b34b5f02..ef7d5f75 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -61,7 +61,7 @@ module Make (Plugin : PLUGIN) = struct let[@inline] var a = Var0.of_int_unsafe (a lsr 1) let[@inline] na v = ((v : var :> int) lsl 1) lor 1 - module AVec = VecSmallInt + module AVec = Veci module ATbl = CCHashtbl.Make (CCInt) end @@ -74,7 +74,7 @@ module Make (Plugin : PLUGIN) = struct end = struct include Int_id.Make () module Tbl = Util.Int_tbl - module CVec = VecSmallInt + module CVec = Veci end type clause = Clause0.t @@ -98,7 +98,7 @@ module Make (Plugin : PLUGIN) = struct type cstore = { c_lits: atom array Vec.t; (* storage for clause content *) c_activity: Vec_float.t; - c_recycle_idx: VecSmallInt.t; (* recycle clause numbers that were GC'd *) + c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *) c_proof: Step_vec.t; (* clause -> proof_rule for its proof *) c_attached: Bitvec.t; c_marked: Bitvec.t; @@ -158,7 +158,7 @@ module Make (Plugin : PLUGIN) = struct { c_lits = Vec.create (); c_activity = Vec_float.create (); - c_recycle_idx = VecSmallInt.create ~cap:0 (); + c_recycle_idx = Veci.create ~cap:0 (); c_proof = Step_vec.create ~cap:0 (); c_dead = Bitvec.create (); c_attached = Bitvec.create (); @@ -172,7 +172,7 @@ module Make (Plugin : PLUGIN) = struct (** iterate on variables *) let iter_vars self f = - Vec.iteri (fun i _ -> f (Var0.of_int_unsafe i)) self.v_level + Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i)) module Var = struct include Var0 @@ -339,10 +339,10 @@ module Make (Plugin : PLUGIN) = struct in (* allocate new ID *) let cid = - if VecSmallInt.is_empty c_recycle_idx then + if Veci.is_empty c_recycle_idx then Vec.size c_lits else - VecSmallInt.pop c_recycle_idx + Veci.pop c_recycle_idx in (* allocate space *) @@ -447,7 +447,7 @@ module Make (Plugin : PLUGIN) = struct Vec.set c_lits cid [||]; Vec_float.set c_activity cid 0.; - VecSmallInt.push c_recycle_idx cid; + Veci.push c_recycle_idx cid; (* recycle idx *) () @@ -659,7 +659,7 @@ module Make (Plugin : PLUGIN) = struct let descr = P.descr let add c = Vec.push clauses_ c - let iter ~f = Vec.iter f clauses_ + let iter ~f = Vec.iter ~f clauses_ let push_level () = () let pop_levels _ = () let size () = Vec.size clauses_ @@ -816,10 +816,10 @@ module Make (Plugin : PLUGIN) = struct } = self in - Vec.iter (fun (c, p) -> add_clause_pool c p) clauses_to_add_in_pool; + Vec.iter clauses_to_add_in_pool ~f:(fun (c, p) -> add_clause_pool c p); CVec.iter ~f:add_clause_learnt clauses_to_add_learnt; - Vec.iter decision decisions; - Vec.iter (fun (p, lvl, c) -> propagate p ~lvl c) prop; + Vec.iter ~f:decision decisions; + Vec.iter prop ~f:(fun (p, lvl, c) -> propagate p ~lvl c); clear self; () end @@ -847,7 +847,7 @@ module Make (Plugin : PLUGIN) = struct store them here. *) trail: AVec.t; (* decision stack + propagated elements (atoms or assignments). *) - var_levels: VecSmallInt.t; (* decision levels in [trail] *) + var_levels: Veci.t; (* decision levels in [trail] *) assumptions: AVec.t; (* current assumptions *) mutable th_head: int; (* Start offset in the queue {!trail} of @@ -911,7 +911,7 @@ module Make (Plugin : PLUGIN) = struct th_head = 0; elt_head = 0; trail = AVec.create (); - var_levels = VecSmallInt.create (); + var_levels = Veci.create (); assumptions = AVec.create (); order = H.create store; var_incr = 1.; @@ -944,10 +944,10 @@ module Make (Plugin : PLUGIN) = struct let iter_clauses_learnt_ (self : t) ~f : unit = let[@inline] iter_pool (module P : CLAUSE_POOL) = P.iter ~f in iter_pool self.clauses_learnt; - Vec.iter iter_pool self.clause_pools; + Vec.iter ~f:iter_pool self.clause_pools; () - let[@inline] decision_level st = VecSmallInt.size st.var_levels + let[@inline] decision_level st = Veci.size st.var_levels let[@inline] nb_clauses st = CVec.size st.clauses_hyps let stat self = self.stat @@ -1172,7 +1172,7 @@ module Make (Plugin : PLUGIN) = struct let new_decision_level st = assert (st.th_head = AVec.size st.trail); assert (st.elt_head = AVec.size st.trail); - VecSmallInt.push st.var_levels (AVec.size st.trail); + Veci.push st.var_levels (AVec.size st.trail); Plugin.push_level st.th; () @@ -1206,7 +1206,7 @@ module Make (Plugin : PLUGIN) = struct else ( Log.debugf 5 (fun k -> k "(@[sat.cancel-until %d@])" lvl); (* We set the head of the solver and theory queue to what it was. *) - let head = ref (VecSmallInt.get self.var_levels lvl) in + let head = ref (Veci.get self.var_levels lvl) in self.elt_head <- !head; self.th_head <- !head; (* Now we need to cleanup the vars that are not valid anymore @@ -1239,7 +1239,7 @@ module Make (Plugin : PLUGIN) = struct assert (n > 0); (* Resize the vectors according to their new size. *) AVec.shrink self.trail !head; - VecSmallInt.shrink self.var_levels lvl; + Veci.shrink self.var_levels lvl; Plugin.pop_levels self.th n; Delayed_actions.clear_on_backtrack self.delayed_actions; (* TODO: for scoped clause pools, backtrack them *) @@ -1598,7 +1598,7 @@ module Make (Plugin : PLUGIN) = struct Step_vec.clear self.temp_step_vec; (* cleanup marks *) - Vec.iter (Store.clear_var store) to_unmark; + Vec.iter ~f:(Store.clear_var store) to_unmark; Vec.clear to_unmark; (* put high-level literals first, so that: @@ -2213,7 +2213,7 @@ module Make (Plugin : PLUGIN) = struct in gc_pool self.clauses_learnt; - Vec.iter gc_pool self.clause_pools; + Vec.iter ~f:gc_pool self.clause_pools; let n_collected = CVec.size to_be_gc in diff --git a/src/simplex/sidekick_simplex.ml b/src/simplex/sidekick_simplex.ml index 32b6fa86..f9a396cf 100644 --- a/src/simplex/sidekick_simplex.ml +++ b/src/simplex/sidekick_simplex.ml @@ -353,23 +353,21 @@ module Make (Arg : ARG) : (Fmt.iter ~sep:(Fmt.return "@ ") ppi) CCInt.(0 -- (n_cols self - 1)); - Vec.iteri - (fun i row -> + Vec.iteri self.rows ~f:(fun i row -> let hd = CCString.pad ~side:`Left 6 @@ Printf.sprintf "r%d (v%d)" i row.vs.idx in Fmt.fprintf out "@,{@[%9s: %a@]}" hd (Fmt.iter ~sep:(Fmt.return "@ ") (Q.pp_approx 6)) - (Vec.to_seq row.cols)) - self.rows; + (Vec.to_iter row.cols)); Fmt.fprintf out "@;<0 -1>}@]" let to_string = Fmt.to_string pp let add_column self = self.n_cols <- 1 + self.n_cols; - Vec.iter (fun r -> Vec.push r.cols Q.zero) self.rows + Vec.iter self.rows ~f:(fun r -> Vec.push r.cols Q.zero) let add_row_and_column self ~f : var_state = let n = n_rows self in @@ -393,7 +391,7 @@ module Make (Arg : ARG) : Vec.set r.cols j n let[@inline] iter_rows ?(skip = ~-1) (self : t) f : unit = - Vec.iteri (fun i row -> if i <> skip then f i row.vs) self.rows + Vec.iteri self.rows ~f:(fun i row -> if i <> skip then f i row.vs) let[@inline] iter_cols ?(skip = ~-1) (self : t) f : unit = for i = 0 to n_cols self - 1 do @@ -498,7 +496,7 @@ module Make (Arg : ARG) : (* for debug purposes *) let _check_invariants self : unit = - Vec.iteri (fun i v -> assert (v.idx = i)) self.vars; + Vec.iteri self.vars ~f:(fun i v -> assert (v.idx = i)); let n = Vec.size self.vars in assert (Matrix.n_rows self.matrix = 0 || Matrix.n_cols self.matrix = n); Matrix.iter_rows self.matrix (fun i x_i -> @@ -507,12 +505,10 @@ module Make (Arg : ARG) : assert (Q.(Matrix.get self.matrix x_i.basic_idx x_i.idx = minus_one)); (* basic vars are only defined in terms of non-basic vars *) - Vec.iteri - (fun j x_j -> + Vec.iteri self.vars ~f:(fun j x_j -> if Var_state.(x_i != x_j) && Q.(Matrix.get self.matrix i j <> zero) then - assert (Var_state.is_n_basic x_j)) - self.vars; + assert (Var_state.is_n_basic x_j)); (* sum of each row must be 0 *) let sum = @@ -786,8 +782,7 @@ module Make (Arg : ARG) : assert (Var_state.is_basic x_i); let map_res = ref [] in let bounds = ref V_map.empty in - Vec.iteri - (fun j x_j -> + Vec.iteri self.vars ~f:(fun j x_j -> if j <> x_i.idx then ( let c = Matrix.get self.matrix x_i.basic_idx j in if Q.(c <> zero) then ( @@ -817,8 +812,7 @@ module Make (Arg : ARG) : bounds := V_map.add x_j.var (op, u) !bounds | None -> assert false (* we could increase [x_j]?! *)) ) - )) - self.vars; + )); !map_res, !bounds let add_constraint ?(is_int = false) ~on_propagate (self : t) @@ -1159,7 +1153,7 @@ module Make (Arg : ARG) : | _ -> eps in eps) - default_eps (Vec.to_seq self.vars) + default_eps (Vec.to_iter self.vars) in if Q.(eps >= one) then Q.one @@ -1171,7 +1165,7 @@ module Make (Arg : ARG) : Log.debugf 50 (fun k -> k "(@[simplex.model@ :epsilon-val %a@])" pp_q_dbg eps); let subst = - Vec.to_seq self.vars + Vec.to_iter self.vars |> Iter.fold (fun subst x -> let { base; eps_factor } = x.value in diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index e5e22699..e1ffadf7 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -2,8 +2,7 @@ module Fmt = CCFormat module Util = Util module Vec = Vec -module VecSmallInt = VecSmallInt -module VecI32 = VecI32 +module Veci = Veci module Vec_float = Vec_float module Vec_unit = Vec_unit module Vec_sig = Vec_sig diff --git a/src/util/Vec.ml b/src/util/Vec.ml index 43ed3329..a25099bc 100644 --- a/src/util/Vec.ml +++ b/src/util/Vec.ml @@ -53,7 +53,7 @@ let ensure_size_with self f n = self.sz <- n ) -let ensure_size self x n = ensure_size_with self (fun () -> x) n +let ensure_size self ~elt:x n = ensure_size_with self (fun () -> x) n (* grow the array *) let[@inline never] grow_to_double_size t x : unit = @@ -125,22 +125,21 @@ let sort t f : unit = Array.fast_sort f sub_arr; t.data <- sub_arr -let[@inline] iter f t = +let iter ~f t = for i = 0 to size t - 1 do f (Array.unsafe_get t.data i) done -let[@inline] iteri f t = +let iteri ~f t = for i = 0 to size t - 1 do f i (Array.unsafe_get t.data i) done -let[@inline] to_seq a k = iter k a -let to_iter v k = iter k v -let exists p t = Iter.exists p @@ to_seq t -let for_all p t = Iter.for_all p @@ to_seq t -let fold f acc a = Iter.fold f acc @@ to_seq a -let to_list a = Iter.to_list @@ to_seq a +let to_iter v k = iter ~f:k v +let exists p t = Iter.exists p @@ to_iter t +let for_all p t = Iter.for_all p @@ to_iter t +let fold f acc a = Iter.fold f acc @@ to_iter a +let to_list a = Iter.to_list @@ to_iter a let to_array a = Array.sub a.data 0 a.sz let of_list l : _ t = @@ -153,11 +152,9 @@ let of_list l : _ t = let pp ?(sep = ", ") pp out v = let first = ref true in - iter - (fun x -> + iter v ~f:(fun x -> if !first then first := false else Format.fprintf out "%s@," sep; pp out x) - v diff --git a/src/util/Vec.mli b/src/util/Vec.mli index b6898970..e94028a7 100644 --- a/src/util/Vec.mli +++ b/src/util/Vec.mli @@ -20,12 +20,11 @@ val to_list : 'a t -> 'a list val to_array : 'a t -> 'a array val of_list : 'a list -> 'a t -val to_seq : 'a t -> 'a Iter.t val clear : 'a t -> unit (** Set size to 0, doesn't free elements *) -val ensure_size : 'a t -> 'a -> int -> unit +val ensure_size : 'a t -> elt:'a -> int -> unit (** ensure size is at least [n] *) val ensure_size_with : 'a t -> (unit -> 'a) -> int -> unit @@ -79,12 +78,12 @@ val filter_in_place : ('a -> bool) -> 'a t -> unit val sort : 'a t -> ('a -> 'a -> int) -> unit (** Sort in place the array *) -val iter : ('a -> unit) -> 'a t -> unit +val iter : f:('a -> unit) -> 'a t -> unit (** Iterate on elements *) val to_iter : 'a t -> 'a Iter.t -val iteri : (int -> 'a -> unit) -> 'a t -> unit +val iteri : f:(int -> 'a -> unit) -> 'a t -> unit (** Iterate on elements with their index *) val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b diff --git a/src/util/VecI32.ml b/src/util/VecI32.ml deleted file mode 100644 index 2987d2f9..00000000 --- a/src/util/VecI32.ml +++ /dev/null @@ -1,104 +0,0 @@ -module A = Bigarray.Array1 - -type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t -type t = { mutable data: int32arr; mutable sz: int } - -let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz -let create ?(cap = 16) () : t = { sz = 0; data = mk_arr_ cap } -let[@inline] clear self = self.sz <- 0 -let[@inline] shrink self n = if n < self.sz then self.sz <- n -let[@inline] size self = self.sz -let[@inline] is_empty self = self.sz = 0 - -let copy self = - if size self = 0 then - create ~cap:0 () - else ( - (* copy bigarray *) - let data = mk_arr_ (size self) in - A.blit (A.sub self.data 0 (size self)) data; - { sz = self.sz; data } - ) - -let[@inline] fast_remove t i = - assert (i >= 0 && i < t.sz); - A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1); - t.sz <- t.sz - 1 - -let filter_in_place f vec = - let i = ref 0 in - while !i < size vec do - if f (A.unsafe_get vec.data !i) then - incr i - else - fast_remove vec !i - done - -(* ensure capacity is [new_cap] *) -let resize_cap_ self new_cap = - assert (A.dim self.data < new_cap); - let new_data = mk_arr_ new_cap in - A.blit self.data (A.sub new_data 0 (A.dim self.data)); - self.data <- new_data - -let ensure_cap self (n : int) = - if n > A.dim self.data then ( - let new_cap = max n (max 4 (A.dim self.data * 2)) in - resize_cap_ self new_cap - ) - -let ensure_size self n = - if n > self.sz then ( - ensure_cap self n; - self.sz <- n - ) - -let[@inline] push (self : t) i : unit = - ensure_cap self (self.sz + 1); - self.data.{self.sz} <- i; - self.sz <- 1 + self.sz - -let[@inline] push_i32 self i = - ensure_cap self (self.sz + 1); - self.data.{self.sz} <- i; - self.sz <- 1 + self.sz - -let[@inline] pop self = - if self.sz > 0 then ( - let x = self.data.{self.sz - 1} in - self.sz <- self.sz - 1; - x - ) else - failwith "vecI32.pop: empty" - -let[@inline] get self i : int32 = - assert (i >= 0 && i < self.sz); - A.unsafe_get self.data i - -let[@inline] set self i x : unit = - assert (i >= 0 && i < self.sz); - A.unsafe_set self.data i x - -let[@inline] set self i x : unit = - assert (i >= 0 && i < self.sz); - A.unsafe_set self.data i x - -let[@inline] iter ~f self = - for i = 0 to self.sz - 1 do - f self.data.{i} - done - -let[@inline] iteri ~f self = - for i = 0 to self.sz - 1 do - f i self.data.{i} - done - -include Vec_sig.Make_extensions (struct - type nonrec elt = int32 - type nonrec t = t - - let get = get - let size = size - let iter = iter - let iteri = iteri -end) diff --git a/src/util/VecI32.mli b/src/util/VecI32.mli deleted file mode 100644 index 84403571..00000000 --- a/src/util/VecI32.mli +++ /dev/null @@ -1,5 +0,0 @@ -(** Vectors of int32 integers - - These vectors are more optimized than {!Vec}. *) - -include Vec_sig.S with type elt := int32 diff --git a/src/util/Vec_float.ml b/src/util/Vec_float.ml index a22d5e95..0546be01 100644 --- a/src/util/Vec_float.ml +++ b/src/util/Vec_float.ml @@ -84,10 +84,13 @@ let[@inline] iteri ~f self = f i self.data.{i} done +let to_iter v k = iter ~f:k v + include Vec_sig.Make_extensions (struct type nonrec elt = float type nonrec t = t + let to_iter = to_iter let get = get let size = size let iter = iter diff --git a/src/util/Vec_sig.ml b/src/util/Vec_sig.ml index cf789303..fd50e110 100644 --- a/src/util/Vec_sig.ml +++ b/src/util/Vec_sig.ml @@ -7,6 +7,7 @@ module type BASE_RO = sig val get : t -> int -> elt val iter : f:(elt -> unit) -> t -> unit val iteri : f:(int -> elt -> unit) -> t -> unit + val to_iter : t -> elt Iter.t end module type BASE = sig @@ -33,7 +34,6 @@ module type EXTENSIONS = sig type elt type t - val to_iter : t -> elt Iter.t val to_array : t -> elt array val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a val pp : elt CCFormat.printer -> t CCFormat.printer @@ -48,8 +48,6 @@ module Make_extensions (B : BASE_RO) : EXTENSIONS with type t := B.t and type elt := B.elt = struct include B - let[@inline] to_iter self k = iter ~f:k self - let to_array self = if size self = 0 then [||] diff --git a/src/util/VecSmallInt.ml b/src/util/Veci.ml similarity index 97% rename from src/util/VecSmallInt.ml rename to src/util/Veci.ml index e88ad6c6..48f74dd5 100644 --- a/src/util/VecSmallInt.ml +++ b/src/util/Veci.ml @@ -97,10 +97,13 @@ let[@inline] iteri ~f self = f i (Int32.to_int self.data.{i}) done +let[@inline] to_iter self k = iter ~f:k self + include Vec_sig.Make_extensions (struct type nonrec elt = int type nonrec t = t + let to_iter = to_iter let get = get let size = size let iter = iter diff --git a/src/util/VecSmallInt.mli b/src/util/Veci.mli similarity index 100% rename from src/util/VecSmallInt.mli rename to src/util/Veci.mli