{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      : Data.Binding.Hobbits.Mb
-- Copyright   : (c) 2019 Edwin Westbrook
--
-- License     : BSD3
--
-- Maintainer  : westbrook@galois.com
-- Stability   : experimental
-- Portability : GHC
--
-- Implements mappings from 'Name's to some associated data, using
-- 'Data.IntMap.Strict'. Note that these mappings are strict.
--
-- All of the functions in this module operate in an identical manner as those
-- of the same name in the 'Data.IntMap.Strict' module.

module Data.Binding.Hobbits.NameMap (
  NameMap(), NameAndElem(..)
  , empty, singleton, fromList
  , insert, delete, adjust, update, alter
  , lookup, (!), member, null, size
  , union, difference, (\\), intersection
  , map, foldr, foldl
  , assocs
  , liftNameMap
  ) where

import Prelude hiding (lookup, null, map, foldr, foldl)
import qualified Prelude as Prelude (map)
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Unsafe.Coerce

import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Mb
import Data.Binding.Hobbits.NuMatching
import Data.Binding.Hobbits.NuMatchingInstances
import Data.Binding.Hobbits.QQ

-- | An element of a 'NameMap', where the name type @a@ is existentially
-- quantified
data NMElem (f :: k -> *) where
  NMElem :: f a -> NMElem f

-- | Coerce an @'NMElem' f@ to an @f a@ for a specific type @a@. This assumes we
-- know that this is the proper type to coerce it to, i.e., it is unsafe.
coerceNMElem :: NMElem f -> f a
coerceNMElem :: NMElem f -> f a
coerceNMElem (NMElem f a
x) = f a -> f a
forall a b. a -> b
unsafeCoerce f a
x

-- | A heterogeneous map from 'Name's of arbitrary type @a@ to elements of @f a@
newtype NameMap (f :: k -> *) =
  NameMap { NameMap f -> IntMap (NMElem f)
unNameMap :: IntMap (NMElem f) }

-- | Internal-only helper function for mapping a unary function on 'IntMap's to
-- a 'NameMap'
mapNMap1 :: (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 :: (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 IntMap (NMElem f) -> IntMap (NMElem f)
f (NameMap IntMap (NMElem f)
m) = IntMap (NMElem f) -> NameMap f
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap (IntMap (NMElem f) -> NameMap f) -> IntMap (NMElem f) -> NameMap f
forall a b. (a -> b) -> a -> b
$ IntMap (NMElem f) -> IntMap (NMElem f)
f IntMap (NMElem f)
m

-- | Internal-only helper function for mapping a binary function on 'IntMap's to
-- 'NameMap's
mapNMap2 :: (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)) ->
            NameMap f -> NameMap f -> NameMap f
mapNMap2 :: (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
mapNMap2 IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)
f (NameMap IntMap (NMElem f)
m1) (NameMap IntMap (NMElem f)
m2) = IntMap (NMElem f) -> NameMap f
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap (IntMap (NMElem f) -> NameMap f) -> IntMap (NMElem f) -> NameMap f
forall a b. (a -> b) -> a -> b
$ IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)
f IntMap (NMElem f)
m1 IntMap (NMElem f)
m2

-- | The empty 'NameMap'
empty :: NameMap f
empty :: NameMap f
empty = IntMap (NMElem f) -> NameMap f
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap IntMap (NMElem f)
forall a. IntMap a
IntMap.empty

-- | The singleton 'NameMap' with precisely one 'Name' and corresponding value
singleton :: Name a -> f a -> NameMap f
singleton :: Name a -> f a -> NameMap f
singleton (MkName Int
i) f a
x = IntMap (NMElem f) -> NameMap f
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap (IntMap (NMElem f) -> NameMap f) -> IntMap (NMElem f) -> NameMap f
forall a b. (a -> b) -> a -> b
$ Int -> NMElem f -> IntMap (NMElem f)
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i (NMElem f -> IntMap (NMElem f)) -> NMElem f -> IntMap (NMElem f)
forall a b. (a -> b) -> a -> b
$ f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem f a
x

-- | A pair of a 'Name' of some type @a@ along with an element of type @f a@
data NameAndElem f where
  NameAndElem :: Name a -> f a -> NameAndElem f

-- | Build a 'NameMap' from a list of pairs of names and values they map to
fromList :: [NameAndElem f] -> NameMap f
fromList :: [NameAndElem f] -> NameMap f
fromList =
  IntMap (NMElem f) -> NameMap f
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap (IntMap (NMElem f) -> NameMap f)
-> ([NameAndElem f] -> IntMap (NMElem f))
-> [NameAndElem f]
-> NameMap f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, NMElem f)] -> IntMap (NMElem f)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, NMElem f)] -> IntMap (NMElem f))
-> ([NameAndElem f] -> [(Int, NMElem f)])
-> [NameAndElem f]
-> IntMap (NMElem f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (NameAndElem f -> (Int, NMElem f))
-> [NameAndElem f] -> [(Int, NMElem f)]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (\NameAndElem f
ne ->
                case NameAndElem f
ne of
                  NameAndElem (MkName Int
i) f a
f -> (Int
i, f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem f a
f))

-- | Insert a 'Name' and a value it maps to into a 'NameMap'
insert :: Name a -> f a -> NameMap f -> NameMap f
insert :: Name a -> f a -> NameMap f -> NameMap f
insert (MkName Int
i) f a
f = (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 ((IntMap (NMElem f) -> IntMap (NMElem f))
 -> NameMap f -> NameMap f)
-> (IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f
-> NameMap f
forall a b. (a -> b) -> a -> b
$ Int -> NMElem f -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem f a
f)

-- | Delete a 'Name' and the value it maps to from a 'NameMap'
delete :: Name a -> NameMap f -> NameMap f
delete :: Name a -> NameMap f -> NameMap f
delete (MkName Int
i) = (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 ((IntMap (NMElem f) -> IntMap (NMElem f))
 -> NameMap f -> NameMap f)
-> (IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f
-> NameMap f
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
i

-- | Apply a function to the value mapped to by a 'Name'
adjust :: (f a -> f a) -> Name a -> NameMap f -> NameMap f
adjust :: (f a -> f a) -> Name a -> NameMap f -> NameMap f
adjust f a -> f a
f (MkName Int
i) = (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 ((IntMap (NMElem f) -> IntMap (NMElem f))
 -> NameMap f -> NameMap f)
-> (IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f
-> NameMap f
forall a b. (a -> b) -> a -> b
$ (NMElem f -> NMElem f)
-> Int -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem (f a -> NMElem f) -> (NMElem f -> f a) -> NMElem f -> NMElem f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f a
f (f a -> f a) -> (NMElem f -> f a) -> NMElem f -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NMElem f -> f a
forall k (f :: k -> *) (a :: k). NMElem f -> f a
coerceNMElem) Int
i

-- | Update the value mapped to by a 'Name', possibly deleting it
update :: (f a -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
update :: (f a -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
update f a -> Maybe (f a)
f (MkName Int
i) = (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 ((IntMap (NMElem f) -> IntMap (NMElem f))
 -> NameMap f -> NameMap f)
-> (IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f
-> NameMap f
forall a b. (a -> b) -> a -> b
$ (NMElem f -> Maybe (NMElem f))
-> Int -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. (a -> Maybe a) -> Int -> IntMap a -> IntMap a
IntMap.update ((f a -> NMElem f) -> Maybe (f a) -> Maybe (NMElem f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem (Maybe (f a) -> Maybe (NMElem f))
-> (NMElem f -> Maybe (f a)) -> NMElem f -> Maybe (NMElem f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Maybe (f a)
f (f a -> Maybe (f a))
-> (NMElem f -> f a) -> NMElem f -> Maybe (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NMElem f -> f a
forall k (f :: k -> *) (a :: k). NMElem f -> f a
coerceNMElem) Int
i

-- | Apply a function to the optional value associated with a 'Name', where
-- 'Nothing' represents the 'Name' not being present in the 'NameMap'
alter :: (Maybe (f a) -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
alter :: (Maybe (f a) -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f
alter Maybe (f a) -> Maybe (f a)
f (MkName Int
i) =
  (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f
mapNMap1 ((IntMap (NMElem f) -> IntMap (NMElem f))
 -> NameMap f -> NameMap f)
-> (IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f
-> NameMap f
forall a b. (a -> b) -> a -> b
$ (Maybe (NMElem f) -> Maybe (NMElem f))
-> Int -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IntMap.alter ((f a -> NMElem f) -> Maybe (f a) -> Maybe (NMElem f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> NMElem f
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem (Maybe (f a) -> Maybe (NMElem f))
-> (Maybe (NMElem f) -> Maybe (f a))
-> Maybe (NMElem f)
-> Maybe (NMElem f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (f a) -> Maybe (f a)
f (Maybe (f a) -> Maybe (f a))
-> (Maybe (NMElem f) -> Maybe (f a))
-> Maybe (NMElem f)
-> Maybe (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NMElem f -> f a) -> Maybe (NMElem f) -> Maybe (f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NMElem f -> f a
forall k (f :: k -> *) (a :: k). NMElem f -> f a
coerceNMElem) Int
i

-- | Look up the value associated with a 'Name', returning 'Nothing' if there is
-- none
lookup :: Name a -> NameMap f -> Maybe (f a)
lookup :: Name a -> NameMap f -> Maybe (f a)
lookup (MkName Int
i) (NameMap IntMap (NMElem f)
m) = (NMElem f -> f a) -> Maybe (NMElem f) -> Maybe (f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NMElem f -> f a
forall k (f :: k -> *) (a :: k). NMElem f -> f a
coerceNMElem (Maybe (NMElem f) -> Maybe (f a))
-> Maybe (NMElem f) -> Maybe (f a)
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (NMElem f) -> Maybe (NMElem f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap (NMElem f)
m

-- | Synonym for 'lookup' with the argument order reversed
(!) :: NameMap f -> Name a -> f a
(NameMap IntMap (NMElem f)
m) ! :: NameMap f -> Name a -> f a
! (MkName Int
i) = NMElem f -> f a
forall k (f :: k -> *) (a :: k). NMElem f -> f a
coerceNMElem (NMElem f -> f a) -> NMElem f -> f a
forall a b. (a -> b) -> a -> b
$ IntMap (NMElem f)
m IntMap (NMElem f) -> Int -> NMElem f
forall a. IntMap a -> Int -> a
IntMap.! Int
i

-- | Test if a 'Name' has a value in a 'NameMap'
member :: Name a -> NameMap f -> Bool
member :: Name a -> NameMap f -> Bool
member (MkName Int
i) (NameMap IntMap (NMElem f)
m) = Int -> IntMap (NMElem f) -> Bool
forall a. Int -> IntMap a -> Bool
IntMap.member Int
i IntMap (NMElem f)
m

-- | Test if a 'NameMap' is empty
null :: NameMap f -> Bool
null :: NameMap f -> Bool
null (NameMap IntMap (NMElem f)
m) = IntMap (NMElem f) -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap (NMElem f)
m

-- | Return the number of 'Name's in a 'NameMap'
size :: NameMap f -> Int
size :: NameMap f -> Int
size (NameMap IntMap (NMElem f)
m) = IntMap (NMElem f) -> Int
forall a. IntMap a -> Int
IntMap.size IntMap (NMElem f)
m

-- | Union two 'NameMap's
union :: NameMap f -> NameMap f -> NameMap f
union :: NameMap f -> NameMap f -> NameMap f
union = (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
mapNMap2 IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union

-- | Remove all bindings in the first 'NameMap' for 'Name's in the second
difference :: NameMap f -> NameMap f -> NameMap f
difference :: NameMap f -> NameMap f -> NameMap f
difference = (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
mapNMap2 IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference

-- | Infix synonym for 'difference'
(\\) :: NameMap f -> NameMap f -> NameMap f
\\ :: NameMap f -> NameMap f -> NameMap f
(\\) = NameMap f -> NameMap f -> NameMap f
forall k (f :: k -> *). NameMap f -> NameMap f -> NameMap f
difference

-- | Intersect two 'NameMap's
intersection :: NameMap f -> NameMap f -> NameMap f
intersection :: NameMap f -> NameMap f -> NameMap f
intersection = (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
forall k (f :: k -> *).
(IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f))
-> NameMap f -> NameMap f -> NameMap f
mapNMap2 IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.intersection

-- | Map a function across the values associated with each 'Name'
map :: (forall a. f a -> g a) -> NameMap f -> NameMap g
map :: (forall (a :: k). f a -> g a) -> NameMap f -> NameMap g
map forall (a :: k). f a -> g a
f (NameMap IntMap (NMElem f)
m) =
  IntMap (NMElem g) -> NameMap g
forall k (f :: k -> *). IntMap (NMElem f) -> NameMap f
NameMap (IntMap (NMElem g) -> NameMap g) -> IntMap (NMElem g) -> NameMap g
forall a b. (a -> b) -> a -> b
$ (NMElem f -> NMElem g) -> IntMap (NMElem f) -> IntMap (NMElem g)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (\NMElem f
e -> case NMElem f
e of
                           NMElem f a
x -> g a -> NMElem g
forall k (f :: k -> *) (a :: k). f a -> NMElem f
NMElem (g a -> NMElem g) -> g a -> NMElem g
forall a b. (a -> b) -> a -> b
$ f a -> g a
forall (a :: k). f a -> g a
f f a
x) IntMap (NMElem f)
m

-- | Perform a right fold across all values in a 'NameMap'
foldr :: (forall a. f a -> b -> b) -> b -> NameMap f -> b
foldr :: (forall (a :: k). f a -> b -> b) -> b -> NameMap f -> b
foldr forall (a :: k). f a -> b -> b
f b
b (NameMap IntMap (NMElem f)
m) =
  (NMElem f -> b -> b) -> b -> IntMap (NMElem f) -> b
forall a b. (a -> b -> b) -> b -> IntMap a -> b
IntMap.foldr (\NMElem f
e -> case NMElem f
e of
                   NMElem f a
x -> f a -> b -> b
forall (a :: k). f a -> b -> b
f f a
x) b
b IntMap (NMElem f)
m

-- | Perform a left fold across all values in a 'NameMap'
foldl :: (forall b. a -> f b -> a) -> a -> NameMap f -> a
foldl :: (forall (b :: k). a -> f b -> a) -> a -> NameMap f -> a
foldl forall (b :: k). a -> f b -> a
f a
a (NameMap IntMap (NMElem f)
m) =
  (a -> NMElem f -> a) -> a -> IntMap (NMElem f) -> a
forall a b. (a -> b -> a) -> a -> IntMap b -> a
IntMap.foldl (\a
a NMElem f
e -> case NMElem f
e of
                   NMElem f a
x -> a -> f a -> a
forall (b :: k). a -> f b -> a
f a
a f a
x) a
a IntMap (NMElem f)
m

-- | Return all 'Name's in a 'NameMap' with their associated values
assocs :: NameMap f -> [NameAndElem f]
assocs :: NameMap f -> [NameAndElem f]
assocs (NameMap IntMap (NMElem f)
m) =
  ((Int, NMElem f) -> NameAndElem f)
-> [(Int, NMElem f)] -> [NameAndElem f]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (\(Int
i, NMElem f
e) -> case NMElem f
e of
                  NMElem f a
f -> Name a -> f a -> NameAndElem f
forall k (a :: k) (f :: k -> *). Name a -> f a -> NameAndElem f
NameAndElem (Int -> Name a
forall k (a :: k). Int -> Name a
MkName Int
i) f a
f) ([(Int, NMElem f)] -> [NameAndElem f])
-> [(Int, NMElem f)] -> [NameAndElem f]
forall a b. (a -> b) -> a -> b
$
  IntMap (NMElem f) -> [(Int, NMElem f)]
forall a. IntMap a -> [(Int, a)]
IntMap.assocs IntMap (NMElem f)
m

$(mkNuMatching [t| forall f. NuMatchingAny1 f => NameAndElem f |])

-- | Lift a 'NameMap' out of a name-binding using a "partial lifting function"
-- that can lift some values in the 'NameMap' out of the binding. The resulting
-- 'NameMap' contains those names and associated values where the names were not
-- bound by the name-binding and the partial lifting function was able to lift
-- their associated values.
liftNameMap :: forall ctx f a. NuMatchingAny1 f =>
               (forall a. Mb ctx (f a) -> Maybe (f a)) ->
               Mb ctx (NameMap f) -> NameMap f
liftNameMap :: (forall (a :: k). Mb ctx (f a) -> Maybe (f a))
-> Mb ctx (NameMap f) -> NameMap f
liftNameMap forall (a :: k). Mb ctx (f a) -> Maybe (f a)
lifter = Mb ctx [NameAndElem f] -> NameMap f
helper (Mb ctx [NameAndElem f] -> NameMap f)
-> (Mb ctx (NameMap f) -> Mb ctx [NameAndElem f])
-> Mb ctx (NameMap f)
-> NameMap f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameMap f -> [NameAndElem f])
-> Mb ctx (NameMap f) -> Mb ctx [NameAndElem f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameMap f -> [NameAndElem f]
forall k (f :: k -> *). NameMap f -> [NameAndElem f]
assocs where
  helper :: Mb ctx [NameAndElem f] -> NameMap f
  helper :: Mb ctx [NameAndElem f] -> NameMap f
helper Mb ctx [NameAndElem f]
[nuP| [] |] = NameMap f
forall k (f :: k -> *). NameMap f
empty
  helper Mb ctx [NameAndElem f]
[nuP| (NameAndElem mb_n mb_f):mb_elems |]
    | Right Name a
n <- Mb ctx (Name a) -> Either (Member ctx a) (Name a)
forall k1 k2 (a :: k1) (ctx :: RList k2).
Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP Mb ctx (Name a)
mb_n
    , Just f a
f <- Mb ctx (f a) -> Maybe (f a)
forall (a :: k). Mb ctx (f a) -> Maybe (f a)
lifter Mb ctx (f a)
mb_f
    = Name a -> f a -> NameMap f -> NameMap f
forall k (a :: k) (f :: k -> *).
Name a -> f a -> NameMap f -> NameMap f
insert Name a
n f a
f (Mb ctx [NameAndElem f] -> NameMap f
helper Mb ctx [NameAndElem f]
mb_elems)
  helper Mb ctx [NameAndElem f]
[nuP| _:mb_elems |] = Mb ctx [NameAndElem f] -> NameMap f
helper Mb ctx [NameAndElem f]
mb_elems