{-# OPTIONS_GHC -Wunused-imports #-}

-- | Maintaining a list of favorites of some partially ordered type.
--   Only the best elements are kept.
--
--   To avoid name clashes, import this module qualified, as in
--   @
--      import Agda.Utils.Favorites (Favorites)
--      import qualified Agda.Utils.Favorites as Fav
--   @

module Agda.Utils.Favorites where

import Prelude hiding ( null )

import qualified Data.List as List
import qualified Data.Set as Set

import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Singleton
import Agda.Utils.Tuple

-- | A list of incomparable favorites.
newtype Favorites a = Favorites { forall a. Favorites a -> [a]
toList :: [a] }
  deriving ((forall m. Monoid m => Favorites m -> m)
-> (forall m a. Monoid m => (a -> m) -> Favorites a -> m)
-> (forall m a. Monoid m => (a -> m) -> Favorites a -> m)
-> (forall a b. (a -> b -> b) -> b -> Favorites a -> b)
-> (forall a b. (a -> b -> b) -> b -> Favorites a -> b)
-> (forall b a. (b -> a -> b) -> b -> Favorites a -> b)
-> (forall b a. (b -> a -> b) -> b -> Favorites a -> b)
-> (forall a. (a -> a -> a) -> Favorites a -> a)
-> (forall a. (a -> a -> a) -> Favorites a -> a)
-> (forall a. Favorites a -> [a])
-> (forall a. Favorites a -> Bool)
-> (forall a. Favorites a -> Int)
-> (forall a. Eq a => a -> Favorites a -> Bool)
-> (forall a. Ord a => Favorites a -> a)
-> (forall a. Ord a => Favorites a -> a)
-> (forall a. Num a => Favorites a -> a)
-> (forall a. Num a => Favorites a -> a)
-> Foldable Favorites
forall a. Eq a => a -> Favorites a -> Bool
forall a. Num a => Favorites a -> a
forall a. Ord a => Favorites a -> a
forall m. Monoid m => Favorites m -> m
forall a. Favorites a -> Bool
forall a. Favorites a -> Int
forall a. Favorites a -> [a]
forall a. (a -> a -> a) -> Favorites a -> a
forall m a. Monoid m => (a -> m) -> Favorites a -> m
forall b a. (b -> a -> b) -> b -> Favorites a -> b
forall a b. (a -> b -> b) -> b -> Favorites a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Favorites m -> m
fold :: forall m. Monoid m => Favorites m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Favorites a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Favorites a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Favorites a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Favorites a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Favorites a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Favorites a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Favorites a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Favorites a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Favorites a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Favorites a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Favorites a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Favorites a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Favorites a -> a
foldr1 :: forall a. (a -> a -> a) -> Favorites a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Favorites a -> a
foldl1 :: forall a. (a -> a -> a) -> Favorites a -> a
$ctoList :: forall a. Favorites a -> [a]
toList :: forall a. Favorites a -> [a]
$cnull :: forall a. Favorites a -> Bool
null :: forall a. Favorites a -> Bool
$clength :: forall a. Favorites a -> Int
length :: forall a. Favorites a -> Int
$celem :: forall a. Eq a => a -> Favorites a -> Bool
elem :: forall a. Eq a => a -> Favorites a -> Bool
$cmaximum :: forall a. Ord a => Favorites a -> a
maximum :: forall a. Ord a => Favorites a -> a
$cminimum :: forall a. Ord a => Favorites a -> a
minimum :: forall a. Ord a => Favorites a -> a
$csum :: forall a. Num a => Favorites a -> a
sum :: forall a. Num a => Favorites a -> a
$cproduct :: forall a. Num a => Favorites a -> a
product :: forall a. Num a => Favorites a -> a
Foldable, Int -> Favorites a -> ShowS
[Favorites a] -> ShowS
Favorites a -> String
(Int -> Favorites a -> ShowS)
-> (Favorites a -> String)
-> ([Favorites a] -> ShowS)
-> Show (Favorites a)
forall a. Show a => Int -> Favorites a -> ShowS
forall a. Show a => [Favorites a] -> ShowS
forall a. Show a => Favorites a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Favorites a -> ShowS
showsPrec :: Int -> Favorites a -> ShowS
$cshow :: forall a. Show a => Favorites a -> String
show :: Favorites a -> String
$cshowList :: forall a. Show a => [Favorites a] -> ShowS
showList :: [Favorites a] -> ShowS
Show, Favorites a
Favorites a -> Bool
Favorites a -> (Favorites a -> Bool) -> Null (Favorites a)
forall a. Favorites a
forall a. a -> (a -> Bool) -> Null a
forall a. Favorites a -> Bool
$cempty :: forall a. Favorites a
empty :: Favorites a
$cnull :: forall a. Favorites a -> Bool
null :: Favorites a -> Bool
Null, Singleton a)

-- | Equality checking is a bit expensive, since we need to sort!
--   Maybe use a 'Set' of favorites in the first place?
instance Ord a => Eq (Favorites a) where
  Favorites a
as == :: Favorites a -> Favorites a -> Bool
== Favorites a
bs = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList (Favorites a -> [a]
forall a. Favorites a -> [a]
toList Favorites a
as) Set a -> Set a -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList (Favorites a -> [a]
forall a. Favorites a -> [a]
toList Favorites a
bs)

-- | Result of comparing a candidate with the current favorites.
data CompareResult a
  = Dominates   { forall a. CompareResult a -> [a]
dominated :: [a], forall a. CompareResult a -> [a]
notDominated :: [a] }
    -- ^ Great, you are dominating a possibly (empty list of favorites)
    --   but there is also a rest that is not dominated.
    --   If @null dominated@, then @notDominated@ is necessarily the
    --   complete list of favorites.
  | IsDominated { forall a. CompareResult a -> a
dominator :: a }
    -- ^ Sorry, but you are dominated by that favorite.


-- | Gosh, got some pretty @a@ here, compare with my current favorites!
--   Discard it if there is already one that is better or equal.
--   (Skewed conservatively: faithful to the old favorites.)
--   If there is no match for it, add it, and
--   dispose of all that are worse than @a@.
--
--   We require a partial ordering.  Less is better! (Maybe paradoxically.)
compareWithFavorites :: PartialOrd a => a -> Favorites a -> CompareResult a
compareWithFavorites :: forall a. PartialOrd a => a -> Favorites a -> CompareResult a
compareWithFavorites a
a Favorites a
favs = [a] -> CompareResult a
loop ([a] -> CompareResult a) -> [a] -> CompareResult a
forall a b. (a -> b) -> a -> b
$ Favorites a -> [a]
forall a. Favorites a -> [a]
toList Favorites a
favs where
  loop :: [a] -> CompareResult a
loop []          = [a] -> [a] -> CompareResult a
forall a. [a] -> [a] -> CompareResult a
Dominates [] []
  loop as :: [a]
as@(a
b : [a]
bs) = case Comparable a
forall a. PartialOrd a => Comparable a
comparable a
a a
b of
    PartialOrdering
POLT -> a -> CompareResult a -> CompareResult a
forall {a}. a -> CompareResult a -> CompareResult a
dominates a
b (CompareResult a -> CompareResult a)
-> CompareResult a -> CompareResult a
forall a b. (a -> b) -> a -> b
$ [a] -> CompareResult a
loop [a]
bs  -- @a@ is a new favorite, bye-bye, @b@
    PartialOrdering
POLE -> a -> CompareResult a -> CompareResult a
forall {a}. a -> CompareResult a -> CompareResult a
dominates a
b (CompareResult a -> CompareResult a)
-> CompareResult a -> CompareResult a
forall a b. (a -> b) -> a -> b
$ [a] -> CompareResult a
loop [a]
bs  -- ditto
    PartialOrdering
POEQ -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b          -- @b@ is as least as good as @a@, bye-bye, @a@
    PartialOrdering
POGE -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b          -- ditto
    PartialOrdering
POGT -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b          -- ditto
    PartialOrdering
POAny -> a -> CompareResult a -> CompareResult a
forall {a}. a -> CompareResult a -> CompareResult a
doesnotd a
b (CompareResult a -> CompareResult a)
-> CompareResult a -> CompareResult a
forall a b. (a -> b) -> a -> b
$ [a] -> CompareResult a
loop [a]
bs -- don't know, compare with my other favorites
  -- add an outperformed favorite
  dominates :: a -> CompareResult a -> CompareResult a
dominates a
b (Dominates [a]
bs [a]
as) = [a] -> [a] -> CompareResult a
forall a. [a] -> [a] -> CompareResult a
Dominates (a
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
bs) [a]
as
  dominates a
b r :: CompareResult a
r@IsDominated{}   = CompareResult a
r
  -- add an uncomparable favorite
  doesnotd :: a -> CompareResult a -> CompareResult a
doesnotd  a
b (Dominates [a]
as [a]
bs) = [a] -> [a] -> CompareResult a
forall a. [a] -> [a] -> CompareResult a
Dominates [a]
as (a
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
bs)
  doesnotd  a
b r :: CompareResult a
r@IsDominated{}   = CompareResult a
r

-- | Compare a new set of favorites to an old one and discard
--   the new favorites that are dominated by the old ones
--   and vice verse.
--   (Skewed conservatively: faithful to the old favorites.)
--
--   @compareFavorites new old = (new', old')@
compareFavorites :: PartialOrd a => Favorites a -> Favorites a ->
                    (Favorites a, Favorites a)
compareFavorites :: forall a.
PartialOrd a =>
Favorites a -> Favorites a -> (Favorites a, Favorites a)
compareFavorites Favorites a
new Favorites a
old = ([a] -> Favorites a)
-> ([a], Favorites a) -> (Favorites a, Favorites a)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst [a] -> Favorites a
forall a. [a] -> Favorites a
Favorites (([a], Favorites a) -> (Favorites a, Favorites a))
-> ([a], Favorites a) -> (Favorites a, Favorites a)
forall a b. (a -> b) -> a -> b
$ [a] -> Favorites a -> ([a], Favorites a)
forall {a}.
PartialOrd a =>
[a] -> Favorites a -> ([a], Favorites a)
loop (Favorites a -> [a]
forall a. Favorites a -> [a]
toList Favorites a
new) Favorites a
old where
  loop :: [a] -> Favorites a -> ([a], Favorites a)
loop []        Favorites a
old = ([], Favorites a
old)
  loop (a
a : [a]
new) Favorites a
old = case a -> Favorites a -> CompareResult a
forall a. PartialOrd a => a -> Favorites a -> CompareResult a
compareWithFavorites a
a Favorites a
old of
    -- Better: Discard all @old@ ones that @a@ dominates and keep @a@
    Dominates [a]
_ [a]
old -> ([a] -> [a]) -> ([a], Favorites a) -> ([a], Favorites a)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (([a], Favorites a) -> ([a], Favorites a))
-> ([a], Favorites a) -> ([a], Favorites a)
forall a b. (a -> b) -> a -> b
$ [a] -> Favorites a -> ([a], Favorites a)
loop [a]
new ([a] -> Favorites a
forall a. [a] -> Favorites a
Favorites [a]
old)
    -- Not better:  Discard @a@
    IsDominated{}   -> [a] -> Favorites a -> ([a], Favorites a)
loop [a]
new Favorites a
old

unionCompared :: (Favorites a, Favorites a) -> Favorites a
unionCompared :: forall a. (Favorites a, Favorites a) -> Favorites a
unionCompared (Favorites [a]
new, Favorites [a]
old) = [a] -> Favorites a
forall a. [a] -> Favorites a
Favorites ([a] -> Favorites a) -> [a] -> Favorites a
forall a b. (a -> b) -> a -> b
$ [a]
new [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
old

-- | After comparing, do the actual insertion.
insertCompared :: a -> Favorites a -> CompareResult a -> Favorites a
insertCompared :: forall a. a -> Favorites a -> CompareResult a -> Favorites a
insertCompared a
a Favorites a
_ (Dominates [a]
_ [a]
as) = [a] -> Favorites a
forall a. [a] -> Favorites a
Favorites (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as)
insertCompared a
_ Favorites a
l IsDominated{}    = Favorites a
l

-- | Compare, then insert accordingly.
--   @insert a l = insertCompared a l (compareWithFavorites a l)@
insert :: PartialOrd a => a -> Favorites a -> Favorites a
insert :: forall a. PartialOrd a => a -> Favorites a -> Favorites a
insert a
a Favorites a
l = a -> Favorites a -> CompareResult a -> Favorites a
forall a. a -> Favorites a -> CompareResult a -> Favorites a
insertCompared a
a Favorites a
l (a -> Favorites a -> CompareResult a
forall a. PartialOrd a => a -> Favorites a -> CompareResult a
compareWithFavorites a
a Favorites a
l)

-- | Insert all the favorites from the first list into the second.
union :: PartialOrd a => Favorites a -> Favorites a -> Favorites a
union :: forall a. PartialOrd a => Favorites a -> Favorites a -> Favorites a
union (Favorites [a]
as) Favorites a
bs = (a -> Favorites a -> Favorites a)
-> Favorites a -> [a] -> Favorites a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr a -> Favorites a -> Favorites a
forall a. PartialOrd a => a -> Favorites a -> Favorites a
insert Favorites a
bs [a]
as

-- | Construct favorites from elements of a partial order.
--   The result depends on the order of the list if it
--   contains equal elements, since earlier seen elements
--   are favored over later seen equals.
--   The first element of the list is seen first.
fromList :: PartialOrd a => [a] -> Favorites a
fromList :: forall a. PartialOrd a => [a] -> Favorites a
fromList = (Favorites a -> a -> Favorites a)
-> Favorites a -> [a] -> Favorites a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' ((a -> Favorites a -> Favorites a)
-> Favorites a -> a -> Favorites a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Favorites a -> Favorites a
forall a. PartialOrd a => a -> Favorites a -> Favorites a
insert) Favorites a
forall a. Null a => a
empty

-- | 'Favorites' forms a 'Monoid' under 'empty' and 'union.
instance PartialOrd a => Semigroup (Favorites a) where
  <> :: Favorites a -> Favorites a -> Favorites a
(<>) = Favorites a -> Favorites a -> Favorites a
forall a. PartialOrd a => Favorites a -> Favorites a -> Favorites a
union
instance PartialOrd a => Monoid (Favorites a) where
  mempty :: Favorites a
mempty  = Favorites a
forall a. Null a => a
empty
  mappend :: Favorites a -> Favorites a -> Favorites a
mappend = Favorites a -> Favorites a -> Favorites a
forall a. Semigroup a => a -> a -> a
(<>)