------------------------------------------------------------------------
-- Andreas Abel and Brigitte Pientka,
-- Wellfounded Recursion with Copatterns and Sized Types.
--
-- Journal of Functional Programming, volume 26, 2016
--
-- Agda code for examples
------------------------------------------------------------------------

{-# OPTIONS --postfix-projections #-}

module StreamProcessors where

open import Prelude

------------------------------------------------------------------------
-- Section 2.5 Example: Stream processor
------------------------------------------------------------------------

-- Streams

record Str (i : Size) (A : Set) : Set where
  coinductive
  field force : ∀{j : Size< i} → A × Str j A
open Str

hd : ∀{i A} → Str (↑ i) A → A
hd s = s .force .fst

tl : ∀{i A} → Str (↑ i) A → Str i A
tl s = s .force .snd

-- Stream processors reading As and writing Bs

data SPμ (i : Size) (A B X : Set) : Set where
  get : ∀{j : Size< i} (f : A → SPμ j A B X) → SPμ i A B X
  put : B × X → SPμ i A B X

record SPν (i : Size) (A B : Set) : Set where
  coinductive
  field out : ∀{j : Size< i} → SPμ ∞ A B (SPν j A B)
open SPν

-- Running a stream processor on a stream of As gives a stream of Bs

mutual
  runμ : ∀{i j A B} → SPμ j A B (SPν i A B) → Str ∞ A → B × Str i B
  runμ (get f)        vs = runμ (f (hd vs)) (tl vs)
  runμ (put (w , sp)) vs = w , runν sp vs

  runν : ∀{i A B} → SPν i A B → Str ∞ A → Str i B
  runν sp vs .force = runμ (sp .out) vs