macros macro

macron edition

1 files changed, 29 insertions, 9 deletions

diff --git a/app/Frontend.hs b/app/Frontend.hs
index 0211958..95f788f 100644
--- a/app/Frontend.hs
+++ b/app/Frontend.hs
@@ -9,7 +9,7 @@ import Control.Monad.Trans.Except (except, runExceptT)
 import Control.Monad.Trans.State.Lazy (evalStateT, gets)
 import qualified Data.Map as M
 import Data.Traversable (for)
-import Env (PrlgEnv, findAtom, withStrTable)
+import Env (PrlgEnv, findAtom, findStruct, withStrTable)
 import qualified IR
 import qualified Interpreter as I
 import qualified Parser as P
@@ -38,8 +38,6 @@ parse = left MP.errorBundlePretty . MP.parse P.parsePrlg "<stdin>"
 shunt ops =
   left (\err -> "operator resolution: " ++ err ++ "\n") . P.shuntPrlg ops
 
-makeAssertion x = IR.CallS "assert" [x]
-
 intern prlgs = do
   prlgi <- withStrTable $ \st -> IR.internPrlg st prlgs
   underscore <- findAtom "_"
@@ -60,22 +58,44 @@ handleError m = do
     Left err -> lift $ outputStr err
     _ -> pure ()
 
-processInput astHook good bad input =
+processInput precompileHook 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
+      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
 
-query = processInput id "yes." "no proof."
-
-assert = processInput makeAssertion "ok." "rejected."
+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."
 
 interpreterStart :: PrlgEnv ()
 interpreterStart = do