before going State

2 files changed, 191 insertions, 31 deletions

diff --git a/app/Frontend.hs b/app/Frontend.hs
index 8dc8b8a..2be4f68 100644
--- a/app/Frontend.hs
+++ b/app/Frontend.hs
@@ -92,6 +92,7 @@ addBuiltins = do
   b <- findAtom "b"
   c <- findAtom "c"
   b0 <- findStruct "b" 0
+  any <- findStruct "any" 1
   modify $ \s ->
     s
       { defs =
@@ -101,6 +102,7 @@ addBuiltins = do
               , [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
                 , [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
                 ])
+            , (any, [[I.U I.VoidVar, I.NoGoal]])
             ]
       , ops = [(",", P.Op 1000 $ P.Infix P.X P.Y)]
       }
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 76cef52..ffc812c 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -1,9 +1,9 @@
+{- VAM 2P, done the lazy way -}
 module Interpreter where
 
 import Data.Function
 import qualified Data.Map as M
 
-{- VAM 2P, done the lazy way -}
 data StrTable =
   StrTable Int (M.Map String Int) (M.Map Int String)
   deriving (Show)
@@ -25,9 +25,9 @@ data Id =
 data Datum
   = Atom Int -- unifies a constant
   | Struct Id -- unifies a structure with arity
-  | 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)
+  | VoidVar -- in code this unifies with anything; everywhere else this is an unbound variable
+  | LocalRef Int -- local variable idx
+  | HeapRef Int -- heap structure idx
   deriving (Show, Eq, Ord)
 
 data Instr
@@ -43,18 +43,32 @@ type Code = [Instr]
 
 type Defs = M.Map Id [Code]
 
+data Heap =
+  Heap Int (M.Map Int Datum)
+  deriving (Show)
+
+emptyHeap = Heap 1 M.empty
+
+type Scope = M.Map Int Int
+
+emptyScope :: Scope
+emptyScope = M.empty
+
 data Cho =
   Cho
     { hed :: Code -- head pointer
+    , hvar :: Scope -- variables unified in head (so far)
     , gol :: Code -- goal pointer
-    , stk :: [(Code, [Cho])] -- remaining "and" goals
+    , gvar :: Scope -- variables unified in the goal
+    , heap :: Heap -- a snapshot of the heap (there's no trail; we rely on CoW copies in other choicepoints)
+    , stk :: [(Code, Scope, [Cho])] -- remaining goals together with their vars and cuts
     , cut :: [Cho] -- snapshot of choicepoints before entering
     }
   deriving (Show)
 
 data Interp =
   Interp
-    { defs :: Defs -- global definitions for lookup
+    { defs :: Defs -- global definitions for lookup (TODO can we externalize?)
     , cur :: Cho -- the choice that is being evaluated right now
     , cho :: [Cho] -- remaining choice points
     }
@@ -65,13 +79,27 @@ prove g ds =
   let i0 =
         Interp
           { defs = ds
-          , cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}
+          , cur =
+              Cho
+                { hed = g
+                , hvar = emptyScope
+                , gol = [LastCall]
+                , gvar = emptyScope
+                , heap = emptyHeap
+                , stk = []
+                , cut = []
+                }
           , cho = []
           }
       run (Left x) = x
       run (Right x) = run $ proveStep Right (\i e -> Left (i, e)) x
    in run (Right i0)
 
+data Dereferenced
+  = FreeRef Int
+  | BoundRef Int Datum
+  | NoRef
+
 {- this gonna need Either String Bool for errors later -}
 proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a
 proveStep c f i = go i
@@ -90,20 +118,119 @@ proveStep c f i = go i
       {- if there's no other choice, answer no -}
       | otherwise = f i $ Right False
     {- Unification -}
-    go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
-     = unify a b
+    go i@Interp {cur = cur@Cho { hed = U h:hs
+                               , gol = U g:gs
+                               , heap = heap@(Heap _ hmap)
+                               }} = unify h g
+        {- termination tools -}
       where
         uok = c i {cur = cur {hed = hs, gol = gs}}
+        setHeap r x =
+          c i {cur = cur {hed = hs, gol = gs, heap = writeHeap r x heap}}
+        {- heap tools -}
+        deref x =
+          case hmap M.!? x of
+            Just (HeapRef x') ->
+              if x == x'
+                then FreeRef x'
+                else deref x'
+            Just x' -> BoundRef x x'
+            _ -> NoRef
+        writeHeap addr x (Heap nxt m) = Heap nxt (M.adjust (const x) addr m)
+        newHeapVar (Heap nxt m) =
+          (nxt, Heap (nxt + 1) (M.insert nxt (HeapRef nxt) m))
+        allocLocal scope reg cont
+          | Just addr <- scope M.!? reg = cont scope heap addr
+          | (addr, heap') <- newHeapVar heap =
+            cont (M.insert reg addr scope) heap' addr
+        newHeapStruct addr s@(Struct Id {arity = arity}) cont = undefined
+        {- simple cases first -}
         unify VoidVar VoidVar = uok
-        unify (Atom a) (Atom b) | a == b = uok
+        unify (Atom a) (Atom b)
+          | a == b = uok
         unify VoidVar (Atom _) = uok
         unify (Atom _) VoidVar = uok
-        unify (Struct a) (Struct b) | a == b = uok
-        unify VoidVar (Struct Id{arity=a}) = c i {cur = cur {hed = replicate a (U VoidVar) ++ hs, gol = gs}}
-        unify (Struct Id{arity=a}) VoidVar = c i {cur = cur {hed = hs, gol = replicate a (U VoidVar) ++ gs}}
+        unify (Struct a) (Struct b)
+          | a == b = uok
+        {- unifying a struct with void must cause us to skip the void -}
+        unify VoidVar (Struct Id {arity = a}) =
+          c i {cur = cur {hed = replicate a (U VoidVar) ++ hs, gol = gs}}
+        unify (Struct Id {arity = a}) VoidVar =
+          c i {cur = cur {hed = hs, gol = replicate a (U VoidVar) ++ gs}}
+        {- handle local refs; first ignore their combination with voids to save memory -}
+        unify (LocalRef _) VoidVar = uok
+        unify VoidVar (LocalRef _) = uok
+        {- allocate heap for LocalRefs and retry with HeapRefs -}
+        unify (LocalRef hv) (LocalRef gv) = undefined -- avoid allocating 2 things
+        unify (LocalRef hv) _ = undefined
+        unify _ (LocalRef gv) = undefined
+        {- handle heap refs; first ignore their combination with voids again -}
+        unify (HeapRef _) VoidVar = uok
+        unify VoidVar (HeapRef _) = uok
+        {- actual HeapRefs, these are dereferenced and then unified; decide between copying and linking -}
+        unify (HeapRef hr') g =
+          case deref hr' of
+            FreeRef hr ->
+              case g of
+                atom@(Atom _) -> setHeap hr atom
+                s@(Struct _) ->
+                  newHeapStruct
+                    hr
+                    s
+                    (\nhs nheap ->
+                       c i {cur = cur {hed = nhs ++ hs, gol = gs, heap = nheap}})
+                HeapRef gr' ->
+                  case deref gr' of
+                    FreeRef gr -> setHeap hr (HeapRef gr)
+                    BoundRef addr _ -> setHeap hr (HeapRef addr)
+                    _ -> ifail "dangling goal ref (from head ref)"
+            BoundRef _ atom@(Atom a) -> unify atom g
+            BoundRef addr struct@(Struct Id {arity = arity}) ->
+              c
+                i
+                  { cur =
+                      cur
+                        { hed =
+                            U struct :
+                            [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ hs
+                        , gol = U g : gs
+                        }
+                  }
+            _ -> ifail "dangling head ref"
+        unify h (HeapRef gr') =
+          case deref gr' of
+            FreeRef gr ->
+              case h of
+                atom@(Atom _) -> setHeap gr atom
+                s@(Struct _) ->
+                  newHeapStruct
+                    gr
+                    s
+                    (\ngs nheap ->
+                       c i {cur = cur {hed = hs, gol = ngs ++ gs, heap = nheap}})
+            BoundRef _ atom@(Atom b) -> unify h atom
+            BoundRef addr struct@(Struct Id {arity = arity}) ->
+              c
+                i
+                  { cur =
+                      cur
+                        { hed = U h : hs
+                        , gol =
+                            U struct :
+                            [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ gs
+                        }
+                  }
+            _ -> ifail "dangling goal ref"
         unify _ _ = backtrack i
-    {- Resulution -}
-    go i@Interp { cur = cur@Cho {hed = hed, gol = gol, stk = stk, cut = cut}
+    {- Resolution -}
+    go i@Interp { cur = cur@Cho { hed = hed
+                                , hvar = hvar
+                                , gol = gol
+                                , gvar = gvar
+                                , heap = heap
+                                , stk = stk
+                                , cut = cut
+                                }
                 , cho = chos
                 }
       {- top-level success -}
@@ -116,22 +243,40 @@ proveStep c f i = go i
       {- succeed and return to caller -}
       | [NoGoal] <- hed
       , Just nchos <- tailcut gol chos cut
-      , (Goal:U (Struct fn):gs, _):ss <- stk =
+      , (Goal:U (Struct fn):gs, ngvar, _):ss <- stk =
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = gs, stk = ss}
-              , cho = [Cho oh gs ss nchos | oh <- ohs] ++ nchos
+              { cur =
+                  cur
+                    { hed = hs
+                    , hvar = emptyScope
+                    , gol = gs
+                    , gvar = ngvar
+                    , stk = ss
+                    }
+              , cho =
+                  [Cho oh emptyScope gs ngvar heap ss nchos | oh <- ohs] ++
+                  nchos
               }
       {- succeed and return to caller, and the caller wants a cut -}
       | [NoGoal] <- hed
       , Just _ <- tailcut gol chos cut
-      , (Cut:Goal:U (Struct fn):gs, rchos):ss <- stk =
+      , (Cut:Goal:U (Struct fn):gs, ngvar, rchos):ss <- stk =
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = gs, stk = ss}
-              , cho = [Cho oh gs ss rchos | oh <- ohs] ++ rchos
+              { cur =
+                  cur
+                    { hed = hs
+                    , hvar = emptyScope
+                    , gol = gs
+                    , gvar = ngvar
+                    , stk = ss
+                    }
+              , cho =
+                  [Cho oh emptyScope gs ngvar heap ss rchos | oh <- ohs] ++
+                  rchos
               }
       {- start matching next goal -}
       | [NoGoal] <- hed
@@ -139,8 +284,9 @@ proveStep c f i = go i
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = gs}
-              , cho = [Cho oh gs stk chos | oh <- ohs] ++ chos
+              { cur = cur {hed = hs, hvar = emptyScope, gol = gs}
+              , cho =
+                  [Cho oh emptyScope gs gvar heap stk chos | oh <- ohs] ++ chos
               }
       {- start matching next goal after a cut -}
       | [NoGoal] <- hed
@@ -148,17 +294,27 @@ proveStep c f i = go i
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = gs}
-              , cho = [Cho oh gs stk cut | oh <- ohs] ++ cut
+              { cur = cur {hed = hs, hvar = emptyScope, gol = gs}
+              , cho =
+                  [Cho oh emptyScope gs gvar heap stk cut | oh <- ohs] ++ cut
               }
       {- goal head matching succeeded, make a normal call -}
       | (Goal:U (Struct fn):ngs) <- hed
       , (Call:gs) <- gol =
         withDef fn $ \(hs:ohs) ->
-          let nstk = (gs, chos) : stk
+          let nstk = (gs, gvar, chos) : stk
            in c i
-                  { cur = cur {hed = hs, gol = ngs, stk = nstk}
-                  , cho = [Cho oh ngs nstk chos | oh <- ohs] ++ chos
+                  { cur =
+                      cur
+                        { hed = hs
+                        , hvar = emptyScope
+                        , gol = ngs
+                        , gvar = hvar
+                        , stk = nstk
+                        }
+                  , cho =
+                      [Cho oh emptyScope ngs hvar heap nstk chos | oh <- ohs] ++
+                      chos
                   }
       {- successful match continued by tail call -}
       | (Goal:U (Struct fn):ngs) <- hed
@@ -166,8 +322,10 @@ proveStep c f i = go i
         withDef fn $ \(hs:ohs) ->
           c
             i
-              { cur = cur {hed = hs, gol = ngs}
-              , cho = [Cho oh ngs stk nchos | oh <- ohs] ++ nchos
+              { cur = cur {hed = hs, hvar = emptyScope, gol = ngs, gvar = hvar}
+              , cho =
+                  [Cho oh emptyScope ngs hvar heap stk nchos | oh <- ohs] ++
+                  nchos
               }
     {- The End -}
-    go _ = ifail "impossible instruction combo"
+    go _ = ifail "code broken: impossible instruction combo"