From ff7008998072ec30b6f7d468305ac773d49512c8 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Sun, 24 Dec 2023 19:13:06 +0300
Subject: [PATCH] [ sync ] Synchronise lazy list impl in `src/Libraries` with
 `base`

This is to assure it is safe to remove `Libraries` implementation in the
next release. This requires synchronisation of `Data.String.Iterator` too
---
 src/Libraries/Data/List/Lazy.idr       | 168 +++++++++++++++++++++++--
 src/Libraries/Data/String/Iterator.idr |  27 +++-
 2 files changed, 178 insertions(+), 17 deletions(-)

diff --git a/src/Libraries/Data/List/Lazy.idr b/src/Libraries/Data/List/Lazy.idr
index 8f02fb8f1d..e815c4b274 100644
--- a/src/Libraries/Data/List/Lazy.idr
+++ b/src/Libraries/Data/List/Lazy.idr
@@ -2,6 +2,11 @@
 
 module Libraries.Data.List.Lazy
 
+import Data.Fuel
+import Data.Stream
+import Data.Colist
+import Data.Colist1
+
 %default total
 
 -- All functions here are public export
@@ -10,19 +15,73 @@ module Libraries.Data.List.Lazy
 public export
 data LazyList : Type -> Type where
   Nil : LazyList a
-  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
+  (::) : (x : a) -> (xs : Lazy (LazyList a)) -> LazyList a
+
+--- Truly lazy functions ---
+
+public export
+foldrLazy : (func : a -> Lazy acc -> acc) -> (init : Lazy acc) -> (input : LazyList a) -> acc
+foldrLazy _  init [] = init
+foldrLazy op init (x::xs) = x `op` foldrLazy op init xs
 
 public export
 (++) : LazyList a -> Lazy (LazyList a) -> LazyList a
-[] ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
+(++) = flip $ foldrLazy (::)
+
+-- Specialized variant of `concatMap` with both `t` and `m` being `LazyList`.
+public export
+bindLazy : (a -> LazyList b) -> LazyList a -> LazyList b
+bindLazy f = foldrLazy ((++) . f) []
+
+public export
+choice : Alternative f => LazyList (f a) -> f a
+choice = foldrLazy (<|>) empty
+
+public export
+choiceMap : Alternative f => (a -> f b) -> LazyList a -> f b
+choiceMap g = foldrLazy ((<|>) . g) empty
+
+public export
+any : (a -> Bool) -> LazyList a -> Bool
+any p = foldrLazy ((||) . p) False
+
+public export
+all : (a -> Bool) -> LazyList a -> Bool
+all p = foldrLazy ((&&) . p) True
 
 --- Interface implementations ---
 
+public export
+Eq a => Eq (LazyList a) where
+  [] == [] = True
+  x :: xs == y :: ys = x == y && xs == ys
+  _ == _ = False
+
+public export
+Ord a => Ord (LazyList a) where
+  compare [] [] = EQ
+  compare [] (x :: xs) = LT
+  compare (x :: xs) [] = GT
+  compare (x :: xs) (y :: ys)
+     = case compare x y of
+            EQ => compare xs ys
+            c => c
+
+export
+Show a => Show (LazyList a) where
+  show []       = "[]"
+  show (h :: t) = "[" ++ show' "" h t ++ "]"
+    where
+      -- Idris didn't like the lazyness involved when using the
+      -- same implementation as for `List`, therefore, this was
+      -- adjusted to first force the head and tail of the list.
+      show' : String -> a -> LazyList a -> String
+      show' acc h Nil       = acc ++ show h
+      show' acc h (x :: xs) = show' (acc ++ show h ++ ", ") x xs
+
 public export
 Semigroup (LazyList a) where
-  [] <+> ys = ys
-  (x :: xs) <+> ys = x :: (xs <+> ys)
+  xs <+> ys = xs ++ ys
 
 public export
 Monoid (LazyList a) where
@@ -36,9 +95,14 @@ Foldable LazyList where
   foldl op acc [] = acc
   foldl op acc (x :: xs) = foldl op (acc `op` x) xs
 
+  foldlM fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init
+
   null []     = True
   null (_::_) = False
 
+  foldMap f [] = neutral
+  foldMap f (x :: xs) = f x <+> foldMap f xs
+
 public export
 Functor LazyList where
   map f [] = []
@@ -47,29 +111,63 @@ Functor LazyList where
 public export
 Applicative LazyList where
   pure x = [x]
-  fs <*> vs = concatMap (\f => map f vs) fs
+  fs <*> vs = bindLazy (\f => map f vs) fs
 
 public export
 Alternative LazyList where
   empty = []
-  xs <|> ys = xs ++ ys
+  (<|>) = (++)
 
 public export
 Monad LazyList where
-  m >>= f = concatMap f m
+  m >>= f = bindLazy f m
 
 -- There is no Traversable instance for lazy lists.
 -- The result of a traversal will be a non-lazy list in general
 -- (you can't delay the "effect" of an applicative functor).
 public export
-traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
+traverse : Monad f => (a -> f b) -> LazyList a -> f (List b)
 traverse g [] = pure []
-traverse g (x :: xs) = [| g x :: traverse g xs |]
+traverse g (x::xs) = pure $ !(g x) :: !(traverse g xs)
 
-public export
-sequence : Applicative f => LazyList (f a) -> f (List a)
+public export %inline
+for : Monad f => LazyList a -> (a -> f b) -> f (List b)
+for = flip traverse
+
+public export %inline
+sequence : Monad f => LazyList (f a) -> f (List a)
 sequence = traverse id
 
+-- Traverse a lazy list with lazy effect lazily
+public export
+traverse_ : Monad m => (a -> m b) -> LazyList a -> m Unit
+traverse_ f = foldrLazy ((>>) . ignore . f) (pure ())
+
+public export %inline
+for_ : Monad m => LazyList a -> (a -> m b) -> m Unit
+for_ = flip Lazy.traverse_
+
+public export %inline
+sequence_ : Monad m => LazyList (m a) -> m Unit
+sequence_ = Lazy.traverse_ id
+
+public export
+Zippable LazyList where
+  zipWith _ [] _ = []
+  zipWith _ _ [] = []
+  zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
+
+  zipWith3 _ [] _ _ = []
+  zipWith3 _ _ [] _ = []
+  zipWith3 _ _ _ [] = []
+  zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
+
+  unzip xs = (fst <$> xs, snd <$> xs)
+  unzipWith = unzip .: map
+
+  unzip3 xs = (fst <$> xs, fst . snd <$> xs, snd . snd <$> xs)
+  unzipWith3 = unzip3 .: map
+
 --- Lists creation ---
 
 public export
@@ -108,7 +206,7 @@ head' : LazyList a -> Maybe a
 head' []     = Nothing
 head' (x::_) = Just x
 
-export
+public export
 tail' : LazyList a -> Maybe (LazyList a)
 tail' []      = Nothing
 tail' (_::xs) = Just xs
@@ -147,3 +245,47 @@ mapMaybe f []      = []
 mapMaybe f (x::xs) = case f x of
   Nothing => mapMaybe f xs
   Just y  => y :: mapMaybe f xs
+
+namespace Stream
+
+  public export
+  take : Fuel -> Stream a -> LazyList a
+  take Dry _ = []
+  take (More f) (x :: xs) = x :: take f xs
+
+namespace Colist
+
+  public export
+  take : Fuel -> Colist a -> LazyList a
+  take Dry _ = []
+  take _ [] = []
+  take (More f) (x :: xs) = x :: take f xs
+
+namespace Colist1
+
+  public export
+  take : Fuel -> Colist1 a -> LazyList a
+  take fuel as = take fuel (forget as)
+
+--- Functions for extending lists ---
+
+public export
+mergeReplicate : a -> LazyList a -> LazyList a
+mergeReplicate sep []      = []
+mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
+
+public export
+intersperse : a -> LazyList a -> LazyList a
+intersperse sep []      = []
+intersperse sep (x::xs) = x :: mergeReplicate sep xs
+
+public export
+intercalate : (sep : LazyList a) -> (xss : LazyList (LazyList a)) -> LazyList a
+intercalate sep xss = choice $ intersperse sep xss
+
+--- Functions converting lazy lists to something ---
+
+public export
+toColist : LazyList a -> Colist a
+toColist [] = []
+toColist (x::xs) = x :: toColist xs
diff --git a/src/Libraries/Data/String/Iterator.idr b/src/Libraries/Data/String/Iterator.idr
index 7ed17fa590..d7540415a7 100644
--- a/src/Libraries/Data/String/Iterator.idr
+++ b/src/Libraries/Data/String/Iterator.idr
@@ -2,6 +2,8 @@ module Libraries.Data.String.Iterator
 
 import public Libraries.Data.List.Lazy
 
+import Control.Monad.Identity
+
 %default total
 
 -- Backend-dependent string iteration type,
@@ -33,6 +35,18 @@ export
 withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
 withString str f = f (fromString str)
 
+||| Runs the action `f` on the slice `res` of the original string `str` represented by the
+||| iterator `it`
+%foreign
+  "scheme:blodwen-string-iterator-to-string"
+  "RefC:stringIteratorToString"
+  "javascript:stringIterator:toString"
+export
+withIteratorString : (str : String)
+                  -> (1 it : StringIterator str)
+                  -> (f : (res : String) -> a)
+                  -> a
+
 -- We use a custom data type instead of Maybe (Char, StringIterator)
 -- to remove one level of pointer indirection
 -- in every iteration of something that's likely to be a hot loop,
@@ -67,10 +81,15 @@ foldl op acc str = withString str (loop acc)
 
 export
 unpack : String -> LazyList Char
-unpack str = withString str unpack'
+unpack str = runIdentity $ withString str unpack'
   where
-    unpack' : (1 it : StringIterator str) -> LazyList Char
+    -- This is a Functor instance of Identity, but linear in second argument
+    %inline
+    mapId : forall a, b. (a -> b) -> (1 x : Identity a) -> Identity b
+    mapId f (Id x) = Id (f x)
+
+    unpack' : (1 it : StringIterator str) -> Identity (Lazy (LazyList Char))
     unpack' it =
       case uncons str it of
-        EOF => []
-        Character c it' => c :: Delay (unpack' $ assert_smaller it it')
+        EOF => pure []
+        Character c it' => mapId (c ::) (unpack' $ assert_smaller it it')