-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | A hash map linking keys' and values' type parameters existentially.

module Data.Ten.HashMap
         ( -- * HashMap10
           HashMap10, (:**)(..)
         , empty, insert, lookup, findWithDefault
         , toList, fromList
           -- * Miscellaneous
         , Hashable1, Show1, Portray1, Diff1
         ) where

import Prelude hiding (lookup)

import qualified Data.Foldable as F
import Data.Maybe (catMaybes, fromMaybe)
import Data.Semigroup (Any(..), All(..))
import Data.Type.Equality ((:~:)(..), TestEquality(..))
import GHC.Exts (IsList)
import qualified GHC.Exts as Exts
import GHC.Generics (Generic1, (:.:)(..))

import Data.GADT.Compare (GEq(..))
import Data.Hashable (Hashable(..))
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HM
import Data.Portray (Portray(..), Portrayal(..))
import Data.Portray.Diff (Diff(..), diffVs)
import Data.Wrapped (Wrapped1(..))

import Data.Ten.Entails (Entails(..), (:!:))
import Data.Ten.Exists (Exists(..))
import Data.Ten.Foldable (Foldable10(..))
import Data.Ten.Foldable.WithIndex (Foldable10WithIndex(..))
import Data.Ten.Functor (Functor10(..))
import Data.Ten.Functor.WithIndex (Index10, Functor10WithIndex(..))
import Data.Ten.Traversable (Traversable10(..))
import Data.Ten.Traversable.WithIndex (Traversable10WithIndex(..))
import Data.Ten.Sigma ((:**)(..))

type Hashable1 k = forall x. Hashable (k x)
type Show1 k = forall x. Show (k x)
type Portray1 k = forall x. Portray (k x)
type Diff1 k = forall x. Diff (k x)

type instance Index10 (HashMap10 k) = k

-- | A "dependent" hash map, where elements' type parameters match their keys'.
newtype HashMap10 k m = HashMap10 (HashMap (Exists k) (k :** m))
  deriving (forall (a :: * -> *). HashMap10 k a -> Rep1 (HashMap10 k) a)
-> (forall (a :: * -> *). Rep1 (HashMap10 k) a -> HashMap10 k a)
-> Generic1 (HashMap10 k)
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (a :: * -> *). Rep1 (HashMap10 k) a -> HashMap10 k a
forall (a :: * -> *). HashMap10 k a -> Rep1 (HashMap10 k) a
forall (k :: * -> *) (a :: * -> *).
Rep1 (HashMap10 k) a -> HashMap10 k a
forall (k :: * -> *) (a :: * -> *).
HashMap10 k a -> Rep1 (HashMap10 k) a
$cto1 :: forall (k :: * -> *) (a :: * -> *).
Rep1 (HashMap10 k) a -> HashMap10 k a
$cfrom1 :: forall (k :: * -> *) (a :: * -> *).
HashMap10 k a -> Rep1 (HashMap10 k) a
Generic1
  deriving
    ( (forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n
(forall (m :: * -> *) (n :: * -> *).
 (forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n)
-> Functor10 (HashMap10 k)
forall k (f :: (k -> *) -> *).
(forall (m :: k -> *) (n :: k -> *).
 (forall (a :: k). m a -> n a) -> f m -> f n)
-> Functor10 f
forall (m :: * -> *) (n :: * -> *).
(forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n
forall (k :: * -> *) (m :: * -> *) (n :: * -> *).
(forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n
fmap10 :: (forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n
$cfmap10 :: forall (k :: * -> *) (m :: * -> *) (n :: * -> *).
(forall a. m a -> n a) -> HashMap10 k m -> HashMap10 k n
Functor10, (forall a. m a -> w) -> HashMap10 k m -> w
(forall w (m :: * -> *).
 Monoid w =>
 (forall a. m a -> w) -> HashMap10 k m -> w)
-> Foldable10 (HashMap10 k)
forall w (m :: * -> *).
Monoid w =>
(forall a. m a -> w) -> HashMap10 k m -> w
forall k (t :: (k -> *) -> *).
(forall w (m :: k -> *).
 Monoid w =>
 (forall (a :: k). m a -> w) -> t m -> w)
-> Foldable10 t
forall (k :: * -> *) w (m :: * -> *).
Monoid w =>
(forall a. m a -> w) -> HashMap10 k m -> w
foldMap10 :: (forall a. m a -> w) -> HashMap10 k m -> w
$cfoldMap10 :: forall (k :: * -> *) w (m :: * -> *).
Monoid w =>
(forall a. m a -> w) -> HashMap10 k m -> w
Foldable10, Functor10 (HashMap10 k)
Foldable10 (HashMap10 k)
Functor10 (HashMap10 k)
-> Foldable10 (HashMap10 k)
-> (forall (f :: * -> *) (m :: * -> *) (n :: * -> *) r.
    Applicative f =>
    (HashMap10 k n -> r)
    -> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r)
-> Traversable10 (HashMap10 k)
(HashMap10 k n -> r)
-> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r
forall k (t :: (k -> *) -> *).
Functor10 t
-> Foldable10 t
-> (forall (f :: * -> *) (m :: k -> *) (n :: k -> *) r.
    Applicative f =>
    (t n -> r) -> (forall (a :: k). m a -> f (n a)) -> t m -> f r)
-> Traversable10 t
forall (k :: * -> *). Functor10 (HashMap10 k)
forall (k :: * -> *). Foldable10 (HashMap10 k)
forall (f :: * -> *) (m :: * -> *) (n :: * -> *) r.
Applicative f =>
(HashMap10 k n -> r)
-> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r
forall (k :: * -> *) (f :: * -> *) (m :: * -> *) (n :: * -> *) r.
Applicative f =>
(HashMap10 k n -> r)
-> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r
mapTraverse10 :: (HashMap10 k n -> r)
-> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r
$cmapTraverse10 :: forall (k :: * -> *) (f :: * -> *) (m :: * -> *) (n :: * -> *) r.
Applicative f =>
(HashMap10 k n -> r)
-> (forall a. m a -> f (n a)) -> HashMap10 k m -> f r
$cp2Traversable10 :: forall (k :: * -> *). Foldable10 (HashMap10 k)
$cp1Traversable10 :: forall (k :: * -> *). Functor10 (HashMap10 k)
Traversable10
    ) via Wrapped1 Generic1 (HashMap10 k)
  deriving
    ( Functor10 (HashMap10 k)
Functor10 (HashMap10 k)
-> (forall (m :: * -> *) (n :: * -> *).
    (forall a. Index10 (HashMap10 k) a -> m a -> n a)
    -> HashMap10 k m -> HashMap10 k n)
-> Functor10WithIndex (HashMap10 k)
(forall a. Index10 (HashMap10 k) a -> m a -> n a)
-> HashMap10 k m -> HashMap10 k n
forall k (f :: (k -> *) -> *).
Functor10 f
-> (forall (m :: k -> *) (n :: k -> *).
    (forall (a :: k). Index10 f a -> m a -> n a) -> f m -> f n)
-> Functor10WithIndex f
forall (k :: * -> *). Functor10 (HashMap10 k)
forall (m :: * -> *) (n :: * -> *).
(forall a. Index10 (HashMap10 k) a -> m a -> n a)
-> HashMap10 k m -> HashMap10 k n
forall (k :: * -> *) (m :: * -> *) (n :: * -> *).
(forall a. Index10 (HashMap10 k) a -> m a -> n a)
-> HashMap10 k m -> HashMap10 k n
imap10 :: (forall a. Index10 (HashMap10 k) a -> m a -> n a)
-> HashMap10 k m -> HashMap10 k n
$cimap10 :: forall (k :: * -> *) (m :: * -> *) (n :: * -> *).
(forall a. Index10 (HashMap10 k) a -> m a -> n a)
-> HashMap10 k m -> HashMap10 k n
$cp1Functor10WithIndex :: forall (k :: * -> *). Functor10 (HashMap10 k)
Functor10WithIndex, Foldable10 (HashMap10 k)
Foldable10 (HashMap10 k)
-> (forall w (m :: * -> *).
    Monoid w =>
    (forall a. Index10 (HashMap10 k) a -> m a -> w)
    -> HashMap10 k m -> w)
-> Foldable10WithIndex (HashMap10 k)
(forall a. Index10 (HashMap10 k) a -> m a -> w)
-> HashMap10 k m -> w
forall w (m :: * -> *).
Monoid w =>
(forall a. Index10 (HashMap10 k) a -> m a -> w)
-> HashMap10 k m -> w
forall k (f :: (k -> *) -> *).
Foldable10 f
-> (forall w (m :: k -> *).
    Monoid w =>
    (forall (a :: k). Index10 f a -> m a -> w) -> f m -> w)
-> Foldable10WithIndex f
forall (k :: * -> *). Foldable10 (HashMap10 k)
forall (k :: * -> *) w (m :: * -> *).
Monoid w =>
(forall a. Index10 (HashMap10 k) a -> m a -> w)
-> HashMap10 k m -> w
ifoldMap10 :: (forall a. Index10 (HashMap10 k) a -> m a -> w)
-> HashMap10 k m -> w
$cifoldMap10 :: forall (k :: * -> *) w (m :: * -> *).
Monoid w =>
(forall a. Index10 (HashMap10 k) a -> m a -> w)
-> HashMap10 k m -> w
$cp1Foldable10WithIndex :: forall (k :: * -> *). Foldable10 (HashMap10 k)
Foldable10WithIndex, Traversable10 (HashMap10 k)
Foldable10WithIndex (HashMap10 k)
Functor10WithIndex (HashMap10 k)
Functor10WithIndex (HashMap10 k)
-> Foldable10WithIndex (HashMap10 k)
-> Traversable10 (HashMap10 k)
-> (forall (g :: * -> *) (n :: * -> *) r (m :: * -> *).
    Applicative g =>
    (HashMap10 k n -> r)
    -> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
    -> HashMap10 k m
    -> g r)
-> Traversable10WithIndex (HashMap10 k)
(HashMap10 k n -> r)
-> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
-> HashMap10 k m
-> g r
forall k (f :: (k -> *) -> *).
Functor10WithIndex f
-> Foldable10WithIndex f
-> Traversable10 f
-> (forall (g :: * -> *) (n :: k -> *) r (m :: k -> *).
    Applicative g =>
    (f n -> r)
    -> (forall (a :: k). Index10 f a -> m a -> g (n a)) -> f m -> g r)
-> Traversable10WithIndex f
forall (k :: * -> *). Traversable10 (HashMap10 k)
forall (k :: * -> *). Foldable10WithIndex (HashMap10 k)
forall (k :: * -> *). Functor10WithIndex (HashMap10 k)
forall (g :: * -> *) (n :: * -> *) r (m :: * -> *).
Applicative g =>
(HashMap10 k n -> r)
-> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
-> HashMap10 k m
-> g r
forall (k :: * -> *) (g :: * -> *) (n :: * -> *) r (m :: * -> *).
Applicative g =>
(HashMap10 k n -> r)
-> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
-> HashMap10 k m
-> g r
imapTraverse10 :: (HashMap10 k n -> r)
-> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
-> HashMap10 k m
-> g r
$cimapTraverse10 :: forall (k :: * -> *) (g :: * -> *) (n :: * -> *) r (m :: * -> *).
Applicative g =>
(HashMap10 k n -> r)
-> (forall a. Index10 (HashMap10 k) a -> m a -> g (n a))
-> HashMap10 k m
-> g r
$cp3Traversable10WithIndex :: forall (k :: * -> *). Traversable10 (HashMap10 k)
$cp2Traversable10WithIndex :: forall (k :: * -> *). Foldable10WithIndex (HashMap10 k)
$cp1Traversable10WithIndex :: forall (k :: * -> *). Functor10WithIndex (HashMap10 k)
Traversable10WithIndex
    ) via HashMap (Exists k) :.: ((:**) k)

deriving stock
  instance (GEq k, Entails k (Eq :!: m)) => Eq (HashMap10 k m)

deriving stock
  instance (Show1 k, Entails k (Show :!: m)) => Show (HashMap10 k m)

instance (GEq k, Hashable1 k) => IsList (HashMap10 k m) where
  type Item (HashMap10 k m) = k :** m
  toList :: HashMap10 k m -> [Item (HashMap10 k m)]
toList = HashMap10 k m -> [Item (HashMap10 k m)]
forall (k :: * -> *) (m :: * -> *). HashMap10 k m -> [k :** m]
toList
  fromList :: [Item (HashMap10 k m)] -> HashMap10 k m
fromList = [Item (HashMap10 k m)] -> HashMap10 k m
forall (k :: * -> *) (m :: * -> *).
(GEq k, Hashable1 k) =>
[k :** m] -> HashMap10 k m
fromList

instance (Portray1 k, Entails k (Portray :!: m))
      => Portray (HashMap10 k m) where
  portray :: HashMap10 k m -> Portrayal
portray = Portrayal -> [Portrayal] -> Portrayal
Apply (Ident -> Portrayal
Name Ident
"fromList") ([Portrayal] -> Portrayal)
-> (HashMap10 k m -> [Portrayal]) -> HashMap10 k m -> Portrayal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Portrayal -> [Portrayal]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Portrayal -> [Portrayal])
-> (HashMap10 k m -> Portrayal) -> HashMap10 k m -> [Portrayal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [k :** m] -> Portrayal
forall a. Portray a => a -> Portrayal
portray ([k :** m] -> Portrayal)
-> (HashMap10 k m -> [k :** m]) -> HashMap10 k m -> Portrayal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap10 k m -> [k :** m]
forall (k :: * -> *) (m :: * -> *). HashMap10 k m -> [k :** m]
toList

data EntryDiff a = InLeft a | InBoth a a | InRight a

diffToM :: Maybe Portrayal -> ((Any, All), Maybe Portrayal)
diffToM :: Maybe Portrayal -> ((Any, All), Maybe Portrayal)
diffToM = \case
  Maybe Portrayal
Nothing -> ((Bool -> Any
Any Bool
False, Bool -> All
All Bool
False), Maybe Portrayal
forall a. Maybe a
Nothing)
  Just Portrayal
d  -> ((Bool -> Any
Any Bool
True, Bool -> All
All Bool
True), Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just Portrayal
d)

diffM :: (Diff a, Portray a) => EntryDiff a -> ((Any, All), Maybe Portrayal)
diffM :: EntryDiff a -> ((Any, All), Maybe Portrayal)
diffM EntryDiff a
e = Maybe Portrayal -> ((Any, All), Maybe Portrayal)
diffToM (Maybe Portrayal -> ((Any, All), Maybe Portrayal))
-> Maybe Portrayal -> ((Any, All), Maybe Portrayal)
forall a b. (a -> b) -> a -> b
$ case EntryDiff a
e of
  InLeft a
x -> Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just (Portrayal -> Maybe Portrayal) -> Portrayal -> Maybe Portrayal
forall a b. (a -> b) -> a -> b
$ a -> Portrayal
forall a. Portray a => a -> Portrayal
portray a
x Portrayal -> Portrayal -> Portrayal
`diffVs` Text -> Portrayal
Opaque Text
"_"
  InBoth a
x a
y -> a -> a -> Maybe Portrayal
forall a. Diff a => a -> a -> Maybe Portrayal
diff a
x a
y
  InRight a
y -> Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just (Portrayal -> Maybe Portrayal) -> Portrayal -> Maybe Portrayal
forall a b. (a -> b) -> a -> b
$ Text -> Portrayal
Opaque Text
"_" Portrayal -> Portrayal -> Portrayal
`diffVs` a -> Portrayal
forall a. Portray a => a -> Portrayal
portray a
y

instance ( TestEquality k, GEq k, Hashable1 k, Portray1 k, Diff1 k
         , Entails k (Portray :!: m), Entails k (Diff :!: m)
         )
      => Diff (HashMap10 k m) where
  diff :: HashMap10 k m -> HashMap10 k m -> Maybe Portrayal
diff (HashMap10 HashMap (Exists k) (k :** m)
l) (HashMap10 HashMap (Exists k) (k :** m)
r) =
    if Bool
anyDiff
      then
        Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just (Portrayal -> Maybe Portrayal) -> Portrayal -> Maybe Portrayal
forall a b. (a -> b) -> a -> b
$ Portrayal -> [Portrayal] -> Portrayal
Apply (Ident -> Portrayal
Name Ident
"fromList") ([Portrayal] -> Portrayal) -> [Portrayal] -> Portrayal
forall a b. (a -> b) -> a -> b
$ Portrayal -> [Portrayal]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Portrayal -> [Portrayal]) -> Portrayal -> [Portrayal]
forall a b. (a -> b) -> a -> b
$ [Portrayal] -> Portrayal
List ([Portrayal] -> Portrayal) -> [Portrayal] -> Portrayal
forall a b. (a -> b) -> a -> b
$
        (if Bool
allDiff then [Portrayal] -> [Portrayal]
forall a. a -> a
id else ([Portrayal] -> [Portrayal] -> [Portrayal]
forall a. [a] -> [a] -> [a]
++ [Text -> Portrayal
Opaque Text
"..."])) ([Portrayal] -> [Portrayal]) -> [Portrayal] -> [Portrayal]
forall a b. (a -> b) -> a -> b
$
        [Maybe Portrayal] -> [Portrayal]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Portrayal] -> [Portrayal])
-> [Maybe Portrayal] -> [Portrayal]
forall a b. (a -> b) -> a -> b
$ HashMap (Exists k) (Maybe Portrayal) -> [Maybe Portrayal]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList HashMap (Exists k) (Maybe Portrayal)
diffs
      else Maybe Portrayal
forall a. Maybe a
Nothing
   where
    ((Any Bool
anyDiff, All Bool
allDiff), HashMap (Exists k) (Maybe Portrayal)
diffs) =
      (EntryDiff (k :** m) -> ((Any, All), Maybe Portrayal))
-> HashMap (Exists k) (EntryDiff (k :** m))
-> ((Any, All), HashMap (Exists k) (Maybe Portrayal))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse EntryDiff (k :** m) -> ((Any, All), Maybe Portrayal)
forall a.
(Diff a, Portray a) =>
EntryDiff a -> ((Any, All), Maybe Portrayal)
diffM (HashMap (Exists k) (EntryDiff (k :** m))
 -> ((Any, All), HashMap (Exists k) (Maybe Portrayal)))
-> HashMap (Exists k) (EntryDiff (k :** m))
-> ((Any, All), HashMap (Exists k) (Maybe Portrayal))
forall a b. (a -> b) -> a -> b
$
      (EntryDiff (k :** m) -> EntryDiff (k :** m) -> EntryDiff (k :** m))
-> HashMap (Exists k) (EntryDiff (k :** m))
-> HashMap (Exists k) (EntryDiff (k :** m))
-> HashMap (Exists k) (EntryDiff (k :** m))
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HM.unionWith EntryDiff (k :** m) -> EntryDiff (k :** m) -> EntryDiff (k :** m)
forall a. EntryDiff a -> EntryDiff a -> EntryDiff a
combine ((k :** m) -> EntryDiff (k :** m)
forall a. a -> EntryDiff a
InLeft ((k :** m) -> EntryDiff (k :** m))
-> HashMap (Exists k) (k :** m)
-> HashMap (Exists k) (EntryDiff (k :** m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Exists k) (k :** m)
l) ((k :** m) -> EntryDiff (k :** m)
forall a. a -> EntryDiff a
InRight ((k :** m) -> EntryDiff (k :** m))
-> HashMap (Exists k) (k :** m)
-> HashMap (Exists k) (EntryDiff (k :** m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Exists k) (k :** m)
r)

    combine :: EntryDiff a -> EntryDiff a -> EntryDiff a
combine (InLeft a
x) (InRight a
y) = a -> a -> EntryDiff a
forall a. a -> a -> EntryDiff a
InBoth a
x a
y
    combine EntryDiff a
_ EntryDiff a
_ = String -> EntryDiff a
forall a. HasCallStack => String -> a
error String
"Impossible"

-- | An empty 'HashMap10'.
empty :: HashMap10 k m
empty :: HashMap10 k m
empty = HashMap (Exists k) (k :** m) -> HashMap10 k m
forall (k :: * -> *) (m :: * -> *).
HashMap (Exists k) (k :** m) -> HashMap10 k m
HashMap10 HashMap (Exists k) (k :** m)
forall k v. HashMap k v
HM.empty

-- | Insert a new pair into a 'HashMap10'
insert
  :: forall a k m
   . (GEq k, Hashable1 k)
  => k a -> m a -> HashMap10 k m -> HashMap10 k m
insert :: k a -> m a -> HashMap10 k m -> HashMap10 k m
insert k a
k m a
m (HashMap10 HashMap (Exists k) (k :** m)
h) = HashMap (Exists k) (k :** m) -> HashMap10 k m
forall (k :: * -> *) (m :: * -> *).
HashMap (Exists k) (k :** m) -> HashMap10 k m
HashMap10 (HashMap (Exists k) (k :** m) -> HashMap10 k m)
-> HashMap (Exists k) (k :** m) -> HashMap10 k m
forall a b. (a -> b) -> a -> b
$ Exists k
-> (k :** m)
-> HashMap (Exists k) (k :** m)
-> HashMap (Exists k) (k :** m)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert (k a -> Exists k
forall k (a :: k) (m :: k -> *). m a -> Exists m
Exists k a
k) (k a
k k a -> m a -> k :** m
forall (k :: * -> *) (m :: * -> *) a. k a -> m a -> k :** m
:** m a
m) HashMap (Exists k) (k :** m)
h

fromEntry
  :: forall a k m
   . GEq k
  => k a -> k :** m -> m a
fromEntry :: k a -> (k :** m) -> m a
fromEntry k a
k (k a
k' :** m a
m) = case k a -> k a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq k a
k k a
k' of
  Just a :~: a
Refl -> m a
m a
m
  Maybe (a :~: a)
Nothing -> String -> m a
forall a. HasCallStack => String -> a
error String
"Internal error: key mapped to entry of the wrong type."

-- | Find an entry based on its key, if present.
lookup
  :: forall a k m
   . (GEq k, Hashable1 k)
  => k a -> HashMap10 k m -> Maybe (m a)
lookup :: k a -> HashMap10 k m -> Maybe (m a)
lookup k a
k (HashMap10 HashMap (Exists k) (k :** m)
h) = k a -> (k :** m) -> m a
forall a (k :: * -> *) (m :: * -> *).
GEq k =>
k a -> (k :** m) -> m a
fromEntry k a
k ((k :** m) -> m a) -> Maybe (k :** m) -> Maybe (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exists k -> HashMap (Exists k) (k :** m) -> Maybe (k :** m)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup (k a -> Exists k
forall k (a :: k) (m :: k -> *). m a -> Exists m
Exists k a
k) HashMap (Exists k) (k :** m)
h

-- | Find an entry based on its key, or return the given fallback value.
findWithDefault
  :: forall a k m
   . (GEq k, Hashable1 k)
  => m a -> k a -> HashMap10 k m -> m a
findWithDefault :: m a -> k a -> HashMap10 k m -> m a
findWithDefault m a
m k a
k = m a -> Maybe (m a) -> m a
forall a. a -> Maybe a -> a
fromMaybe m a
m (Maybe (m a) -> m a)
-> (HashMap10 k m -> Maybe (m a)) -> HashMap10 k m -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k a -> HashMap10 k m -> Maybe (m a)
forall a (k :: * -> *) (m :: * -> *).
(GEq k, Hashable1 k) =>
k a -> HashMap10 k m -> Maybe (m a)
lookup k a
k

-- | Convert to a list of (':**') in unspecified order.
toList :: HashMap10 k m -> [k :** m]
toList :: HashMap10 k m -> [k :** m]
toList (HashMap10 HashMap (Exists k) (k :** m)
m) = HashMap (Exists k) (k :** m) -> [k :** m]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList HashMap (Exists k) (k :** m)
m

-- | Build a map from a list of (k ':**' m) entries.
fromList :: (GEq k, Hashable1 k) => [k :** m] -> HashMap10 k m
fromList :: [k :** m] -> HashMap10 k m
fromList = HashMap (Exists k) (k :** m) -> HashMap10 k m
forall (k :: * -> *) (m :: * -> *).
HashMap (Exists k) (k :** m) -> HashMap10 k m
HashMap10 (HashMap (Exists k) (k :** m) -> HashMap10 k m)
-> ([k :** m] -> HashMap (Exists k) (k :** m))
-> [k :** m]
-> HashMap10 k m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Exists k, k :** m)] -> HashMap (Exists k) (k :** m)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList ([(Exists k, k :** m)] -> HashMap (Exists k) (k :** m))
-> ([k :** m] -> [(Exists k, k :** m)])
-> [k :** m]
-> HashMap (Exists k) (k :** m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k :** m) -> (Exists k, k :** m))
-> [k :** m] -> [(Exists k, k :** m)]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: k :** m
e@(k a
k :** m a
_) -> (k a -> Exists k
forall k (a :: k) (m :: k -> *). m a -> Exists m
Exists k a
k, k :** m
e))