verigraph-1.1.1: Software specification and verification tool based on graph rewriting.

Safe Haskell	Safe
Language	Haskell2010

Abstract.Relation

Contents

Types
Construction
Transformation
Query
- Predicates

Synopsis

Types

data Relation a Source #

Datatype for endorelations on a

Instances

(Eq a, Ord a) => Eq (Relation a) Source #
Methods (==) :: Relation a -> Relation a -> Bool # (/=) :: Relation a -> Relation a -> Bool #
Ord a => Ord (Relation a) Source #
Methods compare :: Relation a -> Relation a -> Ordering # (<) :: Relation a -> Relation a -> Bool # (<=) :: Relation a -> Relation a -> Bool # (>) :: Relation a -> Relation a -> Bool # (>=) :: Relation a -> Relation a -> Bool # max :: Relation a -> Relation a -> Relation a # min :: Relation a -> Relation a -> Relation a #
(Ord a, Read a) => Read (Relation a) Source #
Methods readsPrec :: Int -> ReadS (Relation a) # readList :: ReadS [Relation a] # readPrec :: ReadPrec (Relation a) # readListPrec :: ReadPrec [Relation a] #
Show a => Show (Relation a) Source #
Methods showsPrec :: Int -> Relation a -> ShowS # show :: Relation a -> String # showList :: [Relation a] -> ShowS #

Construction

empty :: Ord a => [a] -> [a] -> Relation a Source #

An empty relation, with domain and codomain specified.

Transformation

compose :: Ord a => Relation a -> Relation a -> Relation a Source #

Compose r1 and r2.

id :: Ord a => [a] -> Relation a Source #

The identity relation on dom.

inverseRelation :: Ord a => Relation a -> Relation a Source #

The inverse relation.

updateRelation :: Ord a => a -> a -> Relation a -> Relation a Source #

Add a mapping between x and y to the relation. If x already exists, y is joined to the corresponding elements.

removeFromDomain :: Ord a => a -> Relation a -> Relation a Source #

Remove an element from the domain of the relation

removeFromCodomain :: Ord a => a -> Relation a -> Relation a Source #

Remove an element from the codomain of the relation

insertOnCodomain :: Ord a => a -> Relation a -> Relation a Source #

Insert an element on the codomain of the relation

Query

apply :: Ord a => Relation a -> a -> [a] Source #

Return a list of all elements that x gets mapped into.

domain :: Relation a -> [a] Source #

codomain :: Relation a -> [a] Source #

image :: Eq a => Relation a -> [a] Source #

Return a list of all elements in the image of the relation.

mapping :: Relation a -> Map a [a] Source #

orphans :: Eq a => Relation a -> [a] Source #

Return the elements in the domain which are not in the image of the relation (orphans)

Predicates

isFunctional :: Relation a -> Bool Source #

Test if r is functional.

isInjective :: Ord a => Relation a -> Bool Source #

Test if r is injective.

isPartialInjective :: Ord a => [a] -> Relation a -> Bool Source #

Test if r is injective out of domain list

isSurjective :: Ord a => Relation a -> Bool Source #

Test if r is surjective.

isTotal :: Ord a => Relation a -> Bool Source #

Test if r is total.