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) = LayoutHint
-> F (Either a c) (Either b d) -> F (Either a c) (Either b d)
forall a b. LayoutHint -> F a b -> F a b
layoutHintF LayoutHint
parHint (FSP (Either a c) (Either b d) -> F (Either a c) (Either b d)
forall hi ho. FSP hi ho -> F hi ho
F{-ff-} (FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
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' :: 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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (Either b d -> Message TCommand (Either b d)
forall a b. b -> Message a b
High (b -> Either b d
forall a b. a -> Either a b
Left b
x)) (FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (TCommand -> Message TCommand (Either b d)
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnLeft TCommand
tcmd) (FSP a b -> FSP c d -> FSP (Either a c) (Either b d)
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 -> (FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
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 -> FSP c d -> FSP (Either a c) (Either b d)
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 :: (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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (Either b d -> Message TCommand (Either b d)
forall a b. b -> Message a b
High (d -> Either b d
forall a b. b -> Either a b
Right d
y)) ((FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (TCommand -> Message TCommand (Either b d)
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnRight TCommand
tcmd) ((FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
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 -> (FEvent (Either a c) -> FSP (Either a c) (Either b d))
-> FSP (Either a c) (Either b d)
forall a b. (a -> SP a b) -> SP a b
GetSP ((FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
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 -> (FEvent (Either a c) -> FSP (Either a c) (Either b d))
-> FSP (Either a c) (Either b d)
forall a b. (a -> SP a b) -> SP a b
GetSP ((FEvent a -> FSP a b)
-> FEvent (Either a c) -> FSP (Either a c) (Either b d)
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 :: 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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (Either b d -> Message TCommand (Either b d)
forall a b. b -> Message a b
High (b -> Either b d
forall a b. a -> Either a b
Left b
x)) (FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
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' -> Message TCommand (Either b d)
-> FSP (Either a c) (Either b d) -> FSP (Either a c) (Either b d)
forall a b. b -> SP a b -> SP a b
PutSP (TCommand -> Message TCommand (Either b d)
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnLeft TCommand
tcmd) (FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
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 -> (FEvent (Either a c) -> FSP (Either a c) (Either b d))
-> FSP (Either a c) (Either b d)
forall a b. (a -> SP a b) -> SP a b
GetSP ((FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
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 -> (FEvent (Either a c) -> FSP (Either a c) (Either b d))
-> FSP (Either a c) (Either b d)
forall a b. (a -> SP a b) -> SP a b
GetSP ((FEvent c -> FSP c d)
-> FEvent (Either a c) -> FSP (Either a c) (Either b d)
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 :: (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) -> FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
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 (a -> FEvent a
forall a b. b -> Message a b
High a
x)) FEvent c -> FSP c d
xf2
      High (Right c
y) -> (FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
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 (c -> FEvent c
forall a b. b -> Message a b
High c
y))
      Low (Path
tag, FResponse
ev) -> case Path
tag of
                         Direction
L : Path
tag' -> FSP a b -> (FEvent c -> FSP c d) -> FSP (Either a c) (Either b d)
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 ((Path, FResponse) -> FEvent a
forall a b. a -> Message a b
Low (Path
tag', FResponse
ev))) FEvent c -> FSP c d
xf2
                         Direction
R : Path
tag' -> (FEvent a -> FSP a b) -> FSP c d -> FSP (Either a c) (Either b d)
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 ((Path, FResponse) -> FEvent c
forall a b. a -> Message a b
Low (Path
tag', FResponse
ev)))
                         Path
_ -> {-ctrace "drop" (tag,ev) $-} (FEvent (Either a c) -> FSP (Either a c) (Either b d))
-> FSP (Either a c) (Either b d)
forall a b. (a -> SP a b) -> SP a b
GetSP ((FEvent a -> FSP a b)
-> (FEvent c -> FSP c d)
-> FEvent (Either a c)
-> FSP (Either a c) (Either b d)
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' -> Message (Path, b1) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
forall a b. b -> SP a b -> SP a b
PutSP (Either a b -> Message (Path, b1) (Either a b)
forall a b. b -> Message a b
High (b -> Either a b
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' -> Message (Path, b1) (Either a b)
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) (Either a b)
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 -> (Message (Path, b) (Either a b)
 -> SP
      (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b)))
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (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)
      SP (Message (Path, b) b) (Message (Path, b1) b)
NullSP -> SP
  (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b))
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 (b -> Message (Path, b) b
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 ((Path, b) -> Message (Path, b) b
forall a b. a -> Message a b
Low (Path
tag, b
ev)))
      Message (Path, b) (Either a b)
_ -> (Message (Path, b) (Either a b)
 -> SP
      (Message (Path, b) (Either a b)) (Message (Path, b1) (Either a b)))
-> SP
     (Message (Path, b) (Either a b)) (Message (Path, b1) (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' -> Message (Path, b1) (Either a b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
forall a b. b -> SP a b -> SP a b
PutSP (Either a b -> Message (Path, b1) (Either a b)
forall a b. b -> Message a b
High (a -> Either a b
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' -> Message (Path, b1) (Either a b)
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) (Either a b)
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 -> (Message (Path, b) (Either b b)
 -> SP
      (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b)))
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (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) 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 -> SP
  (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b))
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 (b -> Message (Path, b) b
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 ((Path, b) -> Message (Path, b) b
forall a b. a -> Message a b
Low (Path
tag, b
ev)))
      Message (Path, b) (Either b b)
_ -> (Message (Path, b) (Either b b)
 -> SP
      (Message (Path, b) (Either b b)) (Message (Path, b1) (Either a b)))
-> SP
     (Message (Path, b) (Either b b)) (Message (Path, b1) (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) 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)