{-# LANGUAGE CPP #-}
module Agda.Utils.Favorites where
import Prelude hiding ( null )
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif
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
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
product :: forall a. Num a => Favorites a -> a
$cproduct :: forall a. Num a => Favorites a -> a
sum :: forall a. Num a => Favorites a -> a
$csum :: forall a. Num a => Favorites a -> a
minimum :: forall a. Ord a => Favorites a -> a
$cminimum :: forall a. Ord a => Favorites a -> a
maximum :: forall a. Ord a => Favorites a -> a
$cmaximum :: forall a. Ord a => Favorites a -> a
elem :: forall a. Eq a => a -> Favorites a -> Bool
$celem :: forall a. Eq a => a -> Favorites a -> Bool
length :: forall a. Favorites a -> Int
$clength :: forall a. Favorites a -> Int
null :: forall a. Favorites a -> Bool
$cnull :: forall a. Favorites a -> Bool
toList :: forall a. Favorites a -> [a]
$ctoList :: forall a. Favorites a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Favorites a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Favorites a -> a
foldr1 :: forall a. (a -> a -> a) -> Favorites a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Favorites a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> Favorites a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Favorites a -> m
fold :: forall m. Monoid m => Favorites m -> m
$cfold :: forall m. Monoid m => Favorites m -> m
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
showList :: [Favorites a] -> ShowS
$cshowList :: forall a. Show a => [Favorites a] -> ShowS
show :: Favorites a -> String
$cshow :: forall a. Show a => Favorites a -> String
showsPrec :: Int -> Favorites a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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
null :: Favorites a -> Bool
$cnull :: forall a. Favorites a -> Bool
empty :: Favorites a
$cempty :: forall a. Favorites a
Null, Singleton a)
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)
data CompareResult a
= Dominates { forall a. CompareResult a -> [a]
dominated :: [a], forall a. CompareResult a -> [a]
notDominated :: [a] }
| IsDominated { forall a. CompareResult a -> a
dominator :: a }
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
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
PartialOrdering
POEQ -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b
PartialOrdering
POGE -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b
PartialOrdering
POGT -> a -> CompareResult a
forall a. a -> CompareResult a
IsDominated a
b
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
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
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
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
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)
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
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
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)
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 (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
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 (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
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
(<>)