{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Cowriter where
open import Size
open import Level as L using (Level)
open import Codata.Sized.Thunk using (Thunk; force)
open import Codata.Sized.Conat
open import Codata.Sized.Delay using (Delay; later; now)
open import Codata.Sized.Stream as Stream using (Stream; _∷_)
open import Data.Unit.Base
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty.Base using (List⁺; _∷_)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Product.Base as Product using (_×_; _,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)
open import Function.Base using (_$_; _∘′_; id)
private
variable
a b w x : Level
A : Set a
B : Set b
W : Set w
X : Set x
data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
[_] : A → Cowriter W A i
_∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i
infixr 5 _∷_
fromDelay : ∀ {i} → Delay A i → Cowriter ⊤ A i
fromDelay (now a) = [ a ]
fromDelay (later da) = _ ∷ λ where .force → fromDelay (da .force)
toDelay : ∀ {i} → Cowriter W A i → Delay A i
toDelay [ a ] = now a
toDelay (_ ∷ ca) = later λ where .force → toDelay (ca .force)
fromStream : ∀ {i} → Stream W i → Cowriter W A i
fromStream (w ∷ ws) = w ∷ λ where .force → fromStream (ws .force)
repeat : W → Cowriter W A ∞
repeat = fromStream ∘′ Stream.repeat
length : ∀ {i} → Cowriter W A i → Conat i
length [ _ ] = zero
length (w ∷ cw) = suc λ where .force → length (cw .force)
splitAt : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (Vec≤ W n × A)
splitAt zero cw = inj₁ ([] , cw)
splitAt (suc n) [ a ] = inj₂ (Vec≤.[] , a)
splitAt (suc n) (w ∷ cw) = Sum.map (Product.map₁ (w ∷_)) (Product.map₁ (w Vec≤.∷_))
$ splitAt n (cw .force)
take : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (Vec≤ W n × A)
take n = Sum.map₁ Product.proj₁ ∘′ splitAt n
infixr 5 _++_ _⁺++_
_++_ : ∀ {i} → List W → Cowriter W A i → Cowriter W A i
[] ++ ca = ca
(w ∷ ws) ++ ca = w ∷ λ where .force → ws ++ ca
_⁺++_ : ∀ {i} → List⁺ W → Thunk (Cowriter W A) i → Cowriter W A i
(w ∷ ws) ⁺++ ca = w ∷ λ where .force → ws ++ ca .force
concat : ∀ {i} → Cowriter (List⁺ W) A i → Cowriter W A i
concat [ a ] = [ a ]
concat (w ∷ ca) = w ⁺++ λ where .force → concat (ca .force)
map : ∀ {i} → (W → X) → (A → B) → Cowriter W A i → Cowriter X B i
map f g [ a ] = [ g a ]
map f g (w ∷ cw) = f w ∷ λ where .force → map f g (cw .force)
map₁ : ∀ {i} → (W → X) → Cowriter W A i → Cowriter X A i
map₁ f = map f id
map₂ : ∀ {i} → (A → X) → Cowriter W A i → Cowriter W X i
map₂ = map id
ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i
ap [ f ] ca = map₂ f ca
ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca
infixl 1 _>>=_
_>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
[ a ] >>= f = f a
(w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f
unfold : ∀ {i} → (X → (W × X) ⊎ A) → X → Cowriter W A i
unfold next seed =
Sum.[ (λ where (w , seed′) → w ∷ λ where .force → unfold next seed′)
, [_]
] (next seed)