    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The Colist type and some operations
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --sized-types #-}

    module Codata.Sized.Colist where

    open import Codata.Sized.Conat as Conat using (Conat ; zero ; suc)
    open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
    open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
    open import Codata.Sized.Stream using (Stream ; _∷_)
    open import Codata.Sized.Thunk using (Thunk; force)
    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
    open import Data.Maybe.Base using (Maybe; nothing; just)
    open import Data.Nat.Base using (ℕ; suc; zero)
    open import Data.Product.Base using (_×_ ; _,_)
    open import Data.These.Base using (These; this; that; these)
    open import Data.Unit.Base using (⊤)
    open import Data.Vec.Base as Vec using (Vec; []; _∷_)
    open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
    open import Function.Base using (_$′_; _∘′_; id; _∘_)
    open import Level using (Level)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
    open import Size using (Size; ∞)

    private
      variable
        a b c w : Level
        i : Size
        A : Set a
        B : Set b
        C : Set c
        W : Set w

    data Colist (A : Set a) (i : Size) : Set a where
      []  : Colist A i
      _∷_ : A → Thunk (Colist A) i → Colist A i

    infixr 5 _∷_

    ------------------------------------------------------------------------
    -- Relationship to Cowriter.

    fromCowriter : Cowriter W A i → Colist W i
    fromCowriter CW.[ _ ] = []
    fromCowriter (w ∷ ca) = w ∷ λ where .force → fromCowriter (ca .force)

    toCowriter : Colist A i → Cowriter A ⊤ i
    toCowriter []       = CW.[ _ ]
    toCowriter (a ∷ as) = a ∷ λ where .force → toCowriter (as .force)

    ------------------------------------------------------------------------
    -- Basic functions.

    [_] : A → Colist A ∞
    [ a ] = a ∷ λ where .force → []

    length : Colist A i → Conat i
    length []       = zero
    length (x ∷ xs) = suc λ where .force → length (xs .force)

    replicate : Conat i → A → Colist A i
    replicate zero    a = []
    replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a

    infixr 5 _++_ _⁺++_
    _++_ : Colist A i → Colist A i → Colist A i
    []       ++ ys = ys
    (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys

    lookup : Colist A ∞ → ℕ → Maybe A
    lookup []       _       = nothing
    lookup (a ∷ as) zero    = just a
    lookup (a ∷ as) (suc n) = lookup (as .force) n

    colookup : Colist A i → Conat i → Delay (Maybe A) i
    colookup []       _       = now nothing
    colookup (a ∷ as) zero    = now (just a)
    colookup (a ∷ as) (suc n) =
      later λ where .force → colookup (as .force) (n .force)

    take : (n : ℕ) → Colist A ∞ → Vec≤ A n
    take zero    xs       = Vec≤.[]
    take n       []       = Vec≤.[]
    take (suc n) (x ∷ xs) = x Vec≤.∷ take n (xs .force)

    cotake : Conat i → Stream A i → Colist A i
    cotake zero    xs       = []
    cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force)

    drop : ℕ → Colist A ∞ → Colist A ∞
    drop zero    xs       = xs
    drop (suc n) []       = []
    drop (suc n) (x ∷ xs) = drop n (xs .force)

    fromList : List A → Colist A ∞
    fromList []       = []
    fromList (x ∷ xs) = x ∷ λ where .force → fromList xs

    fromList⁺ : List⁺ A → Colist A ∞
    fromList⁺ = fromList ∘′ List⁺.toList

    _⁺++_ : List⁺ A → Thunk (Colist A) i → Colist A i
    (x ∷ xs) ⁺++ ys = x ∷ λ where .force → fromList xs ++ ys .force

    concat : Colist (List⁺ A) i → Colist A i
    concat []         = []
    concat (as ∷ ass) = as ⁺++ λ where .force → concat (ass .force)

    fromStream : Stream A i → Colist A i
    fromStream = cotake Conat.infinity

    module ChunksOf (n : ℕ) where

      chunksOf : Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i
      chunksOfAcc : ∀ m →
        -- We have two continuations but we are only ever going to use one.
        -- If we had linear types, we'd write the type using the & conjunction here.
        (k≤ : Vec≤ A m → Vec≤ A n) →
        (k≡ : Vec A m → Vec A n) →
        -- Finally we chop up the input stream.
        Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i

      chunksOf = chunksOfAcc n id id

      chunksOfAcc zero    k≤ k≡ as       = k≡ [] ∷ λ where .force → chunksOf as
      chunksOfAcc (suc k) k≤ k≡ []       = CW.[ k≤ Vec≤.[] ]
      chunksOfAcc (suc k) k≤ k≡ (a ∷ as) =
        chunksOfAcc k (k≤ ∘ (a Vec≤.∷_)) (k≡ ∘ (a ∷_)) (as .force)

    open ChunksOf using (chunksOf) public

    -- Test to make sure that the values are kept in the same order
    _ : chunksOf 3 (fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ []))
      ≡ (1 ∷ 2 ∷ 3 ∷ []) ∷ _
    _ = refl

    map : (A → B) → Colist A i → Colist B i
    map f []       = []
    map f (a ∷ as) = f a ∷ λ where .force → map f (as .force)

    unfold : (A → Maybe (A × B)) → A → Colist B i
    unfold next seed with next seed
    ... | nothing          = []
    ... | just (seed′ , b) = b ∷ λ where .force → unfold next seed′

    scanl : (B → A → B) → B → Colist A i → Colist B i
    scanl c n []       = n ∷ λ where .force → []
    scanl c n (a ∷ as) = n ∷ λ where .force → scanl c (c n a) (as .force)

    alignWith : (These A B → C) → Colist A i → Colist B i → Colist C i
    alignWith f []         bs       = map (f ∘′ that) bs
    alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
    alignWith f (a ∷ as)   (b ∷ bs) =
      f (these a b) ∷ λ where .force → alignWith f (as .force) (bs .force)

    zipWith : (A → B → C) → Colist A i → Colist B i → Colist C i
    zipWith f []       bs       = []
    zipWith f as       []       = []
    zipWith f (a ∷ as) (b ∷ bs) =
      f a b ∷ λ where .force → zipWith f (as .force) (bs .force)

    align : Colist A i → Colist B i → Colist (These A B) i
    align = alignWith id

    zip : Colist A i → Colist B i → Colist (A × B) i
    zip = zipWith _,_

    ap : Colist (A → B) i → Colist A i → Colist B i
    ap = zipWith _$′_