module Agda.Utils.Favorites where
import Control.Monad
import Data.Bool
import Data.Eq
import Data.Ord
import Data.Foldable (Foldable)
import Data.Functor
import Data.Function
import Data.Monoid
import Data.List (all, (++))
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Tuple (uncurry)
import System.IO
import Text.Show
import Test.QuickCheck.All
import Agda.Utils.PartialOrd hiding (tests)
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
newtype Favorites a = Favorites { toList :: [a] }
deriving (Foldable, Show, CoArbitrary)
instance Ord a => Eq (Favorites a) where
as == bs = Set.fromList (toList as) == Set.fromList (toList bs)
null :: Favorites a -> Bool
null = List.null . toList
empty :: Favorites a
empty = Favorites []
singleton :: a -> Favorites a
singleton a = Favorites [a]
data CompareResult a
= Dominates { dominated :: [a], notDominated :: [a] }
| IsDominated { dominator :: a }
compareWithFavorites :: PartialOrd a => a -> Favorites a -> CompareResult a
compareWithFavorites a favs = loop $ toList favs where
loop [] = Dominates [] []
loop as@(b : bs) = case comparable a b of
POLT -> dominates b $ loop bs
POLE -> dominates b $ loop bs
POEQ -> IsDominated a
POGE -> IsDominated a
POGT -> IsDominated a
POAny -> doesnotd b $ loop bs
dominates b (Dominates bs as) = Dominates (b : bs) as
dominates b r@IsDominated{} = r
doesnotd b (Dominates as bs) = Dominates as (b : bs)
doesnotd b r@IsDominated{} = r
compareFavorites :: PartialOrd a => Favorites a -> Favorites a ->
(Favorites a, Favorites a)
compareFavorites new old = mapFst Favorites $ loop (toList new) old where
loop [] old = ([], old)
loop (a : new) old = case compareWithFavorites a old of
Dominates _ old -> mapFst (a:) $ loop new (Favorites old)
IsDominated{} -> loop new old
unionCompared :: PartialOrd a => (Favorites a, Favorites a) -> Favorites a
unionCompared (Favorites new, Favorites old) = Favorites $ new ++ old
insertCompared :: PartialOrd a => a -> Favorites a -> CompareResult a -> Favorites a
insertCompared a _ (Dominates _ as) = Favorites (a : as)
insertCompared _ l IsDominated{} = l
insert :: PartialOrd a => a -> Favorites a -> Favorites a
insert a l = insertCompared a l (compareWithFavorites a l)
union :: PartialOrd a => Favorites a -> Favorites a -> Favorites a
union (Favorites as) bs = List.foldr insert bs as
fromList :: PartialOrd a => [a] -> Favorites a
fromList = List.foldl' (flip insert) empty
instance PartialOrd a => Monoid (Favorites a) where
mempty = empty
mappend = union
instance (PartialOrd a, Arbitrary a) => Arbitrary (Favorites a) where
arbitrary = fromList <$> arbitrary
property_null_empty :: Bool
property_null_empty = null empty
property_not_null_singleton :: a -> Bool
property_not_null_singleton = not . null . singleton
prop_compareWithFavorites :: ISet -> Favorites ISet -> Bool
prop_compareWithFavorites a@ISet{} as =
case compareWithFavorites a as of
Dominates dominated notDominated ->
all (related a POLT) dominated &&
all (related a POAny) notDominated
IsDominated dominator ->
related a POGE dominator
prop_fromList_after_toList :: Favorites ISet -> Bool
prop_fromList_after_toList as =
fromList (toList as) == as
prop_union_union2 :: Favorites ISet -> Favorites ISet -> Bool
prop_union_union2 as bs =
union as bs == union2 as bs
where union2 as bs = unionCompared $ compareFavorites as bs
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Favorites"
$quickCheckAll