{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.HashMap.Common.Refined where

import           Control.Monad.Reader
import           Control.DeepSeq
import           Data.Coerce
import           Data.Constraint (Dict(..))
import           Data.Container.Refined.Hashable
import           Data.Container.Refined.Proofs
import           Data.Container.Refined.Unsafe
import           Data.Distributive
import           Data.Foldable.WithIndex
import           Data.Functor.Rep
import           Data.Functor.WithIndex
import qualified Data.Hashable as Hashable
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashMap.Strict as HashMapStrict
import qualified Data.HashSet as HashSet
import           Data.Proxy
import           Data.Reflection
import           Data.Traversable.WithIndex
import           Data.Type.Coercion
import           Data.Type.Equality ((:~:)(..))
import           Refined
import           Refined.Unsafe
import           Unsafe.Coerce

#if MIN_VERSION_unordered_containers(0, 2, 12)
#else
import           Data.Monoid (All(..))
#endif


-- | A wrapper around a regular 'Data.HashMap.HashMap' with a type parameter @s@
-- identifying the set of keys present in the map.
--
-- A key of type @k@ may not be present in the map, but a @'Key' s k@ is
-- guaranteed to be present (if the @s@ parameters match). Thus the map is
-- isomorphic to a (total) function @'Key' s k -> a@, which motivates many of
-- the instances below.
--
-- A 'HashMap' always knows its set of keys, so given @'HashMap' s k a@ we can
-- always derive @'KnownHashSet' s k@ by pattern matching on the 'Dict' returned
-- by 'keysSet'.
newtype HashMap s k a = HashMap (HashMap.HashMap k a)
  deriving newtype (HashMap s k a -> HashMap s k a -> Bool
(HashMap s k a -> HashMap s k a -> Bool)
-> (HashMap s k a -> HashMap s k a -> Bool) -> Eq (HashMap s k a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s k a.
(Eq k, Eq a) =>
HashMap s k a -> HashMap s k a -> Bool
$c== :: forall s k a.
(Eq k, Eq a) =>
HashMap s k a -> HashMap s k a -> Bool
== :: HashMap s k a -> HashMap s k a -> Bool
$c/= :: forall s k a.
(Eq k, Eq a) =>
HashMap s k a -> HashMap s k a -> Bool
/= :: HashMap s k a -> HashMap s k a -> Bool
Eq, Eq (HashMap s k a)
Eq (HashMap s k a) =>
(HashMap s k a -> HashMap s k a -> Ordering)
-> (HashMap s k a -> HashMap s k a -> Bool)
-> (HashMap s k a -> HashMap s k a -> Bool)
-> (HashMap s k a -> HashMap s k a -> Bool)
-> (HashMap s k a -> HashMap s k a -> Bool)
-> (HashMap s k a -> HashMap s k a -> HashMap s k a)
-> (HashMap s k a -> HashMap s k a -> HashMap s k a)
-> Ord (HashMap s k a)
HashMap s k a -> HashMap s k a -> Bool
HashMap s k a -> HashMap s k a -> Ordering
HashMap s k a -> HashMap s k a -> HashMap s k a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s k a. (Ord k, Ord a) => Eq (HashMap s k a)
forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Bool
forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Ordering
forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> HashMap s k a
$ccompare :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Ordering
compare :: HashMap s k a -> HashMap s k a -> Ordering
$c< :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Bool
< :: HashMap s k a -> HashMap s k a -> Bool
$c<= :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Bool
<= :: HashMap s k a -> HashMap s k a -> Bool
$c> :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Bool
> :: HashMap s k a -> HashMap s k a -> Bool
$c>= :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> Bool
>= :: HashMap s k a -> HashMap s k a -> Bool
$cmax :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> HashMap s k a
max :: HashMap s k a -> HashMap s k a -> HashMap s k a
$cmin :: forall s k a.
(Ord k, Ord a) =>
HashMap s k a -> HashMap s k a -> HashMap s k a
min :: HashMap s k a -> HashMap s k a -> HashMap s k a
Ord, Int -> HashMap s k a -> ShowS
[HashMap s k a] -> ShowS
HashMap s k a -> String
(Int -> HashMap s k a -> ShowS)
-> (HashMap s k a -> String)
-> ([HashMap s k a] -> ShowS)
-> Show (HashMap s k a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s k a. (Show k, Show a) => Int -> HashMap s k a -> ShowS
forall s k a. (Show k, Show a) => [HashMap s k a] -> ShowS
forall s k a. (Show k, Show a) => HashMap s k a -> String
$cshowsPrec :: forall s k a. (Show k, Show a) => Int -> HashMap s k a -> ShowS
showsPrec :: Int -> HashMap s k a -> ShowS
$cshow :: forall s k a. (Show k, Show a) => HashMap s k a -> String
show :: HashMap s k a -> String
$cshowList :: forall s k a. (Show k, Show a) => [HashMap s k a] -> ShowS
showList :: [HashMap s k a] -> ShowS
Show, (forall a b. (a -> b) -> HashMap s k a -> HashMap s k b)
-> (forall a b. a -> HashMap s k b -> HashMap s k a)
-> Functor (HashMap s k)
forall a b. a -> HashMap s k b -> HashMap s k a
forall a b. (a -> b) -> HashMap s k a -> HashMap s k b
forall s k a b. a -> HashMap s k b -> HashMap s k a
forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b
fmap :: forall a b. (a -> b) -> HashMap s k a -> HashMap s k b
$c<$ :: forall s k a b. a -> HashMap s k b -> HashMap s k a
<$ :: forall a b. a -> HashMap s k b -> HashMap s k a
Functor, (forall m. Monoid m => HashMap s k m -> m)
-> (forall m a. Monoid m => (a -> m) -> HashMap s k a -> m)
-> (forall m a. Monoid m => (a -> m) -> HashMap s k a -> m)
-> (forall a b. (a -> b -> b) -> b -> HashMap s k a -> b)
-> (forall a b. (a -> b -> b) -> b -> HashMap s k a -> b)
-> (forall b a. (b -> a -> b) -> b -> HashMap s k a -> b)
-> (forall b a. (b -> a -> b) -> b -> HashMap s k a -> b)
-> (forall a. (a -> a -> a) -> HashMap s k a -> a)
-> (forall a. (a -> a -> a) -> HashMap s k a -> a)
-> (forall a. HashMap s k a -> [a])
-> (forall a. HashMap s k a -> Bool)
-> (forall a. HashMap s k a -> Int)
-> (forall a. Eq a => a -> HashMap s k a -> Bool)
-> (forall a. Ord a => HashMap s k a -> a)
-> (forall a. Ord a => HashMap s k a -> a)
-> (forall a. Num a => HashMap s k a -> a)
-> (forall a. Num a => HashMap s k a -> a)
-> Foldable (HashMap s k)
forall a. Eq a => a -> HashMap s k a -> Bool
forall a. Num a => HashMap s k a -> a
forall a. Ord a => HashMap s k a -> a
forall m. Monoid m => HashMap s k m -> m
forall a. HashMap s k a -> Bool
forall a. HashMap s k a -> Int
forall a. HashMap s k a -> [a]
forall a. (a -> a -> a) -> HashMap s k a -> a
forall m a. Monoid m => (a -> m) -> HashMap s k a -> m
forall b a. (b -> a -> b) -> b -> HashMap s k a -> b
forall a b. (a -> b -> b) -> b -> HashMap s k a -> b
forall s k a. Eq a => a -> HashMap s k a -> Bool
forall s k a. Num a => HashMap s k a -> a
forall s k a. Ord a => HashMap s k a -> a
forall s k m. Monoid m => HashMap s k m -> m
forall s k a. HashMap s k a -> Bool
forall s k a. HashMap s k a -> Int
forall s k a. HashMap s k a -> [a]
forall s k a. (a -> a -> a) -> HashMap s k a -> a
forall s k m a. Monoid m => (a -> m) -> HashMap s k a -> m
forall s k b a. (b -> a -> b) -> b -> HashMap s k a -> b
forall s k a b. (a -> b -> b) -> b -> HashMap s k a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall s k m. Monoid m => HashMap s k m -> m
fold :: forall m. Monoid m => HashMap s k m -> m
$cfoldMap :: forall s k m a. Monoid m => (a -> m) -> HashMap s k a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> HashMap s k a -> m
$cfoldMap' :: forall s k m a. Monoid m => (a -> m) -> HashMap s k a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> HashMap s k a -> m
$cfoldr :: forall s k a b. (a -> b -> b) -> b -> HashMap s k a -> b
foldr :: forall a b. (a -> b -> b) -> b -> HashMap s k a -> b
$cfoldr' :: forall s k a b. (a -> b -> b) -> b -> HashMap s k a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> HashMap s k a -> b
$cfoldl :: forall s k b a. (b -> a -> b) -> b -> HashMap s k a -> b
foldl :: forall b a. (b -> a -> b) -> b -> HashMap s k a -> b
$cfoldl' :: forall s k b a. (b -> a -> b) -> b -> HashMap s k a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> HashMap s k a -> b
$cfoldr1 :: forall s k a. (a -> a -> a) -> HashMap s k a -> a
foldr1 :: forall a. (a -> a -> a) -> HashMap s k a -> a
$cfoldl1 :: forall s k a. (a -> a -> a) -> HashMap s k a -> a
foldl1 :: forall a. (a -> a -> a) -> HashMap s k a -> a
$ctoList :: forall s k a. HashMap s k a -> [a]
toList :: forall a. HashMap s k a -> [a]
$cnull :: forall s k a. HashMap s k a -> Bool
null :: forall a. HashMap s k a -> Bool
$clength :: forall s k a. HashMap s k a -> Int
length :: forall a. HashMap s k a -> Int
$celem :: forall s k a. Eq a => a -> HashMap s k a -> Bool
elem :: forall a. Eq a => a -> HashMap s k a -> Bool
$cmaximum :: forall s k a. Ord a => HashMap s k a -> a
maximum :: forall a. Ord a => HashMap s k a -> a
$cminimum :: forall s k a. Ord a => HashMap s k a -> a
minimum :: forall a. Ord a => HashMap s k a -> a
$csum :: forall s k a. Num a => HashMap s k a -> a
sum :: forall a. Num a => HashMap s k a -> a
$cproduct :: forall s k a. Num a => HashMap s k a -> a
product :: forall a. Num a => HashMap s k a -> a
Foldable, Eq (HashMap s k a)
Eq (HashMap s k a) =>
(Int -> HashMap s k a -> Int)
-> (HashMap s k a -> Int) -> Hashable (HashMap s k a)
Int -> HashMap s k a -> Int
HashMap s k a -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall s k a. (Hashable k, Hashable a) => Eq (HashMap s k a)
forall s k a.
(Hashable k, Hashable a) =>
Int -> HashMap s k a -> Int
forall s k a. (Hashable k, Hashable a) => HashMap s k a -> Int
$chashWithSalt :: forall s k a.
(Hashable k, Hashable a) =>
Int -> HashMap s k a -> Int
hashWithSalt :: Int -> HashMap s k a -> Int
$chash :: forall s k a. (Hashable k, Hashable a) => HashMap s k a -> Int
hash :: HashMap s k a -> Int
Hashable.Hashable, HashMap s k a -> ()
(HashMap s k a -> ()) -> NFData (HashMap s k a)
forall a. (a -> ()) -> NFData a
forall s k a. (NFData k, NFData a) => HashMap s k a -> ()
$crnf :: forall s k a. (NFData k, NFData a) => HashMap s k a -> ()
rnf :: HashMap s k a -> ()
NFData)
  deriving stock (Functor (HashMap s k)
Foldable (HashMap s k)
(Functor (HashMap s k), Foldable (HashMap s k)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> HashMap s k a -> f (HashMap s k b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    HashMap s k (f a) -> f (HashMap s k a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HashMap s k a -> m (HashMap s k b))
-> (forall (m :: * -> *) a.
    Monad m =>
    HashMap s k (m a) -> m (HashMap s k a))
-> Traversable (HashMap s k)
forall s k. Functor (HashMap s k)
forall s k. Foldable (HashMap s k)
forall s k (m :: * -> *) a.
Monad m =>
HashMap s k (m a) -> m (HashMap s k a)
forall s k (f :: * -> *) a.
Applicative f =>
HashMap s k (f a) -> f (HashMap s k a)
forall s k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap s k a -> m (HashMap s k b)
forall s k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap s k a -> f (HashMap s k b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
HashMap s k (m a) -> m (HashMap s k a)
forall (f :: * -> *) a.
Applicative f =>
HashMap s k (f a) -> f (HashMap s k a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap s k a -> m (HashMap s k b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap s k a -> f (HashMap s k b)
$ctraverse :: forall s k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap s k a -> f (HashMap s k b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap s k a -> f (HashMap s k b)
$csequenceA :: forall s k (f :: * -> *) a.
Applicative f =>
HashMap s k (f a) -> f (HashMap s k a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
HashMap s k (f a) -> f (HashMap s k a)
$cmapM :: forall s k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap s k a -> m (HashMap s k b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap s k a -> m (HashMap s k b)
$csequence :: forall s k (m :: * -> *) a.
Monad m =>
HashMap s k (m a) -> m (HashMap s k a)
sequence :: forall (m :: * -> *) a.
Monad m =>
HashMap s k (m a) -> m (HashMap s k a)
Traversable)
type role HashMap nominal nominal representational

-- | Convert to a regular 'Data.HashMap.HashMap', forgetting its set of keys.
toMap :: forall s k a. HashMap s k a -> HashMap.HashMap k a
toMap :: forall s k a. HashMap s k a -> HashMap k a
toMap (HashMap HashMap k a
m) = HashMap k a
m

-- | @'Key' s k@ is a key of type @k@ that has been verified to be an element
-- of the set @s@, and thus verified to be present in all @'HashMap' s k@ maps.
--
-- Thus, @'Key' s k@ is a \"refinement\" type of @k@, and this library
-- integrates with an implementation of refimenement types in "Refined", so
-- the machinery from there can be used to manipulate 'Key's (however see
-- 'Data.Set.Refined.revealPredicate').
--
-- The underlying @k@ value can be obtained with 'unrefine'. A @k@ can be
-- validated into an @'Key' s k@ with 'member'.
type Key s = Refined (InSet 'Hashed s)

unsafeCastKey :: forall s k. Coercion k (Key s k)
unsafeCastKey :: forall s k. Coercion k (Key s k)
unsafeCastKey = Coercion k (Refined (InSet 'Hashed s) k)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined

unsafeKey :: k -> Key s k
unsafeKey :: forall k s. k -> Key s k
unsafeKey = Coercion k (Key s k) -> k -> Key s k
forall a b. Coercion a b -> a -> b
coerceWith Coercion k (Key s k)
forall s k. Coercion k (Key s k)
unsafeCastKey

-- | An existential wrapper for a 'HashMap' with an as-yet-unknown set of keys.
-- Pattern maching on it gives you a way to refer to the set (the parameter
-- @s@), e.g.
--
-- @
-- case 'fromHashMap' ... of
--   'SomeHashMap' \@s m -> doSomethingWith \@s
--
-- case 'fromHashMap' ... of
--   'SomeHashMap' (m :: 'HashMap' s k a) -> doSomethingWith \@s
-- @
data SomeHashMap k a where
  SomeHashMap :: forall s k a. !(HashMap s k a) -> SomeHashMap k a

-- | Apply a map with an unknown set of keys to a continuation that can accept
-- a map with any set of keys. This gives you a way to refer to the set (the
-- parameter @s@), e.g.:
--
-- @
-- 'withHashMap' ('fromHashMap' ...
--   $ \(m :: 'HashMap' s k a) -> doSomethingWith \@s
-- @
withHashMap
  :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r
withHashMap :: forall k a r.
SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r
withHashMap (SomeHashMap HashMap s k a
m) forall s. HashMap s k a -> r
k = HashMap s k a -> r
forall s. HashMap s k a -> r
k HashMap s k a
m

-- | Construct a map from a regular 'Data.HashMap.Lazy.HashMap'.
fromHashMap :: forall k a. HashMap.HashMap k a -> SomeHashMap k a
fromHashMap :: forall k a. HashMap k a -> SomeHashMap k a
fromHashMap HashMap k a
m = HashMap Any k a -> SomeHashMap k a
forall s k a. HashMap s k a -> SomeHashMap k a
SomeHashMap (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap HashMap k a
m)

-- | An existential wrapper for a 'HashMap' with an as-yet-unknown set of keys,
-- together with a proof of some fact @p@ about the set. Pattern matching on it
-- gives you a way to refer to the set (the parameter @s@). Functions that
-- change the set of keys in a map will return the map in this way, together
-- with a proof that somehow relates the keys set to the function's inputs.
data SomeHashMapWith p k a where
  SomeHashMapWith
    :: forall s k a p. !(HashMap s k a) -> !(p s) -> SomeHashMapWith p k a

-- | Apply a map with proof for an unknown set of keys to a continuation that
-- can accept a map with any set of keys satisfying the proof. This gives you a
-- way to refer to the set (the parameter @s@).
withHashMapWith
  :: forall k a r p. SomeHashMapWith p k a
  -> (forall s. HashMap s k a -> p s -> r)
  -> r
withHashMapWith :: forall k a r (p :: * -> *).
SomeHashMapWith p k a -> (forall s. HashMap s k a -> p s -> r) -> r
withHashMapWith (SomeHashMapWith HashMap s k a
m p s
p) forall s. HashMap s k a -> p s -> r
k = HashMap s k a -> p s -> r
forall s. HashMap s k a -> p s -> r
k HashMap s k a
m p s
p

-- | An existential wrapper for a pair of maps with as-yet-unknown sets of keys,
-- together with a proof of some fact @p@ relating them.
data Some2HashMapWith p k a b where
  Some2HashMapWith
    :: forall s t k a b p. !(HashMap s k a)
    -> !(HashMap t k b)
    -> !(p s t)
    -> Some2HashMapWith p k a b

-- | Apply a pair of maps with proof for unknown sets of keys to a continuation
-- that can accept any pair of maps with any sets of keys satisfying the proof.
-- This gives you a way to refer to the sets (the parameters @s@ and @t@).
with2HashMapWith
  :: forall k a b r p. Some2HashMapWith p k a b
  -> (forall s t. HashMap s k a -> HashMap t k b -> p s t -> r)
  -> r
with2HashMapWith :: forall k a b r (p :: * -> * -> *).
Some2HashMapWith p k a b
-> (forall s t. HashMap s k a -> HashMap t k b -> p s t -> r) -> r
with2HashMapWith (Some2HashMapWith HashMap s k a
m1 HashMap t k b
m2 p s t
p) forall s t. HashMap s k a -> HashMap t k b -> p s t -> r
k = HashMap s k a -> HashMap t k b -> p s t -> r
forall s t. HashMap s k a -> HashMap t k b -> p s t -> r
k HashMap s k a
m1 HashMap t k b
m2 p s t
p

-- | An empty map.
empty :: forall k a. SomeHashMapWith (EmptyProof 'Hashed) k a
empty :: forall k a. SomeHashMapWith (EmptyProof 'Hashed) k a
empty = HashMap Any k a
-> EmptyProof 'Hashed Any
-> SomeHashMapWith (EmptyProof 'Hashed) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap HashMap k a
forall k v. HashMap k v
HashMap.empty) (EmptyProof 'Hashed Any
 -> SomeHashMapWith (EmptyProof 'Hashed) k a)
-> EmptyProof 'Hashed Any
-> SomeHashMapWith (EmptyProof 'Hashed) k a
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Hashed Any :-> InSet 'Hashed s)
-> EmptyProof 'Hashed Any
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Hashed Any) x -> Refined (InSet 'Hashed s) x
forall s. InSet 'Hashed Any :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Create a map from a set of keys, and a function that for each key computes
-- the corresponding value.
fromSet :: forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet :: forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet Key s k -> a
f = HashMap k a -> HashMap s k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap s k a) -> HashMap k a -> HashMap s k a
forall a b. (a -> b) -> a -> b
$ (k -> () -> a) -> HashMap k () -> HashMap k a
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapWithKey (\k
k ()
_ -> Key s k -> a
f (Key s k -> a) -> Key s k -> a
forall a b. (a -> b) -> a -> b
$ k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k)
  (HashMap k () -> HashMap k a) -> HashMap k () -> HashMap k a
forall a b. (a -> b) -> a -> b
$ HashSet k -> HashMap k ()
forall a. HashSet a -> HashMap a ()
HashSet.toMap (Proxy s -> HashSet k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet k
reflect (Proxy s -> HashSet k) -> Proxy s -> HashSet k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)

-- | Delete a key and its value from the map if present, returning a potentially
-- smaller map.
delete
  :: forall s k a. Hashable k
  => k -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a
delete :: forall s k a.
Hashable k =>
k -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a
delete k
k (HashMap HashMap k a
m) = HashMap Any k a
-> SupersetProof 'Hashed s Any
-> SomeHashMapWith (SupersetProof 'Hashed s) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ k -> HashMap k a -> HashMap k a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HashMap.delete k
k HashMap k a
m)
  (SupersetProof 'Hashed s Any
 -> SomeHashMapWith (SupersetProof 'Hashed s) k a)
-> SupersetProof 'Hashed s Any
-> SomeHashMapWith (SupersetProof 'Hashed s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed Any :-> InSet 'Hashed s)
-> SupersetProof 'Hashed s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Hashed Any) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed Any :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | If the key is in the map, return the proof of this, and the associated
-- value; otherwise return 'Nothing'.
lookup :: forall s k a. Hashable k => k -> HashMap s k a -> Maybe (Key s k, a)
lookup :: forall s k a.
Hashable k =>
k -> HashMap s k a -> Maybe (Key s k, a)
lookup k
k (HashMap HashMap k a
m) = (k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k,) (a -> (Key s k, a)) -> Maybe a -> Maybe (Key s k, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> HashMap k a -> Maybe a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup k
k HashMap k a
m

-- | Given a key that is proven to be in the map, return the associated value.
--
-- Unlike 'Data.HashMap.!' from "Data.HashMap.Lazy", this function is total, as
-- it is impossible to obtain a @'Key' s k@ for a key that is not in the map
-- @'HashMap' s k a@.
(!) :: forall s k a. Hashable k => HashMap s k a -> Key s k -> a
! :: forall s k a. Hashable k => HashMap s k a -> Key s k -> a
(!) (HashMap HashMap k a
m) Key s k
k = case k -> HashMap k a -> Maybe a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k) HashMap k a
m of
  Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error String
"(!): bug: Data.HashMap.Refined has been subverted"
  Just a
x -> a
x

-- | If a key is in the map, return the proof that it is.
member :: forall s k a. Hashable k => k -> HashMap s k a -> Maybe (Key s k)
member :: forall s k a. Hashable k => k -> HashMap s k a -> Maybe (Key s k)
member k
k (HashMap HashMap k a
m)
  | k
k k -> HashMap k a -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`HashMap.member` HashMap k a
m = Key s k -> Maybe (Key s k)
forall a. a -> Maybe a
Just (k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k)
  | Bool
otherwise = Maybe (Key s k)
forall a. Maybe a
Nothing

-- | If a map is empty, return a proof that it is.
null :: forall s k a. HashMap s k a -> Maybe (EmptyProof 'Hashed s)
null :: forall s k a. HashMap s k a -> Maybe (EmptyProof 'Hashed s)
null (HashMap HashMap k a
m)
  | HashMap k a -> Bool
forall k v. HashMap k v -> Bool
HashMap.null HashMap k a
m = EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s)
forall a. a -> Maybe a
Just (EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s))
-> EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Hashed s :-> InSet 'Hashed s)
-> EmptyProof 'Hashed s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
forall s. InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
  | Bool
otherwise = Maybe (EmptyProof 'Hashed s)
forall a. Maybe a
Nothing

-- | If all keys of the first map are also present in the second map, and the
-- given function returns 'True' for their associated values, return a proof
-- that the keys form a subset.
isSubmapOfBy
  :: forall s t k a b. Hashable k
  => (a -> b -> Bool)
  -> HashMap s k a
  -> HashMap t k b
  -> Maybe (SubsetProof 'Hashed s t)
isSubmapOfBy :: forall s t k a b.
Hashable k =>
(a -> b -> Bool)
-> HashMap s k a
-> HashMap t k b
-> Maybe (SubsetProof 'Hashed s t)
isSubmapOfBy a -> b -> Bool
f (HashMap HashMap k a
m1) (HashMap HashMap k b
m2)
#if MIN_VERSION_unordered_containers(0, 2, 12)
  | (a -> b -> Bool) -> HashMap k a -> HashMap k b -> Bool
forall k v1 v2.
(Eq k, Hashable k) =>
(v1 -> v2 -> Bool) -> HashMap k v1 -> HashMap k v2 -> Bool
HashMap.isSubmapOfBy a -> b -> Bool
f HashMap k a
m1 HashMap k b
m2
#else
  | All True <- flip HashMap.foldMapWithKey m1
    \k v1 -> case HashMap.lookup k m2 of
      Just v2 | f v1 v2 -> mempty
      _ -> All False
#endif
  = SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t)
forall a. a -> Maybe a
Just (SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t))
-> SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> InSet 'Hashed t) -> SubsetProof 'Hashed s t
forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed s :-> InSet 'Hashed t
forall p q x. Refined p x -> Refined q x
unsafeSubset
  | Bool
otherwise = Maybe (SubsetProof 'Hashed s t)
forall a. Maybe a
Nothing

-- | If two maps are disjoint (i.e. their intersection is empty), return a proof
-- of that.
disjoint
  :: forall s t k a b. Hashable k
  => HashMap s k a -> HashMap t k b -> Maybe (DisjointProof 'Hashed s t)
disjoint :: forall s t k a b.
Hashable k =>
HashMap s k a -> HashMap t k b -> Maybe (DisjointProof 'Hashed s t)
disjoint (HashMap HashMap k a
m1) (HashMap HashMap k b
m2)
  | HashMap k () -> Bool
forall k v. HashMap k v -> Bool
HashMap.null (HashMap k () -> Bool) -> HashMap k () -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> b -> ()) -> HashMap k a -> HashMap k b -> HashMap k ()
forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
HashMapStrict.intersectionWith (\a
_ b
_ -> ()) HashMap k a
m1 HashMap k b
m2
  = DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t)
forall a. a -> Maybe a
Just (DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t))
-> DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t)
forall a b. (a -> b) -> a -> b
$ (forall t.
 (InSet 'Hashed t :-> InSet 'Hashed s)
 -> (InSet 'Hashed t :-> InSet 'Hashed t)
 -> forall u x.
    Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed u) x)
-> DisjointProof 'Hashed s t
forall (f :: Flavor) s r.
(forall t.
 (InSet f t :-> InSet f s)
 -> (InSet f t :-> InSet f r)
 -> forall u x. Refined (InSet f t) x -> Refined (InSet f u) x)
-> DisjointProof f s r
DisjointProof \InSet 'Hashed t :-> InSet 'Hashed s
f InSet 'Hashed t :-> InSet 'Hashed t
g -> (InSet 'Hashed t :-> InSet 'Hashed s)
-> (InSet 'Hashed t :-> InSet 'Hashed t)
-> InSet 'Hashed t :-> InSet 'Hashed u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed t :-> InSet 'Hashed s
f Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed t :-> InSet 'Hashed t
g
  | Bool
otherwise = Maybe (DisjointProof 'Hashed s t)
forall a. Maybe a
Nothing

-- | Given two maps proven to have the same keys, for each key apply the
-- function to the associated values, to obtain a new map with the same keys.
zipWithKey
  :: forall s k a b c. Hashable k
  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c
zipWithKey :: forall s k a b c.
Hashable k =>
(Key s k -> a -> b -> c)
-> HashMap s k a -> HashMap s k b -> HashMap s k c
zipWithKey Key s k -> a -> b -> c
f (HashMap HashMap k a
m1) (HashMap HashMap k b
m2) = HashMap k c -> HashMap s k c
forall s k a. HashMap k a -> HashMap s k a
HashMap
  (HashMap k c -> HashMap s k c) -> HashMap k c -> HashMap s k c
forall a b. (a -> b) -> a -> b
$ (k -> a -> b -> c) -> HashMap k a -> HashMap k b -> HashMap k c
forall k v1 v2 v3.
(Eq k, Hashable k) =>
(k -> v1 -> v2 -> v3)
-> HashMap k v1 -> HashMap k v2 -> HashMap k v3
HashMap.intersectionWithKey (Key s k -> a -> b -> c
f (Key s k -> a -> b -> c) -> (k -> Key s k) -> k -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) HashMap k a
m1 HashMap k b
m2

-- | Remove the keys that appear in the second map from the first map.
difference
  :: forall s t k a b. Hashable k
  => HashMap s k a
  -> HashMap t k b
  -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
difference :: forall s t k a b.
Hashable k =>
HashMap s k a
-> HashMap t k b
-> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
difference (HashMap HashMap k a
m1) (HashMap HashMap k b
m2)
  = HashMap Any k a
-> DifferenceProof 'Hashed s t Any
-> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ HashMap k a -> HashMap k b -> HashMap k a
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
HashMap.difference HashMap k a
m1 HashMap k b
m2)
    (DifferenceProof 'Hashed s t Any
 -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a)
-> DifferenceProof 'Hashed s t Any
-> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed Any :-> InSet 'Hashed s)
-> (forall u.
    (InSet 'Hashed u :-> InSet 'Hashed Any)
    -> (InSet 'Hashed u :-> InSet 'Hashed t)
    -> forall v x.
       Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed v) x)
-> (InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed Any))
-> DifferenceProof 'Hashed s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> InSet f s)
-> (forall u.
    (InSet f u :-> InSet f r)
    -> (InSet f u :-> InSet f t)
    -> forall v x. Refined (InSet f u) x -> Refined (InSet f v) x)
-> (InSet f s :-> (InSet f t || InSet f r))
-> DifferenceProof f s t r
DifferenceProof Refined (InSet 'Hashed Any) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed Any :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (\InSet 'Hashed u :-> InSet 'Hashed Any
f InSet 'Hashed u :-> InSet 'Hashed t
g -> (InSet 'Hashed u :-> InSet 'Hashed Any)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed Any) x
InSet 'Hashed u :-> InSet 'Hashed Any
f Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed u :-> InSet 'Hashed t
g) Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed t || InSet 'Hashed Any) x
InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed Any)
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Apply a function to all values in a map, together with their corresponding
-- keys, that are proven to be in the map. The set of keys remains the same.
mapWithKey
  :: forall s k a b. (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
mapWithKey :: forall s k a b.
(Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
mapWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b)
-> (Key s k -> a -> b)
-> HashMap s k a
-> HashMap s k b
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b)
 -> (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b)
-> (Key s k -> a -> b)
-> HashMap s k a
-> HashMap s k b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b) -> HashMap k a -> HashMap k b)
-> (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
forall a b. Coercible a b => a -> b
coerce
  (((k -> a -> b) -> HashMap k a -> HashMap k b)
 -> (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b)
-> ((k -> a -> b) -> HashMap k a -> HashMap k b)
-> (Key s k -> a -> b)
-> HashMap s k a
-> HashMap s k b
forall a b. (a -> b) -> a -> b
$ forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapWithKey @k @a @b

-- | Map an 'Applicative' transformation with access to each value's
-- corresponding key and a proof that it is in the map. The set of keys remains
-- unchanged.
traverseWithKey
  :: forall s f k a b. Applicative f
  => (Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)
traverseWithKey :: forall s (f :: * -> *) k a b.
Applicative f =>
(Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)
traverseWithKey Key s k -> a -> f b
f (HashMap HashMap k a
m)
  = HashMap k b -> HashMap s k b
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k b -> HashMap s k b)
-> f (HashMap k b) -> f (HashMap s k b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (k -> a -> f b) -> HashMap k a -> f (HashMap k b)
forall (f :: * -> *) k v1 v2.
Applicative f =>
(k -> v1 -> f v2) -> HashMap k v1 -> f (HashMap k v2)
HashMap.traverseWithKey (Key s k -> a -> f b
f (Key s k -> a -> f b) -> (k -> Key s k) -> k -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) HashMap k a
m

-- | Map each key-value pair of a map into a monoid (with proof that the key was
-- in the map), and combine the results using '<>'.
foldMapWithKey
  :: forall s k a m. Monoid m => (Key s k -> a -> m) -> HashMap s k a -> m
foldMapWithKey :: forall s k a m.
Monoid m =>
(Key s k -> a -> m) -> HashMap s k a -> m
foldMapWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> m) -> HashMap s k a -> m)
-> (Key s k -> a -> m)
-> HashMap s k a
-> m
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (Key s k -> a -> m) -> HashMap s k a -> m)
 -> (Key s k -> a -> m) -> HashMap s k a -> m)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> m) -> HashMap s k a -> m)
-> (Key s k -> a -> m)
-> HashMap s k a
-> m
forall a b. (a -> b) -> a -> b
$ ((k -> a -> m) -> HashMap k a -> m)
-> (Key s k -> a -> m) -> HashMap s k a -> m
forall a b. Coercible a b => a -> b
coerce
  (((k -> a -> m) -> HashMap k a -> m)
 -> (Key s k -> a -> m) -> HashMap s k a -> m)
-> ((k -> a -> m) -> HashMap k a -> m)
-> (Key s k -> a -> m)
-> HashMap s k a
-> m
forall a b. (a -> b) -> a -> b
$ forall m k v. Monoid m => (k -> v -> m) -> HashMap k v -> m
HashMap.foldMapWithKey @m @k @a

-- | Right associative fold with a lazy accumulator.
foldrWithKey
  :: forall s k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
foldrWithKey :: forall s k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
foldrWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
 -> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b -> b) -> b -> HashMap k a -> b)
-> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
forall a b. Coercible a b => a -> b
coerce
  (((k -> a -> b -> b) -> b -> HashMap k a -> b)
 -> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> ((k -> a -> b -> b) -> b -> HashMap k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall k v a. (k -> v -> a -> a) -> a -> HashMap k v -> a
HashMap.foldrWithKey @k @a @b

-- | Left associative fold with a lazy accumulator.
foldlWithKey
  :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
foldlWithKey :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
foldlWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
 -> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (Coercible k (Key s k) =>
    (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((b -> k -> a -> b) -> b -> HashMap k a -> b)
-> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
forall a b. Coercible a b => a -> b
coerce
  (((b -> k -> a -> b) -> b -> HashMap k a -> b)
 -> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> ((b -> k -> a -> b) -> b -> HashMap k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
HashMap.foldlWithKey @b @k @a

-- | Right associative fold with a strict accumulator.
foldrWithKey'
  :: forall s k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
foldrWithKey' :: forall s k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
foldrWithKey' = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
 -> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Coercible k (Key s k) =>
    (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b -> b) -> b -> HashMap k a -> b)
-> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b
forall a b. Coercible a b => a -> b
coerce
  (((k -> a -> b -> b) -> b -> HashMap k a -> b)
 -> (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b)
-> ((k -> a -> b -> b) -> b -> HashMap k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall k v a. (k -> v -> a -> a) -> a -> HashMap k v -> a
HashMap.foldrWithKey' @k @a @b

-- | Left associative fold with a strict accumulator.
foldlWithKey'
  :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
foldlWithKey' :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
foldlWithKey' = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
    (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
  (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
 -> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (Coercible k (Key s k) =>
    (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((b -> k -> a -> b) -> b -> HashMap k a -> b)
-> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b
forall a b. Coercible a b => a -> b
coerce
  (((b -> k -> a -> b) -> b -> HashMap k a -> b)
 -> (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b)
-> ((b -> k -> a -> b) -> b -> HashMap k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> HashMap s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
HashMap.foldlWithKey' @b @k @a

-- | Return the set of keys in the map, with the contents of the set still
-- tracked by the @s@ parameter. See "Data.HashSet.Refined".
keysSet :: forall s k a. HashMap s k a -> HashSet s k
keysSet :: forall s k a. HashMap s k a -> HashSet s k
keysSet (HashMap HashMap k a
m) = HashSet k
-> (forall s. Reifies s (HashSet k) => Proxy s -> HashSet s k)
-> HashSet s k
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (HashMap k a -> HashSet k
forall k a. HashMap k a -> HashSet k
HashMap.keysSet HashMap k a
m)
  \(Proxy s
_ :: Proxy s') -> case (Any :~: Any) -> s :~: s
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: s :~: s' of
    s :~: s
Refl -> HashSet s k
forall (a :: Constraint). a => Dict a
Dict

-- | Convert to a list of key-value pairs.
toList :: forall s k a. HashMap s k a -> [(Key s k, a)]
toList :: forall s k a. HashMap s k a -> [(Key s k, a)]
toList = Coercion k (Key s k)
-> (Coercible k (Key s k) => HashMap s k a -> [(Key s k, a)])
-> HashMap s k a
-> [(Key s k, a)]
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) => HashMap s k a -> [(Key s k, a)])
 -> HashMap s k a -> [(Key s k, a)])
-> (Coercible k (Key s k) => HashMap s k a -> [(Key s k, a)])
-> HashMap s k a
-> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ (HashMap k a -> [(k, a)]) -> HashMap s k a -> [(Key s k, a)]
forall a b. Coercible a b => a -> b
coerce ((HashMap k a -> [(k, a)]) -> HashMap s k a -> [(Key s k, a)])
-> (HashMap k a -> [(k, a)]) -> HashMap s k a -> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [(k, v)]
HashMap.toList @k @a

-- | Retain only the key-value pairs that satisfy the predicate, returning a
-- potentially smaller map.
filterWithKey
  :: forall s k a. (Key s k -> a -> Bool)
  -> HashMap s k a
  -> SomeHashMapWith (SupersetProof 'Hashed s) k a
filterWithKey :: forall s k a.
(Key s k -> a -> Bool)
-> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a
filterWithKey Key s k -> a -> Bool
p (HashMap HashMap k a
m)
  = HashMap Any k a
-> SupersetProof 'Hashed s Any
-> SomeHashMapWith (SupersetProof 'Hashed s) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Bool) -> HashMap k a -> HashMap k a
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey (Key s k -> a -> Bool
p (Key s k -> a -> Bool) -> (k -> Key s k) -> k -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) HashMap k a
m)
    (SupersetProof 'Hashed s Any
 -> SomeHashMapWith (SupersetProof 'Hashed s) k a)
-> SupersetProof 'Hashed s Any
-> SomeHashMapWith (SupersetProof 'Hashed s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed Any :-> InSet 'Hashed s)
-> SupersetProof 'Hashed s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Hashed Any) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed Any :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Restrict a map to only those keys that are elements of @t@.
restrictKeys
  :: forall s t k a. (Hashable k, KnownHashSet t k)
  => HashMap s k a -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a
restrictKeys :: forall s t k a.
(Hashable k, KnownHashSet t k) =>
HashMap s k a
-> SomeHashMapWith (IntersectionProof 'Hashed s t) k a
restrictKeys (HashMap HashMap k a
m) = HashMap Any k a
-> IntersectionProof 'Hashed s t Any
-> SomeHashMapWith (IntersectionProof 'Hashed s t) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith
  (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ (a -> () -> a) -> HashMap k a -> HashMap k () -> HashMap k a
forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
HashMap.intersectionWith a -> () -> a
forall a b. a -> b -> a
const HashMap k a
m
    (HashMap k () -> HashMap k a) -> HashMap k () -> HashMap k a
forall a b. (a -> b) -> a -> b
$ HashSet k -> HashMap k ()
forall a. HashSet a -> HashMap a ()
HashSet.toMap (HashSet k -> HashMap k ()) -> HashSet k -> HashMap k ()
forall a b. (a -> b) -> a -> b
$ Proxy t -> HashSet k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet k
reflect (Proxy t -> HashSet k) -> Proxy t -> HashSet k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
  (IntersectionProof 'Hashed s t Any
 -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a)
-> IntersectionProof 'Hashed s t Any
-> SomeHashMapWith (IntersectionProof 'Hashed s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed Any :-> (InSet 'Hashed s && InSet 'Hashed t))
-> (forall u.
    (InSet 'Hashed u :-> InSet 'Hashed s)
    -> (InSet 'Hashed u :-> InSet 'Hashed t)
    -> InSet 'Hashed u :-> InSet 'Hashed Any)
-> IntersectionProof 'Hashed s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> (InSet f s && InSet f t))
-> (forall u.
    (InSet f u :-> InSet f s)
    -> (InSet f u :-> InSet f t) -> InSet f u :-> InSet f r)
-> IntersectionProof f s t r
IntersectionProof Refined (InSet 'Hashed Any) x
-> Refined (InSet 'Hashed s && InSet 'Hashed t) x
InSet 'Hashed Any :-> (InSet 'Hashed s && InSet 'Hashed t)
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> Refined (InSet 'Hashed u) x
-> Refined (InSet 'Hashed Any) x
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed Any
forall u.
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed Any
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2

-- | Remove all keys that are elements of @t@ from the map.
withoutKeys
  :: forall s t k a. (Hashable k, KnownHashSet t k)
  => HashMap s k a -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
withoutKeys :: forall s t k a.
(Hashable k, KnownHashSet t k) =>
HashMap s k a -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
withoutKeys (HashMap HashMap k a
m) = HashMap Any k a
-> DifferenceProof 'Hashed s t Any
-> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
forall s k a (p :: * -> *).
HashMap s k a -> p s -> SomeHashMapWith p k a
SomeHashMapWith
  (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ HashMap k a -> HashMap k () -> HashMap k a
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
HashMap.difference HashMap k a
m (HashMap k () -> HashMap k a) -> HashMap k () -> HashMap k a
forall a b. (a -> b) -> a -> b
$ HashSet k -> HashMap k ()
forall a. HashSet a -> HashMap a ()
HashSet.toMap (HashSet k -> HashMap k ()) -> HashSet k -> HashMap k ()
forall a b. (a -> b) -> a -> b
$ Proxy t -> HashSet k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet k
reflect (Proxy t -> HashSet k) -> Proxy t -> HashSet k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
  (DifferenceProof 'Hashed s t Any
 -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a)
-> DifferenceProof 'Hashed s t Any
-> SomeHashMapWith (DifferenceProof 'Hashed s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed Any :-> InSet 'Hashed s)
-> (forall u.
    (InSet 'Hashed u :-> InSet 'Hashed Any)
    -> (InSet 'Hashed u :-> InSet 'Hashed t)
    -> forall v x.
       Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed v) x)
-> (InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed Any))
-> DifferenceProof 'Hashed s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> InSet f s)
-> (forall u.
    (InSet f u :-> InSet f r)
    -> (InSet f u :-> InSet f t)
    -> forall v x. Refined (InSet f u) x -> Refined (InSet f v) x)
-> (InSet f s :-> (InSet f t || InSet f r))
-> DifferenceProof f s t r
DifferenceProof Refined (InSet 'Hashed Any) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed Any :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (\InSet 'Hashed u :-> InSet 'Hashed Any
f InSet 'Hashed u :-> InSet 'Hashed t
g -> (InSet 'Hashed u :-> InSet 'Hashed Any)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed Any) x
InSet 'Hashed u :-> InSet 'Hashed Any
f Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed u :-> InSet 'Hashed t
g) Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed t || InSet 'Hashed Any) x
InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed Any)
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Partition a map into two disjoint submaps: those whose key-value pairs
-- satisfy the predicate, and those whose don't.
partitionWithKey
  :: forall s k a. Hashable k -- TODO: this is only used in the proof
  => (Key s k -> a -> Bool)
  -> HashMap s k a
  -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a
partitionWithKey :: forall s k a.
Hashable k =>
(Key s k -> a -> Bool)
-> HashMap s k a
-> Some2HashMapWith (PartitionProof 'Hashed s k) k a a
partitionWithKey Key s k -> a -> Bool
p (HashMap HashMap k a
m) = HashMap Any k a
-> HashMap Any k a
-> PartitionProof 'Hashed s k Any Any
-> Some2HashMapWith (PartitionProof 'Hashed s k) k a a
forall s t k a b (p :: * -> * -> *).
HashMap s k a -> HashMap t k b -> p s t -> Some2HashMapWith p k a b
Some2HashMapWith
  (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Bool) -> HashMap k a -> HashMap k a
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey (Key s k -> a -> Bool
p (Key s k -> a -> Bool) -> (k -> Key s k) -> k -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) HashMap k a
m)
  (HashMap k a -> HashMap Any k a
forall s k a. HashMap k a -> HashMap s k a
HashMap (HashMap k a -> HashMap Any k a) -> HashMap k a -> HashMap Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Bool) -> HashMap k a -> HashMap k a
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey ((Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> Bool) -> a -> Bool) -> (k -> a -> Bool) -> k -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key s k -> a -> Bool
p (Key s k -> a -> Bool) -> (k -> Key s k) -> k -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) HashMap k a
m)
  (PartitionProof 'Hashed s k Any Any
 -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a)
-> PartitionProof 'Hashed s k Any Any
-> Some2HashMapWith (PartitionProof 'Hashed s k) k a a
forall a b. (a -> b) -> a -> b
$ (Key s k
 -> Either
      (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k))
-> ((InSet 'Hashed Any || InSet 'Hashed Any) :-> InSet 'Hashed s)
-> (forall t.
    (InSet 'Hashed Any :-> InSet 'Hashed t)
    -> (InSet 'Hashed Any :-> InSet 'Hashed t)
    -> InSet 'Hashed s :-> InSet 'Hashed t)
-> (forall t.
    (InSet 'Hashed t :-> InSet 'Hashed Any)
    -> (InSet 'Hashed t :-> InSet 'Hashed Any)
    -> forall u x.
       Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed u) x)
-> PartitionProof 'Hashed s k Any Any
forall (f :: Flavor) s a r q.
(Refined (InSet f s) a
 -> Either (Refined (InSet f r) a) (Refined (InSet f q) a))
-> ((InSet f r || InSet f q) :-> InSet f s)
-> (forall t.
    (InSet f r :-> InSet f t)
    -> (InSet f q :-> InSet f t) -> InSet f s :-> InSet f t)
-> (forall t.
    (InSet f t :-> InSet f r)
    -> (InSet f t :-> InSet f q)
    -> forall u x. Refined (InSet f t) x -> Refined (InSet f u) x)
-> PartitionProof f s a r q
PartitionProof
    do \Key s k
k -> case k -> HashMap k a -> Maybe a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k) HashMap k a
m of
        Maybe a
Nothing -> String
-> Either
     (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k)
forall a. HasCallStack => String -> a
error
          String
"partitionWithKey: bug: Data.HashMap.Refined has been subverted"
        Just a
x -> if Key s k -> a -> Bool
p Key s k
k a
x
          then Refined (InSet 'Hashed Any) k
-> Either
     (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k)
forall a b. a -> Either a b
Left (Refined (InSet 'Hashed Any) k
 -> Either
      (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k))
-> Refined (InSet 'Hashed Any) k
-> Either
     (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k)
forall a b. (a -> b) -> a -> b
$ k -> Refined (InSet 'Hashed Any) k
forall k s. k -> Key s k
unsafeKey (k -> Refined (InSet 'Hashed Any) k)
-> k -> Refined (InSet 'Hashed Any) k
forall a b. (a -> b) -> a -> b
$ Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k
          else Refined (InSet 'Hashed Any) k
-> Either
     (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k)
forall a b. b -> Either a b
Right (Refined (InSet 'Hashed Any) k
 -> Either
      (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k))
-> Refined (InSet 'Hashed Any) k
-> Either
     (Refined (InSet 'Hashed Any) k) (Refined (InSet 'Hashed Any) k)
forall a b. (a -> b) -> a -> b
$ k -> Refined (InSet 'Hashed Any) k
forall k s. k -> Key s k
unsafeKey (k -> Refined (InSet 'Hashed Any) k)
-> k -> Refined (InSet 'Hashed Any) k
forall a b. (a -> b) -> a -> b
$ Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k
    Refined (InSet 'Hashed Any || InSet 'Hashed Any) x
-> Refined (InSet 'Hashed s) x
(InSet 'Hashed Any || InSet 'Hashed Any) :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Hashed Any :-> InSet 'Hashed t)
-> (InSet 'Hashed Any :-> InSet 'Hashed t)
-> Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed t) x
(InSet 'Hashed Any :-> InSet 'Hashed t)
-> (InSet 'Hashed Any :-> InSet 'Hashed t)
-> InSet 'Hashed s :-> InSet 'Hashed t
forall t.
(InSet 'Hashed Any :-> InSet 'Hashed t)
-> (InSet 'Hashed Any :-> InSet 'Hashed t)
-> InSet 'Hashed s :-> InSet 'Hashed t
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 \InSet 'Hashed t :-> InSet 'Hashed Any
f InSet 'Hashed t :-> InSet 'Hashed Any
g -> (InSet 'Hashed t :-> InSet 'Hashed Any)
-> (InSet 'Hashed t :-> InSet 'Hashed Any)
-> InSet 'Hashed t :-> InSet 'Hashed u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed Any) x
InSet 'Hashed t :-> InSet 'Hashed Any
f Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed Any) x
InSet 'Hashed t :-> InSet 'Hashed Any
g

-- | If elements of @s@ can be weakened to elements of @t@ and vice versa, then
-- @s@ and @t@ actually stand for the same set and @'Key' s@ can be safely
-- interconverted with @'Key' t@.
--
-- The requirement that the weakenings are natural transformations ensures that
-- they don't actually alter the keys. To build these you can compose ':->''s
-- from proofs returned by functions in this module, or "Refined" functions like
-- 'andLeft' or 'leftOr'.
castKey
  :: forall s t k. (forall x. Key s x -> Key t x)
  -> (forall x. Key t x -> Key s x)
  -> Coercion (Key s k) (Key t k)
castKey :: forall s t k.
(forall x. Key s x -> Key t x)
-> (forall x. Key t x -> Key s x) -> Coercion (Key s k) (Key t k)
castKey = (InSet 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed t :-> InSet 'Hashed s)
-> Coercion
     (Refined (InSet 'Hashed s) k) (Refined (InSet 'Hashed t) k)
forall a p q.
(p :-> q) -> (q :-> p) -> Coercion (Refined p a) (Refined q a)
castRefined

-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps
-- can be interconverted too. For example, 'zipWithKey' can be implemented via
-- 'Data.HashMap.Refined.intersectionWithKey' by proving that the set of keys
-- remains unchanged:
--
-- @
-- 'zipWithKey'
--   :: forall s k a b c. 'Hashable' k
--   => ('Key' s k -> a -> b -> c) -> 'HashMap' s k a -> 'HashMap' s k b -> 'HashMap' s k c
-- 'zipWithKey' f m1 m2
--   | v'SomeHashMapWith' @r m proof <- 'Data.HashMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2
--   , v'IntersectionProof' p1 p2 <- proof
--   , ( v'Coercion' :: t'Coercion' ('HashMap' r k c) ('HashMap' s k c))
--     <- app $ 'cast' $ 'castKey' ('andLeft' . p1) (p2 'id' 'id')
--   = 'coerce' m
--   where
--     app :: t'Coercion' f g -> t'Coercion' (f x) (g x)
--     app v'Coercion' = v'Coercion'
-- @
cast
  :: forall s t k. (forall x. Coercion (Key s x) (Key t x))
  -> Coercion (HashMap s k) (HashMap t k)
cast :: forall s t k.
(forall x. Coercion (Key s x) (Key t x))
-> Coercion (HashMap s k) (HashMap t k)
cast Coercion (Key s Any) (Key t Any)
forall x. Coercion (Key s x) (Key t x)
Coercion = Coercion (HashMap s k) (HashMap t k)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

instance FunctorWithIndex (Key s k) (HashMap s k) where
  imap :: forall a b. (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
imap = (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
forall s k a b.
(Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
mapWithKey

instance FoldableWithIndex (Key s k) (HashMap s k) where
  ifoldMap :: forall m a. Monoid m => (Key s k -> a -> m) -> HashMap s k a -> m
ifoldMap = (Key s k -> a -> m) -> HashMap s k a -> m
forall s k a m.
Monoid m =>
(Key s k -> a -> m) -> HashMap s k a -> m
foldMapWithKey

instance TraversableWithIndex (Key s k) (HashMap s k) where
  itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)
itraverse = (Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)
forall s (f :: * -> *) k a b.
Applicative f =>
(Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)
traverseWithKey

-- | Similar to the instance for functions -- zip corresponding keys. To use
-- '<*>'/'liftA2' without 'KnownSet' see 'zipWithKey'.
instance (Hashable k, KnownHashSet s k) => Applicative (HashMap s k) where
  pure :: forall a. a -> HashMap s k a
pure a
x = (Key s k -> a) -> HashMap s k a
forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet \Key s k
_ -> a
x
  <*> :: forall a b. HashMap s k (a -> b) -> HashMap s k a -> HashMap s k b
(<*>) = (Key s k -> (a -> b) -> a -> b)
-> HashMap s k (a -> b) -> HashMap s k a -> HashMap s k b
forall s k a b c.
Hashable k =>
(Key s k -> a -> b -> c)
-> HashMap s k a -> HashMap s k b -> HashMap s k c
zipWithKey (((a -> b) -> a -> b) -> Key s k -> (a -> b) -> a -> b
forall a b. a -> b -> a
const (a -> b) -> a -> b
forall a. a -> a
id)

-- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the
-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.
bind
  :: forall s k a b. Hashable k
  => HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b
bind :: forall s k a b.
Hashable k =>
HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b
bind HashMap s k a
m a -> HashMap s k b
f = (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
forall s k a b.
(Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
mapWithKey (\Key s k
k a
x -> a -> HashMap s k b
f a
x HashMap s k b -> Key s k -> b
forall s k a. Hashable k => HashMap s k a -> Key s k -> a
! Key s k
k) HashMap s k a
m

-- | Similar to the instance for functions. To use '>>=' without 'KnownSet' see
-- 'bind'.
instance (Hashable k, KnownHashSet s k) => Monad (HashMap s k) where
  >>= :: forall a b. HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b
(>>=) = HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b
forall s k a b.
Hashable k =>
HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b
bind

-- | Similar to the instance for functions. See also
-- 'Data.HashMap.Refined.backpermuteKeys'.
instance (Hashable k, KnownHashSet s k)
  => MonadReader (Key s k) (HashMap s k) where
  ask :: HashMap s k (Key s k)
ask = (Key s k -> Key s k) -> HashMap s k (Key s k)
forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet Key s k -> Key s k
forall a. a -> a
id
  local :: forall a. (Key s k -> Key s k) -> HashMap s k a -> HashMap s k a
local Key s k -> Key s k
f HashMap s k a
m = (Key s k -> a -> a) -> HashMap s k a -> HashMap s k a
forall s k a b.
(Key s k -> a -> b) -> HashMap s k a -> HashMap s k b
mapWithKey (\Key s k
k a
_ -> HashMap s k a
m HashMap s k a -> Key s k -> a
forall s k a. Hashable k => HashMap s k a -> Key s k -> a
! Key s k -> Key s k
f Key s k
k) HashMap s k a
m

-- | Append the values at the corresponding keys
instance (Hashable k, Semigroup a) => Semigroup (HashMap s k a) where
  <> :: HashMap s k a -> HashMap s k a -> HashMap s k a
(<>) = (Key s k -> a -> a -> a)
-> HashMap s k a -> HashMap s k a -> HashMap s k a
forall s k a b c.
Hashable k =>
(Key s k -> a -> b -> c)
-> HashMap s k a -> HashMap s k b -> HashMap s k c
zipWithKey ((a -> a -> a) -> Key s k -> a -> a -> a
forall a b. a -> b -> a
const a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>))

instance (Hashable k, KnownHashSet s k, Monoid a)
  => Monoid (HashMap s k a) where
  mempty :: HashMap s k a
mempty = (Key s k -> a) -> HashMap s k a
forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet \Key s k
_ -> a
forall a. Monoid a => a
mempty

-- | Similar to the instance for functions
instance (Hashable k, KnownHashSet s k) => Distributive (HashMap s k) where
  collect :: forall (f :: * -> *) a b.
Functor f =>
(a -> HashMap s k b) -> f a -> HashMap s k (f b)
collect = (a -> HashMap s k b) -> f a -> HashMap s k (f b)
forall (f :: * -> *) (w :: * -> *) a b.
(Representable f, Functor w) =>
(a -> f b) -> w a -> f (w b)
collectRep
  distribute :: forall (f :: * -> *) a.
Functor f =>
f (HashMap s k a) -> HashMap s k (f a)
distribute = f (HashMap s k a) -> HashMap s k (f a)
forall (f :: * -> *) (w :: * -> *) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep

-- | Witness isomorphism with functions from @'Key' s k@
instance (Hashable k, KnownHashSet s k) => Representable (HashMap s k) where
  type Rep (HashMap s k) = Key s k
  index :: forall a. HashMap s k a -> Rep (HashMap s k) -> a
index = HashMap s k a -> Rep (HashMap s k) -> a
HashMap s k a -> Key s k -> a
forall s k a. Hashable k => HashMap s k a -> Key s k -> a
(!)
  tabulate :: forall a. (Rep (HashMap s k) -> a) -> HashMap s k a
tabulate = (Rep (HashMap s k) -> a) -> HashMap s k a
(Key s k -> a) -> HashMap s k a
forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a
fromSet