{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS -fwarn-missing-signatures #-}

module Type.Set.Example where
    
import Data.Type.Equality
import Type.Logic
import Type.Set
import Type.Function
import Type.Dummies
import Data.Monoid
import Control.Monad
import Helper
import Control.Applicative
import qualified Data.Map as M

#define CXT\
                     (Fact (set :⊆: OrdType),\
                      Fact (set :⊆: TypeableType),\
                      Fact (set :⊆: EqType))

-- | A 'Map' whose keys are taken from any type which is a member of /set/
newtype SMap set a = SMap (M.Map (V set) a)
    

singleton :: CXT =>
            k :∈: set ->
            k -> a -> SMap set a
singleton p k v = SMap (M.singleton (V p k) v)

insert :: CXT =>
         k :∈: set -> 
         k -> a -> SMap set a -> SMap set a

insert p k v (SMap map) = SMap (M.insert (V p k) v map)

lookup :: CXT =>
         k :∈: set ->
         k -> SMap set a -> Maybe a

lookup p k (SMap map) = M.lookup (V p k) map
  
-- | Either 'Typeable' 'Integral's, or 'String's
type ExampleSet = (TypeableType :∩: IntegralType) :∪: (Singleton String)
                 
instance Fact (ExampleSet :⊆: TypeableType) where
    auto = unionMinimal interFst auto

instance Fact (ExampleSet :⊆: OrdType) where
    auto = unionMinimal (interSnd `subsetTrans` (Subset (\IntegralType -> OrdType))) auto

instance Fact (ExampleSet :⊆: EqType) where
    auto = auto `subsetTrans` (auto :: OrdType :⊆: EqType)

stringInExampleSet :: String :∈: ExampleSet
stringInExampleSet = Union (Right Refl)


intInExampleSet :: Int :∈: ExampleSet
intInExampleSet = Union (Left (Inter auto auto))


test :: SMap ExampleSet Integer
test = singleton stringInExampleSet "hi" 10