module Data.IdMap.Core.Fast
( module Data.Subtyping
, module Data.TypeInt
, module Control.Functor
, Id
, equalBy
, Map
, Set
, insert
, delete
, lookUp
, member
, union
, unsafeInsert
, unsafeEquivalent
, Sets (PlusSet)
, Maps (PlusMap)
, ICC, runICC
, ICCS, runICCS
, Maplike, MaplikeClass
) where
#ifdef __CHECK__
import Data.Control.Kvantum
#else
import Data.Control.Kvantum.Void
#endif
import Data.Array.Simple
import Data.Bits (setBit, clearBit, testBit)
import System.IO.Unsafe (unsafePerformIO)
import GHC.Base (Any)
import Data.Subtyping
import Data.TypeInt
import Control.Functor
import Unsafe.Coerce (unsafeCoerce)
newtype Id k
= Id (Array (Maybe Any))
instance Incl Id where
left = unsafeCoerce
right = unsafeCoerce
equalBy :: Maplike i k a -> Id k -> Id k -> Bool
equalBy !_ a b = a == b
instance Eq (Id a) where
Id a == Id b = a == b
type Map i k a
= Maplike (M i) k a
data M i
newtype Maplike i k a
= Maplike K
insert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> Maplike i k a
insert !(Id a) x (Maplike k) = unsafePerformIO $ do
k' <- renew "insert" k
set (undefined :: i) (Just x) a
return $ Maplike k'
delete :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maplike i k a
lookUp :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maybe a
lookUp (Id a) (Maplike k) = unsafePerformIO $ do
hit k
x <- get (undefined :: i) a
return x
member :: MaplikeClass i a => Id k -> Maplike i k a -> Bool
member i m = case lookUp i m of
Just _ -> True
_ -> False
unsafeInsert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> ()
unsafeInsert !(Id a) x !_ = unsafePerformIO $ do
set (undefined :: i) (Just x) a
return ()
infixr 2 `union`
union :: Maplike i k1 a -> Maplike i k2 a -> Maplike i (k1 :|: k2) a
unsafeEquivalent :: Maplike i k a -> Maplike i k a -> Maplike i k a
type Set i k
= Maplike (S Zero i) k ()
data S i j
infixr 2 `PlusSet`
data Sets i k where
PlusSet :: Set i k -> Sets i k -> Sets (Succ i) k
infixr 2 `PlusMap`
data Maps i k where
PlusMap :: (forall a . Map (Succ i) k a) -> Maps i k -> Maps (Succ i) k
type ICC i k a
= Maps i k
-> (forall b . Map Zero k b)
-> [Id k]
-> a
runICC :: I i => (forall k . ICC i k a) -> a
type ICCS i k a
= Maps i k
-> Sets I32 k
-> [Id k]
-> a
runICCS :: I i => (forall k . ICCS i k a) -> a
newId :: Int -> IO (Id k)
newId n = fmap Id $ newArray (n + 1) Nothing
newIdS :: Int -> IO (Id k)
newIdS n = fmap Id $ do
a <- newArray (n+1) Nothing
writeArray a 0 $ unsafeCoerce (0 :: Int)
return a
class MaplikeClass i x where
set :: i -> Maybe x -> Array (Maybe Any) -> IO ()
get :: i -> Array (Maybe Any) -> IO (Maybe x)
instance I i => MaplikeClass (M i) a where
set m x a = writeArray a (ind m) $ unsafeCoerce x
get m a = fmap unsafeCoerce $ readArray a (ind m)
instance (I i, I j) => MaplikeClass (S j i) () where
set m (Just _) a = do
z <- readArray' m a
writeArray' m a $ z `setBit` indS m
set m Nothing a = do
z <- readArray' m a
writeArray' m a $ z `clearBit` indS m
get m a = do
z <- readArray' m a
return $ if z `testBit` indS m then Just () else Nothing
delete !(Id a) (Maplike k) = unsafePerformIO $ do
k' <- renew "delete" k
set (undefined :: i) (Nothing :: Maybe a) a
return $ Maplike k'
ind :: forall i. I i => M i -> Int
ind _ = num (undefined :: i)
indS :: forall i j. I i => S j i -> Int
indS _ = num (undefined :: i)
readArray' :: forall i j. I i => S i j -> Array (Maybe Any) -> IO Int
readArray' _ a = fmap unsafeCoerce $ readArray a $ num (undefined :: i)
writeArray' :: forall i j. I i => S i j -> Array (Maybe Any) -> Int -> IO ()
writeArray' _ a i = writeArray a (num (undefined :: i)) $ unsafeCoerce i
union (Maplike k1) (Maplike k2) = unsafePerformIO $ do
k <- join k1 k2
return $ Maplike k
instance Functor (Maplike i k) where
fmap _ _ = error "fmap on Map"
instance Functor2 (Maplike i) where
fmap2 _ _ = error "fmap2 on Map"
unsafeEquivalent !_ b = b
runICC = runICC'
runICC' :: forall i a . I i => (forall k . ICC i k a) -> a
runICCS = runICCS'
runICCS' :: forall i a . I i => (forall k . ICCS i k a) -> a
#ifdef __CHECK__
runICC' f = f (maps_ f) (map0_ f) $ unsafeRepeat (newId (num (undefined :: i))) f
runICCS' f = f (maps_ f) (sets_ f) $ unsafeRepeat (newIdS (num (undefined :: i))) f
#else
runICC' f = f maps map0 $ unsafeRepeat (newId (num (undefined :: i))) f
runICCS' f = f maps sets $ unsafeRepeat (newIdS (num (undefined :: i))) f
#endif
map0 :: Map Zero k a
map0 = Maplike kk
maps :: Maps i k
maps = unsafeCoerce (Maplike kk `PlusMap` maps)
sets :: Sets i k
sets = unsafeCoerce (Maplike kk `PlusSet` sets)
kk :: K
kk = unsafePerformIO create
map0_ :: x -> Map I0 k a
map0_ a = unsafePerformIO $ do
k <- create
return $ unsafeCoerce (do_nothing a `seq` Maplike k)
maps_ :: a -> Maps i k
maps_ a = unsafePerformIO $ do
k <- create
return $ unsafeCoerce (Maplike k `PlusMap` maps_ (do_nothing a))
sets_ :: a -> Sets i k
sets_ a = unsafePerformIO $ do
k <- create
return $ unsafeCoerce (Maplike k `PlusSet` sets_ (do_nothing a))
unsafeRepeat :: IO x -> a -> [x]
unsafeRepeat f g = unsafePerformIO $ do
i <- f
return (i: unsafeRepeat f (do_nothing g))
do_nothing :: a -> a
do_nothing i = i