Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.PartialOrd

Contents

Comparison with partial result
Totally ordered types.
Generic partially ordered types.
PartialOrdering is itself partially ordered!

Synopsis

data PartialOrdering
- = POLT
- | POLE
- | POEQ
- | POGE
- | POGT
- | POAny
leqPO :: PartialOrdering -> PartialOrdering -> Bool
oppPO :: PartialOrdering -> PartialOrdering
orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
fromOrdering :: Ordering -> PartialOrdering
fromOrderings :: [Ordering] -> PartialOrdering
toOrderings :: PartialOrdering -> [Ordering]
type Comparable a = a -> a -> PartialOrdering
class PartialOrd a where
comparableOrd :: Ord a => Comparable a
related :: PartialOrd a => a -> PartialOrdering -> a -> Bool
newtype Pointwise a = Pointwise {
- pointwise :: a
}
newtype Inclusion a = Inclusion {
- inclusion :: a
}

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 #
Instance details Defined in Agda.Utils.PartialOrd Methods minBound :: PartialOrdering # maxBound :: PartialOrdering #
Enum PartialOrdering #
Instance details 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 #
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: PartialOrdering -> PartialOrdering -> Bool # (/=) :: PartialOrdering -> PartialOrdering -> Bool #
Show PartialOrdering #
Instance details 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.
Instance details Defined in Agda.Utils.PartialOrd Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering # sconcat :: NonEmpty PartialOrdering -> PartialOrdering # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering #
Monoid PartialOrdering #
Instance details 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).
Instance details 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.

Minimal complete definition

comparable

Methods

comparable :: Comparable a #

Instances

PartialOrd Int #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable Int #
PartialOrd Integer #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable Integer #
PartialOrd () #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable () #
PartialOrd PartialOrdering #	Less is ``less general'' (i.e., more precise).
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable PartialOrdering #
PartialOrd Relevance #	More relevant is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Relevance #
PartialOrd Quantity #
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Quantity #
PartialOrd Modality #	Dominance ordering.
Instance details 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).
Instance details 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`.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Maybe a) #
Ord a => PartialOrd (Inclusion [a]) #	Sublist for ordered lists.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Inclusion [a]) #
Ord a => PartialOrd (Inclusion (Set a)) #	Sets are partially ordered by inclusion.
Instance details 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.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Pointwise [a]) #
PartialOrd (CallMatrixAug cinfo) #
Instance details Defined in Agda.Termination.CallMatrix Methods comparable :: Comparable (CallMatrixAug cinfo) #
PartialOrd a => PartialOrd (CallMatrix' a) #
Instance details 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.
Instance details 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`.
Instance details 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.
Instance details 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 #
Instance details Defined in Agda.Utils.PartialOrd Methods fmap :: (a -> b) -> Pointwise a -> Pointwise b # (<$) :: a -> Pointwise b -> Pointwise a #
Eq a => Eq (Pointwise a) #
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: Pointwise a -> Pointwise a -> Bool # (/=) :: Pointwise a -> Pointwise a -> Bool #
Show a => Show (Pointwise a) #
Instance details 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.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Pointwise [a]) #

newtype Inclusion a #

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Functor Inclusion #
Instance details Defined in Agda.Utils.PartialOrd Methods fmap :: (a -> b) -> Inclusion a -> Inclusion b # (<$) :: a -> Inclusion b -> Inclusion a #
Eq a => Eq (Inclusion a) #
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: Inclusion a -> Inclusion a -> Bool # (/=) :: Inclusion a -> Inclusion a -> Bool #
Ord a => Ord (Inclusion a) #
Instance details 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) #
Instance details 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.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Inclusion [a]) #
Ord a => PartialOrd (Inclusion (Set a)) #	Sets are partially ordered by inclusion.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Inclusion (Set a)) #

PartialOrdering is itself partially ordered!