Some functions, mostly for lazy lists (#854)

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

libs/base/Data/List.idr

@@ -4,6 +4,8 @@ import Data.Nat
 import Data.List1
 import Data.Fin
 
+%default total
+
 public export
 isNil : List a -> Bool
 isNil [] = True
@@ -71,12 +73,18 @@ index' (_::xs) (FS i) = index' xs i
 ||| Generate a list by repeatedly applying a partial function until exhausted.
 ||| @ f the function to iterate
 ||| @ x the initial value that will be the head of the list
+covering
 public export
 iterate : (f : a -> Maybe a) -> (x : a) -> List a
 iterate f x  = x :: case f x of
   Nothing => []
   Just y => iterate f y
 
+public export
+iterateN : Nat -> (a -> a) -> a -> List a
+iterateN Z     _ _ = []
+iterateN (S n) f x = x :: iterateN n f (f x)
+
 public export
 takeWhile : (p : a -> Bool) -> List a -> List a
 takeWhile p []      = []

libs/base/Data/List/Quantifiers.idr

@@ -3,6 +3,8 @@ module Data.List.Quantifiers
 import Data.List
 import Data.List.Elem
 
+%default total
+
 ||| A proof that some element of a list satisfies some property
 |||
 ||| @ p the property to be satisfied

libs/contrib/Data/List/Lazy.idr

@@ -10,6 +10,8 @@ data LazyList : Type -> Type where
   Nil : LazyList a
   (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
 
+--- Interface implementations ---
+
 public export
 Semigroup (LazyList a) where
   [] <+> ys = ys
@@ -53,3 +55,59 @@ public export
 traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
 traverse g [] = pure []
 traverse g (x :: xs) = [| g x :: traverse g xs |]
+
+public export
+sequence : Applicative f => LazyList (f a) -> f (List a)
+sequence = traverse id
+
+--- Lists creation ---
+
+public export
+fromList : List a -> LazyList a
+fromList []      = []
+fromList (x::xs) = x :: fromList xs
+
+covering
+public export
+iterate : (f : a -> Maybe a) -> (x : a) -> LazyList a
+iterate f x = x :: case f x of
+  Nothing => []
+  Just y  => iterate f y
+
+public export
+iterateN : Nat -> (a -> a) -> a -> LazyList a
+iterateN Z     _ _ = []
+iterateN (S n) f x = x :: iterateN n f (f x)
+
+public export
+replicate : (n : Nat) -> (x : a) -> LazyList a
+replicate Z     _ = []
+replicate (S n) x = x :: replicate n x
+
+--- Functions for acquiring different types of sublists ---
+
+public export
+take : Nat -> LazyList a -> LazyList a
+take (S k) (x::xs) = x :: take k xs
+take _ _ = []
+
+public export
+drop : Nat -> LazyList a -> LazyList a
+drop Z     xs      = xs
+drop (S _) []      = []
+drop (S n) (_::xs) = drop n xs
+
+public export
+takeWhile : (a -> Bool) -> LazyList a -> LazyList a
+takeWhile p []      = []
+takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
+
+public export
+dropWhile : (a -> Bool) -> LazyList a -> LazyList a
+dropWhile p []      = []
+dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
+
+public export
+filter : (a -> Bool) -> LazyList a -> LazyList a
+filter p []      = []
+filter p (x::xs) = if p x then x :: filter p xs else filter p xs