Hets - the Heterogeneous Tool Set

Copyright (c) Ewaryst Schulz, DFKI Bremen 2010 GPLv2 or higher, see LICENSE.txt ewaryst.schulz@dfki.de experimental portable Safe-Inferred

CSL.TreePO

Description

This module defines a basic datatype for tree-like partial orderings such as encountered, e.g., in the set lattice.

Synopsis

# Documentation

data Incomparable

Constructors

 Disjoint Overlap

data SetOrdering

Constructors

 Comparable Ordering Incomparable Incomparable

data InfDev

We represent Intervals with opened or closed end points over a linearly ordered type `a` as closed intervals over the type '(a, InfDev)', for infinitesimal deviation. - '(x, EpsLeft)' means an epsilon to the left of x - '(x, Zero)' means x - '(x, EpsRight)' means an epsilon to the right of x We have EpsLeft < Zero < EpsRight and the ordering of `a` lifts to the lexicographical ordering of '(a, InfDev)' which captures well our intended meaning. We inject the type `a` into the type '(a, InfDev)' by mapping `x` to '(x, Zero)'. The mapping of intrvals is as follows: A left opened interval starting at x becomes a left closed interval starting at '(x, EpsRight)'. We have: 'forall y > x. (y, _) > (x, EpsRight)', hence in particular '(y, Zero) > (x, EpsRight)' but also '(x, Zero) < (x, EpsRight)'

Analogously we represent a right opened one ending at y as a closed one ending at '(x, EpsLeft)'.

Constructors

 EpsLeft Zero EpsRight

Instances

 Eq InfDev Data InfDev Ord InfDev Show InfDev ShATermConvertible InfDev Typeable * InfDev

newtype CIType a

Constructors

 CIType (a, InfDev)

Instances

 Eq a => Eq (CIType a) Data a => Data (CIType a) Ord a => Ord (CIType a) This type with the given ordering is to represent opened/closed intervals over `a` as closed intervals over '(a, InfDev)' Show a => Show (CIType a) ShATermConvertible a => ShATermConvertible (CIType a) Typeable (* -> *) CIType

data SetOrInterval a

A finite set or an interval. True = closed, False = opened interval border.

Constructors

 Set (Set a) IntVal (a, Bool) (a, Bool)

Instances

 Eq a => Eq (SetOrInterval a) (Data a, Ord a) => Data (SetOrInterval a) Ord a => Ord (SetOrInterval a) Show a => Show (SetOrInterval a) (Ord a, ShATermConvertible a) => ShATermConvertible (SetOrInterval a) (Ord a, Pretty a) => Pretty (SetOrInterval a) Typeable (* -> *) SetOrInterval

data ClosedInterval a

A closed interval

Constructors

 ClosedInterval a a

Instances

 Eq a => Eq (ClosedInterval a) Data a => Data (ClosedInterval a) Ord a => Ord (ClosedInterval a) Show a => Show (ClosedInterval a) ShATermConvertible a => ShATermConvertible (ClosedInterval a) Pretty a => Pretty (ClosedInterval a) Typeable (* -> *) ClosedInterval

data InfInt

Infinite integers = integers augmented by -Infty and +Infty

Constructors

 PosInf NegInf FinInt Integer

Instances

 Eq InfInt Data InfInt Ord InfInt Show InfInt ShATermConvertible InfInt Discrete InfInt Pretty InfInt Typeable * InfInt

class Continuous a

Instances

 Continuous GroundConstant

class Discrete a where

Methods

nextA :: a -> a

prevA :: a -> a

intsizeA :: a -> a -> Maybe Integer

Instances

 Discrete InfInt

cmpClosedInts

Arguments

 :: Ord a => ClosedInterval a l1, r1 -> ClosedInterval a l2, r2 -> SetOrdering

Compares closed intervals [l1, r1] and [l2, r2]. Assumes non-singular intervals, i.e., l1 < r1 and l2 < r2. Works only for linearly ordered types.

membSoID :: (Discrete a, Ord a) => a -> SetOrInterval a -> Bool

Membership in `SetOrInterval`

nullSoID :: (Discrete a, Ord a) => SetOrInterval a -> Bool

Checks if the set is empty.

toSingularD :: (Discrete a, Ord a) => SetOrInterval a -> Maybe a

If the set is singular, i.e., consists only from one point, then we return this point. Reports error on empty SoI's.

setToClosedIntD :: (Discrete a, Ord a) => SetOrInterval a -> ClosedInterval a

Transforms a `SetOrInterval` to a closed representation

cmpSoIsD :: (Discrete a, Ord a) => SetOrInterval a -> SetOrInterval a -> SetOrdering

Compare sets over discrete types

cmpSoIsExD :: (Discrete a, Ord a) => SetOrInterval a -> SetOrInterval a -> SetOrdering

Compare sets helper function which only works on regular (non-singular) sets

membSoI :: Ord a => a -> SetOrInterval a -> Bool

Membership in `SetOrInterval`

nullSoI :: (Continuous a, Ord a) => SetOrInterval a -> Bool

Checks if the set is empty. Only for continuous types.

toSingular :: (Continuous a, Ord a) => SetOrInterval a -> Maybe a

If the set is singular, i.e., consists only from one point, then we return this point. Reports error on empty SoI's. Only for continuous types.

setToClosedInt :: Ord a => SetOrInterval a -> ClosedInterval (CIType a)

Transforms a `SetOrInterval` to a closed representation Only for continuous types.

cmpSoIs :: (Continuous a, Ord a) => SetOrInterval a -> SetOrInterval a -> SetOrdering

Compare sets over continuous types

cmpSoIsEx :: Ord a => SetOrInterval a -> SetOrInterval a -> SetOrdering

Compare sets helper function which only works on regular (non-singular) sets

We combine the comparison outcome of the individual parameters with the following (symmetrical => commutative) table:

```    \ | > < = O D
-------------
> | > O > O D
< |   < < O D
= |     = O D
O |       O D
D |         D

, where

>       | <      | =     | O       | D
---------------------------------------------
RightOf | LeftOf | Equal | Overlap | Disjoint```

The purpose of this table is to use it for cartesian products as follows

Let

A', A'' subset A B', B'' subset B

In order to get the comparison result for A' x B' and A'' x B'' we compare

A' and A'' as well as B' and B'' and combine the results with the above table.

Note that for empty sets the comparable results ,,= are preferred over the disjoint result.