    {-# 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
    (<>)