{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell #-}

module Agda.Utils.PartialOrd where

import Data.Functor
import Data.Maybe
import Data.Monoid
import Data.List
import Data.Set (Set)
import qualified Data.Set as Set

import Test.QuickCheck.All

-- import Agda.Utils.List
import Agda.Utils.SemiRing
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck

-- | 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 Monoid PartialOrdering where
  mempty  = POEQ
  mappend = seqPO

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

-- * Properties

instance Arbitrary PartialOrdering where
  arbitrary = arbitraryBoundedEnum

-- | We test our properties on integer sets ordered by inclusion.

newtype ISet = ISet { iset :: Inclusion (Set Int) }
  deriving (Eq, Ord, PartialOrd, Show)

instance Arbitrary ISet where
  arbitrary = ISet . Inclusion . Set.fromList <$> listOf (choose (0, 8))

-- | Any two elements are 'related' in the way 'comparable' computes.
prop_comparable_related :: ISet -> ISet -> Bool
prop_comparable_related (ISet a) (ISet b) =
  related a o b where o = comparable a b

-- | @flip comparable a b == oppPO (comparable a b)@
prop_oppPO :: ISet -> ISet -> Bool
prop_oppPO (ISet a) (ISet b) =
  comparable a b == oppPO (comparable b a)

-- | Auxiliary function: lists to sets = sorted duplicate-free lists.
sortUniq :: [Ordering] -> [Ordering]
sortUniq = Set.toAscList . Set.fromList

-- | 'leqPO' is inclusion of the associated 'Ordering' sets.
prop_leqPO_sound :: PartialOrdering -> PartialOrdering -> Bool
prop_leqPO_sound p q =
  (p `leqPO` q) == null (toOrderings p \\ toOrderings q)

-- | 'orPO' amounts to the union of the associated 'Ordering' sets.
--   Except that 'orPO POLT POGT == POAny' which should also include 'POEQ'.
prop_orPO_sound :: PartialOrdering -> PartialOrdering -> Bool
prop_orPO_sound p q =
  (p `orPO` q) == fromOrderings (toOrderings p ++ toOrderings q)

-- | 'orPO' is associative.
prop_associative_orPO :: PartialOrdering -> PartialOrdering ->
                         PartialOrdering -> Bool
prop_associative_orPO = associative orPO

-- | 'orPO' is commutative.
prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool
prop_commutative_orPO = commutative orPO

-- | 'orPO' is idempotent.
prop_idempotent_orPO :: PartialOrdering -> Bool
prop_idempotent_orPO = idempotent orPO

-- | The dominant element wrt. 'orPO' is 'POAny'.
prop_zero_orPO :: PartialOrdering -> Bool
prop_zero_orPO = isZero POAny orPO

-- | Soundness of 'seqPO'.
--
--   As QuickCheck test, this property is inefficient, see 'prop_seqPO'.
property_seqPO :: ISet -> PartialOrdering -> ISet -> PartialOrdering ->
                  ISet -> Property
property_seqPO (ISet a) o (ISet b) p (ISet c) =
  related a o b && related b p c ==> related a (seqPO o p) c

-- | A more efficient way of stating soundness of 'seqPO'.
prop_seqPO :: ISet -> ISet -> ISet -> Bool
prop_seqPO (ISet a) (ISet b) (ISet c) = related a o c
  where o = comparable a b `seqPO` comparable b c

-- | The unit of 'seqPO' is 'POEQ'.
prop_identity_seqPO :: PartialOrdering -> Bool
prop_identity_seqPO = identity POEQ seqPO

-- | The zero of 'seqPO' is 'POAny'.
prop_zero_seqPO :: PartialOrdering -> Bool
prop_zero_seqPO = isZero POAny seqPO

-- | 'seqPO' is associative.
prop_associative_seqPO :: PartialOrdering -> PartialOrdering ->
                          PartialOrdering -> Bool
prop_associative_seqPO = associative seqPO

-- | 'seqPO' is also commutative.
prop_commutative_seqPO :: PartialOrdering -> PartialOrdering -> Bool
prop_commutative_seqPO = commutative seqPO

-- | 'seqPO' is idempotent.
prop_idempotent_seqPO :: PartialOrdering -> Bool
prop_idempotent_seqPO = idempotent seqPO

-- | 'seqPO' distributes over 'orPO'.
prop_distributive_seqPO_orPO :: PartialOrdering -> PartialOrdering ->
                                PartialOrdering -> Bool
prop_distributive_seqPO_orPO = distributive seqPO orPO

-- | The result of 'toOrderings' is a sorted list without duplicates.
prop_sorted_toOrderings :: PartialOrdering -> Bool
prop_sorted_toOrderings p =
  sortUniq os == os where os = toOrderings p

-- | From 'Ordering' to 'PartialOrdering' and back is the identity.
prop_toOrderings_after_fromOrdering :: Ordering -> Bool
prop_toOrderings_after_fromOrdering o =
  toOrderings (fromOrdering o) == [o]

-- | From 'PartialOrdering' to 'Orderings' and back is the identity.
prop_fromOrderings_after_toOrderings :: PartialOrdering -> Bool
prop_fromOrderings_after_toOrderings p =
  fromOrderings (toOrderings p) == p

-- | From 'Orderings' to 'PartialOrdering' and back is the identity.
--   Except for @[LT,GT]@ which is a non-canonical representative of 'POAny'.
prop_toOrderings_after_fromOrderings :: NonEmptyList Ordering -> Bool
prop_toOrderings_after_fromOrderings (NonEmpty os) =
  Set.fromList os  `Set.isSubsetOf`
  Set.fromList (toOrderings (fromOrderings os))

-- | Pairs are related iff both components are related.
prop_related_pair :: ISet -> ISet -> ISet -> ISet -> PartialOrdering -> Bool
prop_related_pair (ISet x1) (ISet x2) (ISet y1) (ISet y2) o =
  related (x1,x2) o (y1,y2) == (related x1 o y1 && related x2 o y2)

-- | Comparing 'PartialOrdering's amounts to compare their representation as
--   'Ordering' sets.

prop_comparable_PartialOrdering :: PartialOrdering -> PartialOrdering -> Bool

prop_comparable_PartialOrdering p q =
  comparable p q == comparable (to p) (to q)
    where to = Inclusion . toOrderings

------------------------------------------------------------------------
-- * All tests
------------------------------------------------------------------------

-- Template Haskell hack to make the following $quickCheckAll work
-- under ghc-7.8.
return [] -- KEEP!

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

tests :: IO Bool
tests = do
  putStrLn "Agda.Utils.PartialOrd"
  $quickCheckAll

-- tests' :: IO Bool
-- tests' = runTests "Agda.Utils.PartialOrd"
--   [ quickCheck' prop_comparable_related
--   , quickCheck' prop_oppPO
--   , quickCheck' prop_seqPO
--   , quickCheck' prop_assoc_seqPO
--   , quickCheck' prop_related_pair
--   ]