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