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