Safe Haskell	None

Agda.Utils.PartialOrd

Contents

Comparison with partial result
Generic partially ordered types.
PartialOrdering is itself partially ordered!
Properties
All tests

Synopsis

Documentation

data PartialOrdering Source

The result of comparing two things (of the same type).

Constructors

POLT	Less than.
POLE	Less or equal than.
POEQ	Equal
POGE	Greater or equal.
POGT	Greater than.
POAny	No information (incomparable).

Instances

Bounded PartialOrdering
Enum PartialOrdering
Eq PartialOrdering
Show PartialOrdering
Arbitrary PartialOrdering
Monoid PartialOrdering	Partial ordering forms a monoid under sequencing.
SemiRing PartialOrdering	Partial ordering forms a semiring under supremum (disjunction) and composition (transitivity, sequencing)
PartialOrd PartialOrdering	Less is ``less general'' (i.e., more precise).

oppPO :: PartialOrdering -> PartialOrdering Source

Opposites.

related a po b iff related b (oppPO po) a.

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source

What if either of two facts hold? x R y || x S y

seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source

Chains (transitivity) x R y S z. Also: conjunction (trying to get the best information out).

fromOrdering :: Ordering -> PartialOrdering Source

Embed Ordering.

fromOrderings :: [Ordering] -> PartialOrdering Source

Represent a non-empty disjunction of Orderings as PartialOrdering.

toOrderings :: PartialOrdering -> [Ordering]Source

A PartialOrdering information is a disjunction of Ordering informations.

Comparison with partial result

type Comparable a = a -> a -> PartialOrdering Source

class PartialOrd a whereSource

Decidable partial orderings.

Methods

comparable :: Comparable aSource

Instances

PartialOrd ()
PartialOrd ISet
PartialOrd PartialOrdering	Less is ``less general'' (i.e., more precise).
PartialOrd Order	Information order: `Unknown` is least information. The more we decrease, the more information we have. When having comparable call-matrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information).
PartialOrd a => PartialOrd (Maybe a)	`Nothing` and `Just _` are unrelated. Partial ordering for `Maybe a` is the same as for `Either () a`.
Ord a => PartialOrd (Inclusion [a])	Sublist for ordered lists.
Ord a => PartialOrd (Inclusion (Set a))	Sets are partially ordered by inclusion.
PartialOrd a => PartialOrd (Pointwise [a])	Lifting the pointwise ordering for tuples to lists. There are other partial orderings for lists, e.g., prefix, sublist, subset.
PartialOrd (CallMatrixAug cinfo)
PartialOrd a => PartialOrd (CallMatrix' a)
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b)	Partial ordering for disjoint sums: `Left _` and `Right _` are unrelated.
(PartialOrd a, PartialOrd b) => PartialOrd (a, b)	Pointwise partial ordering for tuples. `related (x1,x2) o (y1,y2)` iff `related x1 o x2` and `related y1 o y2`.
(Ord i, PartialOrd a) => PartialOrd (Matrix i a)	Pointwise comparison. Only matrices with the same dimension are comparable.

comparableOrd :: Ord a => Comparable aSource

Any Ord is a PartialOrd.

related :: PartialOrd a => a -> PartialOrdering -> a -> Bool Source

Are two elements related in a specific way?

related a o b holds iff comparable a b is contained in o.

Generic partially ordered types.

newtype Pointwise a Source

Pointwise comparison wrapper.

Constructors

Pointwise
Fields pointwise :: a

Instances

Functor Pointwise
Eq a => Eq (Pointwise a)
Show a => Show (Pointwise a)
PartialOrd a => PartialOrd (Pointwise [a])	Lifting the pointwise ordering for tuples to lists. There are other partial orderings for lists, e.g., prefix, sublist, subset.

newtype Inclusion a Source

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Functor Inclusion
Eq a => Eq (Inclusion a)
Ord a => Ord (Inclusion a)
Show a => Show (Inclusion a)
Ord a => PartialOrd (Inclusion [a])	Sublist for ordered lists.
Ord a => PartialOrd (Inclusion (Set a))	Sets are partially ordered by inclusion.

PartialOrdering is itself partially ordered!

Properties

newtype ISet Source

We test our properties on integer sets ordered by inclusion.

Constructors

ISet
Fields iset :: Inclusion (Set Int)

Instances

Eq ISet
Ord ISet
Show ISet
Arbitrary ISet
PartialOrd ISet

prop_comparable_related :: ISet -> ISet -> Bool Source

Any two elements are related in the way comparable computes.

prop_oppPO :: ISet -> ISet -> Bool Source

flip comparable a b == oppPO (comparable a b)

sortUniq :: [Ordering] -> [Ordering]Source

Auxiliary function: lists to sets = sorted duplicate-free lists.

prop_orPO_sound :: PartialOrdering -> PartialOrdering -> Bool Source

orPO amounts to the union of the associated Ordering sets. Except that 'orPO POLT POGT == POAny' which should also include POEQ.

prop_associative_orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering -> Bool Source

orPO is associative.

prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool Source

orPO is communtative.

prop_zero_orPO :: PartialOrdering -> Bool Source

The dominant element wrt. orPO is POAny.

property_seqPO :: ISet -> PartialOrdering -> ISet -> PartialOrdering -> ISet -> Property Source

Soundness of seqPO.

As QuickCheck test, this property is inefficient, see prop_seqPO.

prop_seqPO :: ISet -> ISet -> ISet -> Bool Source

A more efficient way of stating soundness of seqPO.

prop_identity_seqPO :: PartialOrdering -> Bool Source

The unit of seqPO is POEQ.

prop_zero_seqPO :: PartialOrdering -> Bool Source

The zero of seqPO is POAny.

prop_associative_seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering -> Bool Source

seqPO is associative.

prop_commutative_seqPO :: PartialOrdering -> PartialOrdering -> Bool Source

seqPO is also commutative.

prop_distributive_seqPO_orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering -> Bool Source

seqPO distributes over orPO.

prop_sorted_toOrderings :: PartialOrdering -> Bool Source

The result of toOrderings is a sorted list without duplicates.

prop_toOrderings_after_fromOrdering :: Ordering -> Bool Source

From Ordering to PartialOrdering and back is the identity.

prop_fromOrderings_after_toOrderings :: PartialOrdering -> Bool Source

From PartialOrdering to Orderings and back is the identity.

prop_toOrderings_after_fromOrderings :: NonEmptyList Ordering -> Bool Source

From Orderings to PartialOrdering and back is the identity. Except for [LT,GT] which is a non-canonical representative of POAny.

prop_related_pair :: ISet -> ISet -> ISet -> ISet -> PartialOrdering -> Bool Source

Pairs are related iff both components are related.

prop_comparable_PartialOrdering :: PartialOrdering -> PartialOrdering -> Bool Source

Comparing PartialOrderings amounts to compare their representation as Ordering sets.

All tests

tests :: IO Bool Source

All tests as collected by quickCheckAll.

Using quickCheckAll is convenient and superior to the manual enumeration of tests, since the name of the property is added automatically.