module BranchF(branchF,branchFSP) where
import Direction
import Fudget
import Route
import SP
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 (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
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)
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)
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)