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

Agda.Utils.PartialOrd

Synopsis

# Documentation

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

 Source Source Source Source Source Partial ordering forms a monoid under sequencing. Arbitrary PartialOrdering Source Source Less is ``less general'' (i.e., more precise).

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

Includes equality: `x leqPO x == True`.

Opposites.

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

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.

Chains (transitivity) `x R y S z`.

`seqPO` is associative, commutative, and idempotent. `seqPO` has dominant element `POAny` and neutral element (unit) `POEQ`.

Embed `Ordering`.

Represent a non-empty disjunction of `Ordering`s as `PartialOrdering`.

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

Instances

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

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

# Generic partially ordered types.

newtype Pointwise a Source

Pointwise comparison wrapper.

Constructors

 Pointwise Fieldspointwise :: a

Instances

 Source Eq a => Eq (Pointwise a) Source Show a => Show (Pointwise 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.

newtype Inclusion a Source

Inclusion comparison wrapper.

Constructors

 Inclusion Fieldsinclusion :: a

Instances

 Source Eq a => Eq (Inclusion a) Source Ord a => Ord (Inclusion a) Source Show a => Show (Inclusion a) Source Ord a => PartialOrd (Inclusion [a]) Source Sublist for ordered lists. Ord a => PartialOrd (Inclusion (Set a)) Source Sets are partially ordered by inclusion.

# Properties

newtype ISet Source

We test our properties on integer sets ordered by inclusion.

Constructors

 ISet Fieldsiset :: Inclusion (Set Int)

Instances

 Source Source Source Arbitrary ISet Source Source

Any two elements are `related` in the way `comparable` computes.

`flip comparable a b == oppPO (comparable a b)`

sortUniq :: [Ordering] -> [Ordering] Source

Auxiliary function: lists to sets = sorted duplicate-free lists.

`leqPO` is inclusion of the associated `Ordering` sets.

`orPO` amounts to the union of the associated `Ordering` sets. Except that 'orPO POLT POGT == POAny' which should also include `POEQ`.

`orPO` is associative.

`orPO` is commutative.

`orPO` is idempotent.

The dominant element wrt. `orPO` is `POAny`.

property_seqPO :: ISet -> PartialOrdering -> ISet -> PartialOrdering -> ISet -> Property Source

Soundness of `seqPO`.

As QuickCheck test, this property is inefficient, see `prop_seqPO`.

prop_seqPO :: ISet -> ISet -> ISet -> Bool Source

A more efficient way of stating soundness of `seqPO`.

The unit of `seqPO` is `POEQ`.

The zero of `seqPO` is `POAny`.

`seqPO` is associative.

`seqPO` is also commutative.

`seqPO` is idempotent.

`seqPO` distributes over `orPO`.

The result of `toOrderings` is a sorted list without duplicates.

From `Ordering` to `PartialOrdering` and back is the identity.

From `PartialOrdering` to `Orderings` and back is the identity.

prop_toOrderings_after_fromOrderings :: NonEmptyList Ordering -> Bool Source

From `Orderings` to `PartialOrdering` and back is the identity. Except for `[LT,GT]` which is a non-canonical representative of `POAny`.

Pairs are related iff both components are related.

Comparing `PartialOrdering`s amounts to compare their representation as `Ordering` sets.

# All tests

All tests as collected by `quickCheckAll`.

Using `quickCheckAll` is convenient and superior to the manual enumeration of tests, since the name of the property is added automatically.