{-# OPTIONS --cubical-compatible --guardedness #-}
module Codata.Musical.Colist.Base where
open import Level using (Level)
open import Codata.Musical.Notation
open import Codata.Musical.Conat.Base using (Coℕ; zero; suc)
open import Data.Bool.Base using (Bool; true; false)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty.Base using (List⁺; _∷_)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Nat.Base using (ℕ; zero; suc)
private
variable
a b : Level
A : Set a
B : Set b
infixr 5 _∷_
data Colist (A : Set a) : Set a where
[] : Colist A
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
{-# FOREIGN GHC
data AgdaColist a = Nil | Cons a (MAlonzo.RTE.Inf (AgdaColist a))
type AgdaColist' l a = AgdaColist a
#-}
{-# COMPILE GHC Colist = data AgdaColist' (Nil | Cons) #-}
{-# COMPILE UHC Colist = data __LIST__ (__NIL__ | __CONS__) #-}
null : Colist A → Bool
null [] = true
null (_ ∷ _) = false
length : Colist A → Coℕ
length [] = zero
length (x ∷ xs) = suc (♯ length (♭ xs))
map : (A → B) → Colist A → Colist B
map f [] = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
fromList : List A → Colist A
fromList [] = []
fromList (x ∷ xs) = x ∷ ♯ fromList xs
replicate : Coℕ → A → Colist A
replicate zero x = []
replicate (suc n) x = x ∷ ♯ replicate (♭ n) x
lookup : Colist A → ℕ → Maybe A
lookup [] _ = nothing
lookup (x ∷ _) zero = just x
lookup (_ ∷ xs) (suc n) = lookup (♭ xs) n
infixr 5 _++_
_++_ : Colist A → Colist A → Colist A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
infixr 5 _⋎_
_⋎_ : Colist A → Colist A → Colist A
[] ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)
concat : Colist (List⁺ A) → Colist A
concat [] = []
concat ((x ∷ []) ∷ xss) = x ∷ ♯ concat (♭ xss)
concat ((x ∷ (y ∷ xs)) ∷ xss) = x ∷ ♯ concat ((y ∷ xs) ∷ xss)
[_] : A → Colist A
[ x ] = x ∷ ♯ []