diff --git a/app/Builtins.hs b/app/Builtins.hs
index a12da07..c63fb25 100644
--- a/app/Builtins.hs
+++ b/app/Builtins.hs
@@ -1,17 +1,6 @@
 module Builtins where
 
-import Code
-  ( Builtin(..)
-  , Code
-  , Datum(..)
-  , Dereferenced(..)
-  , Instr(..)
-  , InterpFn
-  , InterpFn
-  , derefHeap
-  , heapStruct
-  , newHeapVars
-  )
+import Code (Builtin(..), Code, Datum(..), Instr(..), InterpFn)
 import CodeLens
 import qualified Compiler as Co
 import Control.Exception (IOException, catch)
@@ -23,6 +12,7 @@ import Data.List (intercalate)
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
 import Env (PrlgEnv(..), findAtom, findStruct, prlgError)
+import Heap (Dereferenced(..), derefHeap, heapStruct, newHeapVars)
 import qualified IR
 import Interpreter (backtrack)
 import Lens.Family2.State
@@ -199,8 +189,8 @@ structUnify arity str = do
   h <- use (cur . heap)
   scope <- use (cur . hvar)
   listAtom <- findAtom "[]"
+  pvars <- newHeapVars arity
   let hcode = map U $ maybe VoidRef HeapRef . (scope M.!?) <$> [0 .. 2]
-      (h', pvars) = newHeapVars arity h
       structData =
         Struct IR.Id {IR.arity = arity, IR.str = str} : map HeapRef pvars
       paramsData =
@@ -210,7 +200,6 @@ structUnify arity str = do
         [Atom listAtom]
       gcode = map U $ structData ++ [Atom str] ++ paramsData
   zoom cur $ do
-    heap .= h'
     gol %= (gcode ++)
     hed %= (hcode ++)
   continue
diff --git a/app/Code.hs b/app/Code.hs
index 4473287..684686f 100644
--- a/app/Code.hs
+++ b/app/Code.hs
@@ -23,7 +23,7 @@ data Instr
   | Invoke Builtin -- give control to a builtin (invoked from head)
   | Done -- all done, can return
   | Cut -- remove choicepoints of the current goal
-  | Choices [[Code]] -- split off several possibilities (push choicepoints)
+  | Choices [Code] -- split off several possibilities (push choicepoints)
   deriving (Show)
 
 type Code = [Instr]
@@ -77,59 +77,3 @@ data Builtin =
 
 instance Show Builtin where
   show _ = "Builtin _"
-
-data Dereferenced
-  = FreeRef Int
-  | BoundRef Int Datum
-  | NoRef
-  deriving (Show, Eq)
-
--- TRICKY: HeapRefs alone must not form a cycle other than the FreeRef case.
-derefHeap :: Heap -> Int -> Dereferenced
-derefHeap h@(Heap _ hmap) x =
-  case hmap M.!? x of
-    Just (HeapRef x') ->
-      if x == x'
-        then FreeRef x'
-        else derefHeap h x'
-    Just x' -> BoundRef x x'
-    _ -> NoRef
-
-writeHeap :: Int -> Datum -> Heap -> Heap
-writeHeap addr x (Heap nxt m) = Heap nxt (M.adjust (const x) addr m)
-
-newHeapVar :: Heap -> (Heap, Int)
-newHeapVar heap = head <$> newHeapVars 1 heap
-
-newHeapVars :: Int -> Heap -> (Heap, [Int])
-newHeapVars n (Heap nxt m) =
-  let addrs = [nxt + i - 1 | i <- [1 .. n]]
-   in ( Heap (nxt + n) $
-        foldr (uncurry M.insert) m [(a, HeapRef a) | a <- addrs]
-      , addrs)
-
-withNewHeapStruct :: Int -> Datum -> Heap -> ([Datum] -> Heap -> a) -> a
-withNewHeapStruct addr s@(Struct Id {arity = arity}) heap cont =
-  let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap
-      m'' = M.insert addr (HeapRef $ head addrs) . M.insert (head addrs) s $ m'
-   in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
-
-heapStruct ::
-     Monad m
-  => (Datum -> m a)
-  -> (Datum -> [a] -> m a)
-  -> (Datum -> Int -> m a)
-  -> Heap
-  -> Int
-  -> m a
-heapStruct atom struct rec (Heap _ heap) hr = go [hr] hr
-  where
-    go visited ref
-      | rr@(HeapRef r) <- heap M.! ref =
-        if r == ref || r `elem` visited
-          then rec rr ref
-          else go (r : visited) r
-      | s@(Struct (IR.Id _ arity)) <- heap M.! ref =
-        sequence [go (ref + i : visited) (ref + i) | i <- [1 .. arity]] >>=
-        struct s
-      | x <- heap M.! ref = atom x
diff --git a/app/Compiler.hs b/app/Compiler.hs
index 749ecdb..afa7e71 100644
--- a/app/Compiler.hs
+++ b/app/Compiler.hs
@@ -3,7 +3,8 @@ module Compiler where
 import Data.Char (isUpper)
 import qualified Data.Map as M
 
-import Code (Code, Datum(..), Heap, Instr(..), heapStruct)
+import Code (Code, Datum(..), Heap, Instr(..))
+import Heap (heapStruct)
 import IR (Id(..), PrlgInt(..), StrTable(..))
 
 desugarPrlg :: Int -> PrlgInt -> PrlgInt
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
diff --git a/prlg.cabal b/prlg.cabal
index 929d3ee..5e2fee0 100644
--- a/prlg.cabal
+++ b/prlg.cabal
@@ -25,7 +25,7 @@ executable prlg
     main-is:          Main.hs
 
     -- Modules included in this executable, other than Main.
-    other-modules:    Interpreter, Compiler, Parser, Frontend, IR, Operators, Code, Builtins, Env, Load, CodeLens
+    other-modules:    Interpreter, Compiler, Parser, Frontend, IR, Operators, Code, Builtins, Env, Load, CodeLens, Heap
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions: