interpreter interprets.

1 files changed, 128 insertions, 0 deletions

diff --git a/app/Frontend.hs b/app/Frontend.hs
new file mode 100644
index 0000000..8dc8b8a
--- /dev/null
+++ b/app/Frontend.hs
@@ -0,0 +1,128 @@
+module Frontend where
+
+import qualified Compiler as C
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.State.Lazy
+import Data.Foldable (traverse_)
+import qualified Data.Map as M
+import qualified Interpreter as I
+import qualified Parser as P
+import System.Console.Haskeline
+import qualified Text.Megaparsec as MP
+import Text.Pretty.Simple
+
+data PrlgState =
+  PrlgState
+    { defs :: I.Defs
+    , ops :: P.Ops
+    , strtable :: I.StrTable
+    }
+  deriving (Show)
+
+type PrlgEnv a = StateT PrlgState (InputT IO) a
+
+ppr :: Show a => a -> PrlgEnv ()
+ppr x =
+  liftIO $
+  pPrintOpt
+    CheckColorTty
+    defaultOutputOptionsDarkBg
+      { outputOptionsCompactParens = True
+      , outputOptionsIndentAmount = 2
+      , outputOptionsPageWidth = 80
+      }
+    x
+
+withStrTable :: (I.StrTable -> (I.StrTable, a)) -> PrlgEnv a
+withStrTable f = do
+  st <- gets strtable
+  let (st', x) = f st
+  modify (\s -> s {strtable = st'})
+  return x
+
+findStruct :: String -> Int -> PrlgEnv I.Id
+findStruct str arity = do
+  stri <- findAtom str
+  return I.Id {I.str = stri, I.arity = arity}
+
+findAtom :: String -> PrlgEnv Int
+findAtom = withStrTable . flip I.strtablize
+
+interpret :: String -> PrlgEnv Bool
+interpret = (>> return True) . lex
+  where
+    lex input = do
+      case MP.parse P.lexPrlg "-" input of
+        Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
+        Right toks -> parse toks
+    parse toks = do
+      case MP.parse P.parsePrlg "-" toks of
+        Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
+        Right asts -> traverse_ prologize asts
+    prologize ast = do
+      o <- gets ops
+      case P.ast2prlg o ast of
+        Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
+        Right prlg -> intern prlg
+    intern prlgs = do
+      prlgi <- withStrTable $ flip C.strtablizePrlg prlgs
+      compile prlgi
+    compile prlgi
+      {- TODO: switch between prove goal/compile clause here -}
+     = do
+      commaId <- findStruct "," 2
+      let code = C.seqGoals $ C.compileGoals commaId prlgi
+      execute code
+    execute code = do
+      ds <- gets defs
+      let (_, res) = I.prove code ds
+      case res of
+        Left err -> liftIO $ putStrLn err
+        Right res ->
+          liftIO $
+          putStrLn $
+          if res
+            then "yes."
+            else "no proof."
+
+addBuiltins = do
+  a1 <- findStruct "a" 1
+  a <- findAtom "a"
+  b <- findAtom "b"
+  c <- findAtom "c"
+  b0 <- findStruct "b" 0
+  modify $ \s ->
+    s
+      { defs =
+          M.fromList
+            [ (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
+            , ( b0
+              , [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
+                , [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
+                ])
+            ]
+      , ops = [(",", P.Op 1000 $ P.Infix P.X P.Y)]
+      }
+
+interpreterStart :: PrlgEnv ()
+interpreterStart = do
+  addBuiltins
+  interpreterLoop
+
+interpreterLoop :: PrlgEnv ()
+interpreterLoop = do
+  minput <- lift $ getInputLine "prlg> "
+  case minput of
+    Nothing -> return ()
+    Just input -> do
+      continue <- interpret input
+      if continue
+        then interpreterLoop
+        else return ()
+
+interpreter :: InputT IO ()
+interpreter =
+  evalStateT
+    interpreterStart
+    (PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable})