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