From 31c20628ea7bc85da8ae3f479d418832cf77bfca Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sat, 15 Oct 2022 19:21:17 +0200
Subject: [PATCH] le switch

---
 app/Interpreter.hs | 119 +++++++++++++++++++++++++--------------------
 1 file changed, 67 insertions(+), 52 deletions(-)

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 9f4d94d..cd1ab34 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE TupleSections #-}
-
 module Interpreter where
 
 import Data.Function
@@ -28,26 +26,30 @@ data Instr
 
 type Code = [Instr]
 
-type Alts = [(Code, Code)] -- clauses to try and the corresponding goals to restore
-
-data GolAlts =
-  GA Code Alts -- goal + choicepoints
-  deriving (Show)
-
 type Defs = M.Map (Int, Int) [Code]
 
+data Cho =
+  Cho
+    { hed :: Code -- head pointer
+    , gol :: Code -- goal pointer
+    , stk :: [Code] -- remaining "and" goals
+    , cut :: [Cho] -- snapshot of choicepoints
+    }
+  deriving (Show)
+
 data Interp =
   Interp
     { defs :: Defs -- global definitions for lookup
-    , hed :: Code -- current head
-    , gol :: GolAlts -- current goal with local choicepoints
-    , stk :: [GolAlts] -- stack of caller GolAlts
+    , cur :: Cho -- the choice that is being evaluated right now
+    , cho :: [Cho] -- remaining choice points
     }
   deriving (Show)
 
 prove :: Code -> Defs -> Either (Interp, String) Bool
 prove g ds =
-  let i0 = Interp {defs = ds, hed = g, gol = GA [LastCall] [], stk = []}
+  let i0 =
+        Interp
+          {defs = ds, cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}, cho = []}
       run (Left x) = x
       run (Right x) = run $ proveStep Right Left x
    in run (Right i0)
@@ -57,54 +59,67 @@ proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
 proveStep c f i = go i
   where
     ifail msg = f $ Left (i, msg)
-    withDef f
-      | Just d <- defs i M.!? f = ($ d)
-      | otherwise = const $ ifail $ "no definition: " ++ show f
-    {- Backtracking: try a fallback clause, restoring goal -}
-    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 {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 {gol = GA _ [], stk = []} = f (Right False)
+    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 (Right False)
     {- Unification -}
-    go i@Interp {hed = (U a:hs), gol = GA (U b:gs) ss} -- unify constants
+    go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
      = unify a b
       where
-        uok = c i {hed = hs, gol = GA gs ss}
+        uok = c i {cur = cur {hed = hs, gol = gs}}
         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 = GA [LastCall] _, stk = []} =
-      f (Right True)
-    {- R: Goal succeeded; continue at parent frame -}
-    go i@Interp { hed = [NoGoal]
-                , gol = GA [LastCall] _
-                , stk = GA (Goal:U (Struct f):gs) ss:sss
-                } =
-      withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = GA gs (map (, gs) ohs ++ ss), stk = sss}
-    {- R: Start matching next goal -}
-    go i@Interp { hed = [NoGoal]
-                , gol = GA (Call:Goal:U (Struct f):gs) ss
-                } =
-      withDef f $ \(hs:ohs) ->
-        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 = GA (Call:gs) ss
-                , stk = sss
-                } =
-      withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = GA ngs (map (, ngs) ohs), stk = GA gs ss : sss}
+    {- Resulution -}
+    go i@Interp {cur = cur@Cho {hed = hed, gol = gol, stk = stk}, cho = chos}
+      {- top-level success -}
+      | [NoGoal] <- hed
+      , [LastCall] <- gol
+      , [] <- stk = f (Right True)
+      {- succeed and return to caller -}
+      | [NoGoal] <- hed
+      , [LastCall] <- gol
+      , (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
+              }
+      {- start matching next goal -}
+      | [NoGoal] <- hed
+      , (Call:Goal:U (Struct fn):gs) <- gol =
+        withDef fn $ \(hs:ohs) ->
+          c
+            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 =
+        withDef fn $ \(hs:ohs) ->
+          c
+            i
+              { cur = cur {hed = hs, gol = ngs, stk = gs : stk}
+              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
+              }
     {- R: Successful match continued by tail call -}
-    go i@Interp { hed = (Goal:U (Struct f):ngs)
-                , gol = GA [LastCall] ss
-                } =
-      withDef f $ \(hs:ohs) ->
-        c i {hed = hs, gol = GA ngs (map (, ngs) ohs ++ ss)}
+      | (Goal:U (Struct fn):ngs) <- hed
+      , [LastCall] <- gol =
+        withDef fn $ \(hs:ohs) ->
+          c
+            i
+              { cur = cur {hed = hs, gol = ngs}
+              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
+              }
     {- The End -}
     go _ = ifail "impossible instruction combo"