-- | Constructing singleton collections.

module Agda.Utils.Singleton where

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
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet

-- | 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
  {-# INLINE fromList #-}
instance Collection a        ([a] -> [a]) where
  fromList :: [a] -> [a] -> [a]
fromList = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
  {-# INLINE fromList #-}
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
  {-# INLINE fromList #-}
instance Collection a        (DList a)    where
  fromList :: [a] -> DList a
fromList = [a] -> DList a
forall a. [a] -> DList a
DL.fromList
  {-# INLINE fromList #-}
instance Collection a        (Seq a)      where
  fromList :: [a] -> Seq a
fromList = [a] -> Seq a
forall a. [a] -> Seq a
Seq.fromList
  {-# INLINE fromList #-}
instance Collection Int      IntSet       where
  fromList :: [Int] -> IntSet
fromList = [Int] -> IntSet
IntSet.fromList
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE singleton #-}
instance Singleton a   [a]          where
  singleton :: a -> [a]
singleton = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[])
  {-# INLINE singleton #-}
instance Singleton a   ([a] -> [a]) where
  singleton :: a -> [a] -> [a]
singleton = (:)
  {-# INLINE 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
. (:)
  {-# INLINE singleton #-}
instance Singleton a   (DList a)    where
  singleton :: a -> DList a
singleton = a -> DList a
forall a. a -> DList a
DL.singleton
  {-# INLINE singleton #-}
instance Singleton a   (NESet a)    where
  singleton :: a -> NESet a
singleton = a -> NESet a
forall a. a -> NESet a
Set1.singleton
  {-# INLINE singleton #-}
instance Singleton a   (NonEmpty a) where
  singleton :: a -> NonEmpty a
singleton = (a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [])
  {-# INLINE singleton #-}
instance Singleton a   (Seq a)      where
  singleton :: a -> Seq a
singleton = a -> Seq a
forall a. a -> Seq a
Seq.singleton
  {-# INLINE singleton #-}
instance Singleton a   (Set a)      where
  singleton :: a -> Set a
singleton = a -> Set a
forall a. a -> Set a
Set.singleton
  {-# INLINE singleton #-}
instance Singleton Int IntSet       where
  singleton :: Int -> IntSet
singleton = Int -> IntSet
IntSet.singleton
  {-# INLINE singleton #-}
instance Singleton Int VarSet       where
  singleton :: Int -> VarSet
singleton = Int -> VarSet
VarSet.singleton
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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
  {-# INLINE 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