module Binding
( newVar, unify, instantiate
) where
import Primitives
import Terms
import Nondeterminism
import Control.Monad
import Control.Applicative

newVar :: Name -> PrologStream Slot
newVar name = reversibly (newVarPrim name) unnewVarPrim

getVar :: Slot -> PrologStream (Maybe Term)
getVar slot = liftPrologIO (getVarPrim slot)

setVar :: Slot -> Term -> PrologStream ()
setVar slot value = reversibly set unset
  where
  set = do
    oldValue <- getVarPrim slot
    when (oldValue /= Nothing) (errorPrim "cannot set var that is already set")
    setVarPrim slot (Just value)
  unset = do
    oldValue <- getVarPrim slot
    when (oldValue == Nothing) (errorPrim "cannot unset var that is already unset")
    setVarPrim slot Nothing
  
unify :: Term -> Term -> PrologStream ()
unify (Compound h0 args0) (Compound h1 args1) = do
  when (h0 /= h1) empty 
  when (length args0 /= length args1) empty
  forM_ (zip args0 args1) $ \(arg0, arg1) ->
    unify arg0 arg1
unify (Var v0) (Var v1) | v0 == v1 = return ()  -- succeed with {} (no bindings)
unify (Var v0) t1 = do
  binding <- getVar v0
  case binding of
    Just t0 -> unify t0 t1
    Nothing -> setVar v0 t1
unify t0@(Compound _ _) t1@(Var _) = unify t1 t0

instantiate :: Term -> PrologStream Term
instantiate t@(Var v) = do
  binding <- getVar v
  case binding of
    Just t0 -> instantiate t0
    Nothing -> return t
instantiate (Compound h args) = do
  instantiatedArgs <- mapM instantiate args
  return (Compound h instantiatedArgs)