    {-# LANGUAGE CPP #-}
    module Agda.Utils.PartialOrd where

    import Data.Maybe
    #if __GLASGOW_HASKELL__ < 804
    import Data.Semigroup
    #endif
    import Data.Set (Set)
    import qualified Data.Set as Set

    -- import Agda.Utils.List

    -- | The result of comparing two things (of the same type).
    data PartialOrdering
      = POLT  -- ^ Less than.
      | POLE  -- ^ Less or equal than.
      | POEQ  -- ^ Equal
      | POGE  -- ^ Greater or equal.
      | POGT  -- ^ Greater than.
      | POAny -- ^ No information (incomparable).
      deriving (PartialOrdering -> PartialOrdering -> Bool
    (PartialOrdering -> PartialOrdering -> Bool)
    -> (PartialOrdering -> PartialOrdering -> Bool)
    -> Eq PartialOrdering
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: PartialOrdering -> PartialOrdering -> Bool
    $c/= :: PartialOrdering -> PartialOrdering -> Bool
    == :: PartialOrdering -> PartialOrdering -> Bool
    $c== :: PartialOrdering -> PartialOrdering -> Bool
    Eq, Int -> PartialOrdering -> ShowS
    [PartialOrdering] -> ShowS
    PartialOrdering -> String
    (Int -> PartialOrdering -> ShowS)
    -> (PartialOrdering -> String)
    -> ([PartialOrdering] -> ShowS)
    -> Show PartialOrdering
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [PartialOrdering] -> ShowS
    $cshowList :: [PartialOrdering] -> ShowS
    show :: PartialOrdering -> String
    $cshow :: PartialOrdering -> String
    showsPrec :: Int -> PartialOrdering -> ShowS
    $cshowsPrec :: Int -> PartialOrdering -> ShowS
    Show, Int -> PartialOrdering
    PartialOrdering -> Int
    PartialOrdering -> [PartialOrdering]
    PartialOrdering -> PartialOrdering
    PartialOrdering -> PartialOrdering -> [PartialOrdering]
    PartialOrdering
    -> PartialOrdering -> PartialOrdering -> [PartialOrdering]
    (PartialOrdering -> PartialOrdering)
    -> (PartialOrdering -> PartialOrdering)
    -> (Int -> PartialOrdering)
    -> (PartialOrdering -> Int)
    -> (PartialOrdering -> [PartialOrdering])
    -> (PartialOrdering -> PartialOrdering -> [PartialOrdering])
    -> (PartialOrdering -> PartialOrdering -> [PartialOrdering])
    -> (PartialOrdering
        -> PartialOrdering -> PartialOrdering -> [PartialOrdering])
    -> Enum PartialOrdering
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: PartialOrdering
    -> PartialOrdering -> PartialOrdering -> [PartialOrdering]
    $cenumFromThenTo :: PartialOrdering
    -> PartialOrdering -> PartialOrdering -> [PartialOrdering]
    enumFromTo :: PartialOrdering -> PartialOrdering -> [PartialOrdering]
    $cenumFromTo :: PartialOrdering -> PartialOrdering -> [PartialOrdering]
    enumFromThen :: PartialOrdering -> PartialOrdering -> [PartialOrdering]
    $cenumFromThen :: PartialOrdering -> PartialOrdering -> [PartialOrdering]
    enumFrom :: PartialOrdering -> [PartialOrdering]
    $cenumFrom :: PartialOrdering -> [PartialOrdering]
    fromEnum :: PartialOrdering -> Int
    $cfromEnum :: PartialOrdering -> Int
    toEnum :: Int -> PartialOrdering
    $ctoEnum :: Int -> PartialOrdering
    pred :: PartialOrdering -> PartialOrdering
    $cpred :: PartialOrdering -> PartialOrdering
    succ :: PartialOrdering -> PartialOrdering
    $csucc :: PartialOrdering -> PartialOrdering
    Enum, PartialOrdering
    PartialOrdering -> PartialOrdering -> Bounded PartialOrdering
    forall a. a -> a -> Bounded a
    maxBound :: PartialOrdering
    $cmaxBound :: PartialOrdering
    minBound :: PartialOrdering
    $cminBound :: PartialOrdering
    Bounded)

    -- | Comparing the information content of two elements of
    --   'PartialOrdering'.  More precise information is smaller.
    --
    --   Includes equality: @x `leqPO` x == True@.

    leqPO :: PartialOrdering -> PartialOrdering -> Bool

    leqPO :: PartialOrdering -> PartialOrdering -> Bool
    leqPO PartialOrdering
    _   PartialOrdering
    POAny = Bool
    True

    leqPO PartialOrdering
    POLT PartialOrdering
    POLT = Bool
    True
    leqPO PartialOrdering
    POLT PartialOrdering
    POLE = Bool
    True

    leqPO PartialOrdering
    POLE PartialOrdering
    POLE = Bool
    True

    leqPO PartialOrdering
    POEQ PartialOrdering
    POLE = Bool
    True
    leqPO PartialOrdering
    POEQ PartialOrdering
    POEQ = Bool
    True
    leqPO PartialOrdering
    POEQ PartialOrdering
    POGE = Bool
    True

    leqPO PartialOrdering
    POGE PartialOrdering
    POGE = Bool
    True

    leqPO PartialOrdering
    POGT PartialOrdering
    POGT = Bool
    True
    leqPO PartialOrdering
    POGT PartialOrdering
    POGE = Bool
    True

    leqPO PartialOrdering
    _ PartialOrdering
    _ = Bool
    False

    -- | Opposites.
    --
    --   @related a po b@ iff @related b (oppPO po) a@.

    oppPO :: PartialOrdering -> PartialOrdering
    oppPO :: PartialOrdering -> PartialOrdering
    oppPO PartialOrdering
    POLT  = PartialOrdering
    POGT
    oppPO PartialOrdering
    POLE  = PartialOrdering
    POGE
    oppPO PartialOrdering
    POEQ  = PartialOrdering
    POEQ
    oppPO PartialOrdering
    POGE  = PartialOrdering
    POLE
    oppPO PartialOrdering
    POGT  = PartialOrdering
    POLT
    oppPO PartialOrdering
    POAny = PartialOrdering
    POAny

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

    orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering

    orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
    orPO PartialOrdering
    POAny PartialOrdering
    _   = PartialOrdering
    POAny   -- Shortcut if no information on first.

    orPO PartialOrdering
    POLT PartialOrdering
    POLT = PartialOrdering
    POLT   -- idempotent
    orPO PartialOrdering
    POLT PartialOrdering
    POLE = PartialOrdering
    POLE
    orPO PartialOrdering
    POLT PartialOrdering
    POEQ = PartialOrdering
    POLE

    orPO PartialOrdering
    POLE PartialOrdering
    POLT = PartialOrdering
    POLE
    orPO PartialOrdering
    POLE PartialOrdering
    POLE = PartialOrdering
    POLE   -- idempotent
    orPO PartialOrdering
    POLE PartialOrdering
    POEQ = PartialOrdering
    POLE

    orPO PartialOrdering
    POEQ PartialOrdering
    POLT = PartialOrdering
    POLE
    orPO PartialOrdering
    POEQ PartialOrdering
    POLE = PartialOrdering
    POLE
    orPO PartialOrdering
    POEQ PartialOrdering
    POEQ = PartialOrdering
    POEQ   -- idempotent
    orPO PartialOrdering
    POEQ PartialOrdering
    POGE = PartialOrdering
    POGE
    orPO PartialOrdering
    POEQ PartialOrdering
    POGT = PartialOrdering
    POGE

    orPO PartialOrdering
    POGE PartialOrdering
    POEQ = PartialOrdering
    POGE
    orPO PartialOrdering
    POGE PartialOrdering
    POGE = PartialOrdering
    POGE   -- idempotent
    orPO PartialOrdering
    POGE PartialOrdering
    POGT = PartialOrdering
    POGE

    orPO PartialOrdering
    POGT PartialOrdering
    POEQ = PartialOrdering
    POGE
    orPO PartialOrdering
    POGT PartialOrdering
    POGE = PartialOrdering
    POGE
    orPO PartialOrdering
    POGT PartialOrdering
    POGT = PartialOrdering
    POGT   -- idempotent

    orPO PartialOrdering
    _    PartialOrdering
    _    = PartialOrdering
    POAny

    -- | Chains (transitivity) @x R y S z@.
    --
    --   @seqPO@ is associative, commutative, and idempotent.
    --   @seqPO@ has dominant element @POAny@ and neutral element (unit) @POEQ@.

    seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering

    seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
    seqPO PartialOrdering
    POAny PartialOrdering
    _   = PartialOrdering
    POAny  -- Shortcut if no information on first.
    seqPO PartialOrdering
    POEQ PartialOrdering
    p    = PartialOrdering
    p      -- No need to look at second if first is neutral.

    seqPO PartialOrdering
    POLT PartialOrdering
    POLT = PartialOrdering
    POLT   -- idempotent
    seqPO PartialOrdering
    POLT PartialOrdering
    POLE = PartialOrdering
    POLT
    seqPO PartialOrdering
    POLT PartialOrdering
    POEQ = PartialOrdering
    POLT   -- unit

    seqPO PartialOrdering
    POLE PartialOrdering
    POLT = PartialOrdering
    POLT
    seqPO PartialOrdering
    POLE PartialOrdering
    POLE = PartialOrdering
    POLE   -- idempotent
    seqPO PartialOrdering
    POLE PartialOrdering
    POEQ = PartialOrdering
    POLE   -- unit

    seqPO PartialOrdering
    POGE PartialOrdering
    POEQ = PartialOrdering
    POGE   -- unit
    seqPO PartialOrdering
    POGE PartialOrdering
    POGE = PartialOrdering
    POGE   -- idempotent
    seqPO PartialOrdering
    POGE PartialOrdering
    POGT = PartialOrdering
    POGT

    seqPO PartialOrdering
    POGT PartialOrdering
    POEQ = PartialOrdering
    POGT   -- unit
    seqPO PartialOrdering
    POGT PartialOrdering
    POGE = PartialOrdering
    POGT
    seqPO PartialOrdering
    POGT PartialOrdering
    POGT = PartialOrdering
    POGT   -- idempotent

    seqPO PartialOrdering
    _    PartialOrdering
    _    = PartialOrdering
    POAny

    -- | Partial ordering forms a monoid under sequencing.
    instance Semigroup PartialOrdering where
      <> :: PartialOrdering -> PartialOrdering -> PartialOrdering
    (<>) = PartialOrdering -> PartialOrdering -> PartialOrdering
    seqPO

    instance Monoid PartialOrdering where
      mempty :: PartialOrdering
    mempty  = PartialOrdering
    POEQ
      mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering
    mappend = PartialOrdering -> PartialOrdering -> PartialOrdering
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Embed 'Ordering'.
    fromOrdering :: Ordering -> PartialOrdering
    fromOrdering :: Ordering -> PartialOrdering
    fromOrdering Ordering
    LT = PartialOrdering
    POLT
    fromOrdering Ordering
    EQ = PartialOrdering
    POEQ
    fromOrdering Ordering
    GT = PartialOrdering
    POGT

    -- | Represent a non-empty disjunction of 'Ordering's as 'PartialOrdering'.
    fromOrderings :: [Ordering] -> PartialOrdering
    fromOrderings :: [Ordering] -> PartialOrdering
    fromOrderings = (PartialOrdering -> PartialOrdering -> PartialOrdering)
    -> [PartialOrdering] -> PartialOrdering
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 PartialOrdering -> PartialOrdering -> PartialOrdering
    orPO ([PartialOrdering] -> PartialOrdering)
    -> ([Ordering] -> [PartialOrdering])
    -> [Ordering]
    -> PartialOrdering
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ordering -> PartialOrdering) -> [Ordering] -> [PartialOrdering]
    forall a b. (a -> b) -> [a] -> [b]
    map Ordering -> PartialOrdering
    fromOrdering

    -- | A 'PartialOrdering' information is a disjunction of 'Ordering' informations.
    toOrderings :: PartialOrdering -> [Ordering]
    toOrderings :: PartialOrdering -> [Ordering]
    toOrderings PartialOrdering
    POLT  = [Ordering
    LT]
    toOrderings PartialOrdering
    POLE  = [Ordering
    LT, Ordering
    EQ]
    toOrderings PartialOrdering
    POEQ  = [Ordering
    EQ]
    toOrderings PartialOrdering
    POGE  = [Ordering
    EQ, Ordering
    GT]
    toOrderings PartialOrdering
    POGT  = [Ordering
    GT]
    toOrderings PartialOrdering
    POAny = [Ordering
    LT, Ordering
    EQ, Ordering
    GT]

    -- * Comparison with partial result

    type Comparable a = a -> a -> PartialOrdering

    -- | Decidable partial orderings.
    class PartialOrd a where
      comparable :: Comparable a

    -- | Any 'Ord' is a 'PartialOrd'.
    comparableOrd :: Ord a => Comparable a
    comparableOrd :: forall a. Ord a => Comparable a
    comparableOrd a
    x a
    y = Ordering -> PartialOrdering
    fromOrdering (Ordering -> PartialOrdering) -> Ordering -> PartialOrdering
    forall a b. (a -> b) -> a -> b
    $ a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y

    -- | Are two elements related in a specific way?
    --
    --   @related a o b@ holds iff @comparable a b@ is contained in @o@.

    related :: PartialOrd a => a -> PartialOrdering -> a -> Bool
    related :: forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
    related a
    a PartialOrdering
    o a
    b = Comparable a
    forall a. PartialOrd a => Comparable a
    comparable a
    a a
    b PartialOrdering -> PartialOrdering -> Bool
    `leqPO` PartialOrdering
    o

    -- * Totally ordered types.

    instance PartialOrd Int where
      comparable :: Comparable Int
    comparable = Comparable Int
    forall a. Ord a => Comparable a
    comparableOrd

    instance PartialOrd Integer where
      comparable :: Comparable Integer
    comparable = Comparable Integer
    forall a. Ord a => Comparable a
    comparableOrd

    -- * Generic partially ordered types.

    instance PartialOrd () where
      comparable :: Comparable ()
    comparable ()
    _ ()
    _ = PartialOrdering
    POEQ

    -- | 'Nothing' and @'Just' _@ are unrelated.
    --
    --   Partial ordering for @Maybe a@ is the same as for @Either () a@.

    instance PartialOrd a => PartialOrd (Maybe a) where
      comparable :: Comparable (Maybe a)
    comparable Maybe a
    mx Maybe a
    my = case (Maybe a
    mx, Maybe a
    my) of
        (Maybe a
    Nothing, Maybe a
    Nothing) -> PartialOrdering
    POEQ
        (Maybe a
    Nothing, Just{} ) -> PartialOrdering
    POAny
        (Just{} , Maybe a
    Nothing) -> PartialOrdering
    POAny
        (Just a
    x , Just a
    y ) -> Comparable a
    forall a. PartialOrd a => Comparable a
    comparable a
    x a
    y

    -- | Partial ordering for disjoint sums: @Left _@ and @Right _@ are unrelated.

    instance (PartialOrd a, PartialOrd b) => PartialOrd (Either a b) where
      comparable :: Comparable (Either a b)
    comparable Either a b
    mx Either a b
    my = case (Either a b
    mx, Either a b
    my) of
        (Left  a
    x, Left  a
    y) -> Comparable a
    forall a. PartialOrd a => Comparable a
    comparable a
    x a
    y
        (Left  a
    _, Right b
    _) -> PartialOrdering
    POAny
        (Right b
    _, Left  a
    _) -> PartialOrdering
    POAny
        (Right b
    x, Right b
    y) -> Comparable b
    forall a. PartialOrd a => Comparable a
    comparable b
    x b
    y

    -- | Pointwise partial ordering for tuples.
    --
    --   @related (x1,x2) o (y1,y2)@ iff @related x1 o x2@ and @related y1 o y2@.

    instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
      comparable :: Comparable (a, b)
    comparable (a
    x1, b
    x2) (a
    y1, b
    y2) =
        Comparable a
    forall a. PartialOrd a => Comparable a
    comparable a
    x1 a
    y1 PartialOrdering -> PartialOrdering -> PartialOrdering
    `orPO`
        Comparable b
    forall a. PartialOrd a => Comparable a
    comparable b
    x2 b
    y2

    -- | Pointwise comparison wrapper.

    newtype Pointwise a = Pointwise { forall a. Pointwise a -> a
    pointwise :: a }
      deriving (Pointwise a -> Pointwise a -> Bool
    (Pointwise a -> Pointwise a -> Bool)
    -> (Pointwise a -> Pointwise a -> Bool) -> Eq (Pointwise a)
    forall a. Eq a => Pointwise a -> Pointwise a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Pointwise a -> Pointwise a -> Bool
    $c/= :: forall a. Eq a => Pointwise a -> Pointwise a -> Bool
    == :: Pointwise a -> Pointwise a -> Bool
    $c== :: forall a. Eq a => Pointwise a -> Pointwise a -> Bool
    Eq, Int -> Pointwise a -> ShowS
    [Pointwise a] -> ShowS
    Pointwise a -> String
    (Int -> Pointwise a -> ShowS)
    -> (Pointwise a -> String)
    -> ([Pointwise a] -> ShowS)
    -> Show (Pointwise a)
    forall a. Show a => Int -> Pointwise a -> ShowS
    forall a. Show a => [Pointwise a] -> ShowS
    forall a. Show a => Pointwise a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Pointwise a] -> ShowS
    $cshowList :: forall a. Show a => [Pointwise a] -> ShowS
    show :: Pointwise a -> String
    $cshow :: forall a. Show a => Pointwise a -> String
    showsPrec :: Int -> Pointwise a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Pointwise a -> ShowS
    Show, (forall a b. (a -> b) -> Pointwise a -> Pointwise b)
    -> (forall a b. a -> Pointwise b -> Pointwise a)
    -> Functor Pointwise
    forall a b. a -> Pointwise b -> Pointwise a
    forall a b. (a -> b) -> Pointwise a -> Pointwise b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Pointwise b -> Pointwise a
    $c<$ :: forall a b. a -> Pointwise b -> Pointwise a
    fmap :: forall a b. (a -> b) -> Pointwise a -> Pointwise b
    $cfmap :: forall a b. (a -> b) -> Pointwise a -> Pointwise b
    Functor)

    -- | 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 PartialOrd a => PartialOrd (Pointwise [a]) where
      comparable :: Comparable (Pointwise [a])
    comparable (Pointwise [a]
    xs) (Pointwise [a]
    ys) = Maybe PartialOrdering -> [a] -> [a] -> PartialOrdering
    forall {a}.
    PartialOrd a =>
    Maybe PartialOrdering -> [a] -> [a] -> PartialOrdering
    loop Maybe PartialOrdering
    forall a. Maybe a
    Nothing [a]
    xs [a]
    ys
        -- We need an accumulator since @orPO@ does not have a neutral element.
        where
          loop :: Maybe PartialOrdering -> [a] -> [a] -> PartialOrdering
    loop Maybe PartialOrdering
    mo []     []     = PartialOrdering -> Maybe PartialOrdering -> PartialOrdering
    forall a. a -> Maybe a -> a
    fromMaybe PartialOrdering
    POEQ Maybe PartialOrdering
    mo
          loop Maybe PartialOrdering
    _  []     [a]
    ys     = PartialOrdering
    POAny
          loop Maybe PartialOrdering
    _  [a]
    xs     []     = PartialOrdering
    POAny
          loop Maybe PartialOrdering
    mo (a
    x:[a]
    xs) (a
    y:[a]
    ys) =
            let o :: PartialOrdering
    o = Comparable a
    forall a. PartialOrd a => Comparable a
    comparable a
    x a
    y in
            case PartialOrdering
    -> (PartialOrdering -> PartialOrdering)
    -> Maybe PartialOrdering
    -> PartialOrdering
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe PartialOrdering
    o (PartialOrdering -> PartialOrdering -> PartialOrdering
    orPO PartialOrdering
    o) Maybe PartialOrdering
    mo of
              PartialOrdering
    POAny -> PartialOrdering
    POAny
              PartialOrdering
    o     -> Maybe PartialOrdering -> [a] -> [a] -> PartialOrdering
    loop (PartialOrdering -> Maybe PartialOrdering
    forall a. a -> Maybe a
    Just PartialOrdering
    o) [a]
    xs [a]
    ys

    -- | Inclusion comparison wrapper.

    newtype Inclusion a = Inclusion { forall a. Inclusion a -> a
    inclusion :: a }
      deriving (Inclusion a -> Inclusion a -> Bool
    (Inclusion a -> Inclusion a -> Bool)
    -> (Inclusion a -> Inclusion a -> Bool) -> Eq (Inclusion a)
    forall a. Eq a => Inclusion a -> Inclusion a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Inclusion a -> Inclusion a -> Bool
    $c/= :: forall a. Eq a => Inclusion a -> Inclusion a -> Bool
    == :: Inclusion a -> Inclusion a -> Bool
    $c== :: forall a. Eq a => Inclusion a -> Inclusion a -> Bool
    Eq, Eq (Inclusion a)
    Eq (Inclusion a)
    -> (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)
    -> (Inclusion a -> Inclusion a -> Inclusion a)
    -> (Inclusion a -> Inclusion a -> Inclusion a)
    -> Ord (Inclusion a)
    Inclusion a -> Inclusion a -> Bool
    Inclusion a -> Inclusion a -> Ordering
    Inclusion a -> Inclusion a -> Inclusion a
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall {a}. Ord a => Eq (Inclusion a)
    forall a. Ord a => Inclusion a -> Inclusion a -> Bool
    forall a. Ord a => Inclusion a -> Inclusion a -> Ordering
    forall a. Ord a => Inclusion a -> Inclusion a -> Inclusion a
    min :: Inclusion a -> Inclusion a -> Inclusion a
    $cmin :: forall a. Ord a => Inclusion a -> Inclusion a -> Inclusion a
    max :: Inclusion a -> Inclusion a -> Inclusion a
    $cmax :: forall a. Ord a => Inclusion a -> Inclusion a -> Inclusion a
    >= :: Inclusion a -> Inclusion a -> Bool
    $c>= :: forall a. Ord a => Inclusion a -> Inclusion a -> Bool
    > :: Inclusion a -> Inclusion a -> Bool
    $c> :: forall a. Ord a => Inclusion a -> Inclusion a -> Bool
    <= :: Inclusion a -> Inclusion a -> Bool
    $c<= :: forall a. Ord a => Inclusion a -> Inclusion a -> Bool
    < :: Inclusion a -> Inclusion a -> Bool
    $c< :: forall a. Ord a => Inclusion a -> Inclusion a -> Bool
    compare :: Inclusion a -> Inclusion a -> Ordering
    $ccompare :: forall a. Ord a => Inclusion a -> Inclusion a -> Ordering
    Ord, Int -> Inclusion a -> ShowS
    [Inclusion a] -> ShowS
    Inclusion a -> String
    (Int -> Inclusion a -> ShowS)
    -> (Inclusion a -> String)
    -> ([Inclusion a] -> ShowS)
    -> Show (Inclusion a)
    forall a. Show a => Int -> Inclusion a -> ShowS
    forall a. Show a => [Inclusion a] -> ShowS
    forall a. Show a => Inclusion a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Inclusion a] -> ShowS
    $cshowList :: forall a. Show a => [Inclusion a] -> ShowS
    show :: Inclusion a -> String
    $cshow :: forall a. Show a => Inclusion a -> String
    showsPrec :: Int -> Inclusion a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Inclusion a -> ShowS
    Show, (forall a b. (a -> b) -> Inclusion a -> Inclusion b)
    -> (forall a b. a -> Inclusion b -> Inclusion a)
    -> Functor Inclusion
    forall a b. a -> Inclusion b -> Inclusion a
    forall a b. (a -> b) -> Inclusion a -> Inclusion b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Inclusion b -> Inclusion a
    $c<$ :: forall a b. a -> Inclusion b -> Inclusion a
    fmap :: forall a b. (a -> b) -> Inclusion a -> Inclusion b
    $cfmap :: forall a b. (a -> b) -> Inclusion a -> Inclusion b
    Functor)

    -- | Sublist for ordered lists.

    instance (Ord a) => PartialOrd (Inclusion [a]) where
      comparable :: Comparable (Inclusion [a])
    comparable (Inclusion [a]
    xs) (Inclusion [a]
    ys) = PartialOrdering -> [a] -> [a] -> PartialOrdering
    forall {a}.
    Ord a =>
    PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge PartialOrdering
    POEQ [a]
    xs [a]
    ys
        where
          -- We use an accumulator in order to short-cut computation
          -- once we know the lists are incomparable.
          merge' :: PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge' PartialOrdering
    POAny [a]
    xs [a]
    ys = PartialOrdering
    POAny
          merge' PartialOrdering
    o     [a]
    xs [a]
    ys = PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge PartialOrdering
    o [a]
    xs [a]
    ys
          merge :: PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge PartialOrdering
    o [] [] = PartialOrdering
    o
          merge PartialOrdering
    o [] [a]
    ys = PartialOrdering -> PartialOrdering -> PartialOrdering
    forall a. Monoid a => a -> a -> a
    mappend PartialOrdering
    o PartialOrdering
    POLT
          merge PartialOrdering
    o [a]
    xs [] = PartialOrdering -> PartialOrdering -> PartialOrdering
    forall a. Monoid a => a -> a -> a
    mappend PartialOrdering
    o PartialOrdering
    POGT
          merge PartialOrdering
    o xs :: [a]
    xs@(a
    x:[a]
    xs') ys :: [a]
    ys@(a
    y:[a]
    ys') =
            case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
              -- xs has an element that ys does not have => POGT
              Ordering
    LT -> PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge' (PartialOrdering -> PartialOrdering -> PartialOrdering
    forall a. Monoid a => a -> a -> a
    mappend PartialOrdering
    o PartialOrdering
    POGT) [a]
    xs' [a]
    ys
              -- equal elements can be cancelled
              Ordering
    EQ -> PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge PartialOrdering
    o [a]
    xs' [a]
    ys'
              -- ys has an element that xs does not have => POLT
              Ordering
    GT -> PartialOrdering -> [a] -> [a] -> PartialOrdering
    merge' (PartialOrdering -> PartialOrdering -> PartialOrdering
    forall a. Monoid a => a -> a -> a
    mappend PartialOrdering
    o PartialOrdering
    POLT) [a]
    xs [a]
    ys'

    -- | Sets are partially ordered by inclusion.

    instance Ord a => PartialOrd (Inclusion (Set a)) where
      comparable :: Comparable (Inclusion (Set a))
    comparable Inclusion (Set a)
    s Inclusion (Set a)
    t = Comparable (Inclusion [a])
    forall a. PartialOrd a => Comparable a
    comparable (Set a -> [a]
    forall a. Set a -> [a]
    Set.toAscList (Set a -> [a]) -> Inclusion (Set a) -> Inclusion [a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Inclusion (Set a)
    s) (Set a -> [a]
    forall a. Set a -> [a]
    Set.toAscList (Set a -> [a]) -> Inclusion (Set a) -> Inclusion [a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Inclusion (Set a)
    t)

    -- * PartialOrdering is itself partially ordered!

    -- | Less is ``less general'' (i.e., more precise).
    instance PartialOrd PartialOrdering where
      -- working our way down: POAny is top
      comparable :: PartialOrdering -> PartialOrdering -> PartialOrdering
    comparable PartialOrdering
    POAny PartialOrdering
    POAny = PartialOrdering
    POEQ
      comparable PartialOrdering
    POAny PartialOrdering
    _     = PartialOrdering
    POGT
      comparable PartialOrdering
    _     PartialOrdering
    POAny = PartialOrdering
    POLT
      -- next are the fuzzy notions POLE and POGE
      comparable PartialOrdering
    POLE  PartialOrdering
    POLE  = PartialOrdering
    POEQ
      comparable PartialOrdering
    POLE  PartialOrdering
    POLT  = PartialOrdering
    POGT
      comparable PartialOrdering
    POLE  PartialOrdering
    POEQ  = PartialOrdering
    POGT
      comparable PartialOrdering
    POGE  PartialOrdering
    POGE  = PartialOrdering
    POEQ
      comparable PartialOrdering
    POGE  PartialOrdering
    POGT  = PartialOrdering
    POGT
      comparable PartialOrdering
    POGE  PartialOrdering
    POEQ  = PartialOrdering
    POGT
      -- lowest are the precise notions POLT POEQ POGT
      comparable PartialOrdering
    POLT  PartialOrdering
    POLT  = PartialOrdering
    POEQ
      comparable PartialOrdering
    POLT  PartialOrdering
    POLE  = PartialOrdering
    POLT
      comparable PartialOrdering
    POEQ  PartialOrdering
    POEQ  = PartialOrdering
    POEQ
      comparable PartialOrdering
    POEQ  PartialOrdering
    POLE  = PartialOrdering
    POLT
      comparable PartialOrdering
    POEQ  PartialOrdering
    POGE  = PartialOrdering
    POLT
      comparable PartialOrdering
    POGT  PartialOrdering
    POGT  = PartialOrdering
    POEQ
      comparable PartialOrdering
    POGT  PartialOrdering
    POGE  = PartialOrdering
    POLT
      -- anything horizontal is not comparable
      comparable PartialOrdering
    _     PartialOrdering
    _     = PartialOrdering
    POAny