content: -- Synchronous stream processors
  module SPS where
  
  newtype S i o = S (i->(o,S i o))
  feed (S sps) i = sps i
  
  
  runS _       []     = []
  runS sps (i:is) = continue (feed sps i) is
  continue c is = fst c:runS (snd c) is
  
  mapS_sps f i = (f i,S (mapS_sps f))
  
  mapS f = S (mapS_sps f)
  
  mapAccumS_sps f s1 i =
    case f s1 i of (s2,o2) -> (o2,S (mapAccumS_sps f s2))
  
  mapAccumS f s0 = S (mapAccumS_sps f s0)
  
  --(>*<) :: S i1 o1 -> S i2 o2 -> S (i1,i2) (o1,o2)
  sps1 >*< sps2 = S (sps_times sps1 sps2)
  sps_times sps1 sps2 (i1,i2) =
    case feed sps1 i1 of
      (o1,s1) -> case feed sps2 i2 of
        (o2,s2) -> ((o1,o2), s1 >*< s2)
  
  (>+<) :: S i1 o1 -> S i2 o2 -> S (Either i1 i2) (Either o1 o2)
  sps1 >+< sps2 = S (sps_plus sps1 sps2)
  
  sps_plus sps1 sps2 (Left  i1) = case feed sps1 i1 of (o1,sps1') -> (Left  o1,sps1'>+<sps2)
  sps_plus sps1 sps2 (Right i2) = case feed sps2 i2 of (o2,sps2') -> (Right o2,sps1>+<sps2')
  
  sps1 -<- sps2 = S (sps_compose sps1 sps2)
  sps_compose sps1 sps2 i2 = 
    case feed sps2 i2 of
      (o2,sps2') -> case feed sps1 o2 of
        (o1,sps1') -> (o1,sps1'-<-sps2')
  
  assert Separation1 = {-#cert:Separation1#-}
    All sps1 . All sps2 . All is1 . All is2 .
    {runS (sps1>*<sps2) (zip is1 is2)} === {zip (runS sps1 is1) (runS sps2 is2)}
  --{-
  assert Separation2 =
    All sps1a . All sps1b . All sps2a . All sps2b .
    {(sps1a>*<sps1b)-<-(sps2a>*<sps2b)}===
    {(sps1a-<-sps2a)>*<(sps1b-<-sps2b)}
  --}
  
  assert Separation3 =
    All sps1 . All sps2 . All is .
    {split (runS (sps1>+<sps2) is)} ===
      {(runS sps1 (lefts is),runS sps2 (rights is))}
  
  split zs = (lefts zs,rights zs)
  lefts [] = []
  lefts (Left x:zs) = x : lefts zs
  lefts (Right _:zs) = lefts zs
  rights [] = []
  rights (Left _:zs) = rights zs
  rights (Right x:zs) = x : rights zs
  