agda/test/Internal/Utils/PartialOrd.hs

{-# LANGUAGE TemplateHaskell            #-}

module Internal.Utils.PartialOrd
  ( ISet(ISet)
  , tests
  ) where

import Agda.Utils.PartialOrd

import Data.List ( (\\) )
import Data.Set (Set)
import qualified Data.Set as Set

import Internal.Helpers

------------------------------------------------------------------------------
-- * 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 = isAssociative orPO

-- | 'orPO' is commutative.
prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool
prop_commutative_orPO = isCommutative orPO

-- | 'orPO' is idempotent.
prop_idempotent_orPO :: PartialOrdering -> Bool
prop_idempotent_orPO = isIdempotent 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

-- | 'PartialOrdering' is a monoid, i.e. 'seqPO' is associative and
-- the unit of 'seqPO' is 'POEQ'.
prop_monoid_seqPO :: Property3 PartialOrdering
prop_monoid_seqPO = isMonoid

-- | The zero of 'seqPO' is 'POAny'.
prop_zero_seqPO :: PartialOrdering -> Bool
prop_zero_seqPO = isZero POAny seqPO

-- | 'seqPO' is also commutative.
prop_commutative_seqPO :: PartialOrdering -> PartialOrdering -> Bool
prop_commutative_seqPO = isCommutative seqPO

-- | 'seqPO' is idempotent.
prop_idempotent_seqPO :: PartialOrdering -> Bool
prop_idempotent_seqPO = isIdempotent seqPO

-- | 'seqPO' distributes over 'orPO'.
prop_distributive_seqPO_orPO :: PartialOrdering -> PartialOrdering ->
                                PartialOrdering -> Bool
prop_distributive_seqPO_orPO = isDistributive 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 $allProperties work
-- under ghc-7.8.
return [] -- KEEP!

-- | All tests as collected by 'allProperties'.
--
-- Using 'allProperties' is convenient and superior to the manual
-- enumeration of tests, since the name of the property is added
-- automatically.

tests :: TestTree
tests = testProperties "Internal.Utils.PartialOrd" $allProperties