1 files changed, 118 insertions, 11 deletions

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 4f21709..ecf1ebe 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -1,25 +1,23 @@
-{- pražský přehledný stroj -}
+{-# LANGUAGE RankNTypes #-}
+
 module Interpreter where
 
+{- pražský přehledný stroj -}
 import Code
   ( Builtin(..)
   , Cho(..)
   , Code
   , Datum(..)
-  , Dereferenced(..)
   , Instr(..)
   , InterpFn
-  , derefHeap
   , emptyHeap
   , emptyScope
-  , newHeapVar
-  , withNewHeapStruct
-  , writeHeap
   )
 import CodeLens
 import Control.Monad (when)
 import qualified Data.Map as M
 import Env (PrlgEnv)
+import Heap
 import IR (Id(..), StrTable(..))
 import Lens.Family2
 import Lens.Family2.State
@@ -85,6 +83,7 @@ headStep h = do
   case (h, g) of
     ([Done], _) -> succeedHead
     (Cut:_, _) -> cutHead
+    (Invoke (Builtin bf):_, _) -> advanceHead >> bf
     (_, [Done]) -> tailCall
     (_, [Cut, Done]) -> tailCut
     (_, _) -> pushCall
@@ -117,6 +116,7 @@ advanceHead = do
   cur . hed %= tail
   continue
 
+{- resolution steps -}
 doCut = use (cur . cut) >>= assign cho
 
 retCut = do
@@ -201,11 +201,118 @@ succeedGoal = do
         stk .= st'
       continue
 
-pushChoices :: [[Code]] -> InterpFn
-pushChoices cs = undefined
+pushChoices :: [Code] -> InterpFn
+pushChoices cs = do
+  advance
+  g <- use (cur . gol)
+  let (ng:ogs) = [c ++ g | c <- cs]
+  cc <- use cur
+  cur . gol .= ng
+  cho %= ([cc & gol .~ og | og <- ogs] ++)
+  continue
+
+{- unification -}
+uNext = do
+  advanceHead
+  advance
+  cur . unis -= 1
+
+uOK :: InterpFn
+uOK = uNext >> continue
 
 unify :: Datum -> Datum -> InterpFn
-unify = undefined
+unify VoidRef VoidRef = uOK
+unify (Atom _) VoidRef = uOK
+unify VoidRef (Atom _) = uOK
+unify (Atom a) (Atom b)
+  | a == b = uOK
+unify (Number _) VoidRef = uOK
+unify VoidRef (Number _) = uOK
+unify (Number a) (Number b)
+  | a == b = uOK
+unify (Struct a) VoidRef = do
+  uNext
+  cur . gol %= (replicate (arity a) (U VoidRef) ++)
+  continue
+unify VoidRef (Struct a) = do
+  uNext
+  cur . hed %= (replicate (arity a) (U VoidRef) ++)
+  continue
+unify (Struct a) (Struct b)
+  | a == b = do
+    cur . unis += arity a
+    uOK
+unify (LocalRef _) VoidRef = uOK
+unify VoidRef (LocalRef _) = uOK
+unify (LocalRef lr) g = do
+  r <- findLocalRef hvar lr
+  unify (HeapRef r) g
+unify h (LocalRef lr) = do
+  r <- findLocalRef gvar lr
+  unify h (HeapRef r)
+unify VoidRef (HeapRef _) = uOK
+unify (HeapRef _) VoidRef = uOK
+unify (HeapRef hr) (HeapRef gr) = do
+  [h, g] <- traverse deref [hr, gr]
+  case (h, g) of
+    (BoundRef ha _, BoundRef ga _)
+      | ha == ga -> uOK
+    (BoundRef ha hv@(Struct Id {arity = arity}), BoundRef ga gv@(Struct _)) ->
+      if hv /= gv
+        then backtrack
+        else do
+          writeHeap ha (HeapRef ga) -- cycle unification trick thanks to Bart Demoen
+          uNext
+          cur . hed %= ([U . HeapRef $ ha + i | i <- [1 .. arity]] ++)
+          cur . gol %= ([U . HeapRef $ ga + i | i <- [1 .. arity]] ++)
+          cur . unis += arity
+          continue
+    (BoundRef _ hv, BoundRef _ gv)
+      | hv == gv -> uOK
+    (FreeRef ha, FreeRef ga) -> writeHeap ha (HeapRef ga) >> uOK
+    (FreeRef ha, BoundRef ga _) -> writeHeap ha (HeapRef ga) >> uOK
+    (BoundRef ha _, FreeRef ga) -> writeHeap ga (HeapRef ha) >> uOK
+    _ -> backtrack
+unify s@(Struct _) (HeapRef gr) = setStruct gr s gol
+unify (HeapRef hr) s@(Struct _) = setStruct hr s hed
+unify (Struct sa) (Struct sb)
+  | sa == sb = cur . unis += arity sa >> uOK
+unify h (HeapRef gr) = setSimple gr h
+unify (HeapRef hr) g = setSimple hr g
+unify _ _ = backtrack
+
+{- unification reference-handling tools -}
+findLocalRef :: Lens' Cho (M.Map Int Int) -> Int -> PrlgEnv Int
+findLocalRef store lr = do
+  a' <- (cur . store) `uses` (M.!? lr)
+  case a' of
+    Nothing -> do
+      a <- newHeapVar
+      cur . store %= M.insert lr a
+      pure a
+    Just a -> pure a
+
+setStruct :: Int -> Datum -> Lens' Cho Code -> InterpFn
+setStruct addr s@(Struct Id {arity = arity}) code = do
+  x <- deref addr
+  let cont nc = do
+        uNext
+        cur . unis += arity
+        cur . code %= (map U nc ++)
+        continue
+  case x of
+    FreeRef a -> putHeapStruct a s >>= cont
+    BoundRef a s'@(Struct _)
+      | s == s' -> cont [HeapRef (a + i) | i <- [1 .. arity]]
+    _ -> backtrack
+
+setSimple addr val = do
+  x <- deref addr
+  case x of
+    FreeRef a -> writeHeap a val >> uOK
+    BoundRef _ val'
+      | val == val' -> uOK
+    _ -> backtrack
 {- original, TODO remove -}
 {-proveStep :: InterpFn
 proveStep = St.get >>= go
@@ -281,7 +388,7 @@ proveStep = St.get >>= go
         unify (HeapRef hr) (HeapRef gr)
           | BoundRef ha _ <- deref hr
           , BoundRef ga _ <- deref gr
-          , ha == ga = uok
+          , ha == ga = uok -- BUG, structs!
           | FreeRef ha <- deref hr
           , BoundRef ga _ <- deref gr = setHeap ha (HeapRef ga)
           | BoundRef ha _ <- deref hr
@@ -421,7 +528,7 @@ proveStep = St.get >>= go
       , (Call:Goal:U (Struct fn):gs) <- gol =
         withDef fn $ \(hs:ohs) ->
           c
-            i
+        i
               { cur = cur {hed = hs, hvar = emptyScope, gol = gs}
               , cho =
                   [Cho oh emptyScope gs gvar heap stk chos | oh <- ohs] ++ chos