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

-- | Evaluates an expression
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

-- | Evaluates a top-level expression
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

-- | Evaluates a non top-level expression. Does NOT support Lets
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