{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Binder
( MonadNumbering(..)
, Var
, Box
, MkFree(..)
, var'Key
, var'Name
, var'Box
, nameOf
, boxVar
, newVar
, isClosed
, occur
, unbox
, box
, apBox
, boxApply
, boxApply2
, boxApply3
, boxApply4
, boxPair
, boxTriple
, boxT
, 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
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 -> Box m a
_varBody'Box :: Box m a
}
data Box m a
= Box'Closed a
| Box'Env (EnvVar m) (Closure m a)
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
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 :: 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
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 (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)
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
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)
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
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)
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
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
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