Agda.Utils.PartialOrd

Documentation

data PartialOrdering

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).

leqPO :: PartialOrdering -> PartialOrdering -> Bool

Comparing the information content of two elements of PartialOrdering. More precise information is smaller.

Includes equality: x leqPO x == True.

oppPO :: PartialOrdering -> PartialOrdering

Opposites.

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

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering

Combining two pieces of information (picking the least information). Used for the dominance ordering on tuples.

orPO is associative, commutative, and idempotent. orPO has dominant element POAny, but no neutral element.

seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering

Chains (transitivity) x R y S z.

seqPO is associative, commutative, and idempotent. seqPO has dominant element POAny and neutral element (unit) POEQ.

fromOrdering :: Ordering -> PartialOrdering

Embed Ordering.

fromOrderings :: [Ordering] -> PartialOrdering

Represent a non-empty disjunction of Orderings as PartialOrdering.

toOrderings :: PartialOrdering -> [Ordering]

A PartialOrdering information is a disjunction of Ordering informations.

Comparison with partial result

type Comparable a = a -> a -> PartialOrdering

class PartialOrd a where

Decidable partial orderings.

Methods

comparable :: Comparable a

Instances

PartialOrd Int

PartialOrd Integer

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])

The pointwise ordering for lists of the same length.

There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.

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 a

Any Ord is a PartialOrd.

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

Are two elements related in a specific way?

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

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a

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])

The pointwise ordering for lists of the same length.

There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.

newtype Inclusion a

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

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

Any two elements are related in the way comparable computes.

prop_oppPO :: ISet -> ISet -> Bool

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

sortUniq :: [Ordering] -> [Ordering]

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

prop_leqPO_sound :: PartialOrdering -> PartialOrdering -> Bool

leqPO is inclusion of the associated Ordering sets.

prop_orPO_sound :: PartialOrdering -> PartialOrdering -> Bool

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

orPO is associative.

prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool

orPO is commutative.

prop_idempotent_orPO :: PartialOrdering -> Bool

orPO is idempotent.

prop_zero_orPO :: PartialOrdering -> Bool

The dominant element wrt. orPO is POAny.

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

Soundness of seqPO.

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

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

A more efficient way of stating soundness of seqPO.

prop_identity_seqPO :: PartialOrdering -> Bool

The unit of seqPO is POEQ.

prop_zero_seqPO :: PartialOrdering -> Bool

The zero of seqPO is POAny.

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

seqPO is associative.

prop_commutative_seqPO :: PartialOrdering -> PartialOrdering -> Bool

seqPO is also commutative.

prop_idempotent_seqPO :: PartialOrdering -> Bool

seqPO is idempotent.

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

seqPO distributes over orPO.

prop_sorted_toOrderings :: PartialOrdering -> Bool

The result of toOrderings is a sorted list without duplicates.

prop_toOrderings_after_fromOrdering :: Ordering -> Bool

From Ordering to PartialOrdering and back is the identity.

prop_fromOrderings_after_toOrderings :: PartialOrdering -> Bool

From PartialOrdering to Orderings and back is the identity.

prop_toOrderings_after_fromOrderings :: NonEmptyList Ordering -> Bool

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

Pairs are related iff both components are related.

prop_comparable_PartialOrdering :: PartialOrdering -> PartialOrdering -> Bool

Comparing PartialOrderings amounts to compare their representation as Ordering sets.

All tests

tests :: IO Bool

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.