{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

{-|
Module      : Data.Binder
Description : Variable binding for abstract syntax tree
Copyright   : (c) 2023 Keito Kajitani
License     : MIT
Maintainer  : Keito Kajitani <ijaketak@gmail.com>

binder is purely functional implementation of Ocaml's bindlib.
It follows the style of higher-order abstract syntax,
and offers the representation of abstract syntax tree.
-}
module Data.Binder
-- * Preliminaries
  ( MonadNumbering(..)
-- * Variable and Box
  , Var
  , Box
  , MkFree(..)
-- ** Variable
  , var'Key
  , var'Name
  , var'Box
  , nameOf
  , boxVar
  , newVar
  , isClosed
  , occur
-- ** Box
  , unbox
  , box
  , apBox
  , boxApply
  , boxApply2
  , boxApply3
  , boxApply4
  , boxPair
  , boxTriple
  , boxT
-- * Variable binding
  , Binder
  , binder'Name
  , binder'Body
  , subst
  , buildBinder
  , bind
  , unbind
  , eqBinder
  , boxBinder
  ) where

import Control.Lens
import Data.Kind (Type)
import qualified Data.Map.Lazy as M
import Data.Maybe (fromJust)
import Data.Text (Text)
import Unsafe.Coerce

-- | Numbering monad.
class (Monad m, Ord (Numbering m)) => MonadNumbering m where
  type Numbering m :: Type
  numbering :: m (Numbering m)

-- | Representation of variable
--   for abstract syntax tree type @a@
--   with base numbering monad @m@.
data Var m a = Var
  { forall (m :: * -> *) a. Var m a -> Numbering m
_var'Key :: !(Numbering m)
  , forall (m :: * -> *) a. Var m a -> VarBody m a
_var'Body :: VarBody m a
  }
data VarBody m a = VarBody
  { forall (m :: * -> *) a. VarBody m a -> Text
_varBody'Name :: Text
  , forall (m :: * -> *) a. VarBody m a -> Box m a
_varBody'Box :: Box m a
  }
-- | Representation of under-construction things
--   having type @a@ and containing variables.
data Box m a
  = Box'Closed a
  | Box'Env (EnvVar m) (Closure m a)

-- | Typeclass for free variable constructor.
class MkFree m a where
  mkFree :: Var m a -> a

data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)
type EnvVar m = M.Map (Numbering m) (AnyVar m)
data AnyMkFree m = forall a. MkFree m a => AnyMkFree a
type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)
newtype Closure m a = Closure { forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure :: (EnvMkFree m) -> a }

instance Functor (Closure m) where
  fmap :: forall a b. (a -> b) -> Closure m a -> Closure m b
fmap a -> b
f Closure m a
cla = forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m a
cla

instance Applicative (Closure m) where
  pure :: forall a. a -> Closure m a
pure a
a = forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const a
a
  Closure m (a -> b)
clf <*> :: forall a b. Closure m (a -> b) -> Closure m a -> Closure m b
<*> Closure m a
cla = forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvMkFree m
env -> forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m (a -> b)
clf EnvMkFree m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m a
cla EnvMkFree m
env

instance MonadNumbering m => Eq (Var m a) where
  Var Numbering m
x VarBody m a
_ == :: Var m a -> Var m a -> Bool
== Var Numbering m
y VarBody m a
_ = Numbering m
x forall a. Eq a => a -> a -> Bool
== Numbering m
y

instance MonadNumbering m => Ord (Var m a) where
  Var Numbering m
x VarBody m a
_ compare :: Var m a -> Var m a -> Ordering
`compare` Var Numbering m
y VarBody m a
_ = Numbering m
x forall a. Ord a => a -> a -> Ordering
`compare` Numbering m
y

$(makeLenses ''Var)
$(makeLenses ''VarBody)


var'Name :: Lens' (Var m a) Text
var'Name :: forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name = forall (m :: * -> *) a a.
Lens (Var m a) (Var m a) (VarBody m a) (VarBody m a)
var'Body forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Lens' (VarBody m a) Text
varBody'Name
var'Box :: Lens' (Var m a) (Box m a)
var'Box :: forall (m :: * -> *) a. Lens' (Var m a) (Box m a)
var'Box = forall (m :: * -> *) a a.
Lens (Var m a) (Var m a) (VarBody m a) (VarBody m a)
var'Body forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a (m :: * -> *) a.
Lens (VarBody m a) (VarBody m a) (Box m a) (Box m a)
varBody'Box

instance Show (Var m a) where
  showsPrec :: Int -> Var m a -> ShowS
showsPrec Int
n Var m a
x = forall a. Show a => Int -> a -> ShowS
showsPrec Int
n forall a b. (a -> b) -> a -> b
$ Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name
instance Show (VarBody m a) where
  showsPrec :: Int -> VarBody m a -> ShowS
showsPrec Int
n VarBody m a
x = forall a. Show a => Int -> a -> ShowS
showsPrec Int
n forall a b. (a -> b) -> a -> b
$ VarBody m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (VarBody m a) Text
varBody'Name
instance Show (AnyVar m) where
  showsPrec :: Int -> AnyVar m -> ShowS
showsPrec Int
n (AnyVar Var m a
x) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
n forall a b. (a -> b) -> a -> b
$ Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name

-- | The name of variable.
nameOf :: Var m a -> Text
nameOf :: forall (m :: * -> *) a. Var m a -> Text
nameOf Var m a
x = Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name

-- | Smart constructor for 'Box'.
boxVar :: Var m a -> Box m a
boxVar :: forall (m :: * -> *) a. Var m a -> Box m a
boxVar Var m a
x = Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Box m a)
var'Box

-- | Create a new variable with given name.
newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)
newVar :: forall (m :: * -> *) a.
(MkFree m a, MonadNumbering m) =>
Text -> m (Var m a)
newVar Text
name = do
  Numbering m
i <- forall (m :: * -> *). MonadNumbering m => m (Numbering m)
numbering
  let x :: Var m a
x = let b :: Box m a
b = forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env
                (forall k a. k -> a -> Map k a
M.singleton Numbering m
i forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MkFree m a => Var m a -> AnyVar m
AnyVar Var m a
x)
                (forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvMkFree m
env ->
                  let f :: AnyMkFree m -> p
f (AnyMkFree a
y) = forall a b. a -> b
unsafeCoerce a
y
                   in forall {m :: * -> *} {p}. AnyMkFree m -> p
f forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Numbering m
i EnvMkFree m
env)
           in forall (m :: * -> *) a. Numbering m -> VarBody m a -> Var m a
Var Numbering m
i forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Text -> Box m a -> VarBody m a
VarBody Text
name Box m a
b
  forall (m :: * -> *) a. Monad m => a -> m a
return Var m a
x


-- | 'Box' is closed if it exposes no free variables.
isClosed :: Box m a -> Bool
isClosed :: forall (m :: * -> *) a. Box m a -> Bool
isClosed Box'Closed{} = Bool
True
isClosed Box'Env{} = Bool
False

-- | Check if the variable occurs in the box.
occur :: MonadNumbering m => Var m a -> Box m b -> Bool
occur :: forall (m :: * -> *) a b.
MonadNumbering m =>
Var m a -> Box m b -> Bool
occur Var m a
_ (Box'Closed b
_) = Bool
False
occur Var m a
v (Box'Env EnvVar m
vs Closure m b
_) = forall k a. Ord k => k -> Map k a -> Bool
M.member (Var m a
v forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key) EnvVar m
vs


instance Functor (Box m) where
  fmap :: forall a b. (a -> b) -> Box m a -> Box m b
fmap a -> b
f (Box'Closed a
a) = forall (m :: * -> *) a. a -> Box m a
Box'Closed (a -> b
f a
a)
  fmap a -> b
f (Box'Env EnvVar m
vs Closure m a
ta) = forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env EnvVar m
vs (a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Closure m a
ta)

instance (MonadNumbering m) => Applicative (Box m) where
  pure :: forall a. a -> Box m a
pure = forall (m :: * -> *) a. a -> Box m a
Box'Closed
  Box'Closed a -> b
f <*> :: forall a b. Box m (a -> b) -> Box m a -> Box m b
<*> Box'Closed a
a = forall (m :: * -> *) a. a -> Box m a
Box'Closed (a -> b
f a
a)
  Box'Closed a -> b
f <*> Box'Env EnvVar m
va Closure m a
ta = forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env EnvVar m
va (a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Closure m a
ta)
  Box'Env EnvVar m
vf Closure m (a -> b)
tf <*> Box'Closed a
a = forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env EnvVar m
vf (forall {m :: * -> *} {t} {a}.
Closure m (t -> a) -> t -> Closure m a
appClosure Closure m (a -> b)
tf a
a)
   where
    appClosure :: Closure m (t -> a) -> t -> Closure m a
appClosure Closure m (t -> a)
clf t
x = forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvMkFree m
env -> forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m (t -> a)
clf EnvMkFree m
env t
x
  Box'Env EnvVar m
vf Closure m (a -> b)
tf <*> Box'Env EnvVar m
va Closure m a
ta = forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env (forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union EnvVar m
vf EnvVar m
va) (Closure m (a -> b)
tf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Closure m a
ta)

-- | Pick out and complete the construction of @a@.
unbox :: forall m a. Box m a -> a
unbox :: forall (m :: * -> *) a. Box m a -> a
unbox (Box'Closed a
t) = a
t
unbox (Box'Env EnvVar m
env Closure m a
cl) = forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m a
cl forall a b. (a -> b) -> a -> b
$ AnyVar m -> AnyMkFree m
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnvVar m
env
 where
  f :: AnyVar m -> AnyMkFree m
f (AnyVar Var m a
x) = forall (m :: * -> *) a. MkFree m a => a -> AnyMkFree m
AnyMkFree @m forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MkFree m a => Var m a -> a
mkFree Var m a
x

box :: MonadNumbering m => a -> Box m a
box :: forall (m :: * -> *) a. MonadNumbering m => a -> Box m a
box = forall (f :: * -> *) a. Applicative f => a -> f a
pure
apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b
apBox :: forall (m :: * -> *) a b.
MonadNumbering m =>
Box m (a -> b) -> Box m a -> Box m b
apBox = forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
(<*>)
boxApply :: (a -> b) -> Box m a -> Box m b
boxApply :: forall a b (m :: * -> *). (a -> b) -> Box m a -> Box m b
boxApply = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c
boxApply2 :: forall (m :: * -> *) a b c.
MonadNumbering m =>
(a -> b -> c) -> Box m a -> Box m b -> Box m c
boxApply2 a -> b -> c
f Box m a
ta Box m b
tb = a -> b -> c
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Box m a
ta forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m b
tb
boxApply3 :: MonadNumbering m => (a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d
boxApply3 :: forall (m :: * -> *) a b c d.
MonadNumbering m =>
(a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d
boxApply3 a -> b -> c -> d
f Box m a
ta Box m b
tb Box m c
tc = a -> b -> c -> d
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Box m a
ta forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m b
tb forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m c
tc
boxApply4 :: MonadNumbering m => (a -> b -> c -> d -> e) -> Box m a -> Box m b -> Box m c -> Box m d -> Box m e
boxApply4 :: forall (m :: * -> *) a b c d e.
MonadNumbering m =>
(a -> b -> c -> d -> e)
-> Box m a -> Box m b -> Box m c -> Box m d -> Box m e
boxApply4 a -> b -> c -> d -> e
f Box m a
ta Box m b
tb Box m c
tc Box m d
td = a -> b -> c -> d -> e
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Box m a
ta forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m b
tb forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m c
tc forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m d
td
boxPair :: MonadNumbering m => Box m a -> Box m b -> Box m (a, b)
boxPair :: forall (m :: * -> *) a b.
MonadNumbering m =>
Box m a -> Box m b -> Box m (a, b)
boxPair = forall (m :: * -> *) a b c.
MonadNumbering m =>
(a -> b -> c) -> Box m a -> Box m b -> Box m c
boxApply2 (,)
boxTriple :: MonadNumbering m => Box m a -> Box m b -> Box m c -> Box m (a, b, c)
boxTriple :: forall (m :: * -> *) a b c.
MonadNumbering m =>
Box m a -> Box m b -> Box m c -> Box m (a, b, c)
boxTriple = forall (m :: * -> *) a b c d.
MonadNumbering m =>
(a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d
boxApply3 (,,)
boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a)
boxT :: forall (m :: * -> *) (t :: * -> *) a.
(MonadNumbering m, Traversable t) =>
t (Box m a) -> Box m (t a)
boxT = forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA


-- | Variable binding.
--   Essentially, @Binder a b@ means @a -> b@.
data Binder a b = Binder
  { forall a b. Binder a b -> Text
_binder'Name :: Text
  , forall a b. Binder a b -> a -> b
_binder'Body :: a -> b
  }

$(makeLenses ''Binder)

-- | Variable substitution.
subst :: Binder a b -> a -> b
subst :: forall a b. Binder a b -> a -> b
subst Binder a b
b = Binder a b
b forall s a. s -> Getting a s a -> a
^. forall a b a b. Lens (Binder a b) (Binder a b) (a -> b) (a -> b)
binder'Body

-- | unbinding
unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)
unbind :: forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
Binder a b -> m (Var m a, b)
unbind Binder a b
b = do
  Var m a
x <- forall (m :: * -> *) a.
(MkFree m a, MonadNumbering m) =>
Text -> m (Var m a)
newVar forall a b. (a -> b) -> a -> b
$ Binder a b
b forall s a. s -> Getting a s a -> a
^. forall a b. Lens' (Binder a b) Text
binder'Name
  forall (m :: * -> *) a. Monad m => a -> m a
return (Var m a
x, forall a b. Binder a b -> a -> b
subst Binder a b
b forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MkFree m a => Var m a -> a
mkFree Var m a
x)

unbind2 :: (MkFree m a, MonadNumbering m)
        => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
unbind2 :: forall (m :: * -> *) a b1 b2.
(MkFree m a, MonadNumbering m) =>
Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
unbind2 Binder a b1
b1 Binder a b2
b2 = do
  Var m a
x <- forall (m :: * -> *) a.
(MkFree m a, MonadNumbering m) =>
Text -> m (Var m a)
newVar forall a b. (a -> b) -> a -> b
$ Binder a b1
b1 forall s a. s -> Getting a s a -> a
^. forall a b. Lens' (Binder a b) Text
binder'Name
  let v :: a
v = forall (m :: * -> *) a. MkFree m a => Var m a -> a
mkFree Var m a
x
  forall (m :: * -> *) a. Monad m => a -> m a
return (Var m a
x, forall a b. Binder a b -> a -> b
subst Binder a b1
b1 a
v, forall a b. Binder a b -> a -> b
subst Binder a b2
b2 a
v)

-- | Check if two bindings are equal.
eqBinder :: (MkFree m a, MonadNumbering m)
         => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool
eqBinder :: forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
(b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool
eqBinder b -> b -> m Bool
eq Binder a b
f Binder a b
g = do
  (Var m a
_, b
t, b
u) <- forall (m :: * -> *) a b1 b2.
(MkFree m a, MonadNumbering m) =>
Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
unbind2 Binder a b
f Binder a b
g
  b -> b -> m Bool
eq b
t b
u


-- | Smart constructor for 'Binder'.
buildBinder :: Var m a -> (a -> b) -> Binder a b
buildBinder :: forall (m :: * -> *) a b. Var m a -> (a -> b) -> Binder a b
buildBinder Var m a
x a -> b
body = forall a b. Text -> (a -> b) -> Binder a b
Binder (Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name) a -> b
body

-- | binding
bind :: (MkFree m a, MonadNumbering m)
        => Var m a -> Box m b -> Box m (Binder a b)
bind :: forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
Var m a -> Box m b -> Box m (Binder a b)
bind Var m a
x (Box'Closed b
t) = forall (m :: * -> *) a. a -> Box m a
Box'Closed forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Var m a -> (a -> b) -> Binder a b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const b
t
bind Var m a
x (Box'Env EnvVar m
vs Closure m b
t) =
  let vs' :: EnvVar m
vs' = forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key) EnvVar m
vs in if forall (t :: * -> *) a. Foldable t => t a -> Int
length EnvVar m
vs' forall a. Eq a => a -> a -> Bool
== Int
0
    then forall (m :: * -> *) a. a -> Box m a
Box'Closed forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Var m a -> (a -> b) -> Binder a b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$
      \a
arg -> forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m b
t forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton (Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key) (forall (m :: * -> *) a. MkFree m a => a -> AnyMkFree m
AnyMkFree a
arg)
    else forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env EnvVar m
vs' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (EnvMkFree m -> a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$
      \EnvMkFree m
ms -> forall (m :: * -> *) a b. Var m a -> (a -> b) -> Binder a b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$
      \a
arg -> forall (m :: * -> *) a. Closure m a -> EnvMkFree m -> a
unClosure Closure m b
t forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Var m a
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key) (forall (m :: * -> *) a. MkFree m a => a -> AnyMkFree m
AnyMkFree a
arg) EnvMkFree m
ms

boxBinder :: (MkFree m a, MonadNumbering m)
          => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))
boxBinder :: forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
(b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))
boxBinder b -> m (Box m b)
f Binder a b
b = do
  (Var m a
x, b
t) <- forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
Binder a b -> m (Var m a, b)
unbind Binder a b
b
  Box m b
ft <- b -> m (Box m b)
f b
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
(MkFree m a, MonadNumbering m) =>
Var m a -> Box m b -> Box m (Binder a b)
bind Var m a
x Box m b
ft