Copyright	(C) 2017 ATS Advanced Telematic Systems GmbH
License	BSD-style (see the file LICENSE)
Maintainer	Stevan Andjelkovic <stevan@advancedtelematic.com>
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Test.StateMachine.Z

Description

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.

Synopsis

union :: Eq a => [a] -> [a] -> [a]
intersect :: Eq a => [a] -> [a] -> [a]
isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic
type Rel a b = [(a, b)]
type Fun a b = Rel a b
empty :: Rel a b
identity :: [a] -> Rel a a
singleton :: a -> b -> Rel a b
domain :: Rel a b -> [a]
codomain :: Rel a b -> [b]
compose :: Eq b => Rel b c -> Rel a b -> Rel a c
fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c
inverse :: Rel a b -> Rel b a
lookupDom :: Eq a => a -> Rel a b -> [b]
lookupCod :: Eq b => b -> Rel a b -> [a]
(<|) :: Eq a => [a] -> Rel a b -> Rel a b
(|>) :: Eq b => Rel a b -> [b] -> Rel a b
(<-|) :: Eq a => [a] -> Rel a b -> Rel a b
(|->) :: Eq b => Rel a b -> [b] -> Rel a b
image :: Eq a => Rel a b -> [a] -> [b]
(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)
(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d)
isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic
isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic
isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic
isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic
isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic
isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b
(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b
(.!) :: Rel a b -> a -> (Rel a b, a)
(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b

Documentation

union :: Eq a => [a] -> [a] -> [a] Source #

intersect :: Eq a => [a] -> [a] -> [a] Source #

isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic Source #

(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic Source #

type Rel a b = [(a, b)] Source #

Relations.

type Fun a b = Rel a b Source #

(Partial) functions.

empty :: Rel a b Source #

identity :: [a] -> Rel a a Source #

singleton :: a -> b -> Rel a b Source #

domain :: Rel a b -> [a] Source #

codomain :: Rel a b -> [b] Source #

compose :: Eq b => Rel b c -> Rel a b -> Rel a c Source #

fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c Source #

inverse :: Rel a b -> Rel b a Source #

lookupDom :: Eq a => a -> Rel a b -> [b] Source #

lookupCod :: Eq b => b -> Rel a b -> [a] Source #

(<|) :: Eq a => [a] -> Rel a b -> Rel a b Source #

Domain restriction.

>>> ['a'] <| [ ('a', "apa"), ('b', "bepa") ]
[('a',"apa")]

(|>) :: Eq b => Rel a b -> [b] -> Rel a b Source #

Codomain restriction.

>>> [ ('a', "apa"), ('b', "bepa") ] |> ["apa"]
[('a',"apa")]

(<-|) :: Eq a => [a] -> Rel a b -> Rel a b Source #

Domain substraction.

>>> ['a'] <-| [ ('a', "apa"), ('b', "bepa") ]
[('b',"bepa")]

(|->) :: Eq b => Rel a b -> [b] -> Rel a b Source #

Codomain substraction.

>>> [ ('a', "apa"), ('b', "bepa") ] |-> ["apa"]
[('b',"bepa")]

image :: Eq a => Rel a b -> [a] -> [b] Source #

The image of a relation.

(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b Source #

Overriding.

>>> [('a', "apa")] <+ [('a', "bepa")]
[('a',"bepa")]

>>> [('a', "apa")] <+ [('b', "bepa")]
[('a',"apa"),('b',"bepa")]

(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c) Source #

Direct product.

(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d) Source #

Parallel product.

isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic Source #

isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic Source #

isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic Source #

isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic Source #

isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic Source #

isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic Source #

isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic Source #

isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic Source #

isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic Source #

isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic Source #

(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b Source #

Application.

(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b Source #

(.!) :: Rel a b -> a -> (Rel a b, a) Source #

(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b Source #

Assignment.

>>> singleton 'a' "apa" .! 'a' .= "bepa"
[('a',"bepa")]

>>> singleton 'a' "apa" .! 'b' .= "bepa"
[('a',"apa"),('b',"bepa")]