Safe Haskell	None
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
- comparable :: Comparable a
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 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

Instances details

Bounded PartialOrdering Source #
Instance details Defined in Agda.Utils.PartialOrd Methods minBound :: PartialOrdering # maxBound :: PartialOrdering #
Enum PartialOrdering Source #
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 Source #
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: PartialOrdering -> PartialOrdering -> Bool # (/=) :: PartialOrdering -> PartialOrdering -> Bool #
Show PartialOrdering Source #
Instance details Defined in Agda.Utils.PartialOrd Methods showsPrec :: Int -> PartialOrdering -> ShowS # show :: PartialOrdering -> String # showList :: [PartialOrdering] -> ShowS #
Semigroup PartialOrdering Source #	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 Source #
Instance details Defined in Agda.Utils.PartialOrd Methods mempty :: PartialOrdering # mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering # mconcat :: [PartialOrdering] -> PartialOrdering #
PartialOrd PartialOrdering Source #	Less is ``less general'' (i.e., more precise).
Instance details Defined in Agda.Utils.PartialOrd 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.

Methods

comparable :: Comparable a Source #

Instances

Instances details

PartialOrd Int Source #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable Int Source #
PartialOrd Integer Source #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable Integer Source #
PartialOrd () Source #
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable () Source #
PartialOrd PartialOrdering Source #	Less is ``less general'' (i.e., more precise).
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable PartialOrdering Source #
PartialOrd Cohesion Source #	Flatter is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Cohesion Source #
PartialOrd Relevance Source #	More relevant is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Relevance Source #
PartialOrd Quantity Source #	Note that the order is `ω ≤ 0,1`, more options is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Quantity Source #
PartialOrd Modality Source #	Dominance ordering.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Modality 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).
Instance details Defined in Agda.Termination.Order 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`.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Maybe a) Source #
Ord a => PartialOrd (Inclusion [a]) Source #	Sublist for ordered lists.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Inclusion [a]) Source #
Ord a => PartialOrd (Inclusion (Set a)) Source #	Sets are partially ordered by inclusion.
Instance details Defined in Agda.Utils.PartialOrd 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.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Pointwise [a]) Source #
PartialOrd (CallMatrixAug cinfo) Source #
Instance details Defined in Agda.Termination.CallMatrix Methods comparable :: Comparable (CallMatrixAug cinfo) Source #
PartialOrd a => PartialOrd (CallMatrix' a) Source #
Instance details Defined in Agda.Termination.CallMatrix 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.
Instance details Defined in Agda.Utils.PartialOrd 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`.
Instance details Defined in Agda.Utils.PartialOrd 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.
Instance details Defined in Agda.Termination.SparseMatrix 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

Instances details

Functor Pointwise Source #
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) Source #
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: Pointwise a -> Pointwise a -> Bool # (/=) :: Pointwise a -> Pointwise a -> Bool #
Show a => Show (Pointwise a) Source #
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]) 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.
Instance details Defined in Agda.Utils.PartialOrd Methods comparable :: Comparable (Pointwise [a]) Source #

newtype Inclusion a Source #

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Instances details

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

PartialOrdering is itself partially ordered!