Mirek Kratochvil
0092723895
btw we triggered a ghc bug here with iscallTok in parser. Apparently it kills `call` for whichever reason. New ghc solved it.
93 lines
2.2 KiB
Haskell
93 lines
2.2 KiB
Haskell
module Frontend where
|
|
|
|
import Builtins
|
|
import Code (Interp(..))
|
|
import CodeLens
|
|
import Control.Monad (when)
|
|
import Control.Monad.Trans.Class (lift)
|
|
import Control.Monad.Trans.Except (except, runExceptT)
|
|
import Control.Monad.Trans.State.Lazy (evalStateT)
|
|
import qualified Data.Map as M
|
|
import Env (PrlgEnv)
|
|
import qualified IR
|
|
import qualified Interpreter as I
|
|
import Lens.Micro.Mtl
|
|
import Load
|
|
( compile
|
|
, intern
|
|
, loadExpansion
|
|
, processInput
|
|
, queryExpansion
|
|
, shunt
|
|
)
|
|
import System.Console.Haskeline
|
|
|
|
-- 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
|
|
cmdq .= []
|
|
_ -> (pure () :: PrlgEnv ()) --prevents ambiguity
|
|
|
|
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 <- use 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
|
|
cmdq .= asts
|
|
handleError $ do
|
|
resOK <-
|
|
processCmd
|
|
(if mode
|
|
then queryExpansion
|
|
else loadExpansion)
|
|
ast
|
|
finished <- lift $ null <$> use 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 = []
|
|
})
|