load loads.

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

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)
 

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'
+processCmd precompileHook ast' = do
+  ast <- shunt 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."
+  lift (I.prove code) >>= except
 
 interpreterStart :: PrlgEnv ()
 interpreterStart = do
@@ -104,6 +55,9 @@ interpreterStart = do
 
 interpreterLoop :: Bool -> PrlgEnv ()
 interpreterLoop queryMode = do
+  q <- gets cmdq
+  case q of
+    [] -> do
       minput <-
         lift $
         getInputLine
@@ -114,14 +68,25 @@ interpreterLoop queryMode = do
         Nothing -> return ()
         Just "." -> interpreterLoop (not queryMode)
         Just input -> do
-      continue <-
-        (if queryMode
-           then query
-           else assert)
-          input
-      if continue
-        then interpreterLoop queryMode
-        else return ()
+          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 = []
        })

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)

app/Parser.hs

@@ -4,6 +4,8 @@ module Parser
   ( lexPrlg
   , parsePrlg
   , shuntPrlg
+  , PAST
+  , Lexeme
   ) where
 
 import Control.Monad (void)

prlg.cabal

@@ -25,7 +25,7 @@ executable prlg
     main-is:          Main.hs
 
     -- Modules included in this executable, other than Main.
-    other-modules:    Interpreter, Compiler, Parser, Frontend, IR, Operators, Code, Builtins, Env
+    other-modules:    Interpreter, Compiler, Parser, Frontend, IR, Operators, Code, Builtins, Env, Load
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions: