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 :: 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{-ff-} (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

--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) 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)

--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) 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)

--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) 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)