module Repl.SystemF (runSystemFRepl) where
import Language.Lambda.Shared.Errors (LambdaException())
import Language.Lambda.Shared.UniqueSupply (defaultUniques)
import Language.Lambda.SystemF
import Repl.Shared
import Data.Text (singleton)
import Data.Text.IO (putStrLn)
import RIO
import RIO.State
import RIO.Text (pack, unpack)
import System.Console.Repline
import Control.Monad.Except (ExceptT(..), runExceptT)
type EvalT name m
= StateT (TypecheckState name)
(ExceptT LambdaException m)
type Repl a = HaskelineT (EvalT Text IO) a
runSystemFRepl :: IO ()
runSystemFRepl
= void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState
where replOpts = mkReplOpts banner' (evalSystemF . pack) helpMsg
initialState = mkTypecheckState defaultUniques defaultTyUniques
banner' :: MultiLine -> Repl String
banner' _ = unpack <$> prompt (singleton upperLambda)
evalSystemF :: Text -> Repl ()
evalSystemF input = do
state' <- get
let res = runTypecheck (evalText input) state'
case res of
Left err -> liftIO . putStrLn . textDisplay $ err
Right (res', newState) -> do
put newState
liftIO . putStrLn . prettyPrint $ res'
helpMsg :: Text
helpMsg = " Commands available: \n"
<> " <expression> Evaluate <expression>\n"
<> " :help, :h Show this help\n"
<> " :quit, :q Quit\n\n"
<> " Expressions can take the form:\n"
<> " x variable\n"
<> " x:T type annotated variable\n"
<> " \\x:T. t abstraction\n"
<> " f x function application\n"
<> " \\X. t type abstraction\n"
<> " x [T] type application\n"
<> " let x = t global binding\n\n"
<> " Types can take the form:\n"
<> " T type variable\n"
<> " T -> T type of functions\n"
<> " forall X. T universal type\n\n"
<> " Examples of valid expressions:\n"
<> " x\n"
<> " \\x:T. x\n"
<> " (\\x:T. x) y:T\n"
<> " \\X. \\x:X. x\n"
<> " \\x:(forall T. T). x\n"
<> " (\\n:((T->T)->T->T) f:(T->T) x:T. f (n f x)) (\\f:(T->T) x:T. x)\n"