module Main
%default total
data SP : Type -> Type -> Type where
Get : (a -> SP a b) -> SP a b
Put : b -> Inf (SP a b) -> SP a b
copy : SP a a
copy = Get (\x => Put x copy)
process : SP a b -> Stream a -> Stream b
process (Get f) (x :: xs) = process (f x) xs
process (Put b sp) xs = process sp xs
doubleInt : SP Nat Int
doubleInt = Get (\x => Put (the Int (cast x))
(Put (the Int (cast x) * 2) doubleInt))
countStream : Nat -> Stream Nat
countStream x = x :: countStream (x + 1)
main : IO ()
main = printLn (take 10 (process doubleInt (countStream 1)))