    module Agda.Utils.PartialOrd where

    import Data.Functor
    import Data.Maybe
    import Data.Semigroup
    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 (Eq, Show, Enum, 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 _   POAny = True

    leqPO POLT POLT = True
    leqPO POLT POLE = True

    leqPO POLE POLE = True

    leqPO POEQ POLE = True
    leqPO POEQ POEQ = True
    leqPO POEQ POGE = True

    leqPO POGE POGE = True

    leqPO POGT POGT = True
    leqPO POGT POGE = True

    leqPO _ _ = False

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

    oppPO :: PartialOrdering -> PartialOrdering
    oppPO POLT  = POGT
    oppPO POLE  = POGE
    oppPO POEQ  = POEQ
    oppPO POGE  = POLE
    oppPO POGT  = POLT
    oppPO POAny = 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 POAny _   = POAny   -- Shortcut if no information on first.

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

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

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

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

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

    orPO _    _    = 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 POAny _   = POAny  -- Shortcut if no information on first.
    seqPO POEQ p    = p      -- No need to look at second if first is neutral.

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

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

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

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

    seqPO _    _    = POAny

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

    instance Monoid PartialOrdering where
      mempty  = POEQ
      mappend = (<>)

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

    -- | Represent a non-empty disjunction of 'Ordering's as 'PartialOrdering'.
    fromOrderings :: [Ordering] -> PartialOrdering
    fromOrderings = foldr1 orPO . map fromOrdering

    -- | A 'PartialOrdering' information is a disjunction of 'Ordering' informations.
    toOrderings :: PartialOrdering -> [Ordering]
    toOrderings POLT  = [LT]
    toOrderings POLE  = [LT, EQ]
    toOrderings POEQ  = [EQ]
    toOrderings POGE  = [EQ, GT]
    toOrderings POGT  = [GT]
    toOrderings POAny = [LT, EQ, 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 x y = fromOrdering $ compare x 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 a o b = comparable a b `leqPO` o

    -- * Totally ordered types.

    instance PartialOrd Int where
      comparable = comparableOrd

    instance PartialOrd Integer where
      comparable = comparableOrd

    -- * Generic partially ordered types.

    instance PartialOrd () where
      comparable _ _ = 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 mx my = case (mx, my) of
        (Nothing, Nothing) -> POEQ
        (Nothing, Just{} ) -> POAny
        (Just{} , Nothing) -> POAny
        (Just x , Just y ) -> comparable x y

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

    instance (PartialOrd a, PartialOrd b) => PartialOrd (Either a b) where
      comparable mx my = case (mx, my) of
        (Left  x, Left  y) -> comparable x y
        (Left  _, Right _) -> POAny
        (Right _, Left  _) -> POAny
        (Right x, Right y) -> comparable x 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 (x1, x2) (y1, y2) =
        comparable x1 y1 `orPO`
        comparable x2 y2

    -- | Pointwise comparison wrapper.

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

    -- | Inclusion comparison wrapper.

    newtype Inclusion a = Inclusion { inclusion :: a }
      deriving (Eq, Ord, Show, Functor)

    -- | Sublist for ordered lists.

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

    -- | Sets are partially ordered by inclusion.

    instance Ord a => PartialOrd (Inclusion (Set a)) where
      comparable s t = comparable (Set.toAscList <$> s) (Set.toAscList <$> 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 POAny POAny = POEQ
      comparable POAny _     = POGT
      comparable _     POAny = POLT
      -- next are the fuzzy notions POLE and POGE
      comparable POLE  POLE  = POEQ
      comparable POLE  POLT  = POGT
      comparable POLE  POEQ  = POGT
      comparable POGE  POGE  = POEQ
      comparable POGE  POGT  = POGT
      comparable POGE  POEQ  = POGT
      -- lowest are the precise notions POLT POEQ POGT
      comparable POLT  POLT  = POEQ
      comparable POLT  POLE  = POLT
      comparable POEQ  POEQ  = POEQ
      comparable POEQ  POLE  = POLT
      comparable POEQ  POGE  = POLT
      comparable POGT  POGT  = POEQ
      comparable POGT  POGE  = POLT
      -- anything horizontal is not comparable
      comparable _     _     = POAny