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