1{-# LANGUAGE CPP #-} 2 3-- | Maintaining a list of favorites of some partially ordered type. 4-- Only the best elements are kept. 5-- 6-- To avoid name clashes, import this module qualified, as in 7-- @ 8-- import Agda.Utils.Favorites (Favorites) 9-- import qualified Agda.Utils.Favorites as Fav 10-- @ 11 12module Agda.Utils.Favorites where 13 14import Prelude hiding ( null ) 15 16#if __GLASGOW_HASKELL__ < 804 17import Data.Semigroup 18#endif 19import qualified Data.List as List 20import qualified Data.Set as Set 21 22import Agda.Utils.Null 23import Agda.Utils.PartialOrd 24import Agda.Utils.Singleton 25import Agda.Utils.Tuple 26 27-- | A list of incomparable favorites. 28newtype Favorites a = Favorites { toList :: [a] } 29 deriving (Foldable, Show, Null, Singleton a) 30 31-- | Equality checking is a bit expensive, since we need to sort! 32-- Maybe use a 'Set' of favorites in the first place? 33instance Ord a => Eq (Favorites a) where 34 as == bs = Set.fromList (toList as) == Set.fromList (toList bs) 35 36-- | Result of comparing a candidate with the current favorites. 37data CompareResult a 38 = Dominates { dominated :: [a], notDominated :: [a] } 39 -- ^ Great, you are dominating a possibly (empty list of favorites) 40 -- but there is also a rest that is not dominated. 41 -- If @null dominated@, then @notDominated@ is necessarily the 42 -- complete list of favorites. 43 | IsDominated { dominator :: a } 44 -- ^ Sorry, but you are dominated by that favorite. 45 46 47-- | Gosh, got some pretty @a@ here, compare with my current favorites! 48-- Discard it if there is already one that is better or equal. 49-- (Skewed conservatively: faithful to the old favorites.) 50-- If there is no match for it, add it, and 51-- dispose of all that are worse than @a@. 52-- 53-- We require a partial ordering. Less is better! (Maybe paradoxically.) 54compareWithFavorites :: PartialOrd a => a -> Favorites a -> CompareResult a 55compareWithFavorites a favs = loop $ toList favs where 56 loop [] = Dominates [] [] 57 loop as@(b : bs) = case comparable a b of 58 POLT -> dominates b $ loop bs -- @a@ is a new favorite, bye-bye, @b@ 59 POLE -> dominates b $ loop bs -- ditto 60 POEQ -> IsDominated b -- @b@ is as least as good as @a@, bye-bye, @a@ 61 POGE -> IsDominated b -- ditto 62 POGT -> IsDominated b -- ditto 63 POAny -> doesnotd b $ loop bs -- don't know, compare with my other favorites 64 -- add an outperformed favorite 65 dominates b (Dominates bs as) = Dominates (b : bs) as 66 dominates b r@IsDominated{} = r 67 -- add an uncomparable favorite 68 doesnotd b (Dominates as bs) = Dominates as (b : bs) 69 doesnotd b r@IsDominated{} = r 70 71-- | Compare a new set of favorites to an old one and discard 72-- the new favorites that are dominated by the old ones 73-- and vice verse. 74-- (Skewed conservatively: faithful to the old favorites.) 75-- 76-- @compareFavorites new old = (new', old')@ 77compareFavorites :: PartialOrd a => Favorites a -> Favorites a -> 78 (Favorites a, Favorites a) 79compareFavorites new old = mapFst Favorites $ loop (toList new) old where 80 loop [] old = ([], old) 81 loop (a : new) old = case compareWithFavorites a old of 82 -- Better: Discard all @old@ ones that @a@ dominates and keep @a@ 83 Dominates _ old -> mapFst (a:) $ loop new (Favorites old) 84 -- Not better: Discard @a@ 85 IsDominated{} -> loop new old 86 87unionCompared :: (Favorites a, Favorites a) -> Favorites a 88unionCompared (Favorites new, Favorites old) = Favorites $ new ++ old 89 90-- | After comparing, do the actual insertion. 91insertCompared :: a -> Favorites a -> CompareResult a -> Favorites a 92insertCompared a _ (Dominates _ as) = Favorites (a : as) 93insertCompared _ l IsDominated{} = l 94 95-- | Compare, then insert accordingly. 96-- @insert a l = insertCompared a l (compareWithFavorites a l)@ 97insert :: PartialOrd a => a -> Favorites a -> Favorites a 98insert a l = insertCompared a l (compareWithFavorites a l) 99 100-- | Insert all the favorites from the first list into the second. 101union :: PartialOrd a => Favorites a -> Favorites a -> Favorites a 102union (Favorites as) bs = List.foldr insert bs as 103 104-- | Construct favorites from elements of a partial order. 105-- The result depends on the order of the list if it 106-- contains equal elements, since earlier seen elements 107-- are favored over later seen equals. 108-- The first element of the list is seen first. 109fromList :: PartialOrd a => [a] -> Favorites a 110fromList = List.foldl' (flip insert) empty 111 112-- | 'Favorites' forms a 'Monoid' under 'empty' and 'union. 113instance PartialOrd a => Semigroup (Favorites a) where 114 (<>) = union 115instance PartialOrd a => Monoid (Favorites a) where 116 mempty = empty 117 mappend = (<>) 118