From 0a58e552878a78a62dacfa71e0bfb4eec71c2671 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 May 2017 20:26:29 +0200 Subject: [PATCH] large refactor of `CCSimple_queue` (close #125) --- src/data/CCSimple_queue.ml | 158 ++++++++++++++++++++++++++++++++---- src/data/CCSimple_queue.mli | 37 ++++++++- 2 files changed, 174 insertions(+), 21 deletions(-) diff --git a/src/data/CCSimple_queue.ml b/src/data/CCSimple_queue.ml index 0b16449b..7bc68efd 100644 --- a/src/data/CCSimple_queue.ml +++ b/src/data/CCSimple_queue.ml @@ -3,6 +3,11 @@ (** {1 Functional queues (fifo)} *) +type 'a sequence = ('a -> unit) -> unit +type 'a printer = Format.formatter -> 'a -> unit +type 'a klist = unit -> [`Nil | `Cons of 'a * 'a klist] +type 'a gen = unit -> 'a option + type 'a t = { hd : 'a list; tl : 'a list; @@ -14,19 +19,19 @@ let empty = { } (* invariant: if hd=[], then tl=[] *) -let _make hd tl = match hd with +let make_ hd tl = match hd with | [] -> {hd=List.rev tl; tl=[] } | _::_ -> {hd; tl; } let is_empty q = q.hd = [] -let push x q = {q with tl = x :: q.tl; } +let push x q = make_ q.hd (x :: q.tl) let snoc q x = push x q let peek_exn q = match q.hd with - | [] -> assert (q.tl = []); raise (Invalid_argument "Queue.peek") + | [] -> assert (q.tl = []); invalid_arg "Queue.peek" | x::_ -> x let peek q = match q.hd with @@ -35,45 +40,162 @@ let peek q = match q.hd with let pop_exn q = match q.hd with - | [] -> assert (q.tl = []); raise (Invalid_argument "Queue.peek") + | [] -> assert (q.tl = []); invalid_arg "Queue.peek" | x::hd' -> - let q' = _make hd' q.tl in + let q' = make_ hd' q.tl in x, q' let pop q = try Some (pop_exn q) with Invalid_argument _ -> None +(*$Q + Q.(list small_int) (fun l -> \ + let q = of_list l in \ + equal CCInt.equal (Gen.unfold pop q |> of_gen) q) + *) + let junk q = try let _, q' = pop_exn q in q' with Invalid_argument _ -> q -(** Append two queues. Elements from the second one come - after elements of the first one *) -let append q1 q2 = - { hd=q1.hd; - tl=q2.tl @ (List.rev_append q2.hd q1.tl); - } - let map f q = { hd=List.map f q.hd; tl=List.map f q.tl; } -let size q = List.length q.hd + List.length q.tl +let rev q = make_ q.tl q.hd -let (>|=) q f = map f q +(*$Q + Q.(list small_int) (fun l -> \ + equal CCInt.equal (of_list l |> rev) (of_list (List.rev l))) + Q.(list small_int) (fun l -> \ + let q = of_list l in \ + equal CCInt.equal q (q |> rev |> rev)) +*) + +let length q = List.length q.hd + List.length q.tl + +(*$Q + Q.(list small_int)(fun l -> \ + length (of_list l) = List.length l) +*) + +(*$Q + Q.(list small_int)(fun l -> \ + equal CCInt.equal (of_list l) (List.fold_left snoc empty l)) +*) let fold f acc q = let acc' = List.fold_left f acc q.hd in List.fold_right (fun x acc -> f acc x) q.tl acc' -let iter f q = fold (fun () x -> f x) () q +(* iterate on a list in reverse order *) +let rec rev_iter_ f l = match l with + | [] -> () + | x :: tl -> rev_iter_ f tl; f x -type 'a sequence = ('a -> unit) -> unit +let iter f q = + List.iter f q.hd; + rev_iter_ f q.tl + +let to_list q = fold (fun acc x->x::acc) [] q |> List.rev + +let add_list q l = List.fold_left snoc q l +let of_list l = add_list empty l let to_seq q = fun k -> iter k q -let of_seq seq = - let q = ref empty in +let add_seq q seq = + let q = ref q in seq (fun x -> q := push x !q); !q + +let of_seq s = add_seq empty s + +(*$Q + Q.(list small_int) (fun l -> \ + equal CCInt.equal \ + (of_seq (Sequence.of_list l)) \ + (of_list l)) + Q.(list small_int) (fun l -> \ + l = (of_list l |> to_seq |> Sequence.to_list)) +*) + +let rec klist_iter_ k f = match k() with + | `Nil -> () + | `Cons (x,tl) -> f x; klist_iter_ tl f + +let add_klist q l = add_seq q (klist_iter_ l) +let of_klist l = add_klist empty l + +let to_klist q = + let rec aux1 l () = match l with + | [] -> aux2 (List.rev q.tl) () + | x :: tl -> `Cons (x, aux1 tl) + and aux2 l () = match l with + | [] -> `Nil + | x :: tl -> `Cons (x, aux2 tl) + in + aux1 q.hd + +let rec gen_iter g f = match g() with + | None -> () + | Some x -> f x; gen_iter g f + +let add_gen q g = add_seq q (gen_iter g) +let of_gen g = add_gen empty g + +let to_gen q = + let st = ref (`Left q.hd) in + let rec aux () = match !st with + | `Stop -> None + | `Left [] -> st := `Right q.tl; aux() + | `Left (x::tl) -> st := `Left tl; Some x + | `Right [] -> st := `Stop; None + | `Right (x::tl) -> st := `Right tl; Some x + in + aux + +let rec klist_equal eq l1 l2 = match l1(), l2() with + | `Nil, `Nil -> true + | `Nil, _ + | _, `Nil -> false + | `Cons (x1,l1'), `Cons (x2,l2') -> + eq x1 x2 && klist_equal eq l1' l2' + +let equal eq q1 q2 = klist_equal eq (to_klist q1) (to_klist q2) + +(*$Q + Q.(pair (list small_int)(list small_int)) (fun (l1,l2) -> \ + equal CCInt.equal (of_list l1)(of_list l2) = (l1=l2)) +*) + +let append q1 q2 = + add_seq q1 + (fun yield -> + to_seq q2 yield) + +(*$Q + Q.(pair (list small_int)(list small_int)) (fun (l1,l2) -> \ + equal CCInt.equal \ + (append (of_list l1)(of_list l2)) \ + (of_list (List.append l1 l2))) + *) + +module Infix = struct + let (>|=) q f = map f q + let (<::) = snoc + let (@) = append +end + +include Infix + +(** {2 IO} *) + +let pp ?(sep=fun out () -> Format.fprintf out ",@ ") pp_item out l = + let first = ref true in + iter + (fun x -> + if !first then first := false else sep out (); + pp_item out x) + l diff --git a/src/data/CCSimple_queue.mli b/src/data/CCSimple_queue.mli index 1b3085af..35dc801b 100644 --- a/src/data/CCSimple_queue.mli +++ b/src/data/CCSimple_queue.mli @@ -6,6 +6,11 @@ (** Simple implementation of functional queues @since NEXT_RELEASE *) +type 'a sequence = ('a -> unit) -> unit +type 'a printer = Format.formatter -> 'a -> unit +type 'a klist = unit -> [`Nil | `Cons of 'a * 'a klist] +type 'a gen = unit -> 'a option + type +'a t (** Queue containing elements of type 'a *) @@ -44,16 +49,42 @@ val append : 'a t -> 'a t -> 'a t val map : ('a -> 'b) -> 'a t -> 'b t (** Map values *) -val (>|=) : 'a t -> ('a -> 'b) -> 'b t +val rev : 'a t -> 'a t +(** Reverse the queue. Constant time. *) -val size : 'a t -> int +val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool + +module Infix : sig + val (>|=) : 'a t -> ('a -> 'b) -> 'b t (** Alias to {!map} *) + val (@) : 'a t -> 'a t -> 'a t (** Alias to {!append} *) + val (<::) : 'a t -> 'a -> 'a t (** Alias to {!snoc} *) +end + +include module type of Infix + +val length : 'a t -> int (** Number of elements in the queue (linear in time) *) val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b val iter : ('a -> unit) -> 'a t -> unit -type 'a sequence = ('a -> unit) -> unit +val to_list : 'a t -> 'a list +val add_list : 'a t -> 'a list -> 'a t +val of_list : 'a list -> 'a t + val to_seq : 'a t -> 'a sequence +val add_seq : 'a t -> 'a sequence -> 'a t val of_seq : 'a sequence -> 'a t +val to_klist : 'a t -> 'a klist +val add_klist : 'a t -> 'a klist -> 'a t +val of_klist : 'a klist -> 'a t + +val of_gen : 'a gen -> 'a t +val add_gen : 'a t -> 'a gen -> 'a t +val to_gen : 'a t -> 'a gen + +(** {2 IO} *) + +val pp : ?sep:unit printer -> 'a printer -> 'a t printer