From 6fa4cec10b647ee42aabf1e367ba8fa3c820cadf Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sat, 15 Oct 2022 15:02:13 +0200
Subject: [PATCH] have a normal Stk

---
 app/Interpreter.hs | 70 +++++++++++++++++++++++++---------------------
 1 file changed, 38 insertions(+), 32 deletions(-)

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 5888ca0..2bc14ac 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -26,6 +26,10 @@ type Code = [Instr]
 
 type Alts = [(Code, Code)] -- clauses to try and the corresponding goals to restore
 
+data Stk =
+  Stk Alts [(Code, Alts)]
+  deriving (Show) -- local backtracks (skipped on cut) + return&backtracks
+
 type Defs = M.Map (Int, Int) [Code]
 
 data Interp =
@@ -33,13 +37,13 @@ data Interp =
     { defs :: Defs -- global definitions for lookup
     , hed :: Code -- current head
     , gol :: Code -- current goal
-    , stk :: [Alts] -- possible heads with stored original goal
+    , stk :: Stk -- possible heads with stored original goal
     }
   deriving (Show)
 
 prove :: Code -> Defs -> Either (Interp, String) Bool
 prove g ds =
-  let i0 = Interp ds g [LastCall] [[]]
+  let i0 = Interp ds g [LastCall] (Stk [] [])
       run (Left x) = x
       run (Right x) = run $ proveStep Right Left x
    in run (Right i0)
@@ -52,15 +56,14 @@ proveStep c f i = go i
     withDef f
       | Just d <- defs i M.!? f = ($ d)
       | otherwise = const $ ifail $ "no definition: " ++ show f
-    {- Backtracking -}
-    backtrack i@Interp {stk = ((s, gs):ss):sss} -- backtrack to next clause, restoring goal
-     = c i {hed = s, gol = gs, stk = ss : sss}
-    backtrack i@Interp {stk = []:ss@(_:_):sss} -- no next clause, pop stack and backtrack the caller clause
-     =
-      backtrack
-        i {hed = error "failed hed", gol = error "failed gol", stk = ss : sss}
-    backtrack i@Interp {stk = [[]]} = f (Right False)
-    backtrack i@Interp {stk = []:[]:_} = ifail "broken stk" -- this should not happen
+    {- Backtracking: try a fallback clause, restoring goal -}
+    backtrack i@Interp {stk = Stk ((s, gs):ss) sss} =
+      c i {hed = s, gol = gs, stk = Stk ss sss}
+    {- B: no next clause, pop stack and continue backtracking at the caller -}
+    backtrack i@Interp {stk = Stk [] ((g, ss):sss)} =
+      backtrack i {hed = error "failed hed", gol = g, stk = Stk ss sss}
+    {- B: we ran out of possibilities and there's nothing else to backtrack. No solution found. -}
+    backtrack i@Interp {stk = Stk [] []} = f (Right False)
     {- Unification -}
     go i@Interp {hed = (U a:hs), gol = (U b:gs)} -- unify constants
      = unify a b
@@ -71,33 +74,36 @@ proveStep c f i = go i
         unify (Struct a) (Struct b)
           | a == b = uok
         unify _ _ = backtrack i
-    {- Resolution -}
-    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = [_]} = f (Right True) -- final success
+    {- Resolution: Final success -}
+    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = Stk _ []} =
+      f (Right True)
+    {- R: Goal succeeded; continue at parent frame -}
     go i@Interp { hed = [NoGoal]
                 , gol = [LastCall]
-                , stk = _:((Goal:U (Struct f):gs, _):ss):sss
-                } -- goal succeeded, continue with parent frame
-     =
+                , stk = Stk _ ((Goal:U (Struct f):gs, ss):sss)
+                } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = gs, stk = (map (, gs) ohs ++ ss) : sss}
+        c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
+    {- R: Start matching next goal -}
     go i@Interp { hed = [NoGoal]
                 , gol = (Call:Goal:U (Struct f):gs)
-                , stk = ss:sss
-                } -- next goal
-     =
+                , stk = Stk ss sss
+                } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = gs, stk = (map (, gs) ohs ++ ss) : sss}
-    go i@Interp {hed = (Goal:U (Struct f):ngs), gol = (Call:gs), stk = ss:sss} -- normal call
-     =
+        c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
+    {- R: Goal head matching succeeded, make a normal call -}
+    go i@Interp { hed = (Goal:U (Struct f):ngs)
+                , gol = (Call:gs)
+                , stk = Stk ss sss
+                } =
       withDef f $ \(hs:ohs) ->
-        c
-          i
-            { hed = hs
-            , gol = ngs
-            , stk = (map (, ngs) ohs) : ((gs, error "gol no hed") : ss) : sss
-            }
-    go i@Interp {hed = (Goal:U (Struct f):ngs), gol = [LastCall], stk = _:sss} -- tail call
-     =
+        c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) ((gs, ss) : sss)}
+    {- R: Successful match continued by tail call -}
+    go i@Interp { hed = (Goal:U (Struct f):ngs)
+                , gol = [LastCall]
+                , stk = Stk _ sss
+                } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = ngs, stk = map (, ngs) ohs : sss}
+        c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) sss}
+    {- The End -}
     go _ = ifail "impossible instruction combo"