------------------------------------------------------------------------
-- An ad-hoc but straightforward solution to the problem of showing
-- that elegant definitions of the Hamming numbers (see EWD 792) and
-- the Fibonacci sequence are productive
------------------------------------------------------------------------

module StreamProg where

open import Coinduction
import Stream as S
open S using (Stream; _≺_; _≈_; Ord; lt; eq; gt)
open import Data.Nat
open import Relation.Binary
private
  module SS {A} = Setoid (S.setoid A)
import IO

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

infixr  _≺_

data Prog (A : Set) : Set1 where
  _≺_     : (x : A) (xs : ∞₁ (Prog A)) → Prog A
  zipWith : ∀ {B C} (f : B → C → A)
            (xs : Prog B) (ys : Prog C) → Prog A
  map     : ∀ {B} (f : B → A) (xs : Prog B) → Prog A
  merge   : (cmp : A → A → Ord)
            (xs : Prog A) (ys : Prog A) → Prog A

data WHNF A : Set1 where
  _≺_ : (x : A) (xs : Prog A) → WHNF A

whnf : ∀ {A} → Prog A → WHNF A
whnf (x ≺ xs)          = x ≺ ♭₁ xs
whnf (zipWith f xs ys) with whnf xs | whnf ys
whnf (zipWith f xs ys) | x ≺ xs′ | y ≺ ys′ = f x y ≺ zipWith f xs′ ys′
whnf (map f xs)        with whnf xs
whnf (map f xs)        | x ≺ xs′ = f x ≺ map f xs′
whnf (merge cmp xs ys) with whnf xs | whnf ys
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ with cmp x y
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | lt = x ≺ merge cmp xs′ (y ≺ ♯₁ ys′)
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | eq = x ≺ merge cmp xs′ ys′
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | gt = y ≺ merge cmp (x ≺ ♯₁ xs′) ys′

mutual

  value : ∀ {A} → WHNF A → Stream A
  value (x ≺ xs) = x ≺ ♯ ⟦ xs ⟧

  ⟦_⟧ : ∀ {A} → Prog A → Stream A
  ⟦ xs ⟧ = value (whnf xs)

------------------------------------------------------------------------
-- Examples

fib : Prog ℕ
fib =  ≺ ♯₁ zipWith _+_ fib ( ≺ ♯₁ fib)

cmp : ℕ → ℕ → Ord
cmp m n = toOrd (compare m n)
  where
  toOrd : ∀ {m n} → Ordering m n → Ord
  toOrd (less _ _)    = lt
  toOrd (equal _)     = eq
  toOrd (greater _ _) = gt

hamming : Prog ℕ
hamming =  ≺ ♯₁ merge cmp (map (_*_ ) hamming) (map (_*_ ) hamming)

main = IO.run (S.putStream (S._⋎_ ⟦ fib ⟧ ⟦ hamming ⟧))

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

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

zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
              ⟦ zipWith _∙_ xs ys ⟧ ≈ S.zipWith _∙_ ⟦ xs ⟧ ⟦ ys ⟧
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ≺ xs′ | y ≺ ys′ =
  (x ∙ y) ≺ ♯ zipWith-hom _∙_ xs′ ys′

-- S.zipWith is a congruence.

zipWith-cong : ∀ {A B C} (_∙_ : A → B → C) {xs xs′ ys ys′} →
               xs ≈ xs′ → ys ≈ ys′ →
               S.zipWith _∙_ xs ys ≈ S.zipWith _∙_ xs′ ys′
zipWith-cong _∙_ (x ≺ xs≈) (y ≺ ys≈) =
  (x ∙ y) ≺ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈)

-- Unfortunately Agda's definitional equality for coinductive
-- constructors is currently a little strange, so the result type
-- cannot be written out completely here:

fib-correct′ :
  ⟦ fib ⟧ ≈  ≺ ♯ S.zipWith _+_ ⟦ fib ⟧ ( ≺ _ {- ♯ ⟦ fib ⟧ -})
fib-correct′ =  ≺ ♯ zipWith-hom _+_ fib ( ≺ ♯₁ fib)

-- Fortunately there is a workaround.

fib-correct : ⟦ fib ⟧ ≈  ≺ ♯ S.zipWith _+_ ⟦ fib ⟧ ( ≺ ♯ ⟦ fib ⟧)
fib-correct =
   ≺ ♯ SS.trans (zipWith-hom  _+_ fib     ( ≺ ♯₁ fib))
                 (zipWith-cong _+_ SS.refl ( ≺ ♯ SS.refl))

------------------------------------------------------------------------
-- The definition of hamming is correct

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

map-hom : ∀ {A B} (f : A → B) xs →
          ⟦ map f xs ⟧ ≈ S.map f ⟦ xs ⟧
map-hom f xs with whnf xs
... | x ≺ xs′ = f x ≺ ♯ map-hom f xs′

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

merge-hom : ∀ {A} (cmp : A → A → Ord) xs ys →
            ⟦ merge cmp xs ys ⟧ ≈ S.merge cmp ⟦ xs ⟧ ⟦ ys ⟧
merge-hom cmp xs ys with whnf xs | whnf ys
... | x ≺ xs′ | y ≺ ys′ with cmp x y
...   | lt = x ≺ ♯ merge-hom cmp xs′ _
...   | eq = x ≺ ♯ merge-hom cmp xs′ ys′
...   | gt = y ≺ ♯ merge-hom cmp _ ys′

-- S.merge is a congruence.

merge-cong : ∀ {A} (cmp : A → A → Ord) {xs xs′ ys ys′} →
             xs ≈ xs′ → ys ≈ ys′ →
             S.merge cmp xs ys ≈ S.merge cmp xs′ ys′
merge-cong cmp (x ≺ xs≈) (y ≺ ys≈) with cmp x y
... | lt = x ≺ ♯ merge-cong cmp (♭ xs≈) (y ≺ ys≈)
... | eq = x ≺ ♯ merge-cong cmp (♭ xs≈) (♭ ys≈)
... | gt = y ≺ ♯ merge-cong cmp (x ≺ xs≈) (♭ ys≈)

-- hamming is correct.

hamming-correct : ⟦ hamming ⟧ ≈
                   ≺ ♯ S.merge cmp (S.map (_*_ ) ⟦ hamming ⟧)
                                    (S.map (_*_ ) ⟦ hamming ⟧)
hamming-correct =
   ≺ ♯ SS.trans (merge-hom cmp (map (_*_ ) hamming)
                                (map (_*_ ) hamming))
                 (merge-cong cmp (map-hom (_*_ ) hamming)
                                 (map-hom (_*_ ) hamming))