-- | Infinite lists (streams).
--
-- Wrapper for "Data.List.Infinite" from the @infinite-list@ package
-- that generalizes some type signatures, using 'Integral' for indexing,
-- and adds some missing functions.
--
-- Import this module as follows:
--
-- @
-- import Agda.Utils.ListInf (ListInf, pattern (:<))
-- import Agda.Utils.ListInf qualified as ListInf
-- @
--
-- Motivation: lists constructed by 'repeat', 'iterate', 'cycle' etc.
-- are infinite, so the nil case can never arise when consuming them,
-- e.g. in a 'take' or 'zipWith'.
-- Constructing them as properly infinite lists ('ListInf') should thus
-- lead to slightly more efficient code, eliminating impossible cases.

module Agda.Utils.ListInf
  ( module Agda.Utils.ListInf, module Inf)
  where

import Prelude
  ( Enum, Foldable, Functor, Int, Integral
  , (.), ($), (-), (<=), (>)
  , fromIntegral, id, otherwise, succ
  )

import Data.List.Infinite qualified
import Data.List.Infinite as Inf
  ( pattern (:<), cycle, iterate, prependList, repeat
  , head, tail
  , zip, zipWith
  ) -- add more as needed

type ListInf = Data.List.Infinite.Infinite

---------------------------------------------------------------------------
-- * Construction

-- | There is only one meaningful way to concatenate a finite and an infinite list,
-- justifying the name @append = prependList@.
append :: [a] -> ListInf a -> ListInf a
append :: forall a. [a] -> ListInf a -> ListInf a
append = [a] -> Infinite a -> Infinite a
forall a. [a] -> ListInf a -> ListInf a
prependList

-- | @pad as b@ implements the frequent pattern @as ++ repeat b@.
pad :: [a] -> a -> ListInf a
pad :: forall a. [a] -> a -> ListInf a
pad [a]
as a
b = [a] -> ListInf a -> ListInf a
forall a. [a] -> ListInf a -> ListInf a
append [a]
as (a -> ListInf a
forall a. a -> Infinite a
repeat a
b)

-- | @upFrom n = [n..]@ as properly infinite list.
{-# SPECIALIZE upFrom :: Int -> ListInf Int #-}
upFrom :: Enum n => n -> ListInf n
upFrom :: forall n. Enum n => n -> ListInf n
upFrom = (n -> n) -> n -> Infinite n
forall a. (a -> a) -> a -> Infinite a
iterate n -> n
forall a. Enum a => a -> a
succ

---------------------------------------------------------------------------
-- * Selection

-- | Update the @n@th element of an infinite list.
--   @Θ(n)@.
--
--   Precondition: the index @n@ is >= 0.
{-# SPECIALIZE updateAt :: Int -> (a -> a) -> ListInf a -> ListInf a #-}
updateAt :: Integral n => n -> (a -> a) -> ListInf a -> ListInf a
updateAt :: forall n a. Integral n => n -> (a -> a) -> ListInf a -> ListInf a
updateAt n
n a -> a
f (a
a :< Infinite a
as)
  | n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
> n
0     = a
a a -> Infinite a -> Infinite a
forall a. a -> Infinite a -> Infinite a
:< n -> (a -> a) -> Infinite a -> Infinite a
forall n a. Integral n => n -> (a -> a) -> ListInf a -> ListInf a
updateAt (n
n n -> n -> n
forall a. Num a => a -> a -> a
- n
1) a -> a
f Infinite a
as
  | Bool
otherwise = a -> a
f a
a a -> Infinite a -> Infinite a
forall a. a -> Infinite a -> Infinite a
:< Infinite a
as

-- Generalized versions of the functions from the @infinite-list@ package:

{-# SPECIALIZE (!!) :: ListInf a -> Int -> a #-}
(!!) :: Integral n => ListInf a -> n -> a
ListInf a
as !! :: forall n a. Integral n => ListInf a -> n -> a
!! n
n = ListInf a
as ListInf a -> Word -> a
forall a. Infinite a -> Word -> a
Data.List.Infinite.!! n -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral n
n

{-# SPECIALIZE take :: Int -> ListInf a -> [a] #-}
take :: Integral n => n -> ListInf a -> [a]
take :: forall n a. Integral n => n -> ListInf a -> [a]
take = n -> Infinite a -> [a]
forall n a. Integral n => n -> ListInf a -> [a]
Data.List.Infinite.genericTake

{-# SPECIALIZE drop :: Int -> ListInf a -> ListInf a #-}
drop :: Integral n => n -> ListInf a -> ListInf a
drop :: forall n a. Integral n => n -> ListInf a -> ListInf a
drop = n -> Infinite a -> Infinite a
forall n a. Integral n => n -> ListInf a -> ListInf a
Data.List.Infinite.genericDrop

-- | @splitAt n as == (take n as, drop n as)@
{-# SPECIALIZE splitAt :: Int -> ListInf a -> ([a], ListInf a) #-}
splitAt :: Integral n => n -> ListInf a -> ([a], ListInf a)
splitAt :: forall n a. Integral n => n -> ListInf a -> ([a], ListInf a)
splitAt = n -> Infinite a -> ([a], Infinite a)
forall n a. Integral n => n -> ListInf a -> ([a], ListInf a)
Data.List.Infinite.genericSplitAt