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

Agda.Utils.PartialOrd

Synopsis

# Documentation

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

 Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [PartialOrdering] -> ShowS # Source # Partial ordering forms a monoid under sequencing. Methods Source # Methods Source # Less is less general'' (i.e., more precise). Methods

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

Includes equality: x leqPO x == True.

Opposites.

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

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.

Chains (transitivity) x R y S z.

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

Embed Ordering.

Represent a non-empty disjunction of Orderings as PartialOrdering.

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

Instances

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

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 Fieldspointwise :: a

Instances

 Source # Methodsfmap :: (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 # MethodsshowsPrec :: 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 newtype Inclusion a Source # Inclusion comparison wrapper. Constructors  Inclusion Fieldsinclusion :: a Instances  Source # Methodsfmap :: (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 # Methodscompare :: 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 # MethodsshowsPrec :: Int -> Inclusion a -> ShowS #show :: Inclusion a -> String #showList :: [Inclusion a] -> ShowS # Ord a => PartialOrd (Inclusion [a]) Source # Sublist for ordered lists. Methods Ord a => PartialOrd (Inclusion (Set a)) Source # Sets are partially ordered by inclusion. Methods

# Properties

newtype ISet Source #

We test our properties on integer sets ordered by inclusion.

Constructors

 ISet Fieldsiset :: Inclusion (Set Int)

Instances

 Source # Methods(==) :: ISet -> ISet -> Bool #(/=) :: ISet -> ISet -> Bool # Source # Methodscompare :: ISet -> ISet -> Ordering #(<) :: ISet -> ISet -> Bool #(<=) :: ISet -> ISet -> Bool #(>) :: ISet -> ISet -> Bool #(>=) :: ISet -> ISet -> Bool #max :: ISet -> ISet -> ISet #min :: ISet -> ISet -> ISet # Source # MethodsshowsPrec :: Int -> ISet -> ShowS #show :: ISet -> String #showList :: [ISet] -> ShowS # Source # Methodsshrink :: ISet -> [ISet] # Source # Methods

Any two elements are related in the way comparable computes.

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

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

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

leqPO is inclusion of the associated Ordering sets.

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

orPO is associative.

orPO is commutative.

orPO is idempotent.

The dominant element wrt. orPO is POAny.

Soundness of seqPO.

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

A more efficient way of stating soundness of seqPO.

The unit of seqPO is POEQ.

The zero of seqPO is POAny.

seqPO is associative.

seqPO is also commutative.

seqPO is idempotent.

seqPO distributes over orPO.

The result of toOrderings is a sorted list without duplicates.

From Ordering to PartialOrdering and back is the identity.

From PartialOrdering to Orderings and back is the identity.

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

Pairs are related iff both components are related.

Comparing PartialOrderings amounts to compare their representation as Ordering sets.

# All tests

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.