From c45771f947cd590a8d3d0f36481583166f2b5deb Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sat, 15 Oct 2022 17:28:38 +0200
Subject: [PATCH] attempt

---
 app/Interpreter.hs | 55 +++++++++++++++++++++++-----------------------
 1 file changed, 28 insertions(+), 27 deletions(-)

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 2bc14ac..9f4d94d 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -12,7 +12,10 @@ data StrTable =
 data Datum
   = Atom Int -- unifies a constant
   | Struct (Int, Int) -- unifies a structure with arity
-  deriving (Show)
+  -- | VoidVar -- unifies with anything
+  -- | LocalVar Int -- unifies with a local variable (possibly making a new one when it's not in use yet)
+  -- | Ref Int -- unifies with the referenced value on the heap (not to be used in code)
+  deriving (Show, Eq, Ord)
 
 data Instr
   = U Datum -- something unifiable
@@ -20,15 +23,16 @@ data Instr
   | Goal -- we start a new goal, set up backtracking etc
   | Call -- all seems okay, call the goal
   | LastCall -- tail call the goal
+  | Cut -- remove all alternative clauses of the current goal
   deriving (Show)
 
 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
+data GolAlts =
+  GA Code Alts -- goal + choicepoints
+  deriving (Show)
 
 type Defs = M.Map (Int, Int) [Code]
 
@@ -36,14 +40,14 @@ data Interp =
   Interp
     { defs :: Defs -- global definitions for lookup
     , hed :: Code -- current head
-    , gol :: Code -- current goal
-    , stk :: Stk -- possible heads with stored original goal
+    , gol :: GolAlts -- current goal with local choicepoints
+    , stk :: [GolAlts] -- stack of caller GolAlts
     }
   deriving (Show)
 
 prove :: Code -> Defs -> Either (Interp, String) Bool
 prove g ds =
-  let i0 = Interp ds g [LastCall] (Stk [] [])
+  let i0 = Interp {defs = ds, hed = g, gol = GA [LastCall] [], stk = []}
       run (Left x) = x
       run (Right x) = run $ proveStep Right Left x
    in run (Right i0)
@@ -57,53 +61,50 @@ proveStep c f i = go i
       | Just d <- defs i M.!? f = ($ d)
       | otherwise = const $ ifail $ "no definition: " ++ show f
     {- 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}
+    backtrack i@Interp {gol = GA _ ((s, gs):as)} = c i {hed = s, gol = GA gs as}
     {- 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}
+    backtrack i@Interp {gol = GA _ [], stk = GA g ss:sss} =
+      backtrack i {hed = error "failed hed", gol = GA g ss, stk = 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)
+    backtrack i@Interp {gol = GA _ [], stk = []} = f (Right False)
     {- Unification -}
-    go i@Interp {hed = (U a:hs), gol = (U b:gs)} -- unify constants
+    go i@Interp {hed = (U a:hs), gol = GA (U b:gs) ss} -- unify constants
      = unify a b
       where
-        uok = c i {hed = hs, gol = gs}
+        uok = c i {hed = hs, gol = GA gs ss}
         unify (Atom a) (Atom b)
           | a == b = uok
         unify (Struct a) (Struct b)
           | a == b = uok
         unify _ _ = backtrack i
     {- Resolution: Final success -}
-    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = Stk _ []} =
+    go i@Interp {hed = [NoGoal], gol = GA [LastCall] _, stk = []} =
       f (Right True)
     {- R: Goal succeeded; continue at parent frame -}
     go i@Interp { hed = [NoGoal]
-                , gol = [LastCall]
-                , stk = Stk _ ((Goal:U (Struct f):gs, ss):sss)
+                , gol = GA [LastCall] _
+                , stk = GA (Goal:U (Struct f):gs) ss:sss
                 } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
+        c i {hed = hs, gol = GA gs (map (, gs) ohs ++ ss), stk = sss}
     {- R: Start matching next goal -}
     go i@Interp { hed = [NoGoal]
-                , gol = (Call:Goal:U (Struct f):gs)
-                , stk = Stk ss sss
+                , gol = GA (Call:Goal:U (Struct f):gs) ss
                 } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
+        c i {hed = hs, gol = GA gs (map (, gs) ohs ++ ss)}
     {- 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
+                , gol = GA (Call:gs) ss
+                , stk = sss
                 } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) ((gs, ss) : sss)}
+        c i {hed = hs, gol = GA ngs (map (, ngs) ohs), stk = GA gs ss : sss}
     {- R: Successful match continued by tail call -}
     go i@Interp { hed = (Goal:U (Struct f):ngs)
-                , gol = [LastCall]
-                , stk = Stk _ sss
+                , gol = GA [LastCall] ss
                 } =
       withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) sss}
+        c i {hed = hs, gol = GA ngs (map (, ngs) ohs ++ ss)}
     {- The End -}
     go _ = ifail "impossible instruction combo"