{- Agda can check termination of Stream transducer operations.
(Created: Andreas Abel, 2008-12-01
at Agda Intensive Meeting 9 in Sendai, Japan.
I acknowledge the support by AIST and JST.)
Stream transducers have been described in:
N. Ghani, P. Hancock, and D. Pattinson,
Continuous functions on final coalgebras.
In Proc. CMCS 2006, Electr. Notes in Theoret. Comp. Sci., 2006.
They have been modelled by mixed equi-(co)inductive sized types in
A. Abel,
Mixed Inductive/Coinductive Types and Strong Normalization.
In APLAS 2007, LNCS 4807.
Here we model them by mutual data/codata and mutual recursion/corecursion.
Cf. examples/StreamEating.agda
-}
module StreamProc where
open import Common.Coinduction
data Stream (A : Set) : Set where
cons : A -> ∞ (Stream A) -> Stream A
-- Stream Transducer: Trans A B
-- intended semantics: Stream A -> Stream B
mutual
data Trans (A B : Set) : Set where
〈_〉 : ∞ (Trans' A B) -> Trans A B
data Trans' (A B : Set) : Set where
get : (A -> Trans' A B) -> Trans' A B
put : B -> Trans A B -> Trans' A B
out : forall {A B} -> Trans A B -> Trans' A B
out 〈 p 〉 = p
-- evaluating a stream transducer ("stream eating")
mutual
-- eat is defined by corecursion into Stream B
eat : forall {A B} -> Trans A B -> Stream A -> Stream B
eat 〈 sp 〉 as ~ eat' sp as
-- eat' is defined by a local recursion on Trans' A B
eat' : forall {A B} -> Trans' A B -> Stream A -> Stream B
eat' (get f) (cons a as) = eat' (f a) as
eat' (put b sp) as = cons b (eat sp as)
-- composing two stream transducers
mutual
-- comb is defined by corecursion into Trans A B
comb : forall {A B C} -> Trans A B -> Trans B C -> Trans A C
comb 〈 p1 〉 〈 p2 〉 ~ 〈 comb' p1 p2 〉
-- comb' preforms a local lexicographic recursion on (Trans' B C, Trans' A B)
comb' : forall {A B C} -> Trans' A B -> Trans' B C -> Trans' A C
comb' (put b p1) (get f) = comb' (out p1) (f b)
comb' (put b p1) (put c p2) = put c (comb p1 p2)
comb' (get f) p2 = get (\ a -> comb' (f a) p2)