cuts

1 files changed, 52 insertions, 22 deletions

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index cd1ab34..81ecb3d 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -32,8 +32,8 @@ data Cho =
   Cho
     { hed :: Code -- head pointer
     , gol :: Code -- goal pointer
-    , stk :: [Code] -- remaining "and" goals
-    , cut :: [Cho] -- snapshot of choicepoints
+    , stk :: [(Code, [Cho])] -- remaining "and" goals
+    , cut :: [Cho] -- snapshot of choicepoints before entering
     }
   deriving (Show)
 
@@ -45,20 +45,26 @@ data Interp =
     }
   deriving (Show)
 
-prove :: Code -> Defs -> Either (Interp, String) Bool
+prove :: Code -> Defs -> (Interp, Either String Bool)
 prove g ds =
   let i0 =
         Interp
-          {defs = ds, cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}, cho = []}
+          { defs = ds
+          , cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}
+          , cho = []
+          }
       run (Left x) = x
-      run (Right x) = run $ proveStep Right Left x
+      run (Right x) = run $ proveStep Right (\i e -> Left (i, e)) x
    in run (Right i0)
 
 {- this gonna need Either String Bool for errors later -}
-proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
+proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a
 proveStep c f i = go i
   where
-    ifail msg = f $ Left (i, msg)
+    ifail msg = f i $ 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
@@ -67,7 +73,7 @@ proveStep c f i = go i
       {- 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 (Right False)
+      | otherwise = f i $ Right False
     {- Unification -}
     go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
      = unify a b
@@ -79,20 +85,35 @@ proveStep c f i = go i
           | a == b = uok
         unify _ _ = backtrack i
     {- Resulution -}
-    go i@Interp {cur = cur@Cho {hed = hed, gol = gol, stk = stk}, cho = chos}
+    go i@Interp { cur = cur@Cho {hed = hed, gol = gol, stk = stk, cut = cut}
+                , cho = chos
+                }
       {- top-level success -}
       | [NoGoal] <- hed
-      , [LastCall] <- gol
-      , [] <- stk = f (Right True)
+      , Just nchos <- tailcut gol chos cut
+      , [] <- stk =
+        f i {cur = cur {hed = [], gol = []}, cho = nchos} $ 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 -}
       | [NoGoal] <- hed
-      , [LastCall] <- gol
-      , (Goal:U (Struct fn):gs):ss <- stk =
+      , Just nchos <- tailcut gol chos cut
+      , (Goal:U (Struct fn):gs, _):ss <- stk =
         withDef fn $ \(hs:ohs) ->
           c
             i
               { cur = cur {hed = hs, gol = gs, stk = ss}
-              , cho = [Cho oh gs ss chos | oh <- ohs] ++ chos
+              , cho = [Cho oh gs ss nchos | oh <- ohs] ++ nchos
+              }
+      {- succeed and return to caller, and the caller wants a cut -}
+      | [NoGoal] <- hed
+      , Just _ <- tailcut gol chos cut
+      , (Cut:Goal:U (Struct fn):gs, rchos):ss <- stk =
+        withDef fn $ \(hs:ohs) ->
+          c
+            i
+              { cur = cur {hed = hs, gol = gs, stk = ss}
+              , cho = [Cho oh gs ss rchos | oh <- ohs] ++ rchos
               }
       {- start matching next goal -}
       | [NoGoal] <- hed
@@ -103,23 +124,32 @@ proveStep c f i = go i
               { cur = cur {hed = hs, gol = gs}
               , cho = [Cho oh gs stk chos | oh <- ohs] ++ chos
               }
-      {- goal head matching succeeded, make a normal call -}
-      | (Goal:U (Struct fn):ngs) <- hed
-      , (Call:gs) <- gol =
+      {- start matching next goal after a cut -}
+      | [NoGoal] <- hed
+      , (Call:Cut:Goal:U (Struct fn):gs) <- gol =
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = ngs, stk = gs : stk}
-              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
+              { cur = cur {hed = hs, gol = gs}
+              , cho = [Cho oh gs stk cut | oh <- ohs] ++ cut
               }
-    {- R: Successful match continued by tail call -}
+      {- goal head matching succeeded, make a normal call -}
+      | (Goal:U (Struct fn):ngs) <- hed
+      , (Call:gs) <- gol =
+        withDef fn $ \(hs:ohs) ->
+          let nstk = (gs, chos) : stk
+           in c i
+                  { cur = cur {hed = hs, gol = ngs, stk = nstk}
+                  , cho = [Cho oh ngs nstk chos | oh <- ohs] ++ chos
+                  }
+      {- successful match continued by tail call -}
       | (Goal:U (Struct fn):ngs) <- hed
-      , [LastCall] <- gol =
+      , Just nchos <- tailcut gol chos cut =
         withDef fn $ \(hs:ohs) ->
           c
             i
               { cur = cur {hed = hs, gol = ngs}
-              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
+              , cho = [Cho oh ngs stk nchos | oh <- ohs] ++ nchos
               }
     {- The End -}
     go _ = ifail "impossible instruction combo"