module CompF(compF) where
import Fudget
--import Message(Message(..))
import Route
import SP
import Direction
import LayoutHints

--import Maptrace(ctrace) -- debugging

compF :: F a b -> F c d -> F (Either a c) (Either b d)
compF (F FSP a b
f1) (F FSP c d
f2) = forall a b. LayoutHint -> F a b -> F a b
layoutHintF LayoutHint
parHint (forall hi ho. FSP hi ho -> F hi ho
F{-ff-} (forall a b c d. FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
compF' FSP a b
f1 FSP c d
f2))

compF' :: FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
compF' :: forall a b c d. FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
compF' FSP a b
f1 FSP c d
f2 =
    case FSP a b
f1 of
      PutSP (High b
x) FSP a b
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall a b. b -> Message a b
High (forall a b. a -> Either a b
Left b
x)) (forall a b c d. FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
compF' FSP a b
f1' FSP c d
f2)
      PutSP (Low TCommand
tcmd) FSP a b
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall {b1} {b2}. (Path, b1) -> Message (Path, b1) b2
compTurnLeft TCommand
tcmd) (forall a b c d. FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
compF' FSP a b
f1' FSP c d
f2)
      GetSP FEvent a -> FSP a b
xf1 -> forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 FSP c d
f2
      FSP a b
NullSP -> forall {b} {b} {b1} {b} {a} {a}.
SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 FSP c d
f2

compF1 :: (FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 :: forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 FSP c d
f2 =
    case FSP c d
f2 of
      PutSP (High d
y) FSP c d
f2' -> forall a b. b -> SP a b -> SP a b
PutSP (forall a b. b -> Message a b
High (forall a b. b -> Either a b
Right d
y)) (forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 FSP c d
f2')
      PutSP (Low TCommand
tcmd) FSP c d
f2' -> forall a b. b -> SP a b -> SP a b
PutSP (forall {b1} {b2}. (Path, b1) -> Message (Path, b1) b2
compTurnRight TCommand
tcmd) (forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 FSP c d
f2')
      GetSP FEvent c -> FSP c d
xf2 -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall a b c d.
(FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
compF12 FEvent a -> FSP a b
xf1 FEvent c -> FSP c d
xf2)
      FSP c d
NullSP -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall {b} {b} {b1} {a} {b} {b}.
(Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) a))
-> Message (Path, b) (Either b b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1x FEvent a -> FSP a b
xf1)

compF2 :: FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 :: forall a b c d.
FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 FSP a b
f1 FEvent c -> FSP c d
xf2 =
    case FSP a b
f1 of
      PutSP (High b
x) FSP a b
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall a b. b -> Message a b
High (forall a b. a -> Either a b
Left b
x)) (forall a b c d.
FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 FSP a b
f1' FEvent c -> FSP c d
xf2)
      PutSP (Low TCommand
tcmd) FSP a b
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall {b1} {b2}. (Path, b1) -> Message (Path, b1) b2
compTurnLeft TCommand
tcmd) (forall a b c d.
FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 FSP a b
f1' FEvent c -> FSP c d
xf2)
      GetSP FEvent a -> FSP a b
xf1 -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall a b c d.
(FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
compF12 FEvent a -> FSP a b
xf1 FEvent c -> FSP c d
xf2)
      FSP a b
NullSP -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall {b} {b} {b1} {b} {a} {a}.
(Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) b))
-> Message (Path, b) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2x FEvent c -> FSP c d
xf2)

compF12 :: (FEvent a -> FSP a b) -> (FEvent c -> FSP c d) -> (FEvent (Either a c)) -> FSP (Either a c) (Either b d)
compF12 :: forall a b c d.
(FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
compF12 FEvent a -> FSP a b
xf1 FEvent c -> FSP c d
xf2 FEvent (Either a c)
msg =
    case FEvent (Either a c)
msg of
      High (Left a
x) -> forall a b c d.
FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 (FEvent a -> FSP a b
xf1 (forall a b. b -> Message a b
High a
x)) FEvent c -> FSP c d
xf2
      High (Right c
y) -> forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 (FEvent c -> FSP c d
xf2 (forall a b. b -> Message a b
High c
y))
      Low (Path
tag, FResponse
ev) -> case Path
tag of
                         Direction
L : Path
tag' -> forall a b c d.
FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
compF2 (FEvent a -> FSP a b
xf1 (forall a b. a -> Message a b
Low (Path
tag', FResponse
ev))) FEvent c -> FSP c d
xf2
                         Direction
R : Path
tag' -> forall a b c d.
(FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
compF1 FEvent a -> FSP a b
xf1 (FEvent c -> FSP c d
xf2 (forall a b. a -> Message a b
Low (Path
tag', FResponse
ev)))
                         Path
_ -> {-ctrace "drop" (tag,ev) $-} forall a b. (a -> SP a b) -> SP a b
GetSP (forall a b c d.
(FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
compF12 FEvent a -> FSP a b
xf1 FEvent c -> FSP c d
xf2)

restF2 :: SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 SP (Message (Path, b) b) (Message (Path, b1) b)
f2 =
    case SP (Message (Path, b) b) (Message (Path, b1) b)
f2 of
      PutSP (High b
y) SP (Message (Path, b) b) (Message (Path, b1) b)
f2' -> forall a b. b -> SP a b -> SP a b
PutSP (forall a b. b -> Message a b
High (forall a b. b -> Either a b
Right b
y)) (SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 SP (Message (Path, b) b) (Message (Path, b1) b)
f2')
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) b) (Message (Path, b1) b)
f2' -> forall a b. b -> SP a b -> SP a b
PutSP (forall {b1} {b2}. (Path, b1) -> Message (Path, b1) b2
compTurnRight (Path, b1)
tcmd) (SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 SP (Message (Path, b) b) (Message (Path, b1) b)
f2')
      GetSP Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) b))
-> Message (Path, b) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2)
      SP (Message (Path, b) b) (Message (Path, b1) b)
NullSP -> forall a b. SP a b
NullSP

restF2x :: (Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) b))
-> Message (Path, b) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2 Message (Path, b) (Either a b)
msg =
    case Message (Path, b) (Either a b)
msg of
      High (Right b
y) -> SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 (Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2 (forall a b. b -> Message a b
High b
y))
      Low (Direction
R : Path
tag, b
ev) -> SP (Message (Path, b) b) (Message (Path, b1) b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2 (Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2 (forall a b. a -> Message a b
Low (Path
tag, b
ev)))
      Message (Path, b) (Either a b)
_ -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) b))
-> Message (Path, b) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
restF2x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) b)
xf2)

restF1 :: SP (Message (Path, b) b) (Message (Path, b1) a)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1 SP (Message (Path, b) b) (Message (Path, b1) a)
f1 =
    case SP (Message (Path, b) b) (Message (Path, b1) a)
f1 of
      PutSP (High a
y) SP (Message (Path, b) b) (Message (Path, b1) a)
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall a b. b -> Message a b
High (forall a b. a -> Either a b
Left a
y)) (SP (Message (Path, b) b) (Message (Path, b1) a)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1 SP (Message (Path, b) b) (Message (Path, b1) a)
f1')
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) b) (Message (Path, b1) a)
f1' -> forall a b. b -> SP a b -> SP a b
PutSP (forall {b1} {b2}. (Path, b1) -> Message (Path, b1) b2
compTurnLeft (Path, b1)
tcmd) (SP (Message (Path, b) b) (Message (Path, b1) a)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1 SP (Message (Path, b) b) (Message (Path, b1) a)
f1')
      GetSP Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) a))
-> Message (Path, b) (Either b b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1)
      SP (Message (Path, b) b) (Message (Path, b1) a)
NullSP -> forall a b. SP a b
NullSP

restF1x :: (Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) a))
-> Message (Path, b) (Either b b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1 Message (Path, b) (Either b b)
msg =
    case Message (Path, b) (Either b b)
msg of
      High (Left b
x) -> SP (Message (Path, b) b) (Message (Path, b1) a)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1 (Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1 (forall a b. b -> Message a b
High b
x))
      Low (Direction
L : Path
tag, b
ev) -> SP (Message (Path, b) b) (Message (Path, b1) a)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1 (Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1 (forall a b. a -> Message a b
Low (Path
tag, b
ev)))
      Message (Path, b) (Either b b)
_ -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) b
 -> SP (Message (Path, b) b) (Message (Path, b1) a))
-> Message (Path, b) (Either b b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
restF1x Message (Path, b) b
-> SP (Message (Path, b) b) (Message (Path, b1) a)
xf1)