ContextLattice

models a Lattice for a context type, the top of the lattice is represented by One and inherits a list of all subcontexts, the bottom of the lattice is represented by Zero. To inherit the contextlattice to a new data type the data type has to instanciate: Enumerable c, Eq c, Ord c, Show c

Documentation

data Context c

data type to represent a lattice structure, the actual context is the type variable c

Constructors

One [Context c]

constructor represents the One element of the lattice, all contexts are included in this constructor, for this constructor the model includes all contexts

Ctx [c]

constructor for one context

Zero

constructor represents the bottom element of the lattice, without any context

Instances

Eq c => Eq (Context c)

Ord c => Ord (Context c)

Show c => Show (Context c)

(Enumerable c, Eq c, Enumerable (Context c)) => MeetSemiLattice (Context c)

makes the Context c type to a MeetSemiLattice by implementing the meet function

getFinerContexts

Arguments

:: (Eq c, Enumerable c, Enumerable (Context c))

=> Context c

context that is used as start

-> [Context c]

all finer contexts of the start context included in the lattice

takes a context and returns all finer

extractContext

Arguments

:: Context c

Context where elements are extracted from,

-> [[c]]

extracted context list

extracts a context list of contexts from the element, needed for the One wrapper constructor

propCommutative

Arguments

:: (Eq c, Enumerable c, Enumerable (Context c))

=> Context c

context one

-> Context c

context two

-> Bool

true if the property is full-filled

test for commutativity

>>> (Ctx [Walking]) `propCommutative` One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] = (Ctx [Walking]) `meet` One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] == One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] `meet` (Ctx [Walking])
true

propIdempotent

Arguments

:: (Eq c, Enumerable c, Enumerable (Context c))

=> Context c

context to test

-> Bool

true if the property is full-filled

test for idempotency

>>> propIdempotent (Ctx [Walking]) = (Ctx [Walking]) `meet` (Ctx [Walking]) == (Ctx [Walking])
true

propAssociative

Arguments

:: (Eq c, Enumerable c, Enumerable (Context c))

=> Context c

context one

-> Context c

context two

-> Context c

context three

-> Bool

true if the property is full-filled

test for associativity

>>> propAssociative (Ctx [Walking]) (Ctx [Driving]) (Ctx [Uphill]) =  (Ctx [Walking]) `meet` ((Ctx [Driving]) `meet` (Ctx [Uphill])) == ((Ctx [Walking]) `meet` (Ctx [Driving])) `meet` (Ctx [Uphill])
true