Co.agda

module Co where

open import Level hiding (suc)
open import Size
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Vec using (Vec ; [] ; _∷_)
open import Data.List using (List ; [] ; _∷_)
open import Data.Maybe using (Maybe ; nothing ; just ; maybe)
open import Relation.Binary.PropositionalEquality

record Stream {i : Size} (A : Set) : Set where
  coinductive
  field
    head : A
    tail : ∀ {j : Size< i} -> Stream {j} A
open Stream

constant : {A : Set} -> A -> Stream A
head (constant a) = a
tail (constant a) = constant a

map : ∀ {i A B} -> (A -> B) -> Stream {i} A -> Stream {i} B
head (map f a) = f (head a)
tail (map f a) = map f (tail a)

zipWith : ∀ {i A B C} -> (A -> B -> C) -> Stream {i} A -> Stream {i} B -> Stream {i} C
head (zipWith f a b) = f (head a) (head b)
tail (zipWith f a b) = zipWith f (tail a) (tail b)

index : {A : Set} -> Stream A -> ℕ -> A
index a zero = head a
index a (suc n) = index (tail a) n

fib : ℕ -> ℕ
fib = index go
  where
  go : ∀ {j} -> Stream {j} ℕ
  head go = 0
  head (tail go) = 1
  tail (tail go) = zipWith _+_ go (tail go)

take : {A : Set} -> (n : ℕ) -> Stream A -> Vec A n
take zero a = []
take (suc n) a = head a ∷ take n (tail a)

drop : {A : Set} -> ℕ -> Stream A -> Stream A
drop zero a = a
drop (suc n) a = drop n (tail a)

nats : Stream ℕ
nats = go 0
  where
  go : ℕ -> Stream ℕ
  head (go n) = n
  tail (go n) = go (suc n)

join : ∀ {i A} -> Stream {i} (Stream A) -> Stream {i} A
head (join as) = head (head as)
tail (join as) = zipWith index (tail as) nats

_>>=_ : {A B : Set} -> Stream A -> (A -> Stream B) -> Stream B
a >>= f = join (map f a)

intersperse : ∀ {i A} -> A -> Stream {i} A -> Stream {i} A
head (intersperse a as) = head as
head (tail (intersperse a as)) = a
tail (tail (intersperse a as)) = intersperse a (tail as)

prepend : ∀ {i A} -> List A -> Stream {i} A -> Stream {i} A
head (prepend [] s) = head s
head (prepend (x ∷ _) _) = x
tail (prepend [] s) = tail s
tail (prepend (x ∷ xs) s) = prepend xs s

cycle : ∀ {A n} -> Vec A (suc n) -> Stream A
cycle {A} (x ∷ xs) = go x xs
  where
  go : ∀ {m} -> A -> Vec A m -> Stream A
  head (go y _) = y
  tail (go y []) = cycle (x ∷ xs)
  tail (go _ (z ∷ ys)) = go z ys

record _≈_ {A : Set} (as : Stream A) (bs : Stream A) : Set where
  coinductive
  field
    ≈-head : head as ≡ head bs
    ≈-tail : tail as ≈ tail bs
open _≈_

≈-refl : ∀ {A} (as : Stream A) -> as ≈ as
≈-head (≈-refl as) = refl
≈-tail (≈-refl as) = ≈-refl (tail as)

record M {i : Size} {a b : Level} (A : Set a) (B : A -> Set b) : Set (a ⊔ b) where
  coinductive
  field
    key : A
    inf : ∀ {j : Size< i} -> B key -> M {j} A B
open M

Nat : Set
Nat = M Bool (λ x → if x then ⊥ else ⊤)

𝕫 : Nat
key 𝕫 = true
inf 𝕫 = ⊥-elim

𝕤 : Nat -> Nat
key (𝕤 _) = false
inf (𝕤 n) = λ _ → n

stream : Set -> Set
stream A = M A (λ _ -> ⊤)

cons : ∀ {A} -> A -> stream A -> stream A
key (cons x xs) = x
inf (cons x xs) = λ _ -> xs

const : ∀ {A} -> A -> stream A
key (const a) = a
inf (const a) = λ _ → const a

tak : ∀ {A} -> (n : ℕ) -> stream A -> Vec A n
tak zero a = []
tak (suc n) a = key a ∷ tak n (inf a tt)

tak-test : tak 3 (const 1) ≡ 1 ∷ 1 ∷ 1 ∷ []
tak-test = refl


L : Set -> Set
L A = M (Maybe A) (maybe (λ _ → ⊤) ⊥)

nil : ∀ {A} -> L A
key nil = nothing
inf nil = ⊥-elim

Lcons : ∀ {A} -> A -> L A -> L A
key (Lcons x _) = just x
inf (Lcons x xs) = λ _ → xs

Lmap : ∀ {A B} -> (A -> B) -> L A -> L B
key (Lmap f x) = Data.Maybe.map f (key x)
inf (Lmap {B = B} f x) = λ tt -> Lmap f x

defOfMaybe : ∀ {A : Set} -> (x : Maybe A) -> (∃ λ a → x ≡ just a) ⊎ x ≡ nothing
defOfMaybe (just y) = inj₁ (y , refl)
defOfMaybe nothing = inj₂ refl

toList : ∀ {A} -> L A -> (n : ℕ) -> Maybe (Vec A n)
toList l zero = just []
toList l (suc n) with defOfMaybe (key l)
toList {A} l (suc n) | inj₁ (x , prf) =
  Data.Maybe.map (λ rest → x ∷ rest) (toList (inf l (deconstruct (key l) prf)) n)
  where
  deconstruct : {y : A} -> (k : Maybe A) -> k ≡ just y -> maybe (λ _ → ⊤) ⊥ k
  deconstruct (just y) _ = tt
  deconstruct nothing ()
toList l (suc n) | _ = nothing