module BranchF(branchF,branchFSP) where
import Direction
import Fudget
--import Path(Path(..))
import Route
import SP
--import Message(Message(..))

branchF :: (F (Path, a) b) -> (F (Path, a) b) -> F (Path, a) b
branchF :: forall a b. F (Path, a) b -> F (Path, a) b -> F (Path, a) b
branchF (F FSP (Path, a) b
f1) (F FSP (Path, a) b
f2) = forall hi ho. FSP hi ho -> F hi ho
F{-ff-} (forall a b. FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
branchFSP FSP (Path, a) b
f1 FSP (Path, a) b
f2)

branchFSP :: (FSP (Path, a) b) -> (FSP (Path, a) b) -> FSP (Path, a) b
branchFSP :: forall a b. FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
branchFSP FSP (Path, a) b
f1 FSP (Path, a) b
f2 =
    case FSP (Path, a) b
f1 of
      PutSP (Low TCommand
tcmd) FSP (Path, 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. FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
branchFSP FSP (Path, a) b
f1' FSP (Path, a) b
f2)
      PutSP Message TCommand b
msg FSP (Path, a) b
f1' -> forall a b. b -> SP a b -> SP a b
PutSP Message TCommand b
msg (forall a b. FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
branchFSP FSP (Path, a) b
f1' FSP (Path, a) b
f2)
      GetSP FEvent (Path, a) -> FSP (Path, a) b
xf1 -> forall {b} {b} {b1} {b2}.
(Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 FEvent (Path, a) -> FSP (Path, a) b
xf1 FSP (Path, a) b
f2
      FSP (Path, a) b
NullSP -> forall {b} {b} {b1} {b2}.
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2 FSP (Path, a) b
f2

--and branchF1:: (FEvent *a->F *a *b) -> F *c *d -> F (Either *a *c) (Either *b *d)
branchF1 :: (Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2 =
    case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2 of
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
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) ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2')
      PutSP Message (Path, b1) b2
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2' -> forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b2
msg ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2')
      GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)
      SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
NullSP -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall {b} {b} {b1} {b2}.
(Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1)

--and branchF2:: F *a *b -> (FEvent *c->F *c *d) -> F (Either *a *c) (Either *b *d)
branchF2 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 =
    case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1 of
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
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) (Path, b)) (Message (Path, b1) b2)
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1' Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)
      PutSP Message (Path, b1) b2
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1' -> forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b2
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1' Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)
      GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)
      SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
NullSP -> forall a b. (a -> SP a b) -> SP a b
GetSP (forall {b} {b} {b1} {b2}.
(Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)

--and branchF12:: (FEvent *a->F *a *b) -> (FEvent *c->F *c *d) -> FEvent (Either *a *c) -> F (Either *a *c) (Either *b *d)
branchF12 :: (Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 Message (Path, b) (Path, b)
msg =
    case Message (Path, b) (Path, b)
msg of
      High (Direction
L : Path
path', b
x) -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 (forall a b. b -> Message a b
High (Path
path', b
x))) Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2
      High (Direction
R : Path
path', b
y) -> (Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 (forall a b. b -> Message a b
High (Path
path', b
y)))
      Low (Direction
L : Path
path', b
x) -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 (forall a b. a -> Message a b
Low (Path
path', b
x))) Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2
      Low (Direction
R : Path
path', b
y) -> (Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 (forall a b. a -> Message a b
Low (Path
path', b
y)))
      Message (Path, b) (Path, b)
_ -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> (Message (Path, b) (Path, b)
    -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)

restF2 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2 =
    case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2 of
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
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) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2')
      PutSP Message (Path, b1) b2
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2' -> forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b2
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f2')
      GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf2)
      SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
NullSP -> forall a b. SP a b
NullSP

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

restF1 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1 =
    case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1 of
      PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
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) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1')
      PutSP Message (Path, b1) b2
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1' -> forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b2
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
f1')
      GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1 -> forall a b. (a -> SP a b) -> SP a b
GetSP ((Message (Path, b) (Path, b)
 -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
xf1)
      SP (Message (Path, b) (Path, b)) (Message (Path, b1) b2)
NullSP -> forall a b. SP a b
NullSP

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