------------------------------------------------------------------------
-- Another implementation of the Fibonacci sequence using tail, along
-- with some other examples
------------------------------------------------------------------------

module ArbitraryChunks where

open import Coinduction
open import Data.Bool
open import Data.Nat
open import Data.Stream as S using (Stream; _≈_; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; [_])

------------------------------------------------------------------------
-- Stream programs

-- StreamP m n A encodes programs generating streams in chunks of size
-- (at least) m, where the first chunk has size (at least) n.

infixr 5 _∷_

data StreamP (m : ℕ) : ℕ → Set → Set₁ where
  [_]     : ∀ {A} (xs : ∞ (StreamP m m A)) → StreamP m 0 A
  _∷_     : ∀ {n A} (x : A) (xs : StreamP m n A) → StreamP m (suc n) A
  forget  : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A
  tail    : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A
  zipWith : ∀ {n A B C} (f : A → B → C)
            (xs : StreamP m n A) (ys : StreamP m n B) → StreamP m n C
  map     : ∀ {n A B} (f : A → B) (xs : StreamP m n A) → StreamP m n B

data StreamW (m : ℕ) : ℕ → Set → Set₁ where
  [_] : ∀ {A} (xs : StreamP m m A) → StreamW m 0 A
  _∷_ : ∀ {n A} (x : A) (xs : StreamW m n A) → StreamW m (suc n) A

forgetW : ∀ {m n A} → StreamW (suc m) (suc n) A → StreamW (suc m) n A
forgetW {n = zero}  (x ∷ [ xs ]) = [ x ∷ forget xs ]
forgetW {n = suc n} (x ∷ xs)     = x ∷ forgetW xs

tailW : ∀ {m n A} → StreamW m (suc n) A → StreamW m n A
tailW (x ∷ xs) = xs

zipWithW : ∀ {m n A B C} → (A → B → C) →
           StreamW m n A → StreamW m n B → StreamW m n C
zipWithW f [ xs ]   [ ys ]   = [ zipWith f xs ys ]
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithW f xs ys

mapW : ∀ {m n A B} → (A → B) → StreamW m n A → StreamW m n B
mapW f [ xs ]   = [ map f xs ]
mapW f (x ∷ xs) = f x ∷ mapW f xs

whnf : ∀ {m n A} → StreamP (suc m) n A → StreamW (suc m) n A
whnf [ xs ]            = [ ♭ xs ]
whnf (x ∷ xs)          = x ∷ whnf xs
whnf (forget xs)       = forgetW (whnf xs)
whnf (tail xs)         = tailW (whnf xs)
whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys)
whnf (map f xs)        = mapW f (whnf xs)

mutual

  ⟦_⟧W : ∀ {m n A} → StreamW (suc m) (suc n) A → Stream A
  ⟦ x ∷ [ xs ]   ⟧W = x ∷ ♯ ⟦ xs ⟧P
  ⟦ x ∷ (y ∷ xs) ⟧W = x ∷ ♯ ⟦ y ∷ xs ⟧W

  ⟦_⟧P : ∀ {m n A} → StreamP (suc m) (suc n) A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- Some examples

-- The Fibonacci sequence.

fib : StreamP 1 1 ℕ
fib = 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget fib) (tail fib)) ]

-- Some sequence which is defined using (tail ∘ tail).

someSequence : StreamP 2 2 ℕ
someSequence =
  0 ∷ 1 ∷ [ ♯ (1 ∷ 2 ∷ zipWith _+_ (tail (tail someSequence))
                                   (forget (forget someSequence))) ]

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith.

mutual

  zipWithW-hom :
    ∀ {m n A B C} (_∙_ : A → B → C)
    (xs : StreamW (suc m) (suc n) A) ys →
    ⟦ zipWithW _∙_ xs ys ⟧W ≈ S.zipWith _∙_ ⟦ xs ⟧W ⟦ ys ⟧W
  zipWithW-hom _∙_ (x ∷ [ xs ]) (y ∷ [ ys ])   =
    (x ∙ y) ∷ ♯ zipWith-hom _∙_ xs ys
  zipWithW-hom _∙_ (x ∷ x′ ∷ xs) (y ∷ y′ ∷ ys) =
    (x ∙ y) ∷ ♯ zipWithW-hom _∙_ (x′ ∷ xs) (y′ ∷ ys)

  zipWith-hom : ∀ {m n A B C} (_∙_ : A → B → C)
                (xs : StreamP (suc m) (suc n) A) ys →
                ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
  zipWith-hom _∙_ xs ys = zipWithW-hom _∙_ (whnf xs) (whnf ys)

-- forget is the identity on streams.

open import MapIterate using (_≈P_; _∷_; _≈⟨_⟩_; _∎; soundP)

mutual

  forgetW-lemma : ∀ {m n A} x (xs : StreamW (suc m) (suc n) A) →
                  ⟦ x ∷ forgetW xs ⟧W ≈P x ∷ ♯ ⟦ xs ⟧W
  forgetW-lemma x (x′ ∷ [ xs ])  = x ∷ ♯ (_ ≈⟨ forget-lemma x′ xs ⟩ x′ ∷ ♯ (_ ∎))
  forgetW-lemma x (x′ ∷ x″ ∷ xs) = x ∷ ♯ (_ ≈⟨ forgetW-lemma x′ (x″ ∷ xs) ⟩ x′ ∷ ♯ (_ ∎) )

  forget-lemma : ∀ {m n A} x (xs : StreamP (suc m) (suc n) A) →
                 ⟦ x ∷ forget xs ⟧P ≈P x ∷ ♯ ⟦ xs ⟧P
  forget-lemma x xs with whnf xs | P.inspect whnf xs
  ... | y ∷ y′ ∷ ys | [ eq ] = x ∷ ♯ helper
    where
    helper : ⟦ y ∷ forgetW (y′ ∷ ys) ⟧W ≈P ⟦ xs ⟧P
    helper rewrite eq = _ ≈⟨ forgetW-lemma y (y′ ∷ ys) ⟩ y ∷ ♯ (_ ∎)
  ... | y ∷ [ ys ]  | [ eq ] = x ∷ ♯ helper
    where
    helper : ⟦ y ∷ forget ys ⟧P ≈P ⟦ xs ⟧P
    helper rewrite eq = _ ≈⟨ forget-lemma y ys ⟩ y ∷ ♯ (_ ∎)

-- The stream ⟦ fib ⟧P satisfies its intended defining equation.

open import Relation.Binary
module SS {A : Set} = Setoid (S.setoid A)

fib-correct :
  ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P))
fib-correct =
  0 ∷ ♯ (1 ∷ ♯ SS.trans
    (zipWith-hom _+_ (0 ∷ forget fib′) fib′)
    (S.zipWith-cong _+_ (SS.trans (soundP (forget-lemma 0 fib′))
                                  (0 ∷ ♯ SS.refl)) SS.refl))
  where fib′ = 1 ∷ zipWith _+_ (forget fib) (tail fib)

------------------------------------------------------------------------
-- map₂

-- A variant of S.map which processes streams in chunks of size 2.

map₂ : ∀ {A B} → (A → B) → Stream A → Stream B
map₂ f (x ∷ xs) with ♭ xs
map₂ f (x ∷ xs) | y ∷ ys = f x ∷ ♯ (f y ∷ ♯ map₂ f (♭ ys))

-- This function is extensionally equal to S.map.

map≈map₂ : ∀ {A B} →
           (f : A → B) → (xs : Stream A) → S.map f xs ≈ map₂ f xs
map≈map₂ f (x ∷ xs) with ♭ xs | P.inspect ♭ xs
map≈map₂ f (x ∷ xs) | y ∷ ys | [ eq ] = f x ∷ ♯ helper eq
  where
  map-f-y∷ys = _

  helper : ∀ {xs} → xs ≡ y ∷ ys → S.map f xs ≈ map-f-y∷ys
  helper refl = f y ∷ ♯ map≈map₂ f (♭ ys)

-- However, as explained in "Beating the Productivity Checker Using
-- Embedded Languages", the two functions are not interchangeable
-- (assuming that pattern matching is evaluated strictly). Let us see
-- what happens when we use the language above. We can define the
-- stream of natural numbers using chunks of size 1 and 2.

nats : StreamP 1 1 ℕ
nats = 0 ∷ [ ♯ map suc nats ]

nats₂ : StreamP 2 2 ℕ
nats₂ = 0 ∷ 1 ∷ [ ♯ map suc nats₂ ]

-- The first use of map corresponds to S.map, and the second to map₂.
-- If we try to use map₂ in the first definition, then we get a type
-- error. The following code is not accepted.

-- nats : StreamP 2 1 ℕ
-- nats = 0 ∷ [ ♯ map suc nats ]