{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Z
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  portable
--
-- This module contains Z-inspried combinators for working with relations. The
-- idea is that they can be used to define concise and showable models. This
-- module is an experiment and will likely change or move to its own package.
--
-----------------------------------------------------------------------------

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           Data.Maybe
                   (fromMaybe)
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 = [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
L.union

intersect :: Eq a => [a] -> [a] -> [a]
intersect :: forall a. Eq a => [a] -> [a] -> [a]
intersect = [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
L.intersect

-- | Subset.
--
-- >>> boolean ([1, 2] `isSubsetOf` [3, 2, 1])
-- True
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 [a] -> [a] -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== [a]
r [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
s

-- | Set equality.
--
-- >>> boolean ([1, 1, 2] ~= [2, 1])
-- True
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic
[a]
xs ~= :: forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= [a]
ys = [a]
xs [a] -> [a] -> Logic
forall a. (Eq a, Show a) => [a] -> [a] -> Logic
`isSubsetOf` [a]
ys Logic -> Logic -> Logic
.&& [a]
ys [a] -> [a] -> Logic
forall a. (Eq a, Show a) => [a] -> [a] -> Logic
`isSubsetOf` [a]
xs

------------------------------------------------------------------------

-- | Relations.
type Rel a b = [(a, b)]

-- | (Partial) functions.
type Fun a b = Rel a b

infixr 1 :->
type a :-> b = Fun a b

-- Partial function.
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 b -> b -> Bool
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 = Rel b c -> Rel a b -> Rel a c
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 Rel a b -> ((a, b) -> [b]) -> [b]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
x', b
y) -> [ b
y | a
x a -> a -> Bool
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 Rel a b -> ((a, b) -> [a]) -> [a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
x, b
y') -> [ a
x | b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
y' ]

------------------------------------------------------------------------

-- | Domain restriction.
--
-- >>> ['a'] <| [ ('a', "apa"), ('b', "bepa") ]
-- [('a',"apa")]
--
(<|) :: 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 a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.elem` [a]
xs ]

-- | Codomain restriction.
--
-- >>> [ ('a', "apa"), ('b', "bepa") ] |> ["apa"]
-- [('a',"apa")]
--
(|>) :: 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 b -> [b] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.elem` [b]
ys ]

-- | Domain substraction.
--
-- >>> ['a'] <-| [ ('a', "apa"), ('b', "bepa") ]
-- [('b',"bepa")]
--
(<-|) :: 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 a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.notElem` [a]
xs ]

-- | Codomain substraction.
--
-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"]
-- [('b',"bepa"),('c',"cepa")]
--
-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa", "cepa"]
-- [('b',"bepa")]
--
-- >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"] |-> ["cepa"]
-- [('b',"bepa")]
--
(|->) :: 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 b -> [b] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`P.notElem` [b]
ys ]

-- | The image of a relation.
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 = Rel a b -> [b]
forall a b. Rel a b -> [b]
codomain ([a]
xs [a] -> Rel a b -> Rel a b
forall a b. Eq a => [a] -> Rel a b -> Rel a b
<| Rel a b
r)

-- | Overriding.
--
-- >>> [('a', "apa")] <+ [('a', "bepa")]
-- [('a',"bepa")]
--
-- >>> [('a', "apa")] <+ [('b', "bepa")]
-- [('a',"apa"),('b',"bepa")]
--
(<+) :: (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  = (Rel a b -> [a]
forall a b. Rel a b -> [a]
domain Rel a b
s [a] -> Rel a b -> Rel a b
forall a b. Eq a => [a] -> Rel a b -> Rel a b
<-| Rel a b
r) Rel a b -> Rel a b -> Rel a b
forall a. Eq a => [a] -> [a] -> [a]
`union` Rel a b
s

-- | Direct product.
(<**>) :: 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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x'
  ]

-- | Parallel product.
(<||>) :: 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 = Rel a b -> [a]
forall a b. Rel a b -> [a]
domain Rel a b
r [a] -> [a] -> Logic
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 = Rel a b -> [b]
forall a b. Rel a b -> [b]
codomain Rel a b
r [b] -> [b] -> Logic
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 = Rel a b -> [a] -> Logic
forall a b. (Eq a, Show a) => Rel a b -> [a] -> Logic
isTotalRel Rel a b
r [a]
xs Logic -> Logic -> Logic
:&& Rel a b -> [b] -> 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 Rel a b -> Rel b a -> Rel b b
forall b c a. Eq b => Rel b c -> Rel a b -> Rel a c
`compose` Rel a b -> Rel b a
forall a b. Rel a b -> Rel b a
inverse Rel a b
f) Rel b b -> Rel b b -> Logic
forall a. (Eq a, Show a) => [a] -> [a] -> Logic
~= [b] -> Rel b b
forall a. [a] -> Rel a a
identity (Rel a b -> [b]
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 = Rel a b -> Logic
forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& Rel a b -> [a] -> 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 = Rel a b -> Logic
forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& Rel b a -> Logic
forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun (Rel a b -> Rel b a
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 = Rel a b -> [a] -> Logic
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
:&& Rel b a -> Logic
forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun (Rel a b -> Rel b a
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 = Rel a b -> Logic
forall a b. (Eq a, Eq b, Show b) => Rel a b -> Logic
isPartialFun Rel a b
r Logic -> Logic -> Logic
:&& Rel a b -> [b] -> 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 = Rel a b -> [a] -> Logic
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
:&& Rel a b -> [b] -> 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 = Rel a b -> [a] -> Logic
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
:&& Rel a b -> [a] -> [b] -> 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

-- | Application.
(!) :: (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 = b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
msg) (a -> Fun a b -> Maybe b
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 `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"' in `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Fun a b -> [Char]
forall a. Show a => a -> [Char]
show Fun a b
f [Char] -> [Char] -> [Char]
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 = a -> Fun a b -> Maybe b
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 Fun a b -> a -> (Fun a b, a)
forall a b. Rel a b -> a -> (Rel a b, a)
.! a
x (Fun a b, a) -> b -> Fun a b
forall a b. (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b
.= b -> b
g (Fun a b
f Fun a b -> a -> b
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)

-- | Assignment.
--
-- >>> singleton 'a' "apa" .! 'a' .= "bepa"
-- [('a',"bepa")]
--
-- >>> singleton 'a' "apa" .! 'b' .= "bepa"
-- [('a',"apa"),('b',"bepa")]
--
(.=) :: (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 Rel a b -> Rel a b -> Rel a b
forall a b. (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
<+ a -> b -> Rel a b
forall a b. a -> b -> Rel a b
singleton a
x b
y