reorg.

1 files changed, 9 insertions, 57 deletions

diff --git a/app/Frontend.hs b/app/Frontend.hs
index 2c92e1f..a17a85c 100644
--- a/app/Frontend.hs
+++ b/app/Frontend.hs
@@ -1,27 +1,21 @@
 module Frontend where
 
+import Builtins
+import qualified Code
 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 Env
+import qualified IR
 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 $
@@ -34,21 +28,6 @@ ppr x =
       }
     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
@@ -59,15 +38,14 @@ interpret = (>> return True) . lex
     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
+        Right asts -> traverse_ shunt asts
+    shunt ast = do
       o <- gets ops
-      case P.ast2prlg o ast of
+      case P.shuntPrlg o ast of
         Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
         Right prlg -> intern prlg
     intern prlgs = do
-      prlgi <-
-        withStrTable $ \st -> C.strtablizePrlg (C.varnames prlgs) st prlgs
+      prlgi <- withStrTable $ \st -> C.internPrlg (C.varnames prlgs) st prlgs
       compile prlgi
     compile prlgi
       {- TODO: switch between prove goal/compile clause here -}
@@ -87,32 +65,6 @@ interpret = (>> return True) . lex
             then "yes."
             else "no proof."
 
-addBuiltins = do
-  a1 <- findStruct "a" 1
-  a <- findAtom "a"
-  b <- findAtom "b"
-  c <- findAtom "c"
-  b0 <- findStruct "b" 0
-  any <- findStruct "any" 1
-  eq <- findStruct "=" 2
-  modify $ \s ->
-    s
-      { defs =
-          M.fromList
-            [ (eq, [[I.U (I.LocalRef 0),I.U (I.LocalRef 0), I.NoGoal]])
-            , (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]
-                ])
-            , (any, [[I.U I.VoidRef, I.NoGoal]])
-            ]
-      , ops =
-        [ (",", P.Op 1000 $ P.Infix P.X P.Y)
-        , ("=", P.Op 700 $ P.Infix P.X P.X)
-        ]
-      }
-
 interpreterStart :: PrlgEnv ()
 interpreterStart = do
   addBuiltins
@@ -133,4 +85,4 @@ interpreter :: InputT IO ()
 interpreter =
   evalStateT
     interpreterStart
-    (PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable})
+    (PrlgState {defs = M.empty, ops = [], strtable = IR.emptystrtable})