module Frontend where import Builtins import qualified Code import qualified Compiler as C import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.State.Lazy import Data.Foldable (traverse_) import qualified Data.Map as M import Env import qualified IR import qualified Interpreter as I import qualified Parser as P import System.Console.Haskeline import qualified Text.Megaparsec as MP import Text.Pretty.Simple ppr :: Show a => a -> PrlgEnv () ppr x = liftIO $ pPrintOpt CheckColorTty defaultOutputOptionsDarkBg { outputOptionsCompactParens = True , outputOptionsIndentAmount = 2 , outputOptionsPageWidth = 80 } x interpret :: String -> PrlgEnv Bool interpret = (>> return True) . lex where lex input = do case MP.parse P.lexPrlg "-" input of Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle) Right toks -> parse toks parse toks = do case MP.parse P.parsePrlg "-" toks of Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle) Right asts -> traverse_ shunt asts shunt ast = do o <- gets ops case P.shuntPrlg o ast of Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err Right prlg -> intern prlg intern prlgs = do prlgi <- withStrTable $ \st -> C.internPrlg st prlgs underscore <- findAtom "_" prlgv <- withStrTable $ \st -> (st, C.variablizePrlg underscore (C.varIds st prlgi) prlgi) compile prlgv compile prlgv = do commaId <- findStruct "," 2 let code = C.seqGoals $ C.compileGoals commaId prlgv execute code execute code = do ds <- gets defs let (_, res) = I.prove code ds case res of Left err -> liftIO $ putStrLn err Right res -> liftIO $ putStrLn $ if res then "yes." else "no proof." interpreterStart :: PrlgEnv () interpreterStart = do addBuiltins interpreterLoop interpreterLoop :: PrlgEnv () interpreterLoop = do minput <- lift $ getInputLine "prlg> " case minput of Nothing -> return () Just input -> do continue <- interpret input if continue then interpreterLoop else return () interpreter :: InputT IO () interpreter = evalStateT interpreterStart (PrlgState {defs = M.empty, ops = [], strtable = IR.emptystrtable})