Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Favorites

Contents

Description

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

Synopsis

Documentation

newtype Favorites a Source

A list of incomparable favorites.

Constructors

Favorites 

Fields

toList :: [a]
 

Instances

Foldable Favorites Source 
Singleton a (Favorites a) Source 
Ord a => Eq (Favorites a) Source

Equality checking is a bit expensive, since we need to sort! Maybe use a Set of favorites in the first place?

Show a => Show (Favorites a) Source 
PartialOrd a => Monoid (Favorites a) Source

Favorites forms a Monoid under empty and 'union.

CoArbitrary a => CoArbitrary (Favorites a) Source 
(PartialOrd a, Arbitrary a) => Arbitrary (Favorites a) Source 
Null (Favorites a) Source 

data CompareResult a Source

Result of comparing a candidate with the current favorites.

Constructors

Dominates

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.

Fields

dominated :: [a]
 
notDominated :: [a]
 
IsDominated

Sorry, but you are dominated by that favorite.

Fields

dominator :: a
 

compareWithFavorites :: PartialOrd a => a -> Favorites a -> CompareResult a Source

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.)

compareFavorites :: PartialOrd a => Favorites a -> Favorites a -> (Favorites a, Favorites a) Source

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')

insertCompared :: a -> Favorites a -> CompareResult a -> Favorites a Source

After comparing, do the actual insertion.

insert :: PartialOrd a => a -> Favorites a -> Favorites a Source

Compare, then insert accordingly. insert a l = insertCompared a l (compareWithFavorites a l)

union :: PartialOrd a => Favorites a -> Favorites a -> Favorites a Source

Insert all the favorites from the first list into the second.

fromList :: PartialOrd a => [a] -> Favorites a Source

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.

Properties

prop_union_union2 :: Favorites ISet -> Favorites ISet -> Bool Source

A second way to compute the union is to use compareFavorites.

All tests

tests :: IO Bool Source

All tests as collected by quickCheckAll.

Using quickCheckAll is convenient and superior to the manual enumeration of tests, since the name of the property is added automatically.