{-# 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.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 -- ]