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 :: 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) = FSP (Path, a) b -> F (Path, a) b
forall hi ho. FSP hi ho -> F hi ho
F (FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
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 :: 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' -> Message TCommand b -> FSP (Path, a) b -> FSP (Path, a) b
forall a b. b -> SP a b -> SP a b
PutSP (TCommand -> Message TCommand b
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnLeft TCommand
tcmd) (FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
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' -> Message TCommand b -> FSP (Path, a) b -> FSP (Path, a) b
forall a b. b -> SP a b -> SP a b
PutSP Message TCommand b
msg (FSP (Path, a) b -> FSP (Path, a) b -> FSP (Path, a) b
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 -> (FEvent (Path, a) -> FSP (Path, a) b)
-> FSP (Path, a) b -> FSP (Path, a) b
forall b b b1 b.
(Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 FEvent (Path, a) -> FSP (Path, a) b
xf1 FSP (Path, a) b
f2
FSP (Path, a) b
NullSP -> FSP (Path, a) b -> FSP (Path, a) b
forall b b b1 b.
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 FSP (Path, a) b
f2
branchF1 :: (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2 =
case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2 of
PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) b
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) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2')
PutSP Message (Path, b1) b
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b
msg ((Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2')
GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
NullSP -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall b b b1 b.
(Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1)
branchF2 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 =
case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1 of
PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) b
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnLeft (Path, b1)
tcmd) (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
PutSP Message (Path, b1) b
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
NullSP -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall b b b1 b.
(Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
branchF12 :: (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
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) b)
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 ((Path, b) -> Message (Path, b) (Path, b)
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) b)
xf2
High (Direction
R : Path
path', b
y) -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 ((Path, b) -> Message (Path, b) (Path, b)
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) b)
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 ((Path, b) -> Message (Path, b) (Path, b)
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) b)
xf2
Low (Direction
R : Path
path', b
y) -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 ((Path, b) -> Message (Path, b) (Path, b)
forall a b. a -> Message a b
Low (Path
path', b
y)))
Message (Path, b) (Path, b)
_ -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
branchF12 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
restF2 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2 =
case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2 of
PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) b
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnRight (Path, b1)
tcmd) (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2')
PutSP Message (Path, b1) b
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f2')
GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
NullSP -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. SP a b
NullSP
restF2x :: (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
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) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 ((Path, b) -> Message (Path, b) (Path, b)
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) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2 ((Path, b) -> Message (Path, b) (Path, b)
forall a b. a -> Message a b
Low (Path
path', b
ev)))
Message (Path, b) (Path, b)
_ -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF2x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf2)
restF1 :: SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1 =
case SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1 of
PutSP (Low (Path, b1)
tcmd) SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP ((Path, b1) -> Message (Path, b1) b
forall b1 b2. (Path, b1) -> Message (Path, b1) b2
compTurnLeft (Path, b1)
tcmd) (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1')
PutSP Message (Path, b1) b
msg SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1' -> Message (Path, b1) b
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. b -> SP a b -> SP a b
PutSP Message (Path, b1) b
msg (SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1 SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
f1')
GetSP Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1)
SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
NullSP -> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
forall a b. SP a b
NullSP
restF1x :: (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
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) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 ((Path, b) -> Message (Path, b) (Path, b)
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) b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1 (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1 ((Path, b) -> Message (Path, b) (Path, b)
forall a b. a -> Message a b
Low (Path
path', b
ev)))
Message (Path, b) (Path, b)
_ -> (Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b))
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) 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) b))
-> Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
restF1x Message (Path, b) (Path, b)
-> SP (Message (Path, b) (Path, b)) (Message (Path, b1) b)
xf1)