Safe Haskell	None
Language	Haskell98

Agda.Utils.PartialOrd

Contents

Comparison with partial result
Totally ordered types.
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 Source #
Methods minBound :: PartialOrdering # maxBound :: PartialOrdering #
Enum PartialOrdering Source #
Methods succ :: PartialOrdering -> PartialOrdering # pred :: PartialOrdering -> PartialOrdering # toEnum :: Int -> PartialOrdering # fromEnum :: PartialOrdering -> Int # enumFrom :: PartialOrdering -> [PartialOrdering] # enumFromThen :: PartialOrdering -> PartialOrdering -> [PartialOrdering] # enumFromTo :: PartialOrdering -> PartialOrdering -> [PartialOrdering] # enumFromThenTo :: PartialOrdering -> PartialOrdering -> PartialOrdering -> [PartialOrdering] #
Eq PartialOrdering Source #
Methods (==) :: PartialOrdering -> PartialOrdering -> Bool # (/=) :: PartialOrdering -> PartialOrdering -> Bool #
Show PartialOrdering Source #
Methods showsPrec :: Int -> PartialOrdering -> ShowS # show :: PartialOrdering -> String # showList :: [PartialOrdering] -> ShowS #
Monoid PartialOrdering Source #	Partial ordering forms a monoid under sequencing.
Methods mempty :: PartialOrdering # mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering # mconcat :: [PartialOrdering] -> PartialOrdering #
Arbitrary PartialOrdering Source #
Methods arbitrary :: Gen PartialOrdering # shrink :: PartialOrdering -> [PartialOrdering] #
PartialOrd PartialOrdering Source #	Less is ``less general'' (i.e., more precise).
Methods comparable :: Comparable PartialOrdering Source #

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.

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

Decidable partial orderings.

Minimal complete definition

comparable

Methods

comparable :: Comparable a Source #

Instances

PartialOrd Int Source #
Methods comparable :: Comparable Int Source #
PartialOrd Integer Source #
Methods comparable :: Comparable Integer Source #
PartialOrd () Source #
Methods comparable :: Comparable () Source #
PartialOrd ISet Source #
Methods comparable :: Comparable ISet Source #
PartialOrd PartialOrdering Source #	Less is ``less general'' (i.e., more precise).
Methods comparable :: Comparable PartialOrdering Source #
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).
Methods comparable :: Comparable Order Source #
PartialOrd a => PartialOrd (Maybe a) Source #	`Nothing` and `Just _` are unrelated. Partial ordering for `Maybe a` is the same as for `Either () a`.
Methods comparable :: Comparable (Maybe a) Source #
Ord a => PartialOrd (Inclusion [a]) Source #	Sublist for ordered lists.
Methods comparable :: Comparable (Inclusion [a]) Source #
Ord a => PartialOrd (Inclusion (Set a)) Source #	Sets are partially ordered by inclusion.
Methods comparable :: Comparable (Inclusion (Set 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.
Methods comparable :: Comparable (Pointwise [a]) Source #
PartialOrd (CallMatrixAug cinfo) Source #
Methods comparable :: Comparable (CallMatrixAug cinfo) Source #
PartialOrd a => PartialOrd (CallMatrix' a) Source #
Methods comparable :: Comparable (CallMatrix' a) Source #
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b) Source #	Partial ordering for disjoint sums: `Left _` and `Right _` are unrelated.
Methods comparable :: Comparable (Either a b) Source #
(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`.
Methods comparable :: Comparable (a, b) Source #
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source #	Pointwise comparison. Only matrices with the same dimension are comparable.
Methods comparable :: Comparable (Matrix i a) Source #

comparableOrd :: Ord a => Comparable a Source #

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.

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a Source #

Pointwise comparison wrapper.

Constructors

Pointwise
Fields pointwise :: a

Instances

Functor Pointwise Source #
Methods fmap :: (a -> b) -> Pointwise a -> Pointwise b # (<$) :: a -> Pointwise b -> Pointwise a #
Eq a => Eq (Pointwise a) Source #
Methods (==) :: Pointwise a -> Pointwise a -> Bool # (/=) :: Pointwise a -> Pointwise a -> Bool #
Show a => Show (Pointwise a) Source #
Methods showsPrec :: Int -> Pointwise a -> ShowS # show :: Pointwise a -> String # showList :: [Pointwise a] -> ShowS #
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.
Methods comparable :: Comparable (Pointwise [a]) Source #

newtype Inclusion a Source #

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Functor Inclusion Source #
Methods fmap :: (a -> b) -> Inclusion a -> Inclusion b # (<$) :: a -> Inclusion b -> Inclusion a #
Eq a => Eq (Inclusion a) Source #
Methods (==) :: Inclusion a -> Inclusion a -> Bool # (/=) :: Inclusion a -> Inclusion a -> Bool #
Ord a => Ord (Inclusion a) Source #
Methods compare :: Inclusion a -> Inclusion a -> Ordering # (<) :: Inclusion a -> Inclusion a -> Bool # (<=) :: Inclusion a -> Inclusion a -> Bool # (>) :: Inclusion a -> Inclusion a -> Bool # (>=) :: Inclusion a -> Inclusion a -> Bool # max :: Inclusion a -> Inclusion a -> Inclusion a # min :: Inclusion a -> Inclusion a -> Inclusion a #
Show a => Show (Inclusion a) Source #
Methods showsPrec :: Int -> Inclusion a -> ShowS # show :: Inclusion a -> String # showList :: [Inclusion a] -> ShowS #
Ord a => PartialOrd (Inclusion [a]) Source #	Sublist for ordered lists.
Methods comparable :: Comparable (Inclusion [a]) Source #
Ord a => PartialOrd (Inclusion (Set a)) Source #	Sets are partially ordered by inclusion.
Methods comparable :: Comparable (Inclusion (Set a)) Source #

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 Source #
Methods (==) :: ISet -> ISet -> Bool # (/=) :: ISet -> ISet -> Bool #
Ord ISet Source #
Methods compare :: ISet -> ISet -> Ordering # (<) :: ISet -> ISet -> Bool # (<=) :: ISet -> ISet -> Bool # (>) :: ISet -> ISet -> Bool # (>=) :: ISet -> ISet -> Bool # max :: ISet -> ISet -> ISet # min :: ISet -> ISet -> ISet #
Show ISet Source #
Methods showsPrec :: Int -> ISet -> ShowS # show :: ISet -> String # showList :: [ISet] -> ShowS #
Arbitrary ISet Source #
Methods arbitrary :: Gen ISet # shrink :: ISet -> [ISet] #
PartialOrd ISet Source #
Methods comparable :: Comparable ISet Source #

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

orPO is associative.

prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool Source #

orPO is commutative.

prop_idempotent_orPO :: PartialOrdering -> Bool Source #

orPO is idempotent.

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

seqPO is idempotent.

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.