From eb67b6b665f5f3afefd39799fa6f579dc65d1565 Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Fri, 14 Oct 2022 21:36:08 +0200
Subject: [PATCH] backtracking

---
 app/Interpreter.hs | 105 ++++++++++++++++++++++++++++++++-------------
 app/Main.hs        |  23 +++++++++-
 2 files changed, 98 insertions(+), 30 deletions(-)

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 7610903..5888ca0 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -1,56 +1,103 @@
+{-# LANGUAGE TupleSections #-}
+
 module Interpreter where
 
 import Data.Function
 import qualified Data.Map as M
 
 {- VAM 2P, done the lazy way -}
-
 data StrTable =
   StrTable Int (M.Map Int String)
 
+data Datum
+  = Atom Int -- unifies a constant
+  | Struct (Int, Int) -- unifies a structure with arity
+  deriving (Show)
+
 data Instr
-  = Atom Int -- unify a constant
-  | Struct (Int, Int) -- unify a structure with arity
+  = U Datum -- something unifiable
   | NoGoal -- trivial goal
   | Goal -- we start a new goal, set up backtracking etc
   | Call -- all seems okay, call the goal
   | LastCall -- tail call the goal
-  deriving Show
+  deriving (Show)
 
-type Defs = M.Map (Int, Int) [Instr]
+type Code = [Instr]
+
+type Alts = [(Code, Code)] -- clauses to try and the corresponding goals to restore
+
+type Defs = M.Map (Int, Int) [Code]
 
 data Interp =
   Interp
-    { defs :: Defs
-    , hed :: [Instr]
-    , gol :: [Instr]
-    , stk :: [[Instr]]
+    { defs :: Defs -- global definitions for lookup
+    , hed :: Code -- current head
+    , gol :: Code -- current goal
+    , stk :: [Alts] -- possible heads with stored original goal
     }
+  deriving (Show)
 
-prove :: [Instr] -> Defs -> Bool
+prove :: Code -> Defs -> Either (Interp, String) Bool
 prove g ds =
-  let i0 = Interp ds [NoGoal] [LastCall] [g]
+  let i0 = Interp ds g [LastCall] [[]]
       run (Left x) = x
-      run (Right x) = run $ pr Right Left x
+      run (Right x) = run $ proveStep Right Left x
    in run (Right i0)
 
-pr :: (Interp -> a) -> (Bool -> a) -> Interp -> a
-pr c f i = go i
+{- this gonna need Either String Bool for errors later -}
+proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
+proveStep c f i = go i
   where
-    go i@Interp {hed = (Atom a:hs), gol = (Atom b:gs)} -- unify constants
-      | a == b = c i {hed = hs, gol = gs}
-    go i@Interp {hed = (Struct a:hs), gol = (Struct b:gs)} -- unify structs
-      | a == b = c i {hed = hs, gol = gs}
-    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = []} = f True -- final success
+    ifail msg = f $ Left (i, msg)
+    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
+    {- Unification -}
+    go i@Interp {hed = (U a:hs), gol = (U b:gs)} -- unify constants
+     = unify a b
+      where
+        uok = c i {hed = hs, gol = gs}
+        unify (Atom a) (Atom b)
+          | a == b = uok
+        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
     go i@Interp { hed = [NoGoal]
                 , gol = [LastCall]
-                , stk = ((Goal:Struct f:gs):ss)
-                } -- goal succeeded
-      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs, stk = ss}
-    go i@Interp {hed = [NoGoal], gol = (Call:Goal:Struct f:gs)} -- next goal
-      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs}
-    go i@Interp {hed = (Goal:Struct f:hs), gol = [LastCall]} -- tail call
-      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs}
-    go i@Interp {hed = (Goal:Struct f:hs), gol = (Call:gs), stk = ss} -- normal call
-      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs, stk = gs : ss}
-    go _ = f False -- bad luck
+                , stk = _:((Goal:U (Struct f):gs, _):ss):sss
+                } -- goal succeeded, continue with parent frame
+     =
+      withDef f $ \(hs:ohs) ->
+        c i {hed = hs, gol = gs, stk = (map (, gs) ohs ++ ss) : sss}
+    go i@Interp { hed = [NoGoal]
+                , gol = (Call:Goal:U (Struct f):gs)
+                , stk = ss:sss
+                } -- next goal
+     =
+      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
+     =
+      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
+     =
+      withDef f $ \(hs:ohs) ->
+        c i {hed = hs, gol = ngs, stk = map (, ngs) ohs : sss}
+    go _ = ifail "impossible instruction combo"
diff --git a/app/Main.hs b/app/Main.hs
index 9d8fc29..be4febe 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -2,5 +2,26 @@ module Main where
 
 import Interpreter
 
+import qualified Data.Map as M
+
 main :: IO ()
-main = putStrLn "Hello, Prolog!"
+main =
+  print $
+  prove [Goal, U (Struct (1, 2)), U (Atom 1), U (Atom 2), LastCall] $
+  M.fromList
+    [ ( (1, 2)
+      , [ [U (Atom 333), U (Atom 444), NoGoal]
+        , [ U (Atom 1)
+          , U (Atom 2)
+          , Goal
+          , U (Struct (2, 0))
+          , Call
+          , Goal
+          , U (Struct (1, 2))
+          , U (Atom 333)
+          , U (Atom 444)
+          , LastCall
+          ]
+        ])
+    , ((2, 0), [[NoGoal]])
+    ]