Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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

Bounded PartialOrdering Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods minBound :: PartialOrdering Source # maxBound :: PartialOrdering Source #
Enum PartialOrdering Source # |

Instance details

Defined in Agda.Utils.PartialOrd

Methods

succ :: PartialOrdering -> PartialOrdering Source #

pred :: PartialOrdering -> PartialOrdering Source #

toEnum :: Int -> PartialOrdering Source #

fromEnum :: PartialOrdering -> Int Source #

enumFrom :: PartialOrdering -> [PartialOrdering] Source #

enumFromThen :: PartialOrdering -> PartialOrdering -> [PartialOrdering] Source #

enumFromTo :: PartialOrdering -> PartialOrdering -> [PartialOrdering] Source #

enumFromThenTo :: PartialOrdering -> PartialOrdering -> PartialOrdering -> [PartialOrdering] Source #

Eq PartialOrdering Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: PartialOrdering -> PartialOrdering -> Bool Source # (/=) :: PartialOrdering -> PartialOrdering -> Bool Source #
Show PartialOrdering Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods showsPrec :: Int -> PartialOrdering -> ShowS Source # show :: PartialOrdering -> String Source # showList :: [PartialOrdering] -> ShowS Source #
Semigroup PartialOrdering Source # | Partial ordering forms a monoid under sequencing.
Instance details Defined in Agda.Utils.PartialOrd Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering Source # sconcat :: NonEmpty PartialOrdering -> PartialOrdering Source # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering Source #
Monoid PartialOrdering Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods mempty :: PartialOrdering Source # mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering Source # mconcat :: [PartialOrdering] -> PartialOrdering Source #
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 `Ordering`s 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

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

Functor Pointwise Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods fmap :: (a -> b) -> Pointwise a -> Pointwise b Source # (<$) :: a -> Pointwise b -> Pointwise a Source #
Eq a => Eq (Pointwise a) Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: Pointwise a -> Pointwise a -> Bool Source # (/=) :: Pointwise a -> Pointwise a -> Bool Source #
Show a => Show (Pointwise a) Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods showsPrec :: Int -> Pointwise a -> ShowS Source # show :: Pointwise a -> String Source # showList :: [Pointwise a] -> ShowS 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 #

newtype Inclusion a Source #

Inclusion comparison wrapper.

Constructors

Inclusion |

Fields

- inclusion :: a

Instances

Functor Inclusion Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods fmap :: (a -> b) -> Inclusion a -> Inclusion b Source # (<$) :: a -> Inclusion b -> Inclusion a Source #
Eq a => Eq (Inclusion a) Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods (==) :: Inclusion a -> Inclusion a -> Bool Source # (/=) :: Inclusion a -> Inclusion a -> Bool Source #
Ord a => Ord (Inclusion a) Source # |

Instance details

Defined in Agda.Utils.PartialOrd

Methods

compare :: Inclusion a -> Inclusion a -> Ordering Source #

(<) :: Inclusion a -> Inclusion a -> Bool Source #

(<=) :: Inclusion a -> Inclusion a -> Bool Source #

(>) :: Inclusion a -> Inclusion a -> Bool Source #

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

max :: Inclusion a -> Inclusion a -> Inclusion a Source #

min :: Inclusion a -> Inclusion a -> Inclusion a Source #

Show a => Show (Inclusion a) Source # |
Instance details Defined in Agda.Utils.PartialOrd Methods showsPrec :: Int -> Inclusion a -> ShowS Source # show :: Inclusion a -> String Source # showList :: [Inclusion a] -> ShowS 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 #

# PartialOrdering is itself partially ordered!