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

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]

Eq PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

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

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

Show PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> PartialOrdering -> ShowS

show :: PartialOrdering -> String

showList :: [PartialOrdering] -> ShowS

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

Monoid PartialOrdering

Defined in Agda.Utils.PartialOrd

Methods

mempty :: PartialOrdering

mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering

mconcat :: [PartialOrdering] -> PartialOrdering

PartialOrd PartialOrdering

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

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable PartialOrdering

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 Int

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable Int

PartialOrd Integer

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable Integer

PartialOrd ()

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable ()

PartialOrd PartialOrdering

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

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable PartialOrdering

PartialOrd Cohesion

Flatter is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Cohesion

PartialOrd Relevance

More relevant is smaller.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Relevance

PartialOrd Quantity

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

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Quantity

PartialOrd Modality

Dominance ordering.

Defined in Agda.Syntax.Common

Methods

comparable :: Comparable Modality

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 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 a => PartialOrd (Inclusion [a])

Sublist for ordered lists.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (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))

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 (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrixAug cinfo)

PartialOrd a => PartialOrd (CallMatrix' a)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrix' 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)

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

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

Eq a => Eq (Pointwise a)

Defined in Agda.Utils.PartialOrd

Methods

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

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

Show a => Show (Pointwise a)

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> Pointwise a -> ShowS

show :: Pointwise a -> String

showList :: [Pointwise a] -> ShowS

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

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

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

Show a => Show (Inclusion a)

Defined in Agda.Utils.PartialOrd

Methods

showsPrec :: Int -> Inclusion a -> ShowS

show :: Inclusion a -> String

showList :: [Inclusion a] -> ShowS

Ord a => PartialOrd (Inclusion [a])

Sublist for ordered lists.

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (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))

PartialOrdering is itself partially ordered!