builtins are built in

1 files changed, 36 insertions, 24 deletions

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 743f68b..3d1c569 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -2,11 +2,11 @@
 module Interpreter where
 
 import Code
+import qualified Control.Monad.Trans.State.Lazy as St
+
 --import Data.Function
 import qualified Data.Map as M
-import Env (PrlgEnv(..))
 import IR (Id(..))
-import qualified Control.Monad.Trans.State.Lazy as St
 
 prove :: Code -> PrlgEnv (Either String Bool)
 prove g = do
@@ -27,32 +27,43 @@ prove g = do
   loop
   where
     loop = do
-      i <- St.get
-      proveStep cont finish i
-    cont i = St.put i >> loop
-    finish i res = St.put i >> return res
+      x <- proveStep
+      case x of
+        Nothing -> loop -- not finished yet
+        Just x -> return x
 
 data Dereferenced
   = FreeRef Int
   | BoundRef Int Datum
   | NoRef
 
-proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a
-proveStep c f i = go i
+{- Simple "fail" backtracking -}
+backtrack :: PrlgEnv (Maybe (Either String Bool))
+backtrack = do
+  chos <- St.gets cho
+  case chos
+    {- if available, restore the easiest choicepoint -}
+        of
+    (c:cs) -> do
+      St.modify $ \i -> i {cur = c, cho = cs}
+      pure Nothing
+    {- if there's no other choice, answer no -}
+    _ -> pure . Just $ Right False
+
+proveStep :: PrlgEnv (Maybe (Either String Bool))
+proveStep = St.get >>= go
   where
-    ifail msg = f i $ Left msg
+    finish = pure . Just
+    c i = St.put i >> pure Nothing
+    ifail msg = finish $ Left msg
     tailcut [LastCall] chos _ = Just chos
     tailcut [LastCall, Cut] _ cut = Just cut
     tailcut _ _ _ = Nothing
-    withDef fn
-      | Just d <- defs i M.!? fn = ($ d)
-      | otherwise = const $ ifail $ "no definition: " ++ show fn
-    {- Backtracking -}
-    backtrack i@Interp {cho = chos}
-      {- if available, restore the easiest choicepoint -}
-      | (cho:chos) <- chos = c i {cur = cho, cho = chos}
-      {- if there's no other choice, answer no -}
-      | otherwise = f i $ Right False
+    withDef fn cont = do
+      d <- St.gets defs
+      case d M.!? fn of
+        Just d -> cont d
+        _ -> ifail $ "no definition: " ++ show fn
     {- Unification -}
     go i@Interp {cur = cur@Cho { hed = U h:hs
                                , gol = U g:gs
@@ -206,7 +217,7 @@ proveStep c f i = go i
                         }
                   }
             _ -> ifail "dangling goal ref"
-        unify _ _ = backtrack i
+        unify _ _ = backtrack
     {- Resolution -}
     go i@Interp { cur = cur@Cho { hed = hed
                                 , hvar = hvar
@@ -219,14 +230,15 @@ proveStep c f i = go i
                 , cho = chos
                 }
       {- invoke a built-in (this gets replaced by NoGoal by default but the
-       - builtin can actually do whatever it wants with the code -}
-      | [Builtin (BuiltinFunc bf)] <- hed =
-        c (bf i {cur = cur {hed = [NoGoal]}})
+       - builtin can actually do whatever it wants with the code) -}
+      | [Invoke (Builtin bf)] <- hed =
+        St.put i {cur = cur {hed = [NoGoal]}} >> bf
       {- top-level success -}
       | [NoGoal] <- hed
       , Just nchos <- tailcut gol chos cut
-      , [] <- stk =
-        f i {cur = cur {hed = [], gol = []}, cho = nchos} $ Right True
+      , [] <- stk = do
+        St.put i {cur = cur {hed = [], gol = []}, cho = nchos}
+        finish $ Right True
       {- cut before the first goal (this solves all cuts in head) -}
       | Cut:hs <- hed = c i {cur = cur {hed = hs}, cho = cut}
       {- succeed and return to caller -}