summaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Dependent/EnumMap/Strict/Internal.hs79
1 files changed, 49 insertions, 30 deletions
diff --git a/src/Data/Dependent/EnumMap/Strict/Internal.hs b/src/Data/Dependent/EnumMap/Strict/Internal.hs
index 00cc169..be18ae9 100644
--- a/src/Data/Dependent/EnumMap/Strict/Internal.hs
+++ b/src/Data/Dependent/EnumMap/Strict/Internal.hs
@@ -8,6 +8,7 @@
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
module Data.Dependent.EnumMap.Strict.Internal where
import Prelude hiding (lookup, map)
@@ -109,8 +110,8 @@ fromListWith :: (Enum1 k, TestEquality k)
fromListWith f (l :: [DSum k v]) =
DEnumMap (IM.fromListWithKey
(\i (KV inf1 v1) (KV inf2 v2) ->
- typeCheck2 (Proxy @k) i inf1 inf2 $
- KV inf1 (f v1 (coe1 v2)))
+ case typeCheck2 (Proxy @k) i inf1 inf2 of
+ Refl -> KV inf1 (f v1 v2))
(dSumToKV <$> l))
fromListWithKey :: (Enum1 k, TestEquality k)
@@ -120,7 +121,8 @@ fromListWithKey f l =
DEnumMap (IM.fromListWithKey
(\i (KV inf1 v1) (KV inf2 v2) ->
case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 v1 (coe1 v2)))
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 (f k1 v1 v2))
(dSumToKV <$> l))
-- ** From Ascending Lists
@@ -134,8 +136,8 @@ fromAscListWith :: (Enum1 k, TestEquality k)
fromAscListWith f (l :: [DSum k v]) =
DEnumMap (IM.fromAscListWithKey
(\i (KV inf1 v1) (KV inf2 v2) ->
- typeCheck2 (Proxy @k) i inf1 inf2 $
- KV inf1 (f v1 (coe1 v2)))
+ case typeCheck2 (Proxy @k) i inf1 inf2 of
+ Refl -> KV inf1 (f v1 v2))
(dSumToKV <$> l))
fromAscListWithKey :: (Enum1 k, TestEquality k)
@@ -145,7 +147,8 @@ fromAscListWithKey f l =
DEnumMap (IM.fromAscListWithKey
(\i (KV inf1 v1) (KV inf2 v2) ->
case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 v1 (coe1 v2)))
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 (f k1 v1 v2))
(dSumToKV <$> l))
fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v
@@ -169,7 +172,8 @@ insertWithKey :: (Enum1 k, TestEquality k)
insertWithKey f k v (DEnumMap m) =
let (i, inf) = fromEnum1 k
in DEnumMap (IM.insertWith
- (\_ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
+ (\_ (KV inf' v2) -> case typeCheck1 k i inf' of
+ Refl -> KV inf (f k v v2))
i (KV inf v) m)
insertLookupWithKey :: (Enum1 k, TestEquality k)
@@ -179,7 +183,8 @@ insertLookupWithKey f k v (DEnumMap m) =
let (i, inf) = fromEnum1 k
(!mx, !m') =
IM.insertLookupWithKey
- (\_ _ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
+ (\_ _ (KV inf' v2) -> case typeCheck1 k i inf' of
+ Refl -> KV inf (f k v v2))
i (KV inf v) m
-- Note: type checking unnecessary here, because by the BangPatterns,
-- evaluating mx evaluates dmap, and the IntMap is strict, so the lambda
@@ -200,7 +205,8 @@ adjust = adjustWithKey . const
adjustWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v
adjustWithKey f k (DEnumMap m) =
let (i, _) = fromEnum1 k
- in DEnumMap (IM.adjust (\(KV inf v) -> typeCheck1 k i inf $ KV (coe1 inf) (f k (coe1 v))) i m)
+ in DEnumMap (IM.adjust (\(KV inf v) -> case typeCheck1 k i inf of
+ Refl -> KV inf (f k v)) i m)
update :: (Enum1 k, TestEquality k) => (v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
update = updateWithKey . const
@@ -209,7 +215,8 @@ updateWithKey :: (Enum1 k, TestEquality k)
=> (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
updateWithKey f k (DEnumMap m) =
let (i, _) = fromEnum1 k
- in DEnumMap (IM.update (\(KV inf v) -> typeCheck1 k i inf $ KV (coe1 inf) <$> f k (coe1 v)) i m)
+ in DEnumMap (IM.update (\(KV inf v) -> case typeCheck1 k i inf of
+ Refl -> KV inf <$> f k v) i m)
updateLookupWithKey :: (Enum1 k, TestEquality k)
=> (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> (Maybe (v a), DEnumMap k v)
@@ -217,7 +224,8 @@ updateLookupWithKey f k (DEnumMap m) =
let (i, _) = fromEnum1 k
(!mx, !m') =
IM.updateLookupWithKey
- (\_ (KV inf v) -> typeCheck1 k i inf $ KV (coe1 inf) <$> f k (coe1 v))
+ (\_ (KV inf v) -> case typeCheck1 k i inf of
+ Refl -> KV inf <$> f k v)
i m
-- Note: type checking unnecessary here for the same reason as insertLookupWithKey
in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')
@@ -230,7 +238,8 @@ alter f k (DEnumMap m) = DEnumMap (IM.alter f' i m)
f' :: Maybe (KV k v) -> Maybe (KV k v)
f' Nothing = KV inf <$> f Nothing
- f' (Just (KV inf' v)) = typeCheck1 k i inf' $ KV inf <$> f (Just (coe1 v))
+ f' (Just (KV inf' v)) = case typeCheck1 k i inf' of
+ Refl -> KV inf <$> f (Just v)
alterF :: forall k v a f. (Functor f, Enum1 k, TestEquality k)
=> (Maybe (v a) -> f (Maybe (v a))) -> k a -> DEnumMap k v -> f (DEnumMap k v)
@@ -240,7 +249,8 @@ alterF f k (DEnumMap m) = DEnumMap <$> IM.alterF f' i m
f' :: Maybe (KV k v) -> f (Maybe (KV k v))
f' Nothing = fmap (KV inf) <$> f Nothing
- f' (Just (KV inf' v)) = typeCheck1 k i inf' $ fmap (KV inf) <$> f (Just (coe1 v))
+ f' (Just (KV inf' v)) = case typeCheck1 k i inf' of
+ Refl -> fmap (KV inf) <$> f (Just v)
-- * Query
-- ** Lookup
@@ -248,7 +258,8 @@ alterF f k (DEnumMap m) = DEnumMap <$> IM.alterF f' i m
lookup :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (v a)
lookup k (DEnumMap m) =
let (i, _) = fromEnum1 k
- in (\(KV inf v) -> typeCheck1 k i inf $ coe1 v) <$> IM.lookup i m
+ in (\(KV inf v) -> case typeCheck1 k i inf of
+ Refl -> v) <$> IM.lookup i m
(!?) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> Maybe (v a)
(!?) m k = lookup k m
@@ -257,7 +268,8 @@ findWithDefault :: (Enum1 k, TestEquality k) => v a -> k a -> DEnumMap k v -> v
findWithDefault def k (DEnumMap m) =
let (i, _) = fromEnum1 k
in case IM.findWithDefault (KV undefined def) i m of
- KV inf' v -> typeCheck1 k i inf' $ coe1 v
+ KV inf' v -> case typeCheck1 k i inf' of
+ Refl -> v
find :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> v a
find k = findWithDefault (error ("Data.Dependent.EnumMap.!: key " ++ show (fst (fromEnum1 k)) ++ " is not an element of the map")) k
@@ -297,7 +309,8 @@ unionWith :: (Enum1 k, TestEquality k)
unionWith f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)
where
f' :: Int -> KV k v -> KV k v -> KV k v
- f' i (KV inf1 v1) (KV inf2 v2) = typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 (f v1 (coe1 v2))
+ f' i (KV inf1 v1) (KV inf2 v2) = case typeCheck2 (Proxy @k) i inf1 inf2 of
+ Refl -> KV inf1 (f v1 v2)
unionWithKey :: (Enum1 k, TestEquality k)
=> (forall a. k a -> v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v
@@ -305,7 +318,8 @@ unionWithKey f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionW
where
f' :: Int -> KV k v -> KV k v -> KV k v
f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 v1 (coe1 v2))
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 (f k1 v1 v2)
unions :: (Foldable f, Enum1 k, TestEquality k) => f (DEnumMap k v) -> DEnumMap k v
unions = Foldable.foldl' union empty
@@ -328,7 +342,8 @@ differenceWith f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey f'
where
f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)
f' i (KV inf1 v1) (KV inf2 v2) =
- typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 <$> f v1 (coe1 v2)
+ case typeCheck2 (Proxy @k) i inf1 inf2 of
+ Refl -> KV inf1 <$> f v1 v2
differenceWithKey :: forall k v1 v2. (Enum1 k, TestEquality k)
=> (forall a. k a -> v1 a -> v2 a -> Maybe (v1 a)) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
@@ -336,7 +351,8 @@ differenceWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey
where
f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)
f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 v1 (coe1 v2)
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 <$> f k1 v1 v2
-- | Because the underlying maps are keyed on integers, it is possible to
-- subtract a map from another even if the key types differ. This function
@@ -367,7 +383,8 @@ intersectionWith f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWithKe
where
f' :: Int -> KV k v1 -> KV k v2 -> KV k v3
f' i (KV inf1 v1) (KV inf2 v2) =
- typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 $ f v1 (coe1 v2)
+ case typeCheck2 (Proxy @k) i inf1 inf2 of
+ Refl -> KV inf1 $ f v1 v2
intersectionWithKey :: forall k v1 v2 v3. (Enum1 k, TestEquality k)
=> (forall a. k a -> v1 a -> v2 a -> v3 a) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3
@@ -375,7 +392,8 @@ intersectionWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWit
where
f' :: Int -> KV k v1 -> KV k v2 -> KV k v3
f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 $ f k1 v1 (coe1 v2)
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 $ f k1 v1 v2
-- | Generalises 'intersectionWithKey' in the same way as 'differenceWithKey''
-- generalises 'differenceWithKey'.
@@ -386,7 +404,7 @@ intersectionWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWi
where
f' :: Int -> KV k1 v1 -> KV k2 v2 -> KV k1 v3
f' i (KV inf1 v1) (KV inf2 v2) = case (toEnum1 i inf1, toEnum1 i inf2) of
- (k1, k2) -> KV inf1 $ f k1 v1 k2 (coe1 v2)
+ (k1, k2) -> KV inf1 $ f k1 v1 k2 v2
-- ** Disjoint
@@ -411,7 +429,8 @@ mergeWithKey f g1 g2 (DEnumMap m1) (DEnumMap m2) =
where
f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v3)
f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
- k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 v1 (coe1 v2)
+ k1 -> case typeCheck1 k1 i inf2 of
+ Refl -> KV inf1 <$> f k1 v1 v2
-- * Traversal
-- ** Map
@@ -656,20 +675,20 @@ coe1 :: v a -> v b
coe1 = unsafeCoerce
typeCheck1 :: (Enum1 k, TestEquality k)
- => k a -> Int -> Enum1Info k b -> r -> r
-typeCheck1 k1 i inf2 x =
+ => k a -> Int -> Enum1Info k b -> k a :~: k b
+typeCheck1 k1 i inf2 =
assert (case toEnum1 i inf2 of { k2 ->
case testEquality k1 k2 of
Just Refl -> True
Nothing -> False })
- x
+ (unsafeCoerce Refl)
-typeCheck2 :: forall k proxy r a b. (Enum1 k, TestEquality k)
- => proxy k -> Int -> Enum1Info k a -> Enum1Info k b -> r -> r
-typeCheck2 _ i inf1 inf2 x =
+typeCheck2 :: forall k proxy a b. (Enum1 k, TestEquality k)
+ => proxy k -> Int -> Enum1Info k a -> Enum1Info k b -> k a :~: k b
+typeCheck2 _ i inf1 inf2 =
assert (case toEnum1 @k i inf1 of { k1 ->
case toEnum1 i inf2 of { k2 ->
case testEquality k1 k2 of
Just Refl -> True
Nothing -> False }})
- x
+ (unsafeCoerce Refl)
generated by cgit v1.2.3-70-g09d2 (git 2.51.2) at 2025-12-28 16:54:40 +0100