module Language.Lambda.SystemF.Eval
( evalExpr,
subGlobals,
betaReduce,
alphaConvert,
etaConvert,
freeVarsOf
) where
import Language.Lambda.Shared.Errors
import Language.Lambda.Shared.UniqueSupply (next)
import Language.Lambda.SystemF.Expression
import Language.Lambda.SystemF.State
import Control.Monad.Except (throwError)
import Prettyprinter
import RIO
import qualified RIO.Map as Map
evalExpr
:: (Pretty name, Ord name)
=> SystemFExpr name
-> Typecheck name (SystemFExpr name)
evalExpr :: forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalExpr = forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalTopLevel
evalTopLevel
:: (Pretty name, Ord name)
=> SystemFExpr name
-> Typecheck name (SystemFExpr name)
evalTopLevel :: forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalTopLevel (Let name
n SystemFExpr name
expr) = forall name. name -> SystemFExpr name -> SystemFExpr name
Let name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
expr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner)
evalTopLevel SystemFExpr name
expr = forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
expr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner
evalInner
:: (Pretty name, Ord name)
=> SystemFExpr name
-> Typecheck name (SystemFExpr name)
evalInner :: forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner (Abs name
n Ty name
ty SystemFExpr name
expr) = forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
n Ty name
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
expr
evalInner (App SystemFExpr name
e1 SystemFExpr name
e2) = forall name.
(Pretty name, Ord name) =>
SystemFExpr name
-> SystemFExpr name -> Typecheck name (SystemFExpr name)
evalApp SystemFExpr name
e1 SystemFExpr name
e2
evalInner (TyAbs name
n SystemFExpr name
expr) = forall name. name -> SystemFExpr name -> SystemFExpr name
TyAbs name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
expr
evalInner (TyApp SystemFExpr name
expr Ty name
ty) = forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Ty name -> Typecheck name (SystemFExpr name)
evalTyApp SystemFExpr name
expr Ty name
ty
evalInner (Let name
n SystemFExpr name
expr) = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> LambdaException
InvalidLet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall pretty. Pretty pretty => pretty -> Text
prettyPrint forall a b. (a -> b) -> a -> b
$ forall name. name -> SystemFExpr name -> SystemFExpr name
Let name
n SystemFExpr name
expr
evalInner SystemFExpr name
expr = forall (f :: * -> *) a. Applicative f => a -> f a
pure SystemFExpr name
expr
subGlobals :: Ord name => SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals :: forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
expr = forall name. Typecheck name (Globals name)
getGlobals forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map name (TypedExpr name)
-> StateT
(TypecheckState name) (Except LambdaException) (SystemFExpr name)
subGlobals'
where subGlobals' :: Map name (TypedExpr name)
-> StateT
(TypecheckState name) (Except LambdaException) (SystemFExpr name)
subGlobals' Map name (TypedExpr name)
globals' = case SystemFExpr name
expr of
Var name
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe SystemFExpr name
expr (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr) forall a b. (a -> b) -> a -> b
$ Map name (TypedExpr name)
globals' forall k a. Ord k => Map k a -> k -> Maybe a
Map.!? name
x
VarAnn name
x Ty name
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe SystemFExpr name
expr (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr) forall a b. (a -> b) -> a -> b
$ Map name (TypedExpr name)
globals' forall k a. Ord k => Map k a -> k -> Maybe a
Map.!? name
x
App SystemFExpr name
e1 SystemFExpr name
e2 -> forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
e2
Abs name
name Ty name
ty SystemFExpr name
expr'
| forall k a. Ord k => k -> Map k a -> Bool
Map.member name
name Map name (TypedExpr name)
globals' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SystemFExpr name
expr
| Bool
otherwise -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
Ord name =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
subGlobals SystemFExpr name
expr'
SystemFExpr name
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SystemFExpr name
expr
evalApp
:: (Pretty name, Ord name)
=> SystemFExpr name
-> SystemFExpr name
-> Typecheck name (SystemFExpr name)
evalApp :: forall name.
(Pretty name, Ord name) =>
SystemFExpr name
-> SystemFExpr name -> Typecheck name (SystemFExpr name)
evalApp SystemFExpr name
e1 SystemFExpr name
e2 = do
SystemFExpr name
e1' <- forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
e1
SystemFExpr name
e2' <- forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
e2
forall name.
(Ord name, Pretty name) =>
SystemFExpr name
-> SystemFExpr name -> Typecheck name (SystemFExpr name)
betaReduce SystemFExpr name
e1' SystemFExpr name
e2'
evalTyApp
:: (Pretty name, Ord name)
=> SystemFExpr name
-> Ty name
-> Typecheck name (SystemFExpr name)
evalTyApp :: forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Ty name -> Typecheck name (SystemFExpr name)
evalTyApp SystemFExpr name
expr Ty name
ty = case SystemFExpr name
expr of
TyAbs name
name SystemFExpr name
inner -> forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner forall a b. (a -> b) -> a -> b
$ forall name.
Eq name =>
Ty name -> name -> SystemFExpr name -> SystemFExpr name
substituteTyInExpr Ty name
ty name
name SystemFExpr name
inner
Abs name
name (TyForAll name
tyName Ty name
ty') SystemFExpr name
inner ->
forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name (forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
tyName Ty name
ty') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
inner
VarAnn name
name (TyForAll name
tyName Ty name
ty') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name. name -> Ty name -> SystemFExpr name
VarAnn name
name (forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
tyName Ty name
ty')
SystemFExpr name
_ -> forall name. SystemFExpr name -> Ty name -> SystemFExpr name
TyApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner SystemFExpr name
expr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty name
ty
betaReduce
:: (Ord name, Pretty name)
=> SystemFExpr name
-> SystemFExpr name
-> Typecheck name (SystemFExpr name)
betaReduce :: forall name.
(Ord name, Pretty name) =>
SystemFExpr name
-> SystemFExpr name -> Typecheck name (SystemFExpr name)
betaReduce SystemFExpr name
e1 SystemFExpr name
e2 = case SystemFExpr name
e1 of
App SystemFExpr name
e1' SystemFExpr name
e2' -> forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Ord name, Pretty name) =>
SystemFExpr name
-> SystemFExpr name -> Typecheck name (SystemFExpr name)
betaReduce SystemFExpr name
e1' SystemFExpr name
e2' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SystemFExpr name
e2
Abs name
n Ty name
_ SystemFExpr name
e1' -> do
SystemFExpr name
converted <- forall name.
(Ord name, Pretty name) =>
[name] -> SystemFExpr name -> Typecheck name (SystemFExpr name)
alphaConvert (forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
e2) SystemFExpr name
e1'
forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalInner forall a b. (a -> b) -> a -> b
$ forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
converted name
n SystemFExpr name
e2
Let name
_ SystemFExpr name
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError LambdaException
ImpossibleError
SystemFExpr name
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App SystemFExpr name
e1 SystemFExpr name
e2
alphaConvert
:: (Ord name, Pretty name)
=> [name]
-> SystemFExpr name
-> Typecheck name (SystemFExpr name)
alphaConvert :: forall name.
(Ord name, Pretty name) =>
[name] -> SystemFExpr name -> Typecheck name (SystemFExpr name)
alphaConvert [name]
freeVars (Abs name
name Ty name
ty SystemFExpr name
body) = do
[name]
uniques <- forall name. Typecheck name [name]
getVarUniques
name
nextName <- forall name (m :: * -> *).
(Ord name, MonadError LambdaException m) =>
[name] -> [name] -> m name
next [name]
freeVars [name]
uniques
forall name.
(Ord name, Pretty name) =>
name
-> Ty name
-> SystemFExpr name
-> [name]
-> name
-> Typecheck name (SystemFExpr name)
alphaConvertAbs name
name Ty name
ty SystemFExpr name
body [name]
freeVars name
nextName
alphaConvert [name]
_ SystemFExpr name
expr = forall (f :: * -> *) a. Applicative f => a -> f a
pure SystemFExpr name
expr
etaConvert :: Ord name => SystemFExpr name -> SystemFExpr name
etaConvert :: forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert (Abs name
name Ty name
ty SystemFExpr name
body) = case SystemFExpr name
body of
App SystemFExpr name
e1 (Var name
name')
| name
name forall a. Eq a => a -> a -> Bool
== name
name' -> forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
e1
| Bool
otherwise -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty (forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App (forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
e1) (forall name. name -> SystemFExpr name
Var name
name'))
body' :: SystemFExpr name
body'@Abs{}
| SystemFExpr name
body' forall a. Eq a => a -> a -> Bool
== SystemFExpr name
eta' -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty SystemFExpr name
body'
| Bool
otherwise -> forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert forall a b. (a -> b) -> a -> b
$ forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty SystemFExpr name
eta'
where eta' :: SystemFExpr name
eta' = forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
body'
SystemFExpr name
_ -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty forall a b. (a -> b) -> a -> b
$ forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
body
etaConvert (App SystemFExpr name
e1 SystemFExpr name
e2) = forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App (forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
e1) (forall name. Ord name => SystemFExpr name -> SystemFExpr name
etaConvert SystemFExpr name
e2)
etaConvert SystemFExpr name
expr = SystemFExpr name
expr
substitute
:: Eq name
=> SystemFExpr name
-> name
-> SystemFExpr name
-> SystemFExpr name
substitute :: forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
expr name
forName SystemFExpr name
inExpr
= case SystemFExpr name
expr of
(Var name
n)
| name
n forall a. Eq a => a -> a -> Bool
== name
forName -> SystemFExpr name
inExpr
| Bool
otherwise -> SystemFExpr name
expr
(VarAnn name
n Ty name
_)
| name
n forall a. Eq a => a -> a -> Bool
== name
forName -> SystemFExpr name
inExpr
| Bool
otherwise -> SystemFExpr name
expr
(Abs name
n Ty name
ty SystemFExpr name
body)
| name
n forall a. Eq a => a -> a -> Bool
== name
forName -> SystemFExpr name
expr
| Bool
otherwise -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
n Ty name
ty forall a b. (a -> b) -> a -> b
$ forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
body name
forName SystemFExpr name
inExpr
(App SystemFExpr name
e1 SystemFExpr name
e2) -> forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
e1) (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
e2)
(TyAbs name
n SystemFExpr name
body) -> forall name. name -> SystemFExpr name -> SystemFExpr name
TyAbs name
n forall a b. (a -> b) -> a -> b
$ forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
body name
forName SystemFExpr name
inExpr
(TyApp SystemFExpr name
body Ty name
ty) -> forall name. SystemFExpr name -> Ty name -> SystemFExpr name
TyApp (forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
body name
forName SystemFExpr name
inExpr) Ty name
ty
SystemFExpr name
_ -> SystemFExpr name
inExpr
where sub :: SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
expr' = forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
expr' name
forName SystemFExpr name
inExpr
substituteTyInExpr
:: Eq name
=> Ty name
-> name
-> SystemFExpr name
-> SystemFExpr name
substituteTyInExpr :: forall name.
Eq name =>
Ty name -> name -> SystemFExpr name -> SystemFExpr name
substituteTyInExpr Ty name
ty name
forName SystemFExpr name
inExpr
= case SystemFExpr name
inExpr of
VarAnn name
name Ty name
ty' -> forall name. name -> Ty name -> SystemFExpr name
VarAnn name
name (forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName Ty name
ty')
App SystemFExpr name
e1 SystemFExpr name
e2 -> forall name.
SystemFExpr name -> SystemFExpr name -> SystemFExpr name
App (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
e1) (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
e2)
Abs name
name Ty name
ty' SystemFExpr name
expr -> forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name (forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName Ty name
ty') (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
expr)
TyAbs name
name SystemFExpr name
expr -> forall name. name -> SystemFExpr name -> SystemFExpr name
TyAbs name
name (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
expr)
TyApp SystemFExpr name
expr Ty name
ty' -> forall name. SystemFExpr name -> Ty name -> SystemFExpr name
TyApp (SystemFExpr name -> SystemFExpr name
sub SystemFExpr name
expr) (forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName Ty name
ty')
SystemFExpr name
_ -> SystemFExpr name
inExpr
where sub :: SystemFExpr name -> SystemFExpr name
sub = forall name.
Eq name =>
Ty name -> name -> SystemFExpr name -> SystemFExpr name
substituteTyInExpr Ty name
ty name
forName
freeVarsOf
:: (Ord name, Pretty name)
=> SystemFExpr name
-> [name]
freeVarsOf :: forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf (Abs name
n Ty name
_ SystemFExpr name
expr) = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/=name
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf forall a b. (a -> b) -> a -> b
$ SystemFExpr name
expr
freeVarsOf (App SystemFExpr name
e1 SystemFExpr name
e2) = forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
e1 forall a. [a] -> [a] -> [a]
++ forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
e2
freeVarsOf (Var name
n) = [name
n]
freeVarsOf (VarAnn name
n Ty name
_) = [name
n]
freeVarsOf (Let name
_ SystemFExpr name
expr) = forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
expr
freeVarsOf (TyAbs name
_ SystemFExpr name
expr) = forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
expr
freeVarsOf (TyApp SystemFExpr name
expr Ty name
_) = forall name. (Ord name, Pretty name) => SystemFExpr name -> [name]
freeVarsOf SystemFExpr name
expr
alphaConvertAbs
:: (Ord name, Pretty name)
=> name
-> Ty name
-> SystemFExpr name
-> [name]
-> name
-> Typecheck name (SystemFExpr name)
alphaConvertAbs :: forall name.
(Ord name, Pretty name) =>
name
-> Ty name
-> SystemFExpr name
-> [name]
-> name
-> Typecheck name (SystemFExpr name)
alphaConvertAbs name
name Ty name
ty SystemFExpr name
body [name]
freeVars name
nextName
| name
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [name]
freeVars = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
nextName Ty name
ty (forall name.
Eq name =>
SystemFExpr name -> name -> SystemFExpr name -> SystemFExpr name
substitute SystemFExpr name
body name
name (forall name. name -> SystemFExpr name
Var name
nextName))
| Bool
otherwise = forall name.
name -> Ty name -> SystemFExpr name -> SystemFExpr name
Abs name
name Ty name
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name.
(Ord name, Pretty name) =>
[name] -> SystemFExpr name -> Typecheck name (SystemFExpr name)
alphaConvert [name]
freeVars SystemFExpr name
body