{-|
Module      : POrd
Description : Pre (or partially) ordered set
Copyright   : (c) David Janin, 2015
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

A class for preorder relations (reflexive and transitive relations) with associated equivalence. 
We use it for defining tile semantics (via natural preorder). This class can also be used 
for handling partial order relations (antisymetric preorder relations).

-}

{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}

{-# LANGUAGE MultiParamTypeClasses,
             FlexibleInstances #-}

module Duration.POrd where

-- | Partially ordered sets
class POrd a where
  -- | A partial order relation. Though we do not require Eq a, we should have:
  --
  -- prop> if (Eq a) then (a1 == a2) implies partialCompare a1 a2 == Just EQ
  --
  -- The converse may be false especially when Eq a is a "syntactic" equality as with [a].

  partialCompare :: a -> a -> Maybe Ordering
  -- | The Boolean version of the partial order.
  --
  pLeq :: a -> a -> Bool
  pLeq x y = case (partialCompare x y) of
             Just LT -> True
             Just EQ -> True
             _ -> False
  partialCompare x y = case (pLeq x y,pLeq y x) of
                 (True,True) -> Just EQ
                 (True,False) -> Just LT
                 (False,True) -> Just GT
                 (False,False) -> Nothing                                 
  -- | Derived equality:
  --
  -- @
  -- pOrdEq a1 a2 = case partialCompare a1 a2 of
  --                   Just EQ -> True
  --                   _ -> False
  -- @
  pOrdEq :: a -> a -> Bool
  pOrdEq a1 a2
      = case partialCompare a1 a2 of
          Just EQ -> True
          _ -> False
  -- | Gets just the minimum of a list if it exists, nothing otherwise
  pOrdMin :: [a] -> Maybe a
  pOrdMin [] = Nothing
  pOrdMin [x] = Just x
  pOrdMin (x:y:ys)
      = case pOrdMin (y:ys) of
          Nothing -> Nothing
          Just z -> case (partialCompare x z) of
                      Nothing -> Nothing
                      Just LT -> Just x
                      _ -> Just z
  -- | Gets just the minimum of a list if it exists, nothing otherwise
  pOrdMax :: [a] -> Maybe a
  pOrdMax [] = Nothing
  pOrdMax [x] = Just x
  pOrdMax (x:y:ys)
      = case pOrdMax (y:ys) of
          Nothing -> Nothing
          Just z -> case (partialCompare x z) of
                      Nothing -> Nothing
                      Just GT -> Just x
                      _ -> Just z
  -- | Reduces a list to the antichain of its minimal elements
  pOrdReduceMin :: (POrd a) => [a] -> [a]
  pOrdReduceMin [] = []
  pOrdReduceMin (x:xs)
      = let rxs = pOrdReduceMin xs
        in case rxs of
             [] -> [x]
             (y:ys) -> case partialCompare x y of
                         Nothing -> y:pOrdReduceMin (x:ys)
                         Just LT -> pOrdReduceMin (x:ys)
                         _ -> y:ys                          
  -- | Reduces a list to the antichain of its maximal elements
  pOrdReduceMax :: (POrd a) => [a] -> [a]
  pOrdReduceMax [] = []
  pOrdReduceMax (x:xs)
      = let rxs = pOrdReduceMax xs
        in case rxs of
             [] -> [x]
             (y:ys) -> case partialCompare x y of
                         Nothing -> y:pOrdReduceMax (x:ys)
                         Just GT -> pOrdReduceMax (x:ys)
                         _ -> y:ys
  {-# MINIMAL (partialCompare) | (pLeq) #-}



-- | A total order on () is a partial order
instance POrd () where
  partialCompare x y = Just $ compare x y

-- | A total order on Integer is a partial order
instance POrd Integer where
  partialCompare x y = Just $ compare x y

-- | A total order on Int is a partial order
instance POrd Int where
  partialCompare x y = Just $ compare x y

-- | A total order on Char is a partial order
instance POrd Char where
  partialCompare x y = Just $ compare x y

-- | A total order on Rational is a partial order
instance POrd Rational where
  partialCompare x y = Just $ compare x y

-- | Derived partial order for Either
instance (POrd a,POrd b) => POrd (Either a b) where
    partialCompare (Left a1) (Left a2) = partialCompare a1 a2
    partialCompare (Right b1) (Right b2) = partialCompare b1 b2
    partialCompare _ _ = Nothing

-- |  Derived partial order for Product
instance (POrd a,POrd b) => POrd (a,b) where
    partialCompare (a1,b1) (a2,b2)
        =  case (partialCompare a1 a2,partialCompare b1 b2) of
             (Just EQ, r) -> r
             (r,Just EQ) -> r
             (Just LT,Just LT) -> Just LT                
             (Just GT,Just GT) -> Just GT
             _ -> Nothing