{-# OPTIONS --guardedness #-}

open import Codata.Guarded.Stream renaming (head to hd ; tail to tl)
open import Data.Product using (_×_ ; _,_)
open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality
open import Data.Nat

record BiStream (a b : Set) : Set where
  coinductive
  field
    lhd : a
    rhd : b
    btl : BiStream a b
open BiStream

module _ where
  variable a b : Set
  
  turn : BiStream a b → BiStream b a
  lhd (turn s) = rhd s
  rhd (turn s) = lhd s
  btl (turn s) = turn (btl s)

  zip : Stream a → Stream b → BiStream a b
  lhd (zip s t) = hd s
  rhd (zip s t) = hd t
  btl (zip s t) = zip (tl s) (tl t)

  left : BiStream a b → Stream a
  hd (left s)  = lhd s
  tl (left s)  = left (btl s)

  right : BiStream a b → Stream b
  hd (right s)  = rhd s
  tl (right s)  = right (btl s)

  scrap : BiStream a b → BiStream a b
  lhd (scrap s) = lhd s
  rhd (scrap s) = rhd (btl s)
  btl (scrap s) = scrap (btl (btl s))

  -- testing
  btake : ℕ → BiStream a b → List (a × b)
  btake zero s = []
  btake (suc n) s = (lhd s , rhd s) ∷ btake n (btl s)

  foo : btake 2 (scrap (zip nats nats)) ≡ (0 , 1) ∷ (2 , 3) ∷ []
  foo = refl

  -- nicer?
  scrap' : BiStream a b → BiStream a b
  scrap' s = zip (evens (left s)) (odds (right s))
  
  record _≈_ (s t : BiStream a b) : Set where
    coinductive
    field
      lhead : lhd s ≡ lhd t
      rhead : rhd s ≡ rhd t
      btail : btl s ≈ btl t
  open _≈_

  lemma : ∀ (s : BiStream a b) → scrap s ≈ scrap' s
  lhead (lemma s) = refl
  rhead (lemma s) = refl
  btail (lemma s) = lemma (btl (btl s))