module Language.Lambda.SystemF (
  evalText,
  typecheckText,
  runEvalText,
  runTypecheckText,
  execEvalText,
  execTypecheckText,
  unsafeExecEvalText,
  unsafeExecTypecheckText,
  defaultUniques,
  defaultTyUniques,
  mkState,

  module Language.Lambda.SystemF.Expression,
  module Language.Lambda.SystemF.Parser,
  module Language.Lambda.SystemF.State
  ) where

import Language.Lambda.Shared.Errors
import Language.Lambda.Shared.UniqueSupply (defaultUniques, defaultTyUniques)
import Language.Lambda.SystemF.Eval (evalExpr)
import Language.Lambda.SystemF.Expression
import Language.Lambda.SystemF.Parser
import Language.Lambda.SystemF.State
import Language.Lambda.SystemF.TypeCheck

import Control.Monad.Except
import RIO
import qualified RIO.Text as Text
import qualified RIO.Map as Map

evalText
  :: Text
  -> Typecheck Text (TypedExpr Text)
evalText :: Text -> Typecheck Text (TypedExpr Text)
evalText = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {a}.
ParseError
-> StateT (TypecheckState Text) (Except LambdaException) a
throwParseError SystemFExpr Text -> Typecheck Text (TypedExpr Text)
processExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either ParseError (SystemFExpr Text)
parseExpr
    where throwParseError :: ParseError
-> StateT (TypecheckState Text) (Except LambdaException) a
throwParseError = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> LambdaException
ParseError forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

typecheckText
  :: Text
  -> Typecheck Text (Ty Text)
typecheckText :: Text -> Typecheck Text (Ty Text)
typecheckText = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {a}.
ParseError
-> StateT (TypecheckState Text) (Except LambdaException) a
throwParseError forall name.
(Ord name, Pretty name) =>
SystemFExpr name -> Typecheck name (Ty name)
typecheck forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either ParseError (SystemFExpr Text)
parseExpr
    where throwParseError :: ParseError
-> StateT (TypecheckState Text) (Except LambdaException) a
throwParseError = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> LambdaException
ParseError forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

runEvalText
  :: Text
  -> Globals Text
  -> Either LambdaException (TypedExpr Text, TypecheckState Text)
runEvalText :: Text
-> Globals Text
-> Either LambdaException (TypedExpr Text, TypecheckState Text)
runEvalText Text
input Globals Text
globals' = forall name result.
Typecheck name result
-> TypecheckState name
-> Either LambdaException (result, TypecheckState name)
runTypecheck (Text -> Typecheck Text (TypedExpr Text)
evalText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

runTypecheckText
  :: Text
  -> Globals Text
  -> Either LambdaException (Ty Text, TypecheckState Text)
runTypecheckText :: Text
-> Globals Text
-> Either LambdaException (Ty Text, TypecheckState Text)
runTypecheckText Text
input Globals Text
globals'
  = forall name result.
Typecheck name result
-> TypecheckState name
-> Either LambdaException (result, TypecheckState name)
runTypecheck (Text -> Typecheck Text (Ty Text)
typecheckText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

execEvalText
  :: Text
  -> Globals Text
  -> Either LambdaException (TypedExpr Text)
execEvalText :: Text -> Globals Text -> Either LambdaException (TypedExpr Text)
execEvalText Text
input Globals Text
globals'
  = forall name result.
Typecheck name result
-> TypecheckState name -> Either LambdaException result
execTypecheck (Text -> Typecheck Text (TypedExpr Text)
evalText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

execTypecheckText
  :: Text
  -> Globals Text
  -> Either LambdaException (Ty Text)
execTypecheckText :: Text -> Globals Text -> Either LambdaException (Ty Text)
execTypecheckText Text
input Globals Text
globals'
  = forall name result.
Typecheck name result
-> TypecheckState name -> Either LambdaException result
execTypecheck (Text -> Typecheck Text (Ty Text)
typecheckText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

unsafeExecEvalText
  :: Text
  -> Globals Text
  -> TypedExpr Text
unsafeExecEvalText :: Text -> Globals Text -> TypedExpr Text
unsafeExecEvalText Text
input Globals Text
globals'
  = forall name result.
Typecheck name result -> TypecheckState name -> result
unsafeExecTypecheck (Text -> Typecheck Text (TypedExpr Text)
evalText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

unsafeExecTypecheckText
  :: Text
  -> Globals Text
  -> Ty Text
unsafeExecTypecheckText :: Text -> Globals Text -> Ty Text
unsafeExecTypecheckText Text
input Globals Text
globals'
  = forall name result.
Typecheck name result -> TypecheckState name -> result
unsafeExecTypecheck (Text -> Typecheck Text (Ty Text)
typecheckText Text
input) (Globals Text -> TypecheckState Text
mkState Globals Text
globals')

mkState :: Globals Text -> TypecheckState Text
mkState :: Globals Text -> TypecheckState Text
mkState Globals Text
globals' = forall name.
Globals name -> [name] -> [name] -> TypecheckState name
TypecheckState Globals Text
globals' [Text]
defaultUniques [Text]
defaultTyUniques

processExpr :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
processExpr :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
processExpr (Let Text
n SystemFExpr Text
expr) = SystemFExpr Text -> Typecheck Text (TypedExpr Text)
tcAndEval SystemFExpr Text
expr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> TypedExpr Text -> Typecheck Text (TypedExpr Text)
addBinding Text
n
processExpr SystemFExpr Text
expr = SystemFExpr Text -> Typecheck Text (TypedExpr Text)
tcAndEval SystemFExpr Text
expr

tcAndEval :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
tcAndEval :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
tcAndEval SystemFExpr Text
expr = do
  Ty Text
ty <- forall name.
(Ord name, Pretty name) =>
SystemFExpr name -> Typecheck name (Ty name)
typecheck SystemFExpr Text
expr
  SystemFExpr Text
reduced <- forall name.
(Pretty name, Ord name) =>
SystemFExpr name -> Typecheck name (SystemFExpr name)
evalExpr SystemFExpr Text
expr

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name. SystemFExpr name -> Ty name -> TypedExpr name
TypedExpr SystemFExpr Text
reduced Ty Text
ty

addBinding :: Text -> TypedExpr Text -> Typecheck Text (TypedExpr Text)
addBinding :: Text -> TypedExpr Text -> Typecheck Text (TypedExpr Text)
addBinding Text
name TypedExpr Text
expr = forall name. (Globals name -> Globals name) -> Typecheck name ()
modifyGlobals (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name TypedExpr Text
expr) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypedExpr Text
expr