summaryrefslogtreecommitdiff
path: root/app
diff options
context:
space:
mode:
authorMirek Kratochvil <exa.exa@gmail.com>2023-01-14 23:10:52 +0100
committerMirek Kratochvil <exa.exa@gmail.com>2023-01-14 23:10:52 +0100
commitab86f0f21f09230aaa2225b0355907446038f819 (patch)
tree6c05c8b63b762b3e21740a010d27bb76fadd7d69 /app
parentdab150976d9a9bf705b03d32ce553d176cdef9e1 (diff)
downloadprlg-ab86f0f21f09230aaa2225b0355907446038f819.tar.gz
prlg-ab86f0f21f09230aaa2225b0355907446038f819.tar.bz2
macros macro
macron edition
Diffstat (limited to 'app')
-rw-r--r--app/Builtins.hs18
-rw-r--r--app/Frontend.hs38
2 files changed, 41 insertions, 15 deletions
diff --git a/app/Builtins.hs b/app/Builtins.hs
index a273660..9e72caa 100644
--- a/app/Builtins.hs
+++ b/app/Builtins.hs
@@ -133,8 +133,8 @@ retractall =
BoundRef _ (Struct id) -> dropProcedure id >> continue
_ -> prlgError "retractall needs a struct"
-call :: InterpFn
-call =
+call' :: InterpFn
+call' =
withArgs [0] $ \[arg] -> do
heap@(Heap _ hmap) <- gets (heap . cur)
let exec base struct arity = do
@@ -156,8 +156,8 @@ call =
exec addr (Struct IR.Id {IR.arity = 0, IR.str = a}) 0
_ -> prlgError "not callable"
-exec :: InterpFn
-exec =
+exec' :: (Code -> Code) -> InterpFn
+exec' fgol =
withArgs [0] $ \[arg] -> do
heap <- gets (heap . cur)
case Co.squashVars <$> Co.heapStructPrlgInt Nothing heap arg of
@@ -171,11 +171,17 @@ exec =
cur
{ hvar = M.empty
, hed = Co.seqGoals (Co.compileGoals comma cut gs)
- , gol = [LastCall]
+ , gol = fgol (gol cur)
}
}
continue
- _ -> prlgError "goal exec failure"
+ _ -> prlgError "bad goal"
+
+call :: InterpFn
+call = exec' id
+
+exec :: InterpFn
+exec = exec' (const [LastCall])
{- struct assembly/disassembly -}
struct :: InterpFn
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