consultation mode

app/Frontend.hs

@@ -5,9 +5,10 @@ import Code (Interp(..))
 import qualified Compiler as C
 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 Data.Foldable (traverse_)
 import qualified Data.Map as M
+import Data.Traversable (for)
 import Env (PrlgEnv, findAtom, withStrTable)
 import qualified IR
 import qualified Interpreter as I
@@ -28,61 +29,78 @@ ppr x =
       }
     x
 
-interpret :: String -> PrlgEnv Bool
+left f = either (Left . f) Right
-interpret = (>> return True) . lex
+
-  where
+tokenize = left MP.errorBundlePretty . MP.parse P.lexPrlg "<stdin>"
-    lex input = do
+
-      case MP.parse P.lexPrlg "-" input of
+parse = left MP.errorBundlePretty . MP.parse P.parsePrlg "<stdin>"
-        Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
+
-        Right toks -> parse toks
+shunt ops =
-    parse toks = do
+  left (\err -> "operator resolution: " ++ err ++ "\n") . P.shuntPrlg ops
-      case MP.parse P.parsePrlg "-" toks of
+
-        Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
+makeAssertion x = IR.CallS "assert" [x]
-        Right asts -> traverse_ shunt asts
+
-    shunt ast = do
+intern prlgs = 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.squashVars $ C.variablizePrlg underscore st $ C.desugarPrlg list prlgi)
-            C.variablizePrlg underscore st $ C.desugarPrlg list prlgi)
+
-      compile prlgv
+compile prlgv = do
-    compile prlgv = do
   comma <- findAtom ","
   cut <- findAtom "!"
-      let code = C.seqGoals $ C.compileGoals comma cut prlgv
+  return $ C.seqGoals (C.compileGoals comma cut prlgv)
-      execute code
+
-    execute code = do
+-- the signature of this is too ugly to include here
-      res <- I.prove code
+handleError m = do
-      lift . outputStrLn $
+  res <- runExceptT m
   case res of
-          Left err -> err
+    Left err -> lift $ outputStr err
-          Right res ->
+    _ -> pure ()
+
+processInput astHook good bad input =
+  (True <$) . handleError $ do
+    asts <- except $ tokenize input >>= parse
+    ops <- lift $ gets ops
+    for asts $ \ast' -> do
+      ast <- except $ astHook <$> shunt ops ast'
+      code <- lift $ intern ast >>= compile
+      res <- lift (I.prove code) >>= except . left (++ "\n")
+      lift . lift . outputStrLn $
         if res
-              then "yes."
+          then good
-              else "no proof."
+          else bad
+
+query = processInput id "yes." "no proof."
+
+assert = processInput makeAssertion "ok." "rejected."
 
 interpreterStart :: PrlgEnv ()
 interpreterStart = do
   addPrelude
-  interpreterLoop
+  interpreterLoop True
 
-interpreterLoop :: PrlgEnv ()
+interpreterLoop :: Bool -> PrlgEnv ()
-interpreterLoop = do
+interpreterLoop queryMode = do
-  minput <- lift $ getInputLine "prlg? " --TODO switch with plain .
+  minput <-
+    lift $
+    getInputLine
+      (if queryMode
+         then "prlg? "
+         else "prlg |- ")
   case minput of
     Nothing -> return ()
+    Just "." -> interpreterLoop (not queryMode)
     Just input -> do
-      continue <- interpret input
+      continue <-
+        (if queryMode
+           then query
+           else assert)
+          input
       if continue
-        then interpreterLoop
+        then interpreterLoop queryMode
         else return ()
 
 interpreter :: InputT IO ()