{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Binder
( MonadNumbering(..)
, Var
, Box
, var'Key
, var'Name
, var'mkFree
, var'Box
, nameOf
, boxVar
, newVar
, copyVar
, isClosed
, occur
, unbox
, box
, apBox
, boxApply
, boxApply2
, boxApply3
, boxApply4
, boxPair
, boxTriple
, boxT
, boxList
, boxJoin
, Binder
, binder'Name
, binder'mkFree
, binder'Body
, subst
, buildBinder
, bind
, unbind
, unbind2
, eqBinder
, boxBinder
, bindApply
, VarList
, varList'Keys
, varList'Names
, varList'Boxes
, namesOf
, boxVarList
, newVarList
, copyVarList
, 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
class (Monad m, Ord (Numbering m)) => MonadNumbering m where
type Numbering m :: Type
numbering :: m (Numbering 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
}
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
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
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
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
isClosed :: Box m a -> Bool
isClosed :: forall (m :: * -> *) a. Box m a -> Bool
isClosed Box'Closed{} = Bool
True
isClosed Box'Env{} = Bool
False
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)
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
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)
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
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)
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
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
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
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
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
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
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
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
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)
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
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
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