1 files changed, 80 insertions, 27 deletions

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index b215049..43ea1d5 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -1,4 +1,4 @@
-{- VAM 2P, done the lazy way -}
+{- pražský přehledný stroj -}
 module Interpreter where
 
 import Code
@@ -8,7 +8,6 @@ import Code
   , Datum(..)
   , Dereferenced(..)
   , Instr(..)
-  , Interp(..)
   , InterpFn
   , derefHeap
   , emptyHeap
@@ -17,29 +16,27 @@ import Code
   , withNewHeapStruct
   , writeHeap
   )
-import qualified Control.Monad.Trans.State.Lazy as St
-import Env (PrlgEnv)
-
---import Data.Function
+import CodeLens
 import qualified Data.Map as M
+import Env (PrlgEnv)
 import IR (Id(..), StrTable(..))
+import Lens.Family2.State
 
 prove :: Code -> PrlgEnv (Either String Bool)
 prove g = do
-  St.modify $ \i ->
-    i
-      { cur =
-          Cho
-            { hed = g
-            , hvar = emptyScope
-            , gol = [LastCall]
-            , gvar = emptyScope
-            , heap = emptyHeap
-            , stk = []
-            , cut = []
-            }
-      , cho = []
+  cur .=
+    Cho
+      { _hed = g
+      , _hvar = emptyScope
+      , _gol = [Done]
+      , _gvar = emptyScope
+      , _unis = 0
+      , _retcut = True
+      , _heap = emptyHeap
+      , _stk = []
+      , _cut = []
       }
+  cho .= []
   loop
   where
     loop = do
@@ -48,20 +45,75 @@ prove g = do
         Nothing -> loop -- not finished yet
         Just x -> return x
 
-{- Simple "fail" backtracking -}
+{- toplevel decision -}
+proveStep :: InterpFn
+proveStep = do
+  u <- use (cur . unis)
+  h <- use (cur . hed)
+  case (u, h) of
+    (0, []) -> goalStep
+    (0, _) -> headStep h
+    (_, _)
+      | u > 0 -> unifyStep h
+    _ -> err "invalid state"
+
+err :: String -> InterpFn
+err = return . Just . Left
+
+{- toplevel choices -}
+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
+    _ -> 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
+
+unifyStep h = do
+  g <- use (cur . gol)
+  case (h, g) of
+    (U hd:_, U gd:_) -> undefined hd gd
+    (_, _) -> err "invalid unification code"
+
+{- helpers -}
 backtrack :: InterpFn
 backtrack = do
-  chos <- St.gets cho
-  case chos
-    {- if available, restore the easiest choicepoint -}
-        of
-    (c:cs) -> do
-      St.modify $ \i -> i {cur = c, cho = cs}
+  chos <- use cho
+  case chos of
+    (c:cs)
+      {- if available, restore the easiest choicepoint -}
+     -> do
+      cur .= c
+      cho .= cs
       pure Nothing
     {- if there's no other choice, answer no -}
     _ -> pure . Just $ Right False
 
-proveStep :: InterpFn
+retCut :: InterpFn
+retCut = undefined
+
+cutHead :: InterpFn
+cutHead = undefined
+
+cutGoal :: InterpFn
+cutGoal = undefined
+{- original, TODO remove -}
+{-proveStep :: InterpFn
 proveStep = St.get >>= go
   where
     finish = pure . Just
@@ -325,3 +377,4 @@ proveStep = St.get >>= go
       "code broken: impossible instruction combo hed=" ++
       show (hed . cur $ i) ++
       " gol=" ++ show (gol . cur $ i) ++ " stk=" ++ show (stk . cur $ i)
+-}