module Data.Witness.WitnessDict where
{
import Data.Maybe;
import Data.Type.Equality;
import Data.Witness.Any;
;
newtype WitnessDict (w :: * -> *) = MkWitnessDict [Any w];
;
emptyWitnessDict :: WitnessDict w;
emptyWitnessDict = MkWitnessDict[];
;
witnessDictLookup :: (TestEquality w) => w a -> WitnessDict w -> Maybe a;
witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAny wit) cells);
;
witnessDictModify :: (TestEquality w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w;
witnessDictModify wit amap (MkWitnessDict cells) = MkWitnessDict
(replaceFirst ((fmap ((MkAny wit) . amap)) . (matchAny wit)) cells) where
{
replaceFirst :: (a -> Maybe a) -> [a] -> [a];
replaceFirst ama (a:aa) = case ama a of
{
Just newa -> (newa:aa);
_ -> a : (replaceFirst ama aa);
};
replaceFirst _ _ = [];
};
;
witnessDictReplace :: (TestEquality w) => w a -> a -> WitnessDict w -> WitnessDict w;
witnessDictReplace wit newa = witnessDictModify wit (const newa);
;
witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w;
witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAny wit a):cells);
;
witnessDictRemove :: (TestEquality w) => w a -> WitnessDict w -> WitnessDict w;
witnessDictRemove wit (MkWitnessDict cells) = MkWitnessDict
(removeFirst (\(MkAny cwit _) -> isJust (testEquality wit cwit)) cells) where
{
removeFirst :: (a -> Bool) -> [a] -> [a];
removeFirst p (a:as) | p a = as;
removeFirst p (a:as) = a : (removeFirst p as);
removeFirst _ _ = [];
};
;
witnessDictFromList :: [Any w] -> WitnessDict w;
witnessDictFromList = MkWitnessDict;
}