From 39824c62953fb7a437ea590f0b7c3e76fe1e8a73 Mon Sep 17 00:00:00 2001
From: Stefan Hoeck <hock@zhaw.ch>
Date: Mon, 1 Feb 2021 11:27:07 +0100
Subject: [PATCH] [new] Add Colist and Colist1 to base (#997)

---
 libs/base/Data/Colist.idr  | 220 +++++++++++++++++++++++++++++++++++++
 libs/base/Data/Colist1.idr | 203 ++++++++++++++++++++++++++++++++++
 libs/base/base.ipkg        |   2 +
 3 files changed, 425 insertions(+)
 create mode 100644 libs/base/Data/Colist.idr
 create mode 100644 libs/base/Data/Colist1.idr

diff --git a/libs/base/Data/Colist.idr b/libs/base/Data/Colist.idr
new file mode 100644
index 000000000..2d040ae6c
--- /dev/null
+++ b/libs/base/Data/Colist.idr
@@ -0,0 +1,220 @@
+module Data.Colist
+
+import Data.Maybe
+import Data.List
+import public Data.Zippable
+
+%default total
+
+||| A possibly finite Stream.
+public export
+data Colist : (a : Type) -> Type where
+  Nil : Colist a
+  (::) : a -> Inf (Colist a) -> Colist a
+
+--------------------------------------------------------------------------------
+--          Creating Colists
+--------------------------------------------------------------------------------
+
+||| Convert a list to a `Colist`.
+public export
+fromList : List a -> Colist a
+fromList []        = Nil
+fromList (x :: xs) = x :: fromList xs
+
+||| Convert a stream to a `Colist`.
+public export
+fromStream : Stream a -> Colist a
+fromStream (x :: xs) = x :: fromStream xs
+
+||| Create a `Colist` of only a single element.
+public export
+singleton : a -> Colist a
+singleton a = a :: Nil
+
+||| An infinite `Colist` of repetitions of the same element.
+public export
+repeat : a -> Colist a
+repeat v = v :: repeat v
+
+||| Create a `Colist` of `n` replications of the given element.
+public export
+replicate : Nat -> a -> Colist a
+replicate 0     _ = Nil
+replicate (S k) x = x :: replicate k x
+
+||| Produce a `Colist` by repeating a sequence.
+public export
+cycle : List a -> Colist a
+cycle Nil       = Nil
+cycle (x :: xs) = run x xs
+  where run : a -> List a -> Colist a
+        run v []        = v :: run x xs
+        run v (y :: ys) = v :: run y ys
+
+||| Generate an infinite `Colist` by repeatedly applying a function.
+public export
+iterate : (a -> a) -> a -> Colist a
+iterate f a = a :: iterate f (f a)
+
+||| Generate a `Colist` by repeatedly applying a function.
+||| This stops once the function returns `Nothing`.
+public export
+iterateMaybe : (f : a -> Maybe a) -> Maybe a -> Colist a
+iterateMaybe _ Nothing  = Nil
+iterateMaybe f (Just x) = x :: iterateMaybe f (f x)
+
+||| Generate an `Colist` by repeatedly applying a function
+||| to a seed value.
+||| This stops once the function returns `Nothing`.
+public export
+unfold : (f : s -> Maybe (s,a)) -> s -> Colist a
+unfold f s = case f s of
+                  Just (s2,a) => a :: unfold f s2
+                  Nothing     => Nil
+
+--------------------------------------------------------------------------------
+--          Basic Functions
+--------------------------------------------------------------------------------
+
+||| True, if this is the empty `Colist`.
+public export
+isNil : Colist a -> Bool
+isNil [] = True
+isNil _  = False
+
+||| True, if the given `Colist` is non-empty.
+public export
+isCons : Colist a -> Bool
+isCons [] = False
+isCons _  = True
+
+||| Concatenate two `Colist`s.
+public export
+append : Colist a -> Colist a -> Colist a
+append []        ys = ys
+append (x :: xs) ys = x :: append xs ys
+
+||| Append a `Colist` to a `List`.
+public export
+lappend : List a -> Colist a -> Colist a
+lappend xs = append (fromList xs)
+
+||| Append a `List` to a `Colist`.
+public export
+appendl : Colist a -> List a -> Colist a
+appendl xs = append xs . fromList
+
+||| Try to extract the first element from a `Colist`.
+public export
+head : Colist a -> Maybe a
+head []       = Nothing
+head (x :: _) = Just x
+
+||| Try to drop the first element from a `Colist`.
+||| This returns `Nothing` if the given `Colist` is
+||| empty.
+public export
+tail : Colist a -> Maybe (Colist a)
+tail []        = Nothing
+tail (_ :: xs) = Just xs
+
+||| Take up to `n` elements from a `Colist`.
+public export
+take : (n : Nat) -> Colist a -> List a
+take 0     _         = Nil
+take (S k) []        = Nil
+take (S k) (x :: xs) = x :: take k xs
+
+||| Take elements from a `Colist` up to and including the
+||| first element, for which `p` returns `True`.
+public export
+takeUntil : (p : a -> Bool) -> Colist a -> Colist a
+takeUntil _ []        = Nil
+takeUntil p (x :: xs) = if p x then [x] else x :: takeUntil p xs
+
+||| Take elements from a `Colist` up to (but not including) the
+||| first element, for which `p` returns `True`.
+public export
+takeBefore : (a -> Bool) -> Colist a -> Colist a
+takeBefore _ []        = Nil
+takeBefore p (x :: xs) = if p x then [] else x :: takeBefore p xs
+
+||| Take elements from a `Colist` while the given predicate
+||| returns `True`.
+public export
+takeWhile : (a -> Bool) -> Colist a -> Colist a
+takeWhile p = takeBefore (not . p)
+
+||| Extract all values wrapped in `Just` from the beginning
+||| of a `Colist`. This stops, once the first `Nothing` is encountered.
+public export
+takeWhileJust : Colist (Maybe a) -> Colist a
+takeWhileJust []              = []
+takeWhileJust (Nothing :: _)  = []
+takeWhileJust (Just x  :: xs) = x :: takeWhileJust xs
+
+||| Drop up to `n` elements from the beginning of the `Colist`.
+public export
+drop : (n : Nat) -> Colist a -> Colist a
+drop _ []            = Nil
+drop 0           xs  = xs
+drop (S k) (x :: xs) = drop k xs
+
+||| Try to extract the `n`-th element from a `Colist`.
+public export
+index : (n : Nat) -> Colist a -> Maybe a
+index _     []        = Nothing
+index 0     (x :: _)  = Just x
+index (S k) (_ :: xs) = index k xs
+
+||| Produce a `Colist` of left folds of prefixes of the given `Colist`.
+||| @ f the combining function
+||| @ acc the initial value
+||| @ xs the `Colist` to process
+public export
+scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist b) -> Colist a
+scanl _ acc Nil       = [acc]
+scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
+
+--------------------------------------------------------------------------------
+--          Implementations
+--------------------------------------------------------------------------------
+
+public export
+Semigroup (Colist a) where
+  (<+>) = append
+
+public export
+Monoid (Colist a) where
+  neutral = Nil
+
+public export
+Functor Colist where
+  map f []        = []
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Applicative Colist where
+  pure = repeat
+
+  [] <*> _  = []
+  _  <*> [] = []
+  f :: fs <*> a :: as = f a :: (fs <*> as)
+
+public export
+Zippable Colist where
+  zipWith f as bs = [| f as bs |]
+
+  zipWith3 f as bs cs = [| f as bs cs |]
+
+  unzip xs = (map fst xs, map snd xs)
+
+  unzip3 xs = ( map (\(a,_,_) => a) xs
+              , map (\(_,b,_) => b) xs
+              , map (\(_,_,c) => c) xs
+              )
+
+  unzipWith f = unzip . map f
+
+  unzipWith3 f = unzip3 . map f
diff --git a/libs/base/Data/Colist1.idr b/libs/base/Data/Colist1.idr
new file mode 100644
index 000000000..1c63e8681
--- /dev/null
+++ b/libs/base/Data/Colist1.idr
@@ -0,0 +1,203 @@
+module Data.Colist1
+
+import Data.Colist
+import Data.List1
+import Data.Nat
+import public Data.Zippable
+
+%default total
+
+||| A possibly finite, non-empty Stream.
+public export
+data Colist1 : (a : Type) -> Type where
+  (:::) : a -> Colist a -> Colist1 a
+
+--------------------------------------------------------------------------------
+--          Creating Colist1
+--------------------------------------------------------------------------------
+
+||| Convert a `List1` to a `Colist1`.
+public export
+fromList1 : List1 a -> Colist1 a
+fromList1 (h ::: t) = h ::: fromList t
+
+||| Convert a stream to a `Colist1`.
+public export
+fromStream : Stream a -> Colist1 a
+fromStream (x :: xs) = x ::: fromStream xs
+
+||| Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
+||| the given `Colist` is empty.
+public export
+fromColist : Colist a -> Maybe (Colist1 a)
+fromColist Nil       = Nothing
+fromColist (x :: xs) = Just (x ::: xs)
+
+||| Try to convert a list to a `Colist1`. Returns `Nothing` if
+||| the given list is empty.
+public export
+fromList : List a -> Maybe (Colist1 a)
+fromList = fromColist . fromList
+
+||| Create a `Colist1` of only a single element.
+public export
+singleton : a -> Colist1 a
+singleton a = a ::: Nil
+
+||| An infinite `Colist1` of repetitions of the same element.
+public export
+repeat : a -> Colist1 a
+repeat v = v ::: repeat v
+
+||| Create a `Colist1` of `n` replications of the given element.
+public export
+replicate : (n : Nat) -> {auto 0 prf : IsSucc n} -> a -> Colist1 a
+replicate 0     _ impossible
+replicate (S k) x = x ::: replicate k x
+
+||| Produce a `Colist1` by repeating a sequence
+public export
+cycle : List1 a -> Colist1 a
+cycle (x ::: xs) = x ::: cycle (xs ++ [x])
+
+||| Generate an infinite `Colist1` by repeatedly applying a function.
+public export
+iterate : (f : a -> a) -> a -> Colist1 a
+iterate f a  = a ::: iterate f (f a)
+
+||| Generate a `Colist1` by repeatedly applying a function.
+||| This stops once the function returns `Nothing`.
+public export
+iterateMaybe : (f : a -> Maybe a) -> a -> Colist1 a
+iterateMaybe f a  = a ::: iterateMaybe f (f a)
+
+||| Generate a `Colist1` by repeatedly applying a function
+||| to a seed value.
+||| This stops once the function returns `Nothing`.
+public export
+unfold : (f : s -> Maybe (s,a)) -> s -> a -> Colist1 a
+unfold f s a = a ::: unfold f s
+
+--------------------------------------------------------------------------------
+--          Basic Functions
+--------------------------------------------------------------------------------
+
+||| Convert a `Colist1` to a `Colist`
+public export
+forget : Colist1 a -> Colist a
+forget (h ::: t) = h :: t
+
+||| Prepends an element to a `Colist1`.
+public export
+cons : (x : a) -> (xs : Colist1 a) -> Colist1 a
+cons x xs = x ::: forget xs
+
+||| Concatenate two `Colist1`s
+public export
+append : Colist1 a -> Colist1 a -> Colist1 a
+append (h ::: t) ys = h ::: append t (forget ys)
+
+||| Append a `Colist1` to a `List`.
+public export
+lappend : List a -> Colist1 a -> Colist1 a
+lappend Nil       ys = ys
+lappend (x :: xs) ys = x ::: lappend xs (forget ys)
+
+||| Append a `List` to a `Colist1`.
+public export
+appendl : Colist1 a -> List a -> Colist1 a
+appendl (x ::: xs) ys = x ::: appendl xs ys
+
+||| Extract the first element from a `Colist1`
+public export
+head : Colist1 a -> a
+head (h ::: _) = h
+
+||| Drop the first element from a `Colist1`
+public export
+tail : Colist1 a -> Colist a
+tail (_ ::: t) = t
+
+||| Take up to `n` elements from a `Colist1`
+public export
+take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
+take 0     _          impossible
+take (S k) (x ::: xs) = x ::: take k xs
+
+||| Take elements from a `Colist1` up to and including the
+||| first element, for which `p` returns `True`.
+public export
+takeUntil : (p : a -> Bool) -> Colist1 a -> Colist1 a
+takeUntil p (x ::: xs) = if p x then singleton x else x ::: takeUntil p xs
+
+||| Take elements from a `Colist1` up to (but not including) the
+||| first element, for which `p` returns `True`.
+public export
+takeBefore : (p : a -> Bool) -> Colist1 a -> Colist a
+takeBefore p = takeBefore p . forget
+
+||| Take elements from a `Colist1` while the given predicate `p`
+||| returns `True`.
+public export
+takeWhile : (p : a -> Bool) -> Colist1 a -> Colist a
+takeWhile p = takeWhile p . forget
+
+||| Extract all values wrapped in `Just` from the beginning
+||| of a `Colist1`. This stops, once the first `Nothing` is encountered.
+public export
+takeWhileJust : Colist1 (Maybe a) -> Colist a
+takeWhileJust = takeWhileJust . forget
+
+||| Drop up to `n` elements from the beginning of the `Colist1`.
+public export
+drop : (n : Nat) -> Colist1 a -> Colist a
+drop n = drop n . forget
+
+||| Try to extract the `n`-th element from a `Colist1`.
+public export
+index : (n : Nat) -> Colist1 a -> Maybe a
+index n = index n . forget
+
+||| Produce a `Colist1` of left folds of prefixes of the given `Colist1`.
+||| @ f the combining function
+||| @ acc the initial value
+||| @ xs the `Colist1` to process
+export
+scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist1 b) -> Colist1 a
+scanl f acc (x ::: xs) = acc ::: scanl f (f acc x) xs
+
+--------------------------------------------------------------------------------
+--          Interfaces
+--------------------------------------------------------------------------------
+
+public export
+Semigroup (Colist1 a) where
+  (<+>) = append
+
+public export
+Functor Colist1 where
+  map f (x ::: xs) = f x ::: map f xs
+
+public export
+Applicative Colist1 where
+  pure = repeat
+
+  (f ::: fs) <*> (a ::: as) = f a ::: (fs <*> as)
+
+public export
+Zippable Colist1 where
+  zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys
+
+  zipWith3 f (x ::: xs) (y ::: ys) (z ::: zs) =
+    f x y z ::: zipWith3 f xs ys zs
+
+  unzip xs = (map fst xs, map snd xs)
+
+  unzip3 xs = ( map (\(a,_,_) => a) xs
+              , map (\(_,b,_) => b) xs
+              , map (\(_,_,c) => c) xs
+              )
+
+  unzipWith f = unzip . map f
+
+  unzipWith3 f = unzip3 . map f
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 81f40f4d9..fd56ddff0 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -28,6 +28,8 @@ modules = Control.App,
           Data.Bool,
           Data.Bool.Xor,
           Data.Buffer,
+          Data.Colist,
+          Data.Colist1,
           Data.DPair,
           Data.Either,
           Data.Fin,