module Data.Witness.WitnessFDict where
{
import Data.Maybe;
import Data.Type.Equality;
import Data.Witness.Any;
;
newtype WitnessFDict (w :: k -> *) (f :: k -> *) = MkWitnessFDict [AnyF w f];
;
emptyWitnessFDict :: WitnessFDict w f;
emptyWitnessFDict = MkWitnessFDict [];
;
witnessFDictLookup :: (TestEquality w) => w a -> WitnessFDict w f -> Maybe (f a);
witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells);
;
witnessFDictModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f;
witnessFDictModify wit amap (MkWitnessFDict cells) = MkWitnessFDict
(replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF 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 _ _ = [];
};
;
witnessFDictReplace :: (TestEquality w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa);
;
witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f;
witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa):cells);
;
witnessFDictRemove :: (TestEquality w) => w a -> WitnessFDict w f -> WitnessFDict w f;
witnessFDictRemove wit (MkWitnessFDict cells) = MkWitnessFDict
(removeFirst (\(MkAnyF 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 _ _ = [];
};
;
witnessFDictFromList :: (TestEquality w) => [AnyF w f] -> WitnessFDict w f;
witnessFDictFromList = MkWitnessFDict;
}