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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.PartialOrd

Contents

Synopsis

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

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.

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.

Minimal complete definition

comparable

Methods

comparable :: Comparable a #

Instances

PartialOrd Int # 
PartialOrd Integer # 
PartialOrd () # 

Methods

comparable :: Comparable () #

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.

Methods

comparable :: Comparable (Either a b) #

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

Methods

comparable :: Comparable (a, b) #

(Ord i, PartialOrd a) => PartialOrd (Matrix i a) #

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

Methods

comparable :: Comparable (Matrix i a) #

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

Instances

Functor Pointwise # 

Methods

fmap :: (a -> b) -> Pointwise a -> Pointwise b #

(<$) :: a -> Pointwise b -> Pointwise a #

Eq a => Eq (Pointwise a) # 

Methods

(==) :: Pointwise a -> Pointwise a -> Bool #

(/=) :: Pointwise a -> Pointwise a -> Bool #

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

Instances

Functor Inclusion # 

Methods

fmap :: (a -> b) -> Inclusion a -> Inclusion b #

(<$) :: a -> Inclusion b -> Inclusion a #

Eq a => Eq (Inclusion a) # 

Methods

(==) :: Inclusion a -> Inclusion a -> Bool #

(/=) :: Inclusion a -> Inclusion a -> Bool #

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!