{-# 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
-- ** Variable
  , var'Key
  , var'Name
  , var'mkFree
  , var'Box
  , nameOf
  , boxVar
  , newVar
  , copyVar
  , isClosed
  , occur
-- ** Box
  , unbox
  , box
  , apBox
  , boxApply
  , boxApply2
  , boxApply3
  , boxApply4
  , boxPair
  , boxTriple
  , boxT
  , boxList
  , boxJoin
-- * Variable binding
  , Binder
  , binder'Name
  , binder'mkFree
  , binder'Body
  , subst
  , buildBinder
  , bind
  , unbind
  , unbind2
  , eqBinder
  , boxBinder
  , bindApply
-- * List
-- * Variable list
  , VarList
  , varList'Keys
  , varList'Names
  , varList'Boxes
  , namesOf
  , boxVarList
  , newVarList
  , copyVarList
-- * Binder for list
  , BinderList
  , binderList'Names
  , binderList'Body
  , binderList'mkFree
  , binderList'Arity
  , substList
  , eqBinderList
  , bindList
  , unbindList
  , unbind2List
  , boxBinderList
  , bindListApply
  ) where

import Control.Lens
import Control.Monad (join)
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 -> Var m a -> m a
_varBody'mkFree :: Var m a -> m a
  , 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)

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

instance Functor m => 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. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m a
cla

instance Applicative m => Applicative (Closure m) where
  pure :: forall a. a -> Closure m a
pure a
a = forall (m :: * -> *) a. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure 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. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvOne m
env -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m (a -> b)
clf EnvOne m
env forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m a
cla EnvOne m
env

closureJoin :: Monad m => Closure m (m a) -> Closure m a
closureJoin :: forall (m :: * -> *) a. Monad m => Closure m (m a) -> Closure m a
closureJoin Closure m (m a)
cl = forall (m :: * -> *) a. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvOne m
env -> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m (m a)
cl EnvOne 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'mkFree :: Lens' (Var m a) (Var m a -> m a)
var'mkFree :: forall (m :: * -> *) a. Lens' (Var m a) (Var m a -> m a)
var'mkFree = 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) (Var m a -> m a)
varBody'mkFree
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. Lens' (VarBody 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 :: MonadNumbering m => Text -> (Var m a -> m a) -> m (Var m a)
newVar :: forall (m :: * -> *) a.
MonadNumbering m =>
Text -> (Var m a -> m a) -> m (Var m a)
newVar Text
name Var m a -> m a
mkFree = do
  Numbering m
i <- forall (m :: * -> *). MonadNumbering m => m (Numbering m)
numbering
  forall (m :: * -> *) a.
MonadNumbering m =>
Numbering m -> Text -> (Var m a -> m a) -> m (Var m a)
buildVar Numbering m
i Text
name Var m a -> m a
mkFree

copyVar :: MonadNumbering m => Var m b -> (Var m a -> m a) -> m (Var m a)
copyVar :: forall (m :: * -> *) b a.
MonadNumbering m =>
Var m b -> (Var m a -> m a) -> m (Var m a)
copyVar Var m b
x Var m a -> m a
mkFree = forall (m :: * -> *) a.
MonadNumbering m =>
Numbering m -> Text -> (Var m a -> m a) -> m (Var m a)
buildVar (Var m b
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key) (Var m b
x forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name) Var m a -> m a
mkFree

buildVar :: MonadNumbering m => Numbering m -> Text -> (Var m a -> m a)
         -> m (Var m a)
buildVar :: forall (m :: * -> *) a.
MonadNumbering m =>
Numbering m -> Text -> (Var m a -> m a) -> m (Var m a)
buildVar Numbering m
i Text
name Var m a -> m a
mkFree =
  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. Var m a -> AnyVar m
AnyVar Var m a
x)
                (forall (m :: * -> *) a. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvOne m
env ->
                  let f :: AnyOne -> f a
f (AnyOne a
y) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce a
y
                   in forall {f :: * -> *} {a}. Applicative f => AnyOne -> f a
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 EnvOne 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 -> (Var m a -> m a) -> Box m a -> VarBody m a
VarBody Text
name Var m a -> m a
mkFree Box m a
b
   in 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 m => 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 :: * -> *} {a} {a}.
Applicative m =>
Closure m (a -> a) -> a -> Closure m a
appClosure Closure m (a -> b)
tf a
a)
   where
    appClosure :: Closure m (a -> a) -> a -> Closure m a
appClosure Closure m (a -> a)
clf a
x = forall (m :: * -> *) a. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$ \EnvOne m
env -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m (a -> a)
clf EnvOne m
env forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
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. Monad m => Box m a -> m a
unbox :: forall (m :: * -> *) a. Monad m => Box m a -> m a
unbox (Box'Closed a
t) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t
unbox (Box'Env EnvVar m
env Closure m a
cl) = forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m a
cl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {m :: * -> *}. Functor m => AnyVar m -> m AnyOne
f EnvVar m
env
 where
  f :: AnyVar m -> m AnyOne
f (AnyVar Var m a
x) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> AnyOne
AnyOne 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) (Var m a -> m a)
var'mkFree forall a b. (a -> b) -> a -> b
$ 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 :: Functor m => (a -> b) -> Box m a -> Box m b
boxApply :: forall (m :: * -> *) a b.
Functor 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
boxList :: MonadNumbering m => [Box m a] -> Box m [a]
boxList :: forall (m :: * -> *) a. MonadNumbering m => [Box m a] -> Box m [a]
boxList = forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA
boxJoin :: MonadNumbering m => Box m (m a) -> m (Box m a)
boxJoin :: forall (m :: * -> *) a.
MonadNumbering m =>
Box m (m a) -> m (Box m a)
boxJoin (Box'Closed m a
ma) = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. a -> Box m a
Box'Closed forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m a
ma
boxJoin (Box'Env EnvVar m
env Closure m (m a)
cl) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. EnvVar m -> Closure m a -> Box m a
Box'Env EnvVar m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => Closure m (m a) -> Closure m a
closureJoin Closure m (m a)
cl


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

$(makeLenses ''Binder)

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

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

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

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


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

-- | binding
bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b)
bind :: forall (m :: * -> *) a b.
MonadNumbering m =>
Var m a -> Box m b -> Box m (Binder a m 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 -> m b) -> Binder a m b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> m b) -> Binder a m b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$
      \a
arg -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> 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 a. a -> AnyOne
AnyOne 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. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$
      \EnvOne m
ms -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Var m a -> (a -> m b) -> Binder a m b
buildBinder Var m a
x forall a b. (a -> b) -> a -> b
$
      \a
arg -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> 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 a. a -> AnyOne
AnyOne a
arg) EnvOne m
ms

boxBinder :: MonadNumbering m
          => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b))
boxBinder :: forall (m :: * -> *) b a.
MonadNumbering m =>
(b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b))
boxBinder b -> m (Box m b)
f Binder a m b
b = do
  (Var m a
x, b
t) <- forall (m :: * -> *) a b.
MonadNumbering m =>
Binder a m b -> m (Var m a, b)
unbind Binder a m 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.
MonadNumbering m =>
Var m a -> Box m b -> Box m (Binder a m b)
bind Var m a
x Box m b
ft

bindApply :: MonadNumbering m => Box m (Binder a m b) -> Box m a -> m (Box m b)
bindApply :: forall (m :: * -> *) a b.
MonadNumbering m =>
Box m (Binder a m b) -> Box m a -> m (Box m b)
bindApply Box m (Binder a m b)
b Box m a
arg = forall (m :: * -> *) a.
MonadNumbering m =>
Box m (m a) -> m (Box m a)
boxJoin forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *) b. Binder a m b -> a -> m b
subst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Box m (Binder a m b)
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m a
arg


type VarList m a = [Var m a]

varList'Keys :: Getter (VarList m a) [Numbering m]
varList'Keys :: forall (m :: * -> *) a. Getter (VarList m a) [Numbering m]
varList'Keys = forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall (m :: * -> *) a. Lens' (Var m a) (Numbering m)
var'Key
varList'Names :: Getter (VarList m a) [Text]
varList'Names :: forall (m :: * -> *) a. Getter (VarList m a) [Text]
varList'Names = forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name
varList'Boxes :: Getter (VarList m a) [Box m a]
varList'Boxes :: forall (m :: * -> *) a. Getter (VarList m a) [Box m a]
varList'Boxes = forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall (m :: * -> *) a. Lens' (Var m a) (Box m a)
var'Box

-- | The names of variables.
namesOf :: VarList m a -> [Text]
namesOf :: forall (m :: * -> *) a. VarList m a -> [Text]
namesOf = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall (m :: * -> *) a. Lens' (Var m a) Text
var'Name

-- | Smart constructor for a list of 'Box'.
boxVarList :: VarList m a -> [Box m a]
boxVarList :: forall (m :: * -> *) a. VarList m a -> [Box m a]
boxVarList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall (m :: * -> *) a. Lens' (Var m a) (Box m a)
var'Box

-- | Create new variables with given names.
newVarList :: MonadNumbering m => [Text] -> (Var m a -> m a) -> m (VarList m a)
newVarList :: forall (m :: * -> *) a.
MonadNumbering m =>
[Text] -> (Var m a -> m a) -> m (VarList m a)
newVarList [Text]
names Var m a -> m a
mkFree = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [Text]
names forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
MonadNumbering m =>
Text -> (Var m a -> m a) -> m (Var m a)
newVar Var m a -> m a
mkFree

copyVarList :: MonadNumbering m => VarList m b -> (Var m a -> m a) -> m (VarList m a)
copyVarList :: forall (m :: * -> *) b a.
MonadNumbering m =>
VarList m b -> (Var m a -> m a) -> m (VarList m a)
copyVarList VarList m b
xs Var m a -> m a
mkFree = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse VarList m b
xs forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) b a.
MonadNumbering m =>
Var m b -> (Var m a -> m a) -> m (Var m a)
copyVar Var m a -> m a
mkFree


-- | Essentially, @BinderList a m b@ means @[a] -> m b@.
data BinderList a m b = BinderList
  { forall a (m :: * -> *) b. BinderList a m b -> [Text]
_binderList'Names :: [Text]
  , forall a (m :: * -> *) b. BinderList a m b -> Var m a -> m a
_binderList'mkFree :: Var m a -> m a
  , forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
_binderList'Body :: [a] -> m b
  }

$(makeLenses ''BinderList)

binderList'Arity :: Getter (BinderList a m b) Int
binderList'Arity :: forall a (m :: * -> *) b. Getter (BinderList a m b) Int
binderList'Arity = forall a (m :: * -> *) b. Lens' (BinderList a m b) [Text]
binderList'Names forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to forall (t :: * -> *) a. Foldable t => t a -> Int
length

-- | Variable substitution.
substList :: BinderList a m b -> [a] -> m b
substList :: forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
substList BinderList a m b
ba = BinderList a m b
ba forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b b.
Lens
  (BinderList a m b) (BinderList a m b) ([a] -> m b) ([a] -> m b)
binderList'Body

-- | unbinding
unbindList :: MonadNumbering m => BinderList a m b -> m (VarList m a, b)
unbindList :: forall (m :: * -> *) a b.
MonadNumbering m =>
BinderList a m b -> m (VarList m a, b)
unbindList BinderList a m b
ba = do
  let mkFree :: Var m a -> m a
mkFree = BinderList a m b
ba forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Lens' (BinderList a m b) (Var m a -> m a)
binderList'mkFree
  VarList m a
xs <- forall (m :: * -> *) a.
MonadNumbering m =>
[Text] -> (Var m a -> m a) -> m (VarList m a)
newVarList (BinderList a m b
ba forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Lens' (BinderList a m b) [Text]
binderList'Names) Var m a -> m a
mkFree
  b
y <- forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
substList BinderList a m b
ba forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var m a -> m a
mkFree VarList m a
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return (VarList m a
xs, b
y)

unbind2List :: MonadNumbering m
             => BinderList a m b1 -> BinderList a m b2
             -> m (VarList m a, b1, b2)
unbind2List :: forall (m :: * -> *) a b1 b2.
MonadNumbering m =>
BinderList a m b1 -> BinderList a m b2 -> m (VarList m a, b1, b2)
unbind2List BinderList a m b1
ba1 BinderList a m b2
ba2 = do
  let mkFree :: Var m a -> m a
mkFree = BinderList a m b1
ba1 forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Lens' (BinderList a m b) (Var m a -> m a)
binderList'mkFree
  VarList m a
xs <- forall (m :: * -> *) a.
MonadNumbering m =>
[Text] -> (Var m a -> m a) -> m (VarList m a)
newVarList (BinderList a m b1
ba1 forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Lens' (BinderList a m b) [Text]
binderList'Names) Var m a -> m a
mkFree
  [a]
vs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var m a -> m a
mkFree VarList m a
xs
  b1
y1 <- forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
substList BinderList a m b1
ba1 [a]
vs
  b2
y2 <- forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
substList BinderList a m b2
ba2 [a]
vs
  forall (m :: * -> *) a. Monad m => a -> m a
return (VarList m a
xs, b1
y1, b2
y2)

-- | Check if two bindings are equal.
eqBinderList :: MonadNumbering m
              => (b -> b -> m Bool)
              -> BinderList a m b -> BinderList a m b -> m Bool
eqBinderList :: forall (m :: * -> *) b a.
MonadNumbering m =>
(b -> b -> m Bool)
-> BinderList a m b -> BinderList a m b -> m Bool
eqBinderList b -> b -> m Bool
eq BinderList a m b
f BinderList a m b
g =
  if BinderList a m b
f forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Getter (BinderList a m b) Int
binderList'Arity forall a. Eq a => a -> a -> Bool
/= BinderList a m b
g forall s a. s -> Getting a s a -> a
^. forall a (m :: * -> *) b. Getter (BinderList a m b) Int
binderList'Arity
    then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    else do
      (VarList m a
_, b
t, b
u) <- forall (m :: * -> *) a b1 b2.
MonadNumbering m =>
BinderList a m b1 -> BinderList a m b2 -> m (VarList m a, b1, b2)
unbind2List BinderList a m b
f BinderList a m b
g
      b -> b -> m Bool
eq b
t b
u

-- | Smart constructor for 'BinderList.
buildBinderList :: VarList m a -> ([a] -> m b) -> BinderList a m b
buildBinderList :: forall (m :: * -> *) a b.
VarList m a -> ([a] -> m b) -> BinderList a m b
buildBinderList VarList m a
xs [a] -> m b
body =
  forall a (m :: * -> *) b.
[Text] -> (Var m a -> m a) -> ([a] -> m b) -> BinderList a m b
BinderList (VarList m a
xs forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Getter (VarList m a) [Text]
varList'Names) (forall a. [a] -> a
head VarList m a
xs forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Lens' (Var m a) (Var m a -> m a)
var'mkFree) [a] -> m b
body

deleteList :: Ord k => [k] -> M.Map k a -> M.Map k a
deleteList :: forall k a. Ord k => [k] -> Map k a -> Map k a
deleteList = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a b. (a -> b) -> a -> b
$ \Map k a
m k
k -> forall k a. Ord k => k -> Map k a -> Map k a
M.delete k
k Map k a
m
insertList :: Ord k => [k] -> [a] -> M.Map k a -> M.Map k a
insertList :: forall k a. Ord k => [k] -> [a] -> Map k a -> Map k a
insertList [k]
ks [a]
xs Map k a
m = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {k} {a}. Ord k => Map k a -> (k, a) -> Map k a
f Map k a
m forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [k]
ks [a]
xs
 where
  f :: Map k a -> (k, a) -> Map k a
f Map k a
n (k
k, a
x) = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k a
x Map k a
n
zipList :: Ord k => [k] -> [a] -> M.Map k a
zipList :: forall k a. Ord k => [k] -> [a] -> Map k a
zipList [k]
ks [a]
xs = forall k a. Ord k => [k] -> [a] -> Map k a -> Map k a
insertList [k]
ks [a]
xs forall k a. Map k a
M.empty

-- | binding
bindList :: MonadNumbering m
          => VarList m a -> Box m b -> Box m (BinderList a m b)
bindList :: forall (m :: * -> *) a b.
MonadNumbering m =>
VarList m a -> Box m b -> Box m (BinderList a m b)
bindList VarList m a
xs (Box'Closed b
t) = forall (m :: * -> *) a. a -> Box m a
Box'Closed forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
VarList m a -> ([a] -> m b) -> BinderList a m b
buildBinderList VarList m a
xs forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return b
t
bindList VarList m a
xs (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
deleteList (VarList m a
xs forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Getter (VarList m a) [Numbering m]
varList'Keys) 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.
VarList m a -> ([a] -> m b) -> BinderList a m b
buildBinderList VarList m a
xs forall a b. (a -> b) -> a -> b
$
      \[a]
args -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> m a
unClosure Closure m b
t forall a b. (a -> b) -> a -> b
$
      forall k a. Ord k => [k] -> [a] -> Map k a
zipList (VarList m a
xs forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Getter (VarList m a) [Numbering m]
varList'Keys) (forall a. a -> AnyOne
AnyOne forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
args)
    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. (EnvOne m -> m a) -> Closure m a
Closure forall a b. (a -> b) -> a -> b
$
      \EnvOne m
ms -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
VarList m a -> ([a] -> m b) -> BinderList a m b
buildBinderList VarList m a
xs forall a b. (a -> b) -> a -> b
$
      \[a]
args -> forall (m :: * -> *) a. Closure m a -> EnvOne m -> 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
insertList (VarList m a
xs forall s a. s -> Getting a s a -> a
^. forall (m :: * -> *) a. Getter (VarList m a) [Numbering m]
varList'Keys) (forall a. a -> AnyOne
AnyOne forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
args) EnvOne m
ms

boxBinderList :: MonadNumbering m
               => (b -> m (Box m b)) -> BinderList a m b
               -> m (Box m (BinderList a m b))
boxBinderList :: forall (m :: * -> *) b a.
MonadNumbering m =>
(b -> m (Box m b))
-> BinderList a m b -> m (Box m (BinderList a m b))
boxBinderList b -> m (Box m b)
f BinderList a m b
b = do
  (VarList m a
xs, b
t) <- forall (m :: * -> *) a b.
MonadNumbering m =>
BinderList a m b -> m (VarList m a, b)
unbindList BinderList a m 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.
MonadNumbering m =>
VarList m a -> Box m b -> Box m (BinderList a m b)
bindList VarList m a
xs Box m b
ft

bindListApply :: MonadNumbering m
              => Box m (BinderList a m b) -> Box m [a] -> m (Box m b)
bindListApply :: forall (m :: * -> *) a b.
MonadNumbering m =>
Box m (BinderList a m b) -> Box m [a] -> m (Box m b)
bindListApply Box m (BinderList a m b)
b Box m [a]
args = forall (m :: * -> *) a.
MonadNumbering m =>
Box m (m a) -> m (Box m a)
boxJoin forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *) b. BinderList a m b -> [a] -> m b
substList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Box m (BinderList a m b)
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Box m [a]
args