{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall                       #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

{-|
Module      : Fcf.Data.Set
Description : Set data-structure for type-level programming
Copyright   : (c) gspia 2020-
License     : BSD
Maintainer  : gspia

= Fcf.Data.Set

Set provides an interface which is similar to the that given by the
container-package. If a method is missing here that you need, please do open
up an issue or better, make a PR.

Many of the examples are from containers-package. The internal representation
is based on lists. We hope that a more efficient one will be used one day.

-}


--------------------------------------------------------------------------------

module Fcf.Data.Set where

import qualified GHC.TypeLits as TL

import           Fcf ( Eval, Exp, type (=<<), type (<=<)
                     , Not, If
                     , TyEq, Length)
-- import           Fcf.Data.List as Fcf
import qualified Fcf as Fcf (Foldr, Filter)
import           Fcf.Data.List (Elem)

--------------------------------------------------------------------------------

-- For the doctests:

-- $setup
-- >>> import qualified GHC.TypeLits as TL
-- >>> import           Fcf.Data.Nat

--------------------------------------------------------------------------------

-- | Set-definition.
data Set a = Set [a]

-- | Empty
-- 
-- __Example__
-- 
-- >>> :kind! (Eval Empty :: Set Nat)
-- (Eval Empty :: Set Nat) :: Set Nat
-- = 'Set '[]
--
-- See also the other examples in this module.
data Empty :: Exp (Set v)
type instance Eval Empty = 'Set '[]

-- | Singleton
-- 
-- __Example__
-- 
-- >>> :kind! Eval (Singleton 1)
-- Eval (Singleton 1) :: Set Nat
-- = 'Set '[1]
data Singleton :: v -> Exp (Set v)
type instance Eval (Singleton v) = 'Set '[v]

-- | Use FromList to construct a Set from type-level list.
--
-- __Example__
-- 
-- >>> :kind! Eval (FromList '[1, 2])
-- Eval (FromList '[1, 2]) :: Set Nat
-- = 'Set '[1, 2]
data FromList :: [v] -> Exp (Set v)
type instance Eval (FromList lst) = 'Set lst


-- | Insert
--
-- __Example__
--
-- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])
-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set Nat
-- = 'Set '[3, 1, 2]
--
-- >>> :kind! Eval (Insert 2 =<< FromList '[1, 2])
-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set Nat
-- = 'Set '[1, 2]
data Insert :: v -> Set v -> Exp (Set v)
type instance Eval (Insert v ('Set lst)) =
    If (Eval (Elem v lst))
        ('Set lst)
        ('Set (v ': lst))

-- | Delete
-- 
-- __Example__
-- 
-- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])
-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set Nat
-- = 'Set '[3]
--
-- >>> :kind! Eval (Delete 7 =<< FromList '[5, 3])
-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set Nat
-- = 'Set '[5, 3]
data Delete :: v -> Set v -> Exp (Set v)
type instance Eval (Delete v ('Set lst)) =
    'Set (Eval (Fcf.Filter (Not <=< TyEq v) lst))

-- | Member
--
-- __Example__
-- 
-- >>> :kind! Eval (Member 5 =<< FromList '[5, 3])
-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool
-- = 'True
-- >>> :kind! Eval (Member 7 =<< FromList '[5, 3])
-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool
-- = 'False
data Member :: v -> Set v -> Exp Bool
type instance Eval (Member v ('Set lst)) = Eval (Elem v lst)

-- | NotMember
--
-- __Example__
-- 
-- >>> :kind! Eval (NotMember 5 =<< FromList '[5, 3])
-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool
-- = 'False
-- >>> :kind! Eval (NotMember 7 =<< FromList '[5, 3])
-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool
-- = 'True
data NotMember :: v -> Set v -> Exp Bool
type instance Eval (NotMember k ('Set lst)) =
    Eval (Not =<< Elem k lst)

-- | Null
--
-- __Example__
-- 
-- >>> :kind! Eval (Null =<< FromList '[5, 3])
-- Eval (Null =<< FromList '[5, 3]) :: Bool
-- = 'False
-- >>> :kind! Eval (Null =<< Empty)
-- Eval (Null =<< Empty) :: Bool
-- = 'True
data Null :: Set v -> Exp Bool
type instance Eval (Null ('Set '[])) = 'True
type instance Eval (Null ('Set (_ ': _))) = 'False

-- | Size
--
-- __Example__
-- 
-- >>> :kind! Eval (Size =<< FromList '[5, 3])
-- Eval (Size =<< FromList '[5, 3]) :: Nat
-- = 2
data Size :: Set v -> Exp TL.Nat
type instance Eval (Size ('Set lst)) = Eval (Length lst)

-- | Union
--
-- __Example__
-- 
-- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set 
--                                                                        Nat
-- = 'Set '[7, 5, 3]
data Union :: Set v -> Set v -> Exp (Set v)
type instance Eval (Union ('Set lst1) ('Set lst2)) =
    'Set (Eval (Fcf.Foldr UComb lst1 lst2))

data UComb :: v -> [v] -> Exp [v]
type instance Eval (UComb v lst) =
    If (Eval (Elem v lst))
        lst
        (v ': lst)


-- | Difference
-- 
-- __Example__
-- 
-- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set 
--                                                                            Nat
-- = 'Set '[3]
data Difference :: Set v -> Set v -> Exp (Set v)
type instance Eval (Difference ('Set lst1) ('Set lst2)) =
    'Set (Eval (Fcf.Filter (DiffNotMem lst2) lst1))

-- helper
data DiffNotMem :: [v] -> v -> Exp Bool
type instance Eval (DiffNotMem lst v) = Eval (Not =<< Elem v lst)


-- | Intersection
--
-- __Example__
-- 
-- >>> :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set 
--                                                                              Nat
-- = 'Set '[5]
data Intersection :: Set v -> Set v -> Exp (Set v)
type instance Eval (Intersection ('Set lst1) ('Set lst2)) =
    'Set (Eval (Fcf.Filter (InterMem lst2) lst1))

-- helper
data InterMem :: [v ]-> v -> Exp Bool
type instance Eval (InterMem lst v) = Eval (Elem v lst)