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.SemiRing
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
data PartialOrdering
= POLT
| POLE
| POEQ
| POGE
| POGT
| POAny
deriving (Eq, Show, Enum, Bounded)
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
oppPO :: PartialOrdering -> PartialOrdering
oppPO POLT = POGT
oppPO POLE = POGE
oppPO POEQ = POEQ
oppPO POGE = POLE
oppPO POGT = POLT
oppPO POAny = POAny
orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering
orPO POAny _ = POAny
orPO POLT POLT = POLT
orPO POLT POLE = POLE
orPO POLT POEQ = POLE
orPO POLE POLT = POLE
orPO POLE POLE = POLE
orPO POLE POEQ = POLE
orPO POEQ POLT = POLE
orPO POEQ POLE = POLE
orPO POEQ POEQ = POEQ
orPO POEQ POGE = POGE
orPO POEQ POGT = POGE
orPO POGE POEQ = POGE
orPO POGE POGE = POGE
orPO POGE POGT = POGE
orPO POGT POEQ = POGE
orPO POGT POGE = POGE
orPO POGT POGT = POGT
orPO _ _ = POAny
seqPO POAny _ = POAny
seqPO POEQ p = p
seqPO POLT POLT = POLT
seqPO POLT POLE = POLT
seqPO POLT POEQ = POLT
seqPO POLE POLT = POLT
seqPO POLE POLE = POLE
seqPO POLE POEQ = POLE
seqPO POGE POEQ = POGE
seqPO POGE POGE = POGE
seqPO POGE POGT = POGT
seqPO POGT POEQ = POGT
seqPO POGT POGE = POGT
seqPO POGT POGT = POGT
seqPO _ _ = POAny
instance Monoid PartialOrdering where
mempty = POEQ
mappend = seqPO
instance SemiRing PartialOrdering where
oplus = orPO
otimes = seqPO
fromOrdering :: Ordering -> PartialOrdering
fromOrdering LT = POLT
fromOrdering EQ = POEQ
fromOrdering GT = POGT
fromOrderings :: [Ordering] -> PartialOrdering
fromOrderings = foldr1 orPO . map fromOrdering
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]
type Comparable a = a -> a -> PartialOrdering
class PartialOrd a where
comparable :: Comparable a
comparableOrd :: Ord a => Comparable a
comparableOrd x y = fromOrdering $ compare x y
related :: PartialOrd a => a -> PartialOrdering -> a -> Bool
related a o b = comparable a b `leqPO` o
instance PartialOrd Int where
comparable = comparableOrd
instance PartialOrd Integer where
comparable = comparableOrd
instance PartialOrd () where
comparable _ _ = POEQ
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
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 x, Right y) -> POAny
(Right x, Left y) -> POAny
(Right x, Right y) -> comparable x y
instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
comparable (x1, x2) (y1, y2) =
comparable x1 y1 `orPO`
comparable x2 y2
newtype Pointwise a = Pointwise { pointwise :: a }
deriving (Eq, Show, Functor)
instance PartialOrd a => PartialOrd (Pointwise [a]) where
comparable (Pointwise xs) (Pointwise ys) = loop Nothing xs ys
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
newtype Inclusion a = Inclusion { inclusion :: a }
deriving (Eq, Ord, Show, Functor)
instance (Ord a) => PartialOrd (Inclusion [a]) where
comparable (Inclusion xs) (Inclusion ys) = merge POEQ xs ys
where
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
LT -> merge' (mappend o POGT) xs' ys
EQ -> merge o xs' ys'
GT -> merge' (mappend o POLT) xs ys'
instance Ord a => PartialOrd (Inclusion (Set a)) where
comparable s t = comparable (Set.toAscList <$> s) (Set.toAscList <$> t)
instance PartialOrd PartialOrdering where
comparable POAny POAny = POEQ
comparable POAny _ = POGT
comparable _ POAny = POLT
comparable POLE POLE = POEQ
comparable POLE POLT = POGT
comparable POLE POEQ = POGT
comparable POGE POGE = POEQ
comparable POGE POGT = POGT
comparable POGE 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
comparable _ _ = POAny
instance Arbitrary PartialOrdering where
arbitrary = arbitraryBoundedEnum
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))
prop_comparable_related (ISet a) (ISet b) =
related a o b where o = comparable a b
prop_oppPO (ISet a) (ISet b) =
comparable a b == oppPO (comparable b a)
sortUniq = Set.toAscList . Set.fromList
prop_leqPO_sound p q =
(p `leqPO` q) == null (toOrderings p \\ toOrderings q)
prop_orPO_sound p q =
(p `orPO` q) == fromOrderings (toOrderings p ++ toOrderings q)
prop_associative_orPO = associative orPO
prop_commutative_orPO = commutative orPO
prop_idempotent_orPO = idempotent orPO
prop_zero_orPO = isZero POAny orPO
property_seqPO (ISet a) o (ISet b) p (ISet c) =
related a o b && related b p c ==> related a (seqPO o p) c
prop_seqPO (ISet a) (ISet b) (ISet c) = related a o c
where o = comparable a b `seqPO` comparable b c
prop_identity_seqPO = identity POEQ seqPO
prop_zero_seqPO = isZero POAny seqPO
prop_associative_seqPO = associative seqPO
prop_commutative_seqPO = commutative seqPO
prop_idempotent_seqPO = idempotent seqPO
prop_distributive_seqPO_orPO = distributive seqPO orPO
prop_sorted_toOrderings p =
sortUniq os == os where os = toOrderings p
prop_toOrderings_after_fromOrdering o =
toOrderings (fromOrdering o) == [o]
prop_fromOrderings_after_toOrderings p =
fromOrderings (toOrderings p) == p
prop_toOrderings_after_fromOrderings (NonEmpty os) =
Set.fromList os `Set.isSubsetOf`
Set.fromList (toOrderings (fromOrderings os))
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)
prop_comparable_PartialOrdering p q =
comparable p q == comparable (to p) (to q)
where to = Inclusion . toOrderings
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.PartialOrd"
$quickCheckAll