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

PartialOrd PartialOrdering

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

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable PartialOrdering

Monoid PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

mempty :: PartialOrdering

mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering

mconcat :: [PartialOrdering] -> PartialOrdering

Semigroup PartialOrdering

Partial ordering forms a monoid under sequencing.

Defined in Agda.Utils.PartialOrd

Methods

(<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering

sconcat :: NonEmpty PartialOrdering -> PartialOrdering

stimes :: Integral b => b -> PartialOrdering -> PartialOrdering

Bounded PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

minBound :: PartialOrdering

maxBound :: PartialOrdering

Enum PartialOrdering

Defined in Agda.Utils.PartialOrd

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]

Show PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> PartialOrdering -> ShowS

show :: PartialOrdering -> String

showList :: [PartialOrdering] -> ShowS

Eq PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

(==) :: PartialOrdering -> PartialOrdering -> Bool

(/=) :: PartialOrdering -> PartialOrdering -> Bool

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 Cohesion

Flatter is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Cohesion

PartialOrd Modality

Dominance ordering.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Modality

PartialOrd Quantity

Note that the order is ω ≤ 0,1, more options is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Quantity

PartialOrd Relevance

More relevant is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Relevance

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

Defined in Agda.Termination.Order

Methods

comparable :: Comparable Order

PartialOrd PartialOrdering

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

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable PartialOrdering

PartialOrd Integer

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable Integer

PartialOrd ()

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable ()

PartialOrd Int

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable Int

PartialOrd t => PartialOrd (UnderAddition t)

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable (UnderAddition t)

PartialOrd t => PartialOrd (UnderComposition t)

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable (UnderComposition t)

PartialOrd a => PartialOrd (CallMatrix' a)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrix' a)

PartialOrd (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrixAug cinfo)

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

Sets are partially ordered by inclusion.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Inclusion (Set a))

Ord a => PartialOrd (Inclusion [a])

Sublist for ordered lists.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Inclusion [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.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Pointwise [a])

PartialOrd a => PartialOrd (Maybe a)

Nothing and Just _ are unrelated.

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

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Maybe a)

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

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

Defined in Agda.Termination.SparseMatrix

Methods

comparable :: Comparable (Matrix i a)

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

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

Defined in Agda.Utils.PartialOrd

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.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (a, b)

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

Defined in Agda.Utils.PartialOrd

Methods

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

(<$) :: a -> Pointwise b -> 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.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Pointwise [a])

Show a => Show (Pointwise a)

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> Pointwise a -> ShowS

show :: Pointwise a -> String

showList :: [Pointwise a] -> ShowS

Eq a => Eq (Pointwise a)

Defined in Agda.Utils.PartialOrd

Methods

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

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

newtype Inclusion a

Inclusion comparison wrapper.

Constructors

Inclusion

Fields

• inclusion :: a

Instances

Functor Inclusion

Defined in Agda.Utils.PartialOrd

Methods

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

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

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

Sets are partially ordered by inclusion.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Inclusion (Set a))

Ord a => PartialOrd (Inclusion [a])

Sublist for ordered lists.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Inclusion [a])

Show a => Show (Inclusion a)

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> Inclusion a -> ShowS

show :: Inclusion a -> String

showList :: [Inclusion a] -> ShowS

Eq a => Eq (Inclusion a)

Defined in Agda.Utils.PartialOrd

Methods

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

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

Ord a => Ord (Inclusion a)

Defined in Agda.Utils.PartialOrd

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

PartialOrdering is itself partially ordered!