change type of CCDeque

Change the definition of the type in CCDeque to remove the Zero cell.
This new type enforce one invariant.
This commit is contained in:
Fardale 2019-11-01 22:44:52 +01:00 committed by Simon Cruanes
parent b3ce398624
commit 2fa12665dd

View file

@ -3,23 +3,23 @@
(** {1 Imperative deque} *) (** {1 Imperative deque} *)
type 'a cell = type 'a cell =
| Zero
| One of 'a | One of 'a
| Two of 'a * 'a | Two of 'a * 'a
| Three of 'a * 'a * 'a | Three of 'a * 'a * 'a
(** A cell holding a small number of elements *) (** A cell holding a small number of elements *)
type 'a node = { type 'a inner_node = {
mutable cell : 'a cell; mutable cell : 'a cell;
mutable next : 'a node; mutable next : 'a inner_node;
mutable prev : 'a node; mutable prev : 'a inner_node;
} }
type 'a node = Empty | Node of 'a inner_node
(** Linked list of cells. (** Linked list of cells.
invariant: only the first and last cells are allowed to invariant: only the first and last cells are allowed to
be anything but [Three] (all the intermediate ones are [Three]) be anything but [Three] (all the intermediate ones are [Three])
The first and last cell are [Zero] if and only if the *)
deque is empty *)
type 'a t = { type 'a t = {
mutable cur : 'a node; mutable cur : 'a node;
@ -48,12 +48,10 @@ type 'a t = {
exception Empty exception Empty
let create () = let create () =
let rec cur = { cell=Zero; prev=cur; next=cur } in { cur = Empty; size=0 }
{ cur; size=0 }
let clear q = let clear q =
let rec cur = { cell=Zero; prev=cur; next=cur } in q.cur <- Empty;
q.cur <- cur;
q.size <- 0; q.size <- 0;
() ()
@ -69,48 +67,54 @@ let clear q =
let incr_size_ d = d.size <- d.size + 1 let incr_size_ d = d.size <- d.size + 1
let decr_size_ d = d.size <- d.size - 1 let decr_size_ d = d.size <- d.size - 1
let is_zero_ n = match n.cell with
| Zero -> true
| One _
| Two _
| Three _ -> false
let bool_eq (a : bool) b = Stdlib.(=) a b let bool_eq (a : bool) b = Stdlib.(=) a b
let is_empty d = let is_empty d =
let res = d.size = 0 in let res = d.size = 0 in
assert (bool_eq res (is_zero_ d.cur)); assert (bool_eq res (d.cur = Empty));
res res
(*let rec cur = { cell=Zero; prev=cur; next=cur } in*)
let push_front d x = let push_front d x =
incr_size_ d; incr_size_ d;
match d.cur.cell with match d.cur with
| Zero -> d.cur.cell <- One x | Empty ->
| One y -> d.cur.cell <- Two (x, y) let rec node = { cell=One x; prev = node; next = node } in
| Two (y, z) -> d.cur.cell <- Three (x,y,z) d.cur <- Node node
| Three _ -> | Node n ->
let node = { cell = One x; prev = d.cur.prev; next=d.cur; } in match n.cell with
d.cur.prev.next <- node; | One y -> n.cell <- Two (x, y)
d.cur.prev <- node; | Two (y, z) -> n.cell <- Three (x,y,z)
d.cur <- node (* always point to first node *) | Three _ ->
let node = { cell = One x; prev = n.prev; next = n; } in
n.prev.next <- node;
n.prev <- node;
d.cur <- Node node (* always point to first node *)
let push_back d x = let push_back d x =
incr_size_ d; incr_size_ d;
let n = d.cur.prev in (* last node *) match d.cur with
match n.cell with | Empty ->
| Zero -> n.cell <- One x let rec node = { cell=One x; prev = node; next = node } in
| One y -> n.cell <- Two (y, x) d.cur <- Node node
| Two (y,z) -> n.cell <- Three (y, z, x) | Node cur ->
| Three _ -> let n = cur.prev in (* last node *)
let elt = { cell = One x; next=d.cur; prev=n; } in match n.cell with
n.next <- elt; | One y -> n.cell <- Two (y, x)
d.cur.prev <- elt | Two (y,z) -> n.cell <- Three (y, z, x)
| Three _ ->
let elt = { cell = One x; next=cur; prev=n; } in
n.next <- elt;
cur.prev <- elt
let peek_front_opt d = match d.cur.cell with let peek_front_opt d =
| Zero -> None match d.cur with
| One x -> Some x | Empty -> None
| Two (x,_) -> Some x | Node cur ->
| Three (x,_,_) -> Some x match cur.cell with
| One x -> Some x
| Two (x,_) -> Some x
| Three (x,_,_) -> Some x
let peek_front d = match peek_front_opt d with let peek_front d = match peek_front_opt d with
| None -> raise Empty | None -> raise Empty
@ -135,12 +139,13 @@ let peek_front d = match peek_front_opt d with
*) *)
let peek_back_opt d = let peek_back_opt d =
if is_empty d then None match d.cur with
else match d.cur.prev.cell with | Empty -> None
| Zero -> assert false | Node cur ->
| One x -> Some x match cur.prev.cell with
| Two (_,x) -> Some x | One x -> Some x
| Three (_,_,x) -> Some x | Two (_,x) -> Some x
| Three (_,_,x) -> Some x
let peek_back d = match peek_back_opt d with let peek_back d = match peek_back_opt d with
| None -> raise Empty | None -> raise Empty
@ -164,10 +169,9 @@ let peek_back d = match peek_back_opt d with
*) *)
let take_back_node_ n = match n.cell with let take_back_node_ n = match n.cell with
| Zero -> assert false | One x -> (true, x)
| One x -> n.cell <- Zero; x | Two (x,y) -> n.cell <- One x; (false, y)
| Two (x,y) -> n.cell <- One x; y | Three (x,y,z) -> n.cell <- Two (x,y); (false, z)
| Three (x,y,z) -> n.cell <- Two (x,y); z
let remove_node_ n = let remove_node_ n =
let next = n.next in let next = n.next in
@ -175,20 +179,24 @@ let remove_node_ n =
next.prev <- n.prev next.prev <- n.prev
let take_back_opt d = let take_back_opt d =
if is_empty d then None match d.cur with
else if Stdlib.(==) d.cur d.cur.prev | Empty -> None
then ( | Node cur ->
(* only one cell *) if Stdlib.(==) cur cur.prev
decr_size_ d; then (
Some (take_back_node_ d.cur) (* only one cell *)
) else ( decr_size_ d;
let n = d.cur.prev in let is_zero, x = take_back_node_ cur in
let x = take_back_node_ n in if is_zero then d.cur <- Empty;
decr_size_ d; Some x
(* remove previous node *) ) else (
if is_zero_ n then remove_node_ n; let n = cur.prev in
Some x let is_zero, x = take_back_node_ n in
) decr_size_ d;
(* remove previous node *)
if is_zero then remove_node_ n;
Some x
)
let take_back d = match take_back_opt d with let take_back d = match take_back_opt d with
| None -> raise Empty | None -> raise Empty
@ -202,32 +210,35 @@ let take_back d = match take_back_opt d with
*) *)
let take_front_node_ n = match n.cell with let take_front_node_ n = match n.cell with
| Zero -> assert false | One x -> (true, x)
| One x -> n.cell <- Zero; x | Two (x,y) -> n.cell <- One y; (false, x)
| Two (x,y) -> n.cell <- One y; x | Three (x,y,z) -> n.cell <- Two (y,z); (false, x)
| Three (x,y,z) -> n.cell <- Two (y,z); x
(*$T (*$T
let q = of_list [1;2;3] in take_front q = 1 && to_list q = [2;3] let q = of_list [1;2;3] in take_front q = 1 && to_list q = [2;3]
*) *)
let take_front_opt d = let take_front_opt d =
if is_empty d then None match d.cur with
else if Stdlib.(==) d.cur.prev d.cur | Empty -> None
then ( | Node cur ->
(* only one cell *) if Stdlib.(==) cur.prev cur
decr_size_ d; then (
Some (take_front_node_ d.cur) (* only one cell *)
) else ( decr_size_ d;
decr_size_ d; let is_zero, x = take_front_node_ cur in
let x = take_front_node_ d.cur in if is_zero then d.cur <- Empty;
if is_zero_ d.cur then ( Some x
d.cur.prev.next <- d.cur.next; ) else (
d.cur.next.prev <- d.cur.prev; decr_size_ d;
d.cur <- d.cur.next; let is_zero, x = take_front_node_ cur in
); if is_zero then (
Some x cur.prev.next <- cur.next;
) cur.next.prev <- cur.prev;
d.cur <- Node cur.next;
);
Some x
)
let take_front d = match take_front_opt d with let take_front d = match take_front_opt d with
| None -> raise Empty | None -> raise Empty
@ -246,28 +257,30 @@ let remove_front d = ignore (take_front_opt d)
*) *)
let update_front d f = let update_front d f =
match d.cur.cell with match d.cur with
| Zero -> () | Empty -> ()
| One x -> | Node cur ->
begin match f x with match cur.cell with
| None -> if Stdlib.(!=) d.cur.prev d.cur then ( | One x ->
d.cur.prev.next <- d.cur.next; begin match f x with
d.cur.next.prev <- d.cur.prev; | None -> if Stdlib.(!=) cur.prev cur then (
d.cur <- d.cur.next; cur.prev.next <- cur.next;
) cur.next.prev <- cur.prev;
else d.cur.cell <- Zero d.cur <- Node cur.next;
| Some x -> d.cur.cell <- One x )
end else d.cur <- Empty
| Two (x, y) -> | Some x -> cur.cell <- One x
begin match f x with end
| None -> d.cur.cell <- One (y) | Two (x, y) ->
| Some x -> d.cur.cell <- Two (x,y) begin match f x with
end | None -> cur.cell <- One (y)
| Three (x,y,z) -> | Some x -> cur.cell <- Two (x,y)
begin match f x with end
| None -> d.cur.cell <- Two (y,z) | Three (x,y,z) ->
| Some x -> d.cur.cell <- Three (x,y,z) begin match f x with
end | None -> cur.cell <- Two (y,z)
| Some x -> cur.cell <- Three (x,y,z)
end
(*$T update_front (*$T update_front
let q = of_list [1;2;3;4;5;6;7] in update_front q (fun _ -> None); to_list q = [2;3;4;5;6;7] let q = of_list [1;2;3;4;5;6;7] in update_front q (fun _ -> None); to_list q = [2;3;4;5;6;7]
@ -287,25 +300,27 @@ let update_front d f =
*) *)
let update_back d f = let update_back d f =
let n = d.cur.prev in match d.cur with
match n.cell with | Empty -> ()
| Zero -> () | Node cur ->
| One x -> let n = cur.prev in
begin match f x with match n.cell with
| None -> if Stdlib.(!=) d.cur.prev d.cur then remove_node_ n | One x ->
else n.cell <- Zero begin match f x with
| Some x -> n.cell <- One x | None -> if Stdlib.(!=) cur.prev cur then remove_node_ n
end else d.cur <- Empty
| Two (x, y) -> | Some x -> n.cell <- One x
begin match f y with end
| None -> n.cell <- One (x) | Two (x, y) ->
| Some y -> n.cell <- Two (x,y) begin match f y with
end | None -> n.cell <- One (x)
| Three (x,y,z) -> | Some y -> n.cell <- Two (x,y)
begin match f z with end
| None -> n.cell <- Two (x,y) | Three (x,y,z) ->
| Some z -> n.cell <- Three (x,y,z) begin match f z with
end | None -> n.cell <- Two (x,y)
| Some z -> n.cell <- Three (x,y,z)
end
(*$T update_back (*$T update_back
let q = of_list [1;2;3;4;5;6;7] in update_back q (fun _ -> None); to_list q = [1;2;3;4;5;6] let q = of_list [1;2;3;4;5;6;7] in update_back q (fun _ -> None); to_list q = [1;2;3;4;5;6]
@ -327,14 +342,16 @@ let update_back d f =
let iter f d = let iter f d =
let rec iter f ~first n = let rec iter f ~first n =
begin match n.cell with begin match n.cell with
| Zero -> ()
| One x -> f x | One x -> f x
| Two (x,y) -> f x; f y | Two (x,y) -> f x; f y
| Three (x,y,z) -> f x; f y; f z | Three (x,y,z) -> f x; f y; f z
end; end;
if n.next != first then iter f ~first n.next if n.next != first then iter f ~first n.next
in in
iter f ~first:d.cur d.cur match d.cur with
| Empty -> ()
| Node cur ->
iter f ~first:cur cur
(*$T (*$T
let n = ref 0 in iter (fun _ -> incr n) (of_list [1;2;3]); !n = 3 let n = ref 0 in iter (fun _ -> incr n) (of_list [1;2;3]); !n = 3
@ -362,14 +379,16 @@ let append_back ~into q = iter (push_back into) q
let fold f acc d = let fold f acc d =
let rec aux ~first f acc n = let rec aux ~first f acc n =
let acc = match n.cell with let acc = match n.cell with
| Zero -> acc
| One x -> f acc x | One x -> f acc x
| Two (x,y) -> f (f acc x) y | Two (x,y) -> f (f acc x) y
| Three (x,y,z) -> f (f (f acc x) y) z | Three (x,y,z) -> f (f (f acc x) y) z
in in
if Stdlib.(==) n.next first then acc else aux ~first f acc n.next if Stdlib.(==) n.next first then acc else aux ~first f acc n.next
in in
aux ~first:d.cur f acc d.cur match d.cur with
| Empty -> acc
| Node cur ->
aux ~first:cur f acc cur
(*$T (*$T
fold (+) 0 (of_list [1;2;3]) = 6 fold (+) 0 (of_list [1;2;3]) = 6
@ -436,46 +455,46 @@ let to_rev_list q = fold (fun l x -> x::l) [] q
let to_list q = List.rev (to_rev_list q) let to_list q = List.rev (to_rev_list q)
let size_cell_ = function let size_cell_ = function
| Zero -> 0
| One _ -> 1 | One _ -> 1
| Two _ -> 2 | Two _ -> 2
| Three _ -> 3 | Three _ -> 3
(* filter over a cell *) (* filter over a cell *)
let filter_cell_ f = function let filter_cell_ f = function
| Zero -> Zero | One x as c -> if f x then Some c else None
| One x as c -> if f x then c else Zero
| Two (x,y) as c -> | Two (x,y) as c ->
let fx = f x in let fx = f x in
let fy = f y in let fy = f y in
begin match fx, fy with begin match fx, fy with
| true, true -> c | true, true -> Some c
| true, false -> One x | true, false -> Some (One x)
| false, true -> One y | false, true -> Some (One y)
| _ -> Zero | _ -> None
end end
| Three (x,y,z) as c -> | Three (x,y,z) as c ->
let fx = f x in let fx = f x in
let fy = f y in let fy = f y in
let fz = f z in let fz = f z in
begin match fx, fy, fz with begin match fx, fy, fz with
| true, true, true -> c | true, true, true -> Some c
| true, true, false -> Two (x,y) | true, true, false -> Some (Two (x,y))
| true, false, true -> Two (x,z) | true, false, true -> Some (Two (x,z))
| true, false, false -> One x | true, false, false -> Some (One x)
| false, true, true -> Two (y,z) | false, true, true -> Some (Two (y,z))
| false, true, false -> One y | false, true, false -> Some (One y)
| false, false, true -> One z | false, false, true -> Some (One z)
| false, false, false -> Zero | false, false, false -> None
end end
let filter_in_place (d:_ t) f : unit = let filter_in_place (d:_ t) f : unit =
(* update size, compute new cell *) (* update size, compute new cell *)
let update_local_ n = let update_local_ n =
d.size <- d.size - size_cell_ n.cell; d.size <- d.size - size_cell_ n.cell;
let new_cell = filter_cell_ f n.cell in match filter_cell_ f n.cell with
d.size <- d.size + size_cell_ new_cell; | None -> None
new_cell |Some n as new_cell->
d.size <- d.size + size_cell_ n;
new_cell
in in
let rec loop ~stop_at n : unit = let rec loop ~stop_at n : unit =
if n != stop_at then ( if n != stop_at then (
@ -484,21 +503,43 @@ let filter_in_place (d:_ t) f : unit =
let new_cell = update_local_ n in let new_cell = update_local_ n in
(* merge into previous cell *) (* merge into previous cell *)
begin match n_prev.cell, new_cell with begin match n_prev.cell, new_cell with
| _, Zero -> remove_node_ n | _, None -> remove_node_ n
| Zero, _ -> remove_node_ n; n_prev.cell <- new_cell; | Three _, Some new_cell -> n.cell <- new_cell
| Three _, _ -> n.cell <- new_cell | One x, Some (One y) -> remove_node_ n; n_prev.cell <- Two (x,y)
| One x, One y -> remove_node_ n; n_prev.cell <- Two (x,y) | One (x), Some (Two (y,z))
| One (x), Two (y,z) | Two (x,y), Some (One z) -> remove_node_ n; n_prev.cell <- Three (x,y,z)
| Two (x,y), One z -> remove_node_ n; n_prev.cell <- Three (x,y,z) | One x, Some (Three (y,z,w))
| One x, Three (y,z,w) | Two (x,y), Some (Two (z,w)) -> n_prev.cell <- Three (x,y,z); n.cell <- One w
| Two (x,y), Two (z,w) -> n_prev.cell <- Three (x,y,z); n.cell <- One w | Two (x,y), Some (Three (z,w1,w2)) -> n_prev.cell <- Three (x,y,z); n.cell <- Two (w1,w2)
| Two (x,y), Three (z,w1,w2) -> n_prev.cell <- Three (x,y,z); n.cell <- Two (w1,w2)
end; end;
loop ~stop_at n_next; loop ~stop_at n_next;
); );
in in
d.cur.cell <- update_local_ d.cur; (* special case for first cell *) let rec new_first_cell ~stop_at n =
loop ~stop_at:d.cur d.cur.next if n != stop_at then (
match update_local_ n with
| None ->
new_first_cell ~stop_at n.next
| Some c ->
n.cell <- c; Some n
) else None
in
match d.cur with
| Empty -> ()
| Node cur ->
(* special case for first cell *)
match update_local_ cur with
| None ->
begin match new_first_cell ~stop_at:cur cur.next with
| None -> d.cur <- Empty
| Some n ->
cur.prev.next <- n;
n.prev <- cur.prev;
d.cur <- Node n;
loop ~stop_at:n n.next
end
| Some c -> cur.cell <- c;
loop ~stop_at:cur cur.next
(*$R (*$R
let q = of_list [1;2;3;4;5;6] in let q = of_list [1;2;3;4;5;6] in
@ -546,22 +587,25 @@ let of_gen g =
q q
let to_gen q = let to_gen q =
let first = q.cur in match q.cur with
let cell = ref q.cur.cell in | Empty -> (fun () -> None)
let cur = ref q.cur in | Node cur ->
let rec next () = match !cell with let first = cur in
| Zero when Stdlib.(==) (!cur).next first -> None let cell = ref (Some cur.cell) in
| Zero -> let cur = ref cur in
(* go to next node *) let rec next () = match !cell with
let n = !cur in | None when Stdlib.(==) (!cur).next first -> None
cur := n.next; | None ->
cell := n.next.cell; (* go to next node *)
next () let n = !cur in
| One x -> cell := Zero; Some x cur := n.next;
| Two (x,y) -> cell := One y; Some x cell := Some (n.next.cell);
| Three (x,y,z) -> cell := Two (y,z); Some x next ()
in | Some (One x) -> cell := None; Some x
next | Some (Two (x,y)) -> cell := Some (One y); Some x
| Some (Three (x,y,z)) -> cell := Some (Two (y,z)); Some x
in
next
(*$T (*$T
of_list [1;2;3] |> to_gen |> of_gen |> to_list = [1;2;3] of_list [1;2;3] |> to_gen |> of_gen |> to_list = [1;2;3]
@ -627,3 +671,4 @@ let pp pp_x out d =
pp_x out x pp_x out x
) d; ) d;
Format.fprintf out "}@]" Format.fprintf out "}@]"