diff options
Diffstat (limited to 'app')
| -rw-r--r-- | app/Builtins.hs | 25 | ||||
| -rw-r--r-- | app/Code.hs | 2 | ||||
| -rw-r--r-- | app/Frontend.hs | 140 | ||||
| -rw-r--r-- | app/Interpreter.hs | 6 | ||||
| -rw-r--r-- | app/Parser.hs | 2 |
5 files changed, 87 insertions, 88 deletions
diff --git a/app/Builtins.hs b/app/Builtins.hs index 9e72caa..7ef4c10 100644 --- a/app/Builtins.hs +++ b/app/Builtins.hs @@ -16,8 +16,10 @@ import Code , newHeapVars ) import qualified Compiler as Co +import Control.Exception (IOException, catch) import Control.Monad.IO.Class (liftIO) import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Except (runExceptT) import Control.Monad.Trans.State.Lazy (get, gets, modify) import Data.Functor.Identity (runIdentity) import Data.List (intercalate) @@ -26,6 +28,7 @@ import Data.Maybe (fromJust) import Env (PrlgEnv(..), findAtom, findStruct, prlgError) import qualified IR import Interpreter (backtrack) +import Load (processInput) import qualified Operators as O import System.Console.Haskeline (getInputChar, outputStr, outputStrLn) @@ -299,6 +302,25 @@ addBi :: InterpFn -> String -> Int -> PrlgEnv () addBi b n a = addProc [[U (LocalRef $ r - 1) | r <- [1 .. a]] ++ [Invoke $ bi b]] n a +{- loading code -} +load :: Bool -> InterpFn +load queryMode = + withArgs [0] $ \[arg] -> do + heap <- gets (heap . cur) + IR.StrTable _ _ itos <- gets strtable --TODO the argument here should preferably be a string, right? + case derefHeap heap arg of + BoundRef _ (Atom a) -> do + let fn = itos M.! a + src' <- liftIO $ catch (Right <$> readFile fn) (pure . Left) + case src' of + Right src -> do + res <- runExceptT $ processInput fn queryMode src + case res of + Right _ -> continue + Left e -> prlgError $ "loading from '" ++ fn ++ "': " ++ e + Left e -> prlgError $ show (e :: IOException) + _ -> prlgError "load needs an atom" + {- actual prlgude -} addPrelude :: PrlgEnv () addPrelude = do @@ -330,6 +352,9 @@ addPrelude = do addBi retractall "retractall" 1 addBi call "call" 1 addBi struct "struct" 3 + {- code loading -} + addBi (load False) "load" 1 + addBi (load True) "source" 1 {- operators -} addBi op "op" 3 addBi stashOps "stash_operators" 0 diff --git a/app/Code.hs b/app/Code.hs index df2e5c7..f2a3856 100644 --- a/app/Code.hs +++ b/app/Code.hs @@ -6,6 +6,7 @@ import Control.Monad.Trans.State.Lazy (StateT) import qualified Data.Map as M import IR (Id(..), StrTable) import Operators (Ops) +import Parser (PAST) import System.Console.Haskeline (InputT) data Datum @@ -62,6 +63,7 @@ data Interp = , ops :: Ops -- currently defined operators , opstash :: [Ops] -- saved operators , strtable :: StrTable -- string table + , cmdq :: [(Bool, PAST)] -- isQuery, lexemes } deriving (Show) diff --git a/app/Frontend.hs b/app/Frontend.hs index 95f788f..6bae624 100644 --- a/app/Frontend.hs +++ b/app/Frontend.hs @@ -2,19 +2,24 @@ module Frontend where import Builtins import Code (Interp(..)) -import qualified Compiler as C +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) +import Control.Monad.Trans.State.Lazy (evalStateT, gets, modify) import qualified Data.Map as M -import Data.Traversable (for) -import Env (PrlgEnv, findAtom, findStruct, withStrTable) +import Env (PrlgEnv) import qualified IR import qualified Interpreter as I -import qualified Parser as P +import Load + ( compile + , intern + , loadExpansion + , processInput + , queryExpansion + , shunt + ) import System.Console.Haskeline -import qualified Text.Megaparsec as MP import qualified Text.Pretty.Simple as Ppr ppr :: Show a => a -> PrlgEnv () @@ -29,73 +34,19 @@ ppr x = } x -left f = either (Left . f) Right - -tokenize = left MP.errorBundlePretty . MP.parse P.lexPrlg "<stdin>" - -parse = left MP.errorBundlePretty . MP.parse P.parsePrlg "<stdin>" - -shunt ops = - left (\err -> "operator resolution: " ++ err ++ "\n") . P.shuntPrlg ops - -intern prlgs = do - prlgi <- withStrTable $ \st -> IR.internPrlg st prlgs - underscore <- findAtom "_" - list <- findAtom "[]" - withStrTable $ \st -> - ( st - , C.squashVars $ C.variablizePrlg underscore st $ C.desugarPrlg list prlgi) - -compile prlgv = do - comma <- findAtom "," - cut <- findAtom "!" - return $ C.seqGoals (C.compileGoals comma cut prlgv) - -- the signature of this is too ugly to include here handleError m = do res <- runExceptT m case res of - Left err -> lift $ outputStr err + Left err -> do + lift $ outputStrLn err + modify $ \s -> s {cmdq = []} _ -> pure () -processInput precompileHook good bad input = - (True <$) . handleError $ do - asts <- except $ tokenize input >>= parse - ops <- lift $ gets ops - for asts $ \ast' -> do - ast <- except $ shunt ops ast' - code <- lift $ intern ast >>= precompileHook >>= compile - res <- lift (I.prove code) >>= except . left (++ "\n") - lift . lift . outputStrLn $ - if res - then good - else bad - -expansion noexpand expander output x = do - es <- findStruct expander 2 - o <- findAtom output - comma <- findAtom "," - expand <- gets (M.member es . defs) - pure $ - if expand - then IR.CallI - comma - [ IR.CallI (IR.str es) [x, IR.VarI (-1) 0] - , IR.CallI o [IR.VarI (-1) 0] - ] - else noexpand o x - -query = - processInput - (expansion (\_ -> id) "query_expansion" "call") - "yes." - "no proof." - -assert = - processInput - (expansion (\o x -> IR.CallI o [x]) "load_expansion" "assert") - "ok." - "rejected." +processCmd precompileHook ast' = do + ast <- shunt ast' + code <- lift $ intern ast >>= precompileHook >>= compile + lift (I.prove code) >>= except interpreterStart :: PrlgEnv () interpreterStart = do @@ -104,24 +55,38 @@ interpreterStart = do interpreterLoop :: Bool -> PrlgEnv () interpreterLoop queryMode = do - minput <- - lift $ - getInputLine - (if queryMode - then "prlg? " - else "prlg |- ") - case minput of - Nothing -> return () - Just "." -> interpreterLoop (not queryMode) - Just input -> do - continue <- - (if queryMode - then query - else assert) - input - if continue - then interpreterLoop queryMode - else return () + 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 = @@ -129,9 +94,10 @@ interpreter = interpreterStart (Interp { defs = M.empty + , cur = error "no cur" + , cho = [] , ops = [] , opstash = [] , strtable = IR.emptystrtable - , cur = error "no cur" - , cho = [] + , cmdq = [] }) diff --git a/app/Interpreter.hs b/app/Interpreter.hs index 439418c..1ef39f9 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -317,4 +317,8 @@ proveStep = St.get >>= go nchos } {- The End -} - go _ = ifail "code broken: impossible instruction combo" + go i = + ifail $ + "code broken: impossible instruction combo hed=" ++ + show (hed . cur $ i) ++ + " gol=" ++ show (gol . cur $ i) ++ " stk=" ++ show (stk . cur $ i) diff --git a/app/Parser.hs b/app/Parser.hs index 8ca8ac2..43b38b5 100644 --- a/app/Parser.hs +++ b/app/Parser.hs @@ -4,6 +4,8 @@ module Parser ( lexPrlg , parsePrlg , shuntPrlg + , PAST + , Lexeme ) where import Control.Monad (void) |