simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 21:24:06 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

core: add iter_all in monoid class

Browse source
This commit is contained in:
Simon Cruanes 2019-12-09 21:49:48 -06:00
parent bf23f7c826
commit d52fb1e5fd
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/Sidekick_core.ml
View file

@ -680,6 +680,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig
val pop_levels : t -> int -> unit val pop_levels : t -> int -> unit
val mem : t -> M.SI.CC.N.t -> bool val mem : t -> M.SI.CC.N.t -> bool
val get : t -> M.SI.CC.N.t -> M.t option val get : t -> M.SI.CC.N.t -> M.t option
val iter_all : t -> (M.SI.CC.N.t * M.t) Iter.t
end = struct end = struct
module SI = M.SI module SI = M.SI
module T = SI.T.Term module T = SI.T.Term
@ -713,6 +714,9 @@ end = struct
N_tbl.add self.values n v N_tbl.add self.values n v
| None -> () | None -> ()
let iter_all (self:t) : _ Iter.t =
N_tbl.to_iter self.values
(* find cell for [n] *) (* find cell for [n] *)
let get_cell (self:t) (n:N.t) : M.t option = let get_cell (self:t) (n:N.t) : M.t option =
N_tbl.get self.values n N_tbl.get self.values n
@ -736,6 +740,7 @@ end = struct
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 with begin match M.merge cc n1 v1 n2 v2 with
| Ok v' -> | Ok v' ->
N_tbl.remove self.values n2; (* only keep repr *)
N_tbl.add self.values n1 v'; N_tbl.add self.values n1 v';
| Error expl -> | Error expl ->
(* add [n1=n2] to the conflict *) (* add [n1=n2] to the conflict *)
@ -744,7 +749,8 @@ end = struct
end end
| None, Some cr -> | None, Some cr ->
SI.CC.set_bitfield cc self.field_has_value true n1; SI.CC.set_bitfield cc self.field_has_value true n1;
N_tbl.add self.values n1 cr N_tbl.add self.values n1 cr;
N_tbl.remove self.values n2; (* only keep reprs *)
| Some _, None -> () (* already there on the left *) | Some _, None -> () (* already there on the left *)
| None, None -> () | None, None -> ()
end end