diff options
Diffstat (limited to 'src/full/Agda/Utils/PartialOrd.hs')
-rw-r--r-- | src/full/Agda/Utils/PartialOrd.hs | 173 |
1 files changed, 5 insertions, 168 deletions
diff --git a/src/full/Agda/Utils/PartialOrd.hs b/src/full/Agda/Utils/PartialOrd.hs index 0f1e331..1b1608c 100644 --- a/src/full/Agda/Utils/PartialOrd.hs +++ b/src/full/Agda/Utils/PartialOrd.hs @@ -1,22 +1,14 @@ -{-# 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.Semigroup 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 @@ -128,9 +120,12 @@ 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 = seqPO + mappend = (<>) -- | Embed 'Ordering'. fromOrdering :: Ordering -> PartialOrdering @@ -291,161 +286,3 @@ instance PartialOrd PartialOrdering where 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 --- ] |