105 lines
2.6 KiB
Haskell
105 lines
2.6 KiB
Haskell
module Frontend where
|
|
|
|
import Builtins
|
|
import Code (Interp(..))
|
|
import Control.Monad (when)
|
|
import Control.Monad.IO.Class (liftIO)
|
|
import Control.Monad.Trans.Class (lift)
|
|
import Control.Monad.Trans.Except (except, runExceptT)
|
|
import Control.Monad.Trans.State.Lazy (evalStateT, gets, modify)
|
|
import qualified Data.Map as M
|
|
import Env (PrlgEnv)
|
|
import qualified IR
|
|
import qualified Interpreter as I
|
|
import Load
|
|
( compile
|
|
, intern
|
|
, loadExpansion
|
|
, processInput
|
|
, queryExpansion
|
|
, shunt
|
|
)
|
|
import System.Console.Haskeline
|
|
import qualified Text.Pretty.Simple as Ppr
|
|
|
|
ppr :: Show a => a -> PrlgEnv ()
|
|
ppr x =
|
|
liftIO $
|
|
Ppr.pPrintOpt
|
|
Ppr.CheckColorTty
|
|
Ppr.defaultOutputOptionsDarkBg
|
|
{ Ppr.outputOptionsCompactParens = True
|
|
, Ppr.outputOptionsIndentAmount = 2
|
|
, Ppr.outputOptionsPageWidth = 80
|
|
}
|
|
x
|
|
|
|
-- the signature of this is too ugly to include here
|
|
handleError m = do
|
|
res <- runExceptT m
|
|
case res of
|
|
Left err -> do
|
|
lift $ outputStrLn err
|
|
modify $ \s -> s {cmdq = []}
|
|
_ -> pure ()
|
|
|
|
processCmd precompileHook ast' = do
|
|
ast <- shunt ast'
|
|
code <- lift $ intern ast >>= precompileHook >>= compile
|
|
lift (I.prove code) >>= except
|
|
|
|
interpreterStart :: PrlgEnv ()
|
|
interpreterStart = do
|
|
addPrelude
|
|
interpreterLoop True
|
|
|
|
interpreterLoop :: Bool -> PrlgEnv ()
|
|
interpreterLoop queryMode = do
|
|
q <- gets cmdq
|
|
case q of
|
|
[] -> do
|
|
minput <-
|
|
lift $
|
|
getInputLine
|
|
(if queryMode
|
|
then "prlg? "
|
|
else "prlg |- ")
|
|
case minput of
|
|
Nothing -> return ()
|
|
Just "." -> interpreterLoop (not queryMode)
|
|
Just input -> do
|
|
handleError $ processInput "<user input>" queryMode input
|
|
interpreterLoop queryMode
|
|
((mode, ast):asts) -> do
|
|
modify $ \s -> s {cmdq = asts}
|
|
handleError $ do
|
|
resOK <-
|
|
processCmd
|
|
(if mode
|
|
then queryExpansion
|
|
else loadExpansion)
|
|
ast
|
|
finished <- lift $ gets (null . cmdq)
|
|
when finished . lift . lift . outputStrLn $
|
|
case (resOK, queryMode) of
|
|
(True, True) -> "yes."
|
|
(False, True) -> "no proof."
|
|
(True, False) -> "ok."
|
|
(False, False) -> "rejected."
|
|
interpreterLoop queryMode
|
|
|
|
interpreter :: InputT IO ()
|
|
interpreter =
|
|
evalStateT
|
|
interpreterStart
|
|
(Interp
|
|
{ defs = M.empty
|
|
, cur = error "no cur"
|
|
, cho = []
|
|
, ops = []
|
|
, opstash = []
|
|
, macrostash = []
|
|
, strtable = IR.emptystrtable
|
|
, cmdq = []
|
|
})
|