module Interpreter where

import Data.Function
import qualified Data.Map as M

{- VAM 2P, done the lazy way -}

data StrTable =
  StrTable Int (M.Map Int String)

data Instr
  = Atom Int -- unify a constant
  | Struct (Int, Int) -- unify a structure with arity
  | NoGoal -- trivial goal
  | Goal -- we start a new goal, set up backtracking etc
  | Call -- all seems okay, call the goal
  | LastCall -- tail call the goal
  deriving Show

type Defs = M.Map (Int, Int) [Instr]

data Interp =
  Interp
    { defs :: Defs
    , hed :: [Instr]
    , gol :: [Instr]
    , stk :: [[Instr]]
    }

prove :: [Instr] -> Defs -> Bool
prove g ds =
  let i0 = Interp ds [NoGoal] [LastCall] [g]
      run (Left x) = x
      run (Right x) = run $ pr Right Left x
   in run (Right i0)

pr :: (Interp -> a) -> (Bool -> a) -> Interp -> a
pr c f i = go i
  where
    go i@Interp {hed = (Atom a:hs), gol = (Atom b:gs)} -- unify constants
      | a == b = c i {hed = hs, gol = gs}
    go i@Interp {hed = (Struct a:hs), gol = (Struct b:gs)} -- unify structs
      | a == b = c i {hed = hs, gol = gs}
    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = []} = f True -- final success
    go i@Interp { hed = [NoGoal]
                , gol = [LastCall]
                , stk = ((Goal:Struct f:gs):ss)
                } -- goal succeeded
      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs, stk = ss}
    go i@Interp {hed = [NoGoal], gol = (Call:Goal:Struct f:gs)} -- next goal
      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs}
    go i@Interp {hed = (Goal:Struct f:hs), gol = [LastCall]} -- tail call
      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs}
    go i@Interp {hed = (Goal:Struct f:hs), gol = (Call:gs), stk = ss} -- normal call
      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs, stk = gs : ss}
    go _ = f False -- bad luck