From 27494c044e54f1bfe8fac466f9416b6e17d58b4d Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sun, 26 Feb 2023 12:16:06 +0100
Subject: [PATCH] PAS continues

---
 app/Interpreter.hs | 140 +++++++++++++++++++++++++++++++++++++--------
 1 file changed, 117 insertions(+), 23 deletions(-)

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 43ea1d5..4f21709 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -17,9 +17,11 @@ import Code
   , writeHeap
   )
 import CodeLens
+import Control.Monad (when)
 import qualified Data.Map as M
 import Env (PrlgEnv)
 import IR (Id(..), StrTable(..))
+import Lens.Family2
 import Lens.Family2.State
 
 prove :: Code -> PrlgEnv (Either String Bool)
@@ -55,7 +57,13 @@ proveStep = do
     (0, _) -> headStep h
     (_, _)
       | u > 0 -> unifyStep h
-    _ -> err "invalid state"
+    _ -> err "invalid interpreter state"
+
+continue :: InterpFn
+continue = pure Nothing
+
+finish :: Bool -> InterpFn
+finish = pure . Just . Right
 
 err :: String -> InterpFn
 err = return . Just . Left
@@ -65,29 +73,26 @@ goalStep :: InterpFn
 goalStep = do
   g <- use (cur . gol)
   case g of
-    U (Struct _):gs -> undefined -- TODO these things NEED lens-family.
-    [Done] -> undefined
-    [Cut, Done] -> undefined
-    Cut:gs -> undefined
-    [Choices cs, Done] -> undefined
-    [Choices cs, Cut, Done] -> undefined
-    Choices cs:gs -> undefined
+    U (Struct s):gs -> openGoal s
+    [Done] -> succeedGoal
+    Cut:gs -> cutGoal
+    Choices cs:gs -> pushChoices cs
     _ -> err "invalid goal code"
 
 headStep :: [Instr] -> InterpFn
 headStep h = do
   g <- use (cur . gol)
   case (h, g) of
-    ([Done], _) -> undefined
-    ([Cut, Done], _) -> undefined
-    (_, [Done]) -> undefined
-    (_, [Cut, Done]) -> undefined
-    (_, _) -> undefined
+    ([Done], _) -> succeedHead
+    (Cut:_, _) -> cutHead
+    (_, [Done]) -> tailCall
+    (_, [Cut, Done]) -> tailCut
+    (_, _) -> pushCall
 
 unifyStep h = do
   g <- use (cur . gol)
   case (h, g) of
-    (U hd:_, U gd:_) -> undefined hd gd
+    (U hd:_, U gd:_) -> unify hd gd
     (_, _) -> err "invalid unification code"
 
 {- helpers -}
@@ -100,18 +105,107 @@ backtrack = do
      -> do
       cur .= c
       cho .= cs
-      pure Nothing
-    {- if there's no other choice, answer no -}
-    _ -> pure . Just $ Right False
+      continue
+    {- if there's no other choice available, answer no -}
+    _ -> finish False
 
-retCut :: InterpFn
-retCut = undefined
+advance = do
+  cur . gol %= tail
+  continue
 
-cutHead :: InterpFn
-cutHead = undefined
+advanceHead = do
+  cur . hed %= tail
+  continue
 
-cutGoal :: InterpFn
-cutGoal = undefined
+doCut = use (cur . cut) >>= assign cho
+
+retCut = do
+  rc <- use (cur . retcut)
+  when rc $ do
+    doCut
+    cur . retcut .= False
+
+cutHead = doCut >> advanceHead
+
+cutGoal = doCut >> advance
+
+openGoal :: IR.Id -> InterpFn
+openGoal fn = do
+  def <- defs `uses` (M.!? fn)
+  case def of
+    Just hs@(_:_) -> do
+      advance
+      cur . hvar .= emptyScope
+      cur . unis .= arity fn
+      cc <- use cur
+      let (newcur:newcho) = [cc & hed .~ h | h <- hs]
+      cur .= newcur
+      cho %= (newcho ++)
+      continue
+    _ -> do
+      StrTable _ _ itos <- use strtable
+      err $ "no definition: '" ++ (itos M.! str fn) ++ "'/" ++ show (arity fn)
+
+pushCall :: InterpFn
+pushCall = do
+  sgol <- use (cur . gol)
+  sgvar <- use (cur . gvar)
+  ngol <- use (cur . hed)
+  ngvar <- use (cur . hvar)
+  scut <- use (cur . cut)
+  sretcut <- use (cur . retcut)
+  cur . stk %= ((sgol, sgvar, scut, sretcut) :)
+  cur . gol .= ngol
+  cur . gvar .= ngvar
+  cur . hed .= []
+  cur . hvar .= emptyScope
+  cur . retcut .= False
+  continue
+
+tailCall :: InterpFn
+tailCall = do
+  ngol <- use (cur . hed)
+  ngvar <- use (cur . hvar)
+  cur . gol .= ngol
+  cur . gvar .= ngvar
+  cur . hed .= []
+  cur . hvar .= emptyScope
+  continue
+
+tailCut :: InterpFn
+tailCut = do
+  cur . retcut .= True
+  advance
+  tailCall
+
+succeedHead :: InterpFn
+succeedHead = do
+  cur . hvar .= emptyScope
+  cur . hed .= []
+  continue
+
+succeedGoal :: InterpFn
+succeedGoal = do
+  retCut
+  st <- use (cur . stk)
+  case st of
+    [] -> do
+      cur . gol .= []
+      finish True
+    ((sgol, sgvar, scut, sretcut):st') -> do
+      zoom cur $ do
+        gol .= sgol
+        gvar .= sgvar
+        cut .= scut
+        retcut .= sretcut
+        stk .= st'
+      continue
+
+pushChoices :: [[Code]] -> InterpFn
+pushChoices cs = undefined
+
+unify :: Datum -> Datum -> InterpFn
+unify = undefined
 {- original, TODO remove -}
 {-proveStep :: InterpFn
 proveStep = St.get >>= go