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

Documentation

data PartialOrdering Source #

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 Source #
Methods minBound :: PartialOrdering # maxBound :: PartialOrdering #
Enum PartialOrdering Source #
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 Source #
Methods (==) :: PartialOrdering -> PartialOrdering -> Bool # (/=) :: PartialOrdering -> PartialOrdering -> Bool #
Show PartialOrdering Source #
Methods showsPrec :: Int -> PartialOrdering -> ShowS # show :: PartialOrdering -> String # showList :: [PartialOrdering] -> ShowS #
Semigroup PartialOrdering Source #	Partial ordering forms a monoid under sequencing.
Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering # sconcat :: NonEmpty PartialOrdering -> PartialOrdering # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering #
Monoid PartialOrdering Source #
Methods mempty :: PartialOrdering # mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering # mconcat :: [PartialOrdering] -> PartialOrdering #
PartialOrd PartialOrdering Source #	Less is ``less general'' (i.e., more precise).
Methods comparable :: Comparable PartialOrdering Source #

leqPO :: PartialOrdering -> PartialOrdering -> Bool Source #

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

Includes equality: x leqPO x == True.

oppPO :: PartialOrdering -> PartialOrdering Source #

Opposites.

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

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering Source #

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 Source #

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 Source #

Embed Ordering.

fromOrderings :: [Ordering] -> PartialOrdering Source #

Represent a non-empty disjunction of Orderings as PartialOrdering.

toOrderings :: PartialOrdering -> [Ordering] Source #

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

comparable :: Comparable a Source #

Instances

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

comparableOrd :: Ord a => Comparable a Source #

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.

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a Source #

Pointwise comparison wrapper.

Constructors

Pointwise
Fields pointwise :: a

Instances

Functor Pointwise Source #
Methods fmap :: (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 #
Methods showsPrec :: 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 comparable :: Comparable (Pointwise [a]) Source #

newtype Inclusion a Source #

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Functor Inclusion Source #
Methods fmap :: (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 #
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) Source #
Methods showsPrec :: Int -> Inclusion a -> ShowS # show :: Inclusion a -> String # showList :: [Inclusion a] -> ShowS #
Ord a => PartialOrd (Inclusion [a]) Source #	Sublist for ordered lists.
Methods comparable :: Comparable (Inclusion [a]) Source #
Ord a => PartialOrd (Inclusion (Set a)) Source #	Sets are partially ordered by inclusion.
Methods comparable :: Comparable (Inclusion (Set a)) Source #

PartialOrdering is itself partially ordered!