99 lines
2.7 KiB
Haskell
99 lines
2.7 KiB
Haskell
module Frontend where
|
|
|
|
import Builtins
|
|
import Code (Interp(..))
|
|
import qualified Compiler as C
|
|
import Control.Monad.IO.Class (liftIO)
|
|
import Control.Monad.Trans.Class (lift)
|
|
import Control.Monad.Trans.State.Lazy (evalStateT, gets)
|
|
import Data.Foldable (traverse_)
|
|
import qualified Data.Map as M
|
|
import Env (PrlgEnv, findAtom, findStruct, withStrTable)
|
|
import qualified IR
|
|
import qualified Interpreter as I
|
|
import qualified Parser as P
|
|
import System.Console.Haskeline
|
|
import qualified Text.Megaparsec as MP
|
|
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
|
|
|
|
interpret :: String -> PrlgEnv Bool
|
|
interpret = (>> return True) . lex
|
|
where
|
|
lex input = do
|
|
case MP.parse P.lexPrlg "-" input of
|
|
Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
|
|
Right toks -> parse toks
|
|
parse toks = do
|
|
case MP.parse P.parsePrlg "-" toks of
|
|
Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
|
|
Right asts -> traverse_ shunt asts
|
|
shunt ast = do
|
|
o <- gets ops
|
|
case P.shuntPrlg o ast of
|
|
Left err -> lift . outputStrLn $ "expression parsing: " ++ err
|
|
Right prlg -> intern prlg
|
|
intern prlgs = do
|
|
prlgi <- withStrTable $ \st -> IR.internPrlg st prlgs
|
|
underscore <- findAtom "_"
|
|
list <- findAtom "[]"
|
|
prlgv <-
|
|
withStrTable $ \st ->
|
|
( st
|
|
, C.squashVars $
|
|
C.variablizePrlg underscore st $ C.desugarPrlg list prlgi)
|
|
compile prlgv
|
|
compile prlgv = do
|
|
commaId <- findStruct "," 2
|
|
cut <- findAtom "!"
|
|
let code = C.seqGoals $ C.compileGoals commaId cut prlgv
|
|
execute code
|
|
execute code = do
|
|
res <- I.prove code
|
|
lift . outputStrLn $
|
|
case res of
|
|
Left err -> err
|
|
Right res ->
|
|
if res
|
|
then "yes."
|
|
else "no proof."
|
|
|
|
interpreterStart :: PrlgEnv ()
|
|
interpreterStart = do
|
|
addPrelude
|
|
interpreterLoop
|
|
|
|
interpreterLoop :: PrlgEnv ()
|
|
interpreterLoop = do
|
|
minput <- lift $ getInputLine "prlg? " --TODO switch with plain .
|
|
case minput of
|
|
Nothing -> return ()
|
|
Just input -> do
|
|
continue <- interpret input
|
|
if continue
|
|
then interpreterLoop
|
|
else return ()
|
|
|
|
interpreter :: InputT IO ()
|
|
interpreter =
|
|
evalStateT
|
|
interpreterStart
|
|
(Interp
|
|
{ defs = M.empty
|
|
, ops = []
|
|
, strtable = IR.emptystrtable
|
|
, cur = error "no cur"
|
|
, cho = []
|
|
})
|