From a3d763bfd9b0f0006d83fab6592251f6756b931b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 21 Apr 2016 15:20:18 +0200 Subject: [PATCH] add `CCLazy_list` in containers.iter (with a few functions) --- _oasis | 2 +- doc/intro.txt | 5 +- src/iter/CCLazy_list.ml | 109 +++++++++++++++++++++++++++++++++++++++ src/iter/CCLazy_list.mli | 57 ++++++++++++++++++++ 4 files changed, 171 insertions(+), 2 deletions(-) create mode 100644 src/iter/CCLazy_list.ml create mode 100644 src/iter/CCLazy_list.mli diff --git a/_oasis b/_oasis index 23277415..41eebafd 100644 --- a/_oasis +++ b/_oasis @@ -88,7 +88,7 @@ Library "containers_data" Library "containers_iter" Path: src/iter - Modules: CCKTree, CCKList + Modules: CCKTree, CCKList, CCLazy_list FindlibParent: containers FindlibName: iter diff --git a/doc/intro.txt b/doc/intro.txt index e72e0356..6e69309d 100644 --- a/doc/intro.txt +++ b/doc/intro.txt @@ -116,7 +116,10 @@ CCSexpM Iterators: -{!modules: CCKList CCKTree} +{!modules: +CCKList +CCKTree +CCLazy_list} {4 String} diff --git a/src/iter/CCLazy_list.ml b/src/iter/CCLazy_list.ml new file mode 100644 index 00000000..8ffcdd6a --- /dev/null +++ b/src/iter/CCLazy_list.ml @@ -0,0 +1,109 @@ + +(* This file is free software, part of containers. See file "license" for more details. *) + +(** {1 Lazy List} *) + +type +'a t = 'a node lazy_t +and +'a node = + | Nil + | Cons of 'a * 'a t + +let empty = Lazy.from_val Nil + +let return x = Lazy.from_val (Cons (x, empty)) + +let is_empty = function + | lazy Nil -> true + | lazy (Cons _) -> false + +let cons x tl = Lazy.from_val (Cons (x,tl)) + +let head = function + | lazy Nil -> None + | lazy (Cons (x, tl)) -> Some (x,tl) + +let length l = + let rec aux acc l = match l with + | lazy Nil -> acc + | lazy (Cons (_, tl)) -> aux (acc+1) tl + in + aux 0 l + +(*$Q + Q.(list int) (fun l -> length (of_list l) = List.length l) +*) + +let rec map ~f l = + lazy ( + match l with + | lazy Nil -> Nil + | lazy (Cons (x,tl)) -> Cons (f x, map ~f tl) + ) + +let rec append a b = + lazy ( + match a with + | lazy Nil -> Lazy.force b + | lazy (Cons (x,tl)) -> Cons (x, append tl b) + ) + +(*$Q + Q.(pair (list int) (list int)) (fun (l1,l2) ->\ + length (append (of_list l1) (of_list l2)) = List.length l1 + List.length l2) +*) + +let rec flat_map ~f l = + lazy ( + match l with + | lazy Nil -> Nil + | lazy (Cons (x,tl)) -> + let res = append (f x) (flat_map ~f tl) in + Lazy.force res + ) + +module Infix = struct + let (>|=) x f = map ~f x + let (>>=) x f = flat_map ~f x +end + +include Infix + +type 'a gen = unit -> 'a option + +let rec of_gen g = + lazy ( + match g() with + | None -> Nil + | Some x -> Cons (x, of_gen g) + ) + +(*$Q + Q.(list int) (fun l -> l = (Gen.of_list l |> of_gen |> to_list)) +*) + +let rec of_list = function + | [] -> empty + | x :: tl -> cons x (of_list tl) + +let to_list_rev l = + let rec aux acc = function + | lazy Nil -> acc + | lazy (Cons (x,tl)) -> aux (x::acc) tl + in + aux [] l + +let to_list l = to_list_rev l |> List.rev + +(*$Q + Q.(list int) (fun l -> l = to_list (of_list l)) +*) + +let to_gen l = + let l = ref l in + fun () -> match !l with + | lazy Nil -> None + | lazy (Cons (x,tl)) -> l := tl; Some x + +(*$Q + Q.(list int) (fun l -> l = (of_list l |> to_gen |> Gen.to_list)) +*) diff --git a/src/iter/CCLazy_list.mli b/src/iter/CCLazy_list.mli new file mode 100644 index 00000000..42f1b19b --- /dev/null +++ b/src/iter/CCLazy_list.mli @@ -0,0 +1,57 @@ + +(* This file is free software, part of containers. See file "license" for more details. *) + +(** {1 Lazy List} + + @since NEXT_RELEASE *) + +type +'a t = 'a node lazy_t +and +'a node = + | Nil + | Cons of 'a * 'a t + +val empty : 'a t +(** Empty list *) + +val return : 'a -> 'a t +(** Return a computed value *) + +val is_empty : _ t -> bool +(** Evaluates the head *) + +val length : _ t -> int +(** [length l] returns the number of elements in [l], eagerly (linear time). + Caution, will not terminate if [l] is infinite *) + +val cons : 'a -> 'a t -> 'a t + +val head : 'a t -> ('a * 'a t) option +(** Evaluate head, return it, or [None] if the list is empty *) + +val map : f:('a -> 'b) -> 'a t -> 'b t +(** Lazy map *) + +val append : 'a t -> 'a t -> 'a t +(** Lazy concatenation *) + +val flat_map : f:('a -> 'b t) -> 'a t -> 'b t +(** Monadic flatten + map *) + +module Infix : sig + val (>|=) : 'a t -> ('a -> 'b) -> 'b t + val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +end + +include module type of Infix + +type 'a gen = unit -> 'a option + +val of_gen : 'a gen -> 'a t + +val of_list : 'a list -> 'a t + +val to_list : 'a t -> 'a list + +val to_list_rev : 'a t -> 'a list + +val to_gen : 'a t -> 'a gen