module StreamProg where
open import Coinduction
open import Data.Nat
open import Data.Stream as S using (Stream; _∷_; _≈_)
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P
private
module SS {A} = Setoid (S.setoid A)
data Ord : Set where
lt : Ord
eq : Ord
gt : Ord
merge : ∀ {A} → (A → A → Ord) → Stream A → Stream A → Stream A
merge cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ ♯ merge cmp (♭ xs) (y ∷ ys)
... | eq = x ∷ ♯ merge cmp (♭ xs) (♭ ys)
... | gt = y ∷ ♯ merge cmp (x ∷ xs) (♭ ys)
infixr 5 _∷_
data StreamP (A : Set) : Set1 where
_∷_ : (x : A) (xs : ∞ (StreamP A)) → StreamP A
zipWith : ∀ {B C} (f : B → C → A)
(xs : StreamP B) (ys : StreamP C) → StreamP A
map : ∀ {B} (f : B → A) (xs : StreamP B) → StreamP A
mergeP : (cmp : A → A → Ord)
(xs : StreamP A) (ys : StreamP A) → StreamP A
data StreamW A : Set1 where
_∷_ : (x : A) (xs : StreamP A) → StreamW A
zipWithW : {A B C : Set} →
(A → B → C) → StreamW A → StreamW B → StreamW C
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
mapW : {A B : Set} → (A → B) → StreamW A → StreamW B
mapW f (x ∷ xs) = f x ∷ map f xs
mergeW : {A : Set} →
(A → A → Ord) → StreamW A → StreamW A → StreamW A
mergeW cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ mergeP cmp xs (y ∷ ♯ ys)
... | eq = x ∷ mergeP cmp xs ys
... | gt = y ∷ mergeP cmp (x ∷ ♯ xs) ys
whnf : ∀ {A} → StreamP A → StreamW A
whnf (x ∷ xs) = x ∷ ♭ xs
whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys)
whnf (map f xs) = mapW f (whnf xs)
whnf (mergeP cmp xs ys) = mergeW cmp (whnf xs) (whnf ys)
mutual
⟦_⟧W : ∀ {A} → StreamW A → Stream A
⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P
⟦_⟧P : ∀ {A} → StreamP A → Stream A
⟦ xs ⟧P = ⟦ whnf xs ⟧W
fib : StreamP ℕ
fib = 0 ∷ ♯ zipWith _+_ fib (1 ∷ ♯ fib)
fib′ : StreamP ℕ
fib′ = zipWith _+_ (0 ∷ ♯ fib′) (0 ∷ ♯ (1 ∷ ♯ 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 : StreamP ℕ
hamming = 1 ∷ ♯ mergeP cmp (map (_*_ 2) hamming) (map (_*_ 3) hamming)
zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ∷ xs′ | y ∷ ys′ =
(x ∙ y) ∷ ♯ zipWith-hom _∙_ xs′ ys′
fib-correct′ :
⟦ fib ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ _ )
fib-correct′ = 0 ∷ ♯ zipWith-hom _+_ fib (1 ∷ ♯ fib)
fib-correct : ⟦ fib ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ ♯ ⟦ fib ⟧P)
fib-correct =
0 ∷ ♯ SS.trans (zipWith-hom _+_ fib (1 ∷ ♯ fib))
(S.zipWith-cong _+_ SS.refl (1 ∷ ♯ SS.refl))
map-hom : ∀ {A B} (f : A → B) xs →
⟦ map f xs ⟧P ≈ S.map f ⟦ xs ⟧P
map-hom f xs with whnf xs
... | x ∷ xs′ = f x ∷ ♯ map-hom f xs′
merge-hom : ∀ {A} (cmp : A → A → Ord) xs ys →
⟦ mergeP cmp xs ys ⟧P ≈ merge cmp ⟦ xs ⟧P ⟦ ys ⟧P
merge-hom cmp xs ys with whnf xs | whnf ys
... | x ∷ xs′ | y ∷ ys′ with cmp x y
... | lt = x ∷ ♯ merge-hom cmp xs′ (y ∷ ♯ ys′)
... | eq = x ∷ ♯ merge-hom cmp xs′ ys′
... | gt = y ∷ ♯ merge-hom cmp (x ∷ ♯ xs′) ys′
merge-cong : ∀ {A} (cmp : A → A → Ord) {xs xs′ ys ys′} →
xs ≈ xs′ → ys ≈ ys′ →
merge cmp xs ys ≈ 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-correct : ⟦ hamming ⟧P ≈
1 ∷ ♯ merge cmp (S.map (_*_ 2) ⟦ hamming ⟧P)
(S.map (_*_ 3) ⟦ hamming ⟧P)
hamming-correct =
1 ∷ ♯ SS.trans (merge-hom cmp (map (_*_ 2) hamming)
(map (_*_ 3) hamming))
(merge-cong cmp (map-hom (_*_ 2) hamming)
(map-hom (_*_ 3) hamming))