Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.PartialOrd

Contents

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 Source 
Enum PartialOrdering Source 
Eq PartialOrdering Source 
Show PartialOrdering Source 
Monoid PartialOrdering Source

Partial ordering forms a monoid under sequencing.

Arbitrary PartialOrdering Source 
PartialOrd PartialOrdering Source

Less is ``less general'' (i.e., more precise).

leqPO :: PartialOrdering -> PartialOrdering -> Bool Source

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

Includes equality: x leqPO x == True.

oppPO :: PartialOrdering -> PartialOrdering Source

Opposites.

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

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source

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 Source

Chains (transitivity) x R y S z.

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

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 where Source

Decidable partial orderings.

Instances

PartialOrd Int Source 
PartialOrd Integer Source 
PartialOrd () Source 
PartialOrd ISet Source 
PartialOrd PartialOrdering Source

Less is ``less general'' (i.e., more precise).

PartialOrd Order Source

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

Nothing and Just _ are unrelated.

Partial ordering for Maybe a is the same as for Either () a.

Ord a => PartialOrd (Inclusion [a]) Source

Sublist for ordered lists.

Ord a => PartialOrd (Inclusion (Set a)) Source

Sets are partially ordered by inclusion.

PartialOrd a => PartialOrd (Pointwise [a]) Source

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) Source 
PartialOrd a => PartialOrd (CallMatrix' a) Source 
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b) Source

Partial ordering for disjoint sums: Left _ and Right _ are unrelated.

(PartialOrd a, PartialOrd b) => PartialOrd (a, b) Source

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

Pointwise comparison. Only matrices with the same dimension are comparable.

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.

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a Source

Pointwise comparison wrapper.

Constructors

Pointwise 

Fields

pointwise :: a
 

Instances

Functor Pointwise Source 
Eq a => Eq (Pointwise a) Source 
Show a => Show (Pointwise a) Source 
PartialOrd a => PartialOrd (Pointwise [a]) Source

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 Source

Inclusion comparison wrapper.

Constructors

Inclusion 

Fields

inclusion :: a
 

Instances

Functor Inclusion Source 
Eq a => Eq (Inclusion a) Source 
Ord a => Ord (Inclusion a) Source 
Show a => Show (Inclusion a) Source 
Ord a => PartialOrd (Inclusion [a]) Source

Sublist for ordered lists.

Ord a => PartialOrd (Inclusion (Set a)) Source

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)
 

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_leqPO_sound :: PartialOrdering -> PartialOrdering -> Bool Source

leqPO is inclusion of the associated Ordering sets.

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_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_sorted_toOrderings :: PartialOrdering -> Bool Source

The result of toOrderings is a sorted list without duplicates.

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.