    -- | Constructing singleton collections.

    module Agda.Utils.Singleton where

    import Data.Semigroup (Semigroup(..))
    import Data.Maybe
    import Data.Monoid (Endo(..))

    import Data.DList (DList)
    import qualified Data.DList as DL
    import Data.Hashable (Hashable)
    import Data.HashMap.Strict (HashMap)
    import qualified Data.HashMap.Strict as HashMap
    import Data.HashSet (HashSet)
    import qualified Data.HashSet as HashSet
    import Data.List.NonEmpty (NonEmpty(..))

    import Data.EnumMap (EnumMap)
    import qualified Data.EnumMap as EnumMap
    import Data.EnumSet (EnumSet)
    import qualified Data.EnumSet as EnumSet
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet

    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Sequence (Seq)
    import qualified Data.Sequence as Seq
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Set.NonEmpty (NESet)
    import qualified Data.Set.NonEmpty as Set1

    import Agda.Utils.Null     (Null, empty)
    import Agda.Utils.SmallSet (SmallSet, SmallSetElement)
    import qualified Agda.Utils.SmallSet as SmallSet

    -- | A create-only possibly empty collection is a monoid with the possibility
    --   to inject elements.

    class (Semigroup coll, Monoid coll, Singleton el coll) => Collection el coll
        | coll -> el where
      fromList :: [el] -> coll
      fromList = [coll] -> coll
    forall a. Monoid a => [a] -> a
    mconcat ([coll] -> coll) -> ([el] -> [coll]) -> [el] -> coll
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (el -> coll) -> [el] -> [coll]
    forall a b. (a -> b) -> [a] -> [b]
    map el -> coll
    forall el coll. Singleton el coll => el -> coll
    singleton

    instance Collection a        [a]          where fromList :: [a] -> [a]
    fromList = [a] -> [a]
    forall a. a -> a
    id
    instance Collection a        ([a] -> [a]) where fromList :: [a] -> [a] -> [a]
    fromList = [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    (++)
    instance Collection a        (Endo [a])   where fromList :: [a] -> Endo [a]
    fromList = ([a] -> [a]) -> Endo [a]
    forall a. (a -> a) -> Endo a
    Endo (([a] -> [a]) -> Endo [a])
    -> ([a] -> [a] -> [a]) -> [a] -> Endo [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [a] -> [a]
    forall el coll. Collection el coll => [el] -> coll
    fromList
    instance Collection a        (DList a)    where fromList :: [a] -> DList a
    fromList = [a] -> DList a
    forall a. [a] -> DList a
    DL.fromList
    instance Collection a        (Seq a)      where fromList :: [a] -> Seq a
    fromList = [a] -> Seq a
    forall a. [a] -> Seq a
    Seq.fromList
    instance Collection Int      IntSet       where fromList :: [Int] -> IntSet
    fromList = [Int] -> IntSet
    IntSet.fromList
    instance Collection (Int, a) (IntMap a)   where fromList :: [(Int, a)] -> IntMap a
    fromList = [(Int, a)] -> IntMap a
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList

    instance Enum k             => Collection k      (EnumSet k)   where fromList :: [k] -> EnumSet k
    fromList = [k] -> EnumSet k
    forall k. Enum k => [k] -> EnumSet k
    EnumSet.fromList
    instance Enum k             => Collection (k, a) (EnumMap k a) where fromList :: [(k, a)] -> EnumMap k a
    fromList = [(k, a)] -> EnumMap k a
    forall k a. Enum k => [(k, a)] -> EnumMap k a
    EnumMap.fromList
    instance (Eq k, Hashable k) => Collection k      (HashSet k)   where fromList :: [k] -> HashSet k
    fromList = [k] -> HashSet k
    forall k. (Eq k, Hashable k) => [k] -> HashSet k
    HashSet.fromList
    instance (Eq k, Hashable k) => Collection (k, a) (HashMap k a) where fromList :: [(k, a)] -> HashMap k a
    fromList = [(k, a)] -> HashMap k a
    forall k a. (Eq k, Hashable k) => [(k, a)] -> HashMap k a
    HashMap.fromList
    instance Ord k              => Collection k      (Set k)       where fromList :: [k] -> Set k
    fromList = [k] -> Set k
    forall k. Ord k => [k] -> Set k
    Set.fromList
    instance Ord k              => Collection (k, a) (Map k a)     where fromList :: [(k, a)] -> Map k a
    fromList = [(k, a)] -> Map k a
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
    instance SmallSetElement k  => Collection k      (SmallSet k)  where fromList :: [k] -> SmallSet k
    fromList = [k] -> SmallSet k
    forall k. SmallSetElement k => [k] -> SmallSet k
    SmallSet.fromList

    -- | Create-only collection with at most one element.

    class (Null coll, Singleton el coll) => CMaybe el coll | coll -> el where
      cMaybe :: Maybe el -> coll
      cMaybe = coll -> (el -> coll) -> Maybe el -> coll
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe coll
    forall a. Null a => a
    empty el -> coll
    forall el coll. Singleton el coll => el -> coll
    singleton

    instance CMaybe a (Maybe a) where cMaybe :: Maybe a -> Maybe a
    cMaybe = Maybe a -> Maybe a
    forall a. a -> a
    id
    instance CMaybe a [a]       where cMaybe :: Maybe a -> [a]
    cMaybe = Maybe a -> [a]
    forall a. Maybe a -> [a]
    maybeToList

    -- | Overloaded @singleton@ constructor for collections.

    class Singleton el coll | coll -> el where
      singleton :: el -> coll

    instance Singleton a   (Maybe a)    where singleton :: a -> Maybe a
    singleton = a -> Maybe a
    forall a. a -> Maybe a
    Just
    instance Singleton a   [a]          where singleton :: a -> [a]
    singleton = (a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[])
    instance Singleton a   ([a] -> [a]) where singleton :: a -> [a] -> [a]
    singleton = (:)
    instance Singleton a   (Endo [a])   where singleton :: a -> Endo [a]
    singleton = ([a] -> [a]) -> Endo [a]
    forall a. (a -> a) -> Endo a
    Endo (([a] -> [a]) -> Endo [a]) -> (a -> [a] -> [a]) -> a -> Endo [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (:)
    instance Singleton a   (DList a)    where singleton :: a -> DList a
    singleton = a -> DList a
    forall a. a -> DList a
    DL.singleton
    instance Singleton a   (NESet a)    where singleton :: a -> NESet a
    singleton = a -> NESet a
    forall a. a -> NESet a
    Set1.singleton
    instance Singleton a   (NonEmpty a) where singleton :: a -> NonEmpty a
    singleton = (a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [])
    instance Singleton a   (Seq a)      where singleton :: a -> Seq a
    singleton = a -> Seq a
    forall a. a -> Seq a
    Seq.singleton
    instance Singleton a   (Set a)      where singleton :: a -> Set a
    singleton = a -> Set a
    forall a. a -> Set a
    Set.singleton
    instance Singleton Int IntSet       where singleton :: Int -> IntSet
    singleton = Int -> IntSet
    IntSet.singleton

    instance Enum a            => Singleton a (EnumSet  a) where singleton :: a -> EnumSet a
    singleton = a -> EnumSet a
    forall a. Enum a => a -> EnumSet a
    EnumSet.singleton
    instance SmallSetElement a => Singleton a (SmallSet a) where singleton :: a -> SmallSet a
    singleton = a -> SmallSet a
    forall a. SmallSetElement a => a -> SmallSet a
    SmallSet.singleton

    instance Singleton (k  ,a) (Map  k a)                  where singleton :: (k, a) -> Map k a
    singleton = (k -> a -> Map k a) -> (k, a) -> Map k a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry k -> a -> Map k a
    forall k a. k -> a -> Map k a
    Map.singleton
    instance Singleton (Int,a) (IntMap a)                  where singleton :: (Int, a) -> IntMap a
    singleton = (Int -> a -> IntMap a) -> (Int, a) -> IntMap a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Int -> a -> IntMap a
    forall a. Int -> a -> IntMap a
    IntMap.singleton

    instance Hashable k => Singleton k     (HashSet   k)   where singleton :: k -> HashSet k
    singleton = k -> HashSet k
    forall k. Hashable k => k -> HashSet k
    HashSet.singleton
    instance Hashable k => Singleton (k,a) (HashMap k a)   where singleton :: (k, a) -> HashMap k a
    singleton = (k -> a -> HashMap k a) -> (k, a) -> HashMap k a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry k -> a -> HashMap k a
    forall k v. Hashable k => k -> v -> HashMap k v
    HashMap.singleton
    instance Enum k     => Singleton (k,a) (EnumMap k a)   where singleton :: (k, a) -> EnumMap k a
    singleton = (k -> a -> EnumMap k a) -> (k, a) -> EnumMap k a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry k -> a -> EnumMap k a
    forall k a. Enum k => k -> a -> EnumMap k a
    EnumMap.singleton

    -- Testing newtype-deriving:

    -- newtype Wrap c = Wrap c
    --   deriving (Singleton k)  -- Succeeds

    -- Type family version:

    -- class Singleton c where
    --   type Elem c
    --   singleton :: Elem c -> c

    -- instance Singleton [a] where
    --   type Elem [a] = a
    --   singleton = (:[])

    -- instance Singleton (Maybe a) where
    --   type Elem (Maybe a) = a
    --   singleton = Just

    -- instance Singleton (Set a) where
    --   type Elem (Set a) = a
    --   singleton = Set.singleton

    -- instance Singleton (Map k a) where
    --   type Elem (Map k a) = (k,a)
    --   singleton = uncurry Map.singleton

    -- newtype Wrap a = Wrap a
    --   deriving (Singleton)  -- Fails