{-# LANGUAGE TypeOperators #-}
module Test.StateMachine.Z
( cons
, union
, intersect
, isSubsetOf
, (~=)
, Rel
, Fun
, (:<->)
, (:->)
, (:/->)
, empty
, identity
, singleton
, domain
, codomain
, compose
, fcompose
, inverse
, lookupDom
, lookupCod
, (<|)
, (|>)
, (<-|)
, (|->)
, image
, (<+)
, (<**>)
, (<||>)
, isTotalRel
, isSurjRel
, isTotalSurjRel
, isPartialFun
, isTotalFun
, isPartialInj
, isTotalInj
, isPartialSurj
, isTotalSurj
, isBijection
, (!)
, (!?)
, (.%)
, (.!)
, (.=)
) where
import qualified Data.List as L
import Prelude hiding
(elem, notElem)
import qualified Prelude as P
import Test.StateMachine.Logic
infixr 6 `union`
infixr 7 `intersect`
infix 5 `isSubsetOf`
infix 5 ~=
infixr 4 <|
infixl 4 |>
infixr 4 <-|
infixl 4 |->
infixr 4 <+
infixl 4 <**>
infixl 4 <||>
infixr 4 .%
infixr 9 .!
infix 4 .=
cons :: a -> [a] -> [a]
cons :: forall a. a -> [a] -> [a]
cons = (:)
union :: Eq a => [a] -> [a] -> [a]
union :: forall a. Eq a => [a] -> [a] -> [a]
union = forall a. Eq a => [a] -> [a] -> [a]
L.union
intersect :: Eq a => [a] -> [a] -> [a]
intersect :: forall a. Eq a => [a] -> [a] -> [a]
intersect = forall a. Eq a => [a] -> [a] -> [a]
L.intersect
isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic
[a]
r isSubsetOf :: forall a. (Eq a, Show a) => [a] -> [a] -> Logic
`isSubsetOf` [a]
s = [a]
r forall a. (Eq a, Show a) => a -> a -> Logic
.== [a]
r forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
s
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic
[a]
xs ~= :: forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= [a]
ys = [a]
xs forall a. (Eq a, Show a) => [a] -> [a] -> Logic
`isSubsetOf` [a]
ys Logic -> Logic -> Logic
.&& [a]
ys forall a. (Eq a, Show a) => [a] -> [a] -> Logic
`isSubsetOf` [a]
xs
type Rel a b = [(a, b)]
type Fun a b = Rel a b
infixr 1 :->
type a :-> b = Fun a b
infixr 1 :/->
type a :/-> b = Fun a b
infixr 1 :<->
type a :<-> b = Rel a b
empty :: Rel a b
empty :: forall a b. Rel a b
empty = []
identity :: [a] -> Rel a a
identity :: forall a. [a] -> Rel a a
identity [a]
xs = [ (a
x, a
x) | a
x <- [a]
xs ]
singleton :: a -> b -> Rel a b
singleton :: forall a b. a -> b -> Rel a b
singleton a
x b
y = [(a
x, b
y)]
domain :: Rel a b -> [a]
domain :: forall a b. Rel a b -> [a]
domain Rel a b
xys = [ a
x | (a
x, b
_) <- Rel a b
xys ]
codomain :: Rel a b -> [b]
codomain :: forall a b. Rel a b -> [b]
codomain Rel a b
xys = [ b
y | (a
_, b
y) <- Rel a b
xys ]
compose :: Eq b => Rel b c -> Rel a b -> Rel a c
compose :: forall b c a. Eq b => Rel b c -> Rel a b -> Rel a c
compose Rel b c
yzs Rel a b
xys =
[ (a
x, c
z)
| (a
x, b
y) <- Rel a b
xys
, (b
y', c
z) <- Rel b c
yzs
, b
y forall a. Eq a => a -> a -> Bool
== b
y'
]
fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c
fcompose :: forall b a c. Eq b => Rel a b -> Rel b c -> Rel a c
fcompose Rel a b
r Rel b c
s = forall b c a. Eq b => Rel b c -> Rel a b -> Rel a c
compose Rel b c
s Rel a b
r
inverse :: Rel a b -> Rel b a
inverse :: forall a b. Rel a b -> Rel b a
inverse Rel a b
xys = [ (b
y, a
x) | (a
x, b
y) <- Rel a b
xys ]
lookupDom :: Eq a => a -> Rel a b -> [b]
lookupDom :: forall a b. Eq a => a -> Rel a b -> [b]
lookupDom a
x Rel a b
xys = Rel a b
xys forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
x', b
y) -> [ b
y | a
x forall a. Eq a => a -> a -> Bool
== a
x' ]
lookupCod :: Eq b => b -> Rel a b -> [a]
lookupCod :: forall b a. Eq b => b -> Rel a b -> [a]
lookupCod b
y Rel a b
xys = Rel a b
xys forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
x, b
y') -> [ a
x | b
y forall a. Eq a => a -> a -> Bool
== b
y' ]
(<|) :: Eq a => [a] -> Rel a b -> Rel a b
[a]
xs <| :: forall a b. Eq a => [a] -> Rel a b -> Rel a b
<| Rel a b
xys = [ (a
x, b
y) | (a
x, b
y) <- Rel a b
xys, a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.elem` [a]
xs ]
(|>) :: Eq b => Rel a b -> [b] -> Rel a b
Rel a b
xys |> :: forall b a. Eq b => Rel a b -> [b] -> Rel a b
|> [b]
ys = [ (a
x, b
y) | (a
x, b
y) <- Rel a b
xys, b
y forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.elem` [b]
ys ]
(<-|) :: Eq a => [a] -> Rel a b -> Rel a b
[a]
xs <-| :: forall a b. Eq a => [a] -> Rel a b -> Rel a b
<-| Rel a b
xys = [ (a
x, b
y) | (a
x, b
y) <- Rel a b
xys, a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.notElem` [a]
xs ]
(|->) :: Eq b => Rel a b -> [b] -> Rel a b
Rel a b
xys |-> :: forall b a. Eq b => Rel a b -> [b] -> Rel a b
|-> [b]
ys = [ (a
x, b
y) | (a
x, b
y) <- Rel a b
xys, b
y forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.notElem` [b]
ys ]
image :: Eq a => Rel a b -> [a] -> [b]
image :: forall a b. Eq a => Rel a b -> [a] -> [b]
image Rel a b
r [a]
xs = forall a b. Rel a b -> [b]
codomain ([a]
xs forall a b. Eq a => [a] -> Rel a b -> Rel a b
<| Rel a b
r)
(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
Rel a b
r <+ :: forall a b. (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
<+ Rel a b
s = (forall a b. Rel a b -> [a]
domain Rel a b
s forall a b. Eq a => [a] -> Rel a b -> Rel a b
<-| Rel a b
r) forall a. Eq a => [a] -> [a] -> [a]
`union` Rel a b
s
(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)
Rel a b
xys <**> :: forall a b c. Eq a => Rel a b -> Rel a c -> Rel a (b, c)
<**> Rel a c
xzs =
[ (a
x, (b
y, c
z))
| (a
x , b
y) <- Rel a b
xys
, (a
x', c
z) <- Rel a c
xzs
, a
x forall a. Eq a => a -> a -> Bool
== a
x'
]
(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d)
Rel a c
acs <||> :: forall a c b d. Rel a c -> Rel b d -> Rel (a, b) (c, d)
<||> Rel b d
bds =
[ ((a
a, b
b), (c
c, d
d))
| (a
a, c
c) <- Rel a c
acs
, (b
b, d
d) <- Rel b d
bds
]
isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic
isTotalRel :: forall a b. (Eq a, Show a) => Rel a b -> [a] -> Logic
isTotalRel Rel a b
r [a]
xs = forall a b. Rel a b -> [a]
domain Rel a b
r forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= [a]
xs
isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic
isSurjRel :: forall b a. (Eq b, Show b) => Rel a b -> [b] -> Logic
isSurjRel Rel a b
r [b]
ys = forall a b. Rel a b -> [b]
codomain Rel a b
r forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= [b]
ys
isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isTotalSurjRel :: forall a b.
(Eq a, Eq b, Show a, Show b) =>
Rel a b -> [a] -> [b] -> Logic
isTotalSurjRel Rel a b
r [a]
xs [b]
ys = forall a b. (Eq a, Show a) => Rel a b -> [a] -> Logic
isTotalRel Rel a b
r [a]
xs Logic -> Logic -> Logic
:&& forall b a. (Eq b, Show b) => Rel a b -> [b] -> Logic
isSurjRel Rel a b
r [b]
ys
isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun :: forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
f = (Rel a b
f forall b c a. Eq b => Rel b c -> Rel a b -> Rel a c
`compose` forall a b. Rel a b -> Rel b a
inverse Rel a b
f) forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= forall a. [a] -> Rel a a
identity (forall a b. Rel a b -> [b]
codomain Rel a b
f)
isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalFun :: forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalFun Rel a b
r [a]
xs = forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& forall a b. (Eq a, Show a) => Rel a b -> [a] -> Logic
isTotalRel Rel a b
r [a]
xs
isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic
isPartialInj :: forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic
isPartialInj Rel a b
r = forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun (forall a b. Rel a b -> Rel b a
inverse Rel a b
r)
isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalInj :: forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalInj Rel a b
r [a]
xs = forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalFun Rel a b
r [a]
xs Logic -> Logic -> Logic
:&& forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun (forall a b. Rel a b -> Rel b a
inverse Rel a b
r)
isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic
isPartialSurj :: forall a b. (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic
isPartialSurj Rel a b
r [b]
ys = forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& forall b a. (Eq b, Show b) => Rel a b -> [b] -> Logic
isSurjRel Rel a b
r [b]
ys
isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isTotalSurj :: forall a b.
(Eq a, Eq b, Show a, Show b) =>
Rel a b -> [a] -> [b] -> Logic
isTotalSurj Rel a b
r [a]
xs [b]
ys = forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalFun Rel a b
r [a]
xs Logic -> Logic -> Logic
:&& forall b a. (Eq b, Show b) => Rel a b -> [b] -> Logic
isSurjRel Rel a b
r [b]
ys
isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isBijection :: forall a b.
(Eq a, Eq b, Show a, Show b) =>
Rel a b -> [a] -> [b] -> Logic
isBijection Rel a b
r [a]
xs [b]
ys = forall a b. (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isTotalInj Rel a b
r [a]
xs Logic -> Logic -> Logic
:&& forall a b.
(Eq a, Eq b, Show a, Show b) =>
Rel a b -> [a] -> [b] -> Logic
isTotalSurj Rel a b
r [a]
xs [b]
ys
(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b
Fun a b
f ! :: forall a b. (Eq a, Show a, Show b) => Fun a b -> a -> b
! a
x = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error [Char]
msg) forall a. a -> a
Prelude.id (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x Fun a b
f)
where
msg :: [Char]
msg = [Char]
"!: failed to lookup `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
x forall a. [a] -> [a] -> [a]
++ [Char]
"' in `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Fun a b
f forall a. [a] -> [a] -> [a]
++ [Char]
"'"
(!?) :: Eq a => Fun a b -> a -> Maybe b
Fun a b
f !? :: forall a b. Eq a => Fun a b -> a -> Maybe b
!? a
x = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x Fun a b
f
(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b
(Fun a b
f, a
x) .% :: forall a b.
(Eq a, Eq b, Show a, Show b) =>
(Fun a b, a) -> (b -> b) -> Fun a b
.% b -> b
g = Fun a b
f forall a b. Rel a b -> a -> (Rel a b, a)
.! a
x forall a b. (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b
.= b -> b
g (Fun a b
f forall a b. (Eq a, Show a, Show b) => Fun a b -> a -> b
! a
x)
(.!) :: Rel a b -> a -> (Rel a b, a)
Rel a b
f .! :: forall a b. Rel a b -> a -> (Rel a b, a)
.! a
x = (Rel a b
f, a
x)
(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b
(Rel a b
f, a
x) .= :: forall a b. (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b
.= b
y = Rel a b
f forall a b. (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
<+ forall a b. a -> b -> Rel a b
singleton a
x b
y