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