module CompSP(prepostMapSP, postMapSP, preMapSP, idRightSP, idLeftSP, idHighSP,
idLowSP, compMsgSP, compSP, compEitherSP, serCompSP) where
import Message(Message(..))
import SP
import Spops
serCompSP :: SP a b -> SP a a -> SP a b
serCompSP SP a b
sp1 SP a a
sp2 =
case SP a b
sp1 of
PutSP b
y SP a b
sp1' -> b -> SP a b -> SP a b
forall a b. b -> SP a b -> SP a b
PutSP b
y (SP a b -> SP a a -> SP a b
serCompSP SP a b
sp1' SP a a
sp2)
GetSP a -> SP a b
xsp1 -> (a -> SP a b) -> SP a a -> SP a b
serCompSP1 a -> SP a b
xsp1 SP a a
sp2
SP a b
NullSP -> SP a b
forall a b. SP a b
NullSP
serCompSP1 :: (a -> SP a b) -> SP a a -> SP a b
serCompSP1 a -> SP a b
xsp1 SP a a
sp2 =
case SP a a
sp2 of
PutSP a
y SP a a
sp2' -> SP a b -> SP a a -> SP a b
serCompSP (a -> SP a b
xsp1 a
y) SP a a
sp2'
GetSP a -> SP a a
xsp2 -> (a -> SP a b) -> SP a b
forall a b. (a -> SP a b) -> SP a b
GetSP ((a -> SP a b) -> SP a a -> SP a b
serCompSP1 a -> SP a b
xsp1 (SP a a -> SP a b) -> (a -> SP a a) -> a -> SP a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SP a a
xsp2)
SP a a
NullSP -> SP a b
forall a b. SP a b
NullSP
compSP :: SP a a -> SP a b -> SP (Either a a) (Either a b)
compSP = SP a a -> SP a b -> SP (Either a a) (Either a b)
forall a a a b. SP a a -> SP a b -> SP (Either a a) (Either a b)
compEitherSP
compEitherSP :: SP a a -> SP a b -> SP (Either a a) (Either a b)
compEitherSP SP a a
sp1 SP a b
sp2 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Either a b
-> SP (Either a a) (Either a b) -> SP (Either a a) (Either a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Either a b
forall a b. a -> Either a b
Left a
y) (SP a a -> SP a b -> SP (Either a a) (Either a b)
compEitherSP SP a a
sp1' SP a b
sp2)
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> SP a b -> SP (Either a a) (Either a b)
forall a a a b.
(a -> SP a a) -> SP a b -> SP (Either a a) (Either a b)
compEitherSP1 a -> SP a a
xsp1 SP a b
sp2
SP a a
NullSP -> SP a b -> SP (Either a a) (Either a b)
forall a b a a. SP a b -> SP (Either a a) (Either a b)
rEitherSP SP a b
sp2
compEitherSP1 :: (a -> SP a a) -> SP a b -> SP (Either a a) (Either a b)
compEitherSP1 a -> SP a a
xsp1 SP a b
sp2 =
case SP a b
sp2 of
PutSP b
y SP a b
sp2' -> Either a b
-> SP (Either a a) (Either a b) -> SP (Either a a) (Either a b)
forall a b. b -> SP a b -> SP a b
PutSP (b -> Either a b
forall a b. b -> Either a b
Right b
y) ((a -> SP a a) -> SP a b -> SP (Either a a) (Either a b)
compEitherSP1 a -> SP a a
xsp1 SP a b
sp2')
GetSP a -> SP a b
xsp2 -> (a -> SP a a) -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP12 a -> SP a a
xsp1 a -> SP a b
xsp2
SP a b
NullSP -> SP a a -> SP (Either a a) (Either a b)
forall a a b b. SP a a -> SP (Either a b) (Either a b)
lEitherSP ((a -> SP a a) -> SP a a
forall a b. (a -> SP a b) -> SP a b
GetSP a -> SP a a
xsp1)
compEitherSP2 :: SP a a -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP2 SP a a
sp1 a -> SP a b
xsp2 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Either a b
-> SP (Either a a) (Either a b) -> SP (Either a a) (Either a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Either a b
forall a b. a -> Either a b
Left a
y) (SP a a -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP2 SP a a
sp1' a -> SP a b
xsp2)
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP12 a -> SP a a
xsp1 a -> SP a b
xsp2
SP a a
NullSP -> SP a b -> SP (Either a a) (Either a b)
forall a b a a. SP a b -> SP (Either a a) (Either a b)
rEitherSP ((a -> SP a b) -> SP a b
forall a b. (a -> SP a b) -> SP a b
GetSP a -> SP a b
xsp2)
compEitherSP12 :: (a -> SP a a) -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP12 a -> SP a a
xsp1 a -> SP a b
xsp2 =
(Either a a -> SP (Either a a) (Either a b))
-> SP (Either a a) (Either a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Either a a
x ->
case Either a a
x of
Left a
a -> SP a a -> (a -> SP a b) -> SP (Either a a) (Either a b)
compEitherSP2 (a -> SP a a
xsp1 a
a) a -> SP a b
xsp2
Right a
b -> (a -> SP a a) -> SP a b -> SP (Either a a) (Either a b)
compEitherSP1 a -> SP a a
xsp1 (a -> SP a b
xsp2 a
b))
lEitherSP :: SP a a -> SP (Either a b) (Either a b)
lEitherSP SP a a
sp1 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Either a b
-> SP (Either a b) (Either a b) -> SP (Either a b) (Either a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Either a b
forall a b. a -> Either a b
Left a
y) (SP a a -> SP (Either a b) (Either a b)
lEitherSP SP a a
sp1')
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> SP (Either a b) (Either a b)
lEitherSP1 a -> SP a a
xsp1
SP a a
NullSP -> SP (Either a b) (Either a b)
forall a b. SP a b
NullSP
lEitherSP1 :: (a -> SP a a) -> SP (Either a b) (Either a b)
lEitherSP1 a -> SP a a
xsp1 =
(Either a b -> SP (Either a b) (Either a b))
-> SP (Either a b) (Either a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Either a b
x ->
case Either a b
x of
Left a
a -> SP a a -> SP (Either a b) (Either a b)
lEitherSP (a -> SP a a
xsp1 a
a)
Right b
b -> (a -> SP a a) -> SP (Either a b) (Either a b)
lEitherSP1 a -> SP a a
xsp1)
rEitherSP :: SP a b -> SP (Either a a) (Either a b)
rEitherSP SP a b
sp2 =
case SP a b
sp2 of
PutSP b
y SP a b
sp2' -> Either a b
-> SP (Either a a) (Either a b) -> SP (Either a a) (Either a b)
forall a b. b -> SP a b -> SP a b
PutSP (b -> Either a b
forall a b. b -> Either a b
Right b
y) (SP a b -> SP (Either a a) (Either a b)
rEitherSP SP a b
sp2')
GetSP a -> SP a b
xsp2 -> (a -> SP a b) -> SP (Either a a) (Either a b)
rEitherSP2 a -> SP a b
xsp2
SP a b
NullSP -> SP (Either a a) (Either a b)
forall a b. SP a b
NullSP
rEitherSP2 :: (a -> SP a b) -> SP (Either a a) (Either a b)
rEitherSP2 a -> SP a b
xsp2 =
(Either a a -> SP (Either a a) (Either a b))
-> SP (Either a a) (Either a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Either a a
x ->
case Either a a
x of
Right a
a -> SP a b -> SP (Either a a) (Either a b)
rEitherSP (a -> SP a b
xsp2 a
a)
Left a
b -> (a -> SP a b) -> SP (Either a a) (Either a b)
rEitherSP2 a -> SP a b
xsp2)
preMapSP :: SP a b -> (t -> a) -> SP t b
preMapSP SP a b
sp t -> a
pre =
case SP a b
sp of
PutSP b
y SP a b
sp' -> b -> SP t b -> SP t b
forall a b. b -> SP a b -> SP a b
PutSP b
y (SP a b -> (t -> a) -> SP t b
preMapSP SP a b
sp' t -> a
pre)
GetSP a -> SP a b
xsp -> (t -> SP t b) -> SP t b
forall a b. (a -> SP a b) -> SP a b
GetSP (\t
x -> SP a b -> (t -> a) -> SP t b
preMapSP (a -> SP a b
xsp (t -> a
pre t
x)) t -> a
pre)
SP a b
NullSP -> SP t b
forall a b. SP a b
NullSP
postMapSP :: (t -> b) -> SP a t -> SP a b
postMapSP t -> b
post SP a t
sp =
case SP a t
sp of
PutSP t
y SP a t
sp' -> b -> SP a b -> SP a b
forall a b. b -> SP a b -> SP a b
PutSP (t -> b
post t
y) ((t -> b) -> SP a t -> SP a b
postMapSP t -> b
post SP a t
sp')
GetSP a -> SP a t
xsp -> (a -> SP a b) -> SP a b
forall a b. (a -> SP a b) -> SP a b
GetSP (\a
x -> (t -> b) -> SP a t -> SP a b
postMapSP t -> b
post (a -> SP a t
xsp a
x))
SP a t
NullSP -> SP a b
forall a b. SP a b
NullSP
prepostMapSP :: (t -> a) -> (t -> b) -> SP a t -> SP t b
prepostMapSP t -> a
pre t -> b
post SP a t
sp =
case SP a t
sp of
PutSP t
y SP a t
sp' -> b -> SP t b -> SP t b
forall a b. b -> SP a b -> SP a b
PutSP (t -> b
post t
y) ((t -> a) -> (t -> b) -> SP a t -> SP t b
prepostMapSP t -> a
pre t -> b
post SP a t
sp')
GetSP a -> SP a t
xsp -> (t -> SP t b) -> SP t b
forall a b. (a -> SP a b) -> SP a b
GetSP (\t
x -> (t -> a) -> (t -> b) -> SP a t -> SP t b
prepostMapSP t -> a
pre t -> b
post (a -> SP a t
xsp (t -> a
pre t
x)))
SP a t
NullSP -> SP t b
forall a b. SP a b
NullSP
idLowSP :: SP a b -> SP (Message a a) (Message a b)
idLowSP SP a b
sp = SP a a -> SP a b -> SP (Message a a) (Message a b)
forall a a a b. SP a a -> SP a b -> SP (Message a a) (Message a b)
compMsgSP SP a a
forall b. SP b b
idSP SP a b
sp
idHighSP :: SP a a -> SP (Message a b) (Message a b)
idHighSP SP a a
sp = SP a a -> SP b b -> SP (Message a b) (Message a b)
forall a a a b. SP a a -> SP a b -> SP (Message a a) (Message a b)
compMsgSP SP a a
sp SP b b
forall b. SP b b
idSP
idLeftSP :: SP a b -> SP (Either a a) (Either a b)
idLeftSP SP a b
sp = SP a a -> SP a b -> SP (Either a a) (Either a b)
forall a a a b. SP a a -> SP a b -> SP (Either a a) (Either a b)
compEitherSP SP a a
forall b. SP b b
idSP SP a b
sp
idRightSP :: SP a a -> SP (Either a b) (Either a b)
idRightSP SP a a
sp = SP a a -> SP b b -> SP (Either a b) (Either a b)
forall a a a b. SP a a -> SP a b -> SP (Either a a) (Either a b)
compEitherSP SP a a
sp SP b b
forall b. SP b b
idSP
compMsgSP :: SP a a -> SP a b -> SP (Message a a) (Message a b)
compMsgSP SP a a
sp1 SP a b
sp2 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Message a b
-> SP (Message a a) (Message a b) -> SP (Message a a) (Message a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Message a b
forall a b. a -> Message a b
Low a
y) (SP a a -> SP a b -> SP (Message a a) (Message a b)
compMsgSP SP a a
sp1' SP a b
sp2)
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> SP a b -> SP (Message a a) (Message a b)
forall a a a b.
(a -> SP a a) -> SP a b -> SP (Message a a) (Message a b)
compMsgSP1 a -> SP a a
xsp1 SP a b
sp2
SP a a
NullSP -> SP a b -> SP (Message a a) (Message a b)
forall a b a a. SP a b -> SP (Message a a) (Message a b)
rMsgSP SP a b
sp2
compMsgSP1 :: (a -> SP a a) -> SP a b -> SP (Message a a) (Message a b)
compMsgSP1 a -> SP a a
xsp1 SP a b
sp2 =
case SP a b
sp2 of
PutSP b
y SP a b
sp2' -> Message a b
-> SP (Message a a) (Message a b) -> SP (Message a a) (Message a b)
forall a b. b -> SP a b -> SP a b
PutSP (b -> Message a b
forall a b. b -> Message a b
High b
y) ((a -> SP a a) -> SP a b -> SP (Message a a) (Message a b)
compMsgSP1 a -> SP a a
xsp1 SP a b
sp2')
GetSP a -> SP a b
xsp2 -> (a -> SP a a) -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP12 a -> SP a a
xsp1 a -> SP a b
xsp2
SP a b
NullSP -> SP a a -> SP (Message a a) (Message a b)
forall a a b b. SP a a -> SP (Message a b) (Message a b)
lMsgSP ((a -> SP a a) -> SP a a
forall a b. (a -> SP a b) -> SP a b
GetSP a -> SP a a
xsp1)
compMsgSP2 :: SP a a -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP2 SP a a
sp1 a -> SP a b
xsp2 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Message a b
-> SP (Message a a) (Message a b) -> SP (Message a a) (Message a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Message a b
forall a b. a -> Message a b
Low a
y) (SP a a -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP2 SP a a
sp1' a -> SP a b
xsp2)
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP12 a -> SP a a
xsp1 a -> SP a b
xsp2
SP a a
NullSP -> SP a b -> SP (Message a a) (Message a b)
forall a b a a. SP a b -> SP (Message a a) (Message a b)
rMsgSP ((a -> SP a b) -> SP a b
forall a b. (a -> SP a b) -> SP a b
GetSP a -> SP a b
xsp2)
compMsgSP12 :: (a -> SP a a) -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP12 a -> SP a a
xsp1 a -> SP a b
xsp2 =
(Message a a -> SP (Message a a) (Message a b))
-> SP (Message a a) (Message a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Message a a
x ->
case Message a a
x of
Low a
a -> SP a a -> (a -> SP a b) -> SP (Message a a) (Message a b)
compMsgSP2 (a -> SP a a
xsp1 a
a) a -> SP a b
xsp2
High a
b -> (a -> SP a a) -> SP a b -> SP (Message a a) (Message a b)
compMsgSP1 a -> SP a a
xsp1 (a -> SP a b
xsp2 a
b))
lMsgSP :: SP a a -> SP (Message a b) (Message a b)
lMsgSP SP a a
sp1 =
case SP a a
sp1 of
PutSP a
y SP a a
sp1' -> Message a b
-> SP (Message a b) (Message a b) -> SP (Message a b) (Message a b)
forall a b. b -> SP a b -> SP a b
PutSP (a -> Message a b
forall a b. a -> Message a b
Low a
y) (SP a a -> SP (Message a b) (Message a b)
lMsgSP SP a a
sp1')
GetSP a -> SP a a
xsp1 -> (a -> SP a a) -> SP (Message a b) (Message a b)
lMsgSP1 a -> SP a a
xsp1
SP a a
NullSP -> SP (Message a b) (Message a b)
forall a b. SP a b
NullSP
lMsgSP1 :: (a -> SP a a) -> SP (Message a b) (Message a b)
lMsgSP1 a -> SP a a
xsp1 =
(Message a b -> SP (Message a b) (Message a b))
-> SP (Message a b) (Message a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Message a b
x ->
case Message a b
x of
Low a
a -> SP a a -> SP (Message a b) (Message a b)
lMsgSP (a -> SP a a
xsp1 a
a)
High b
b -> (a -> SP a a) -> SP (Message a b) (Message a b)
lMsgSP1 a -> SP a a
xsp1)
rMsgSP :: SP a b -> SP (Message a a) (Message a b)
rMsgSP SP a b
sp2 =
case SP a b
sp2 of
PutSP b
y SP a b
sp2' -> Message a b
-> SP (Message a a) (Message a b) -> SP (Message a a) (Message a b)
forall a b. b -> SP a b -> SP a b
PutSP (b -> Message a b
forall a b. b -> Message a b
High b
y) (SP a b -> SP (Message a a) (Message a b)
rMsgSP SP a b
sp2')
GetSP a -> SP a b
xsp2 -> (a -> SP a b) -> SP (Message a a) (Message a b)
rMsgSP2 a -> SP a b
xsp2
SP a b
NullSP -> SP (Message a a) (Message a b)
forall a b. SP a b
NullSP
rMsgSP2 :: (a -> SP a b) -> SP (Message a a) (Message a b)
rMsgSP2 a -> SP a b
xsp2 =
(Message a a -> SP (Message a a) (Message a b))
-> SP (Message a a) (Message a b)
forall a b. (a -> SP a b) -> SP a b
GetSP (\Message a a
x ->
case Message a a
x of
High a
a -> SP a b -> SP (Message a a) (Message a b)
rMsgSP (a -> SP a b
xsp2 a
a)
Low a
b -> (a -> SP a b) -> SP (Message a a) (Message a b)
rMsgSP2 a -> SP a b
xsp2)