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 Datum
  = Atom Int -- unifies a constant
  | Struct (Int, Int) -- 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)
  deriving (Show, Eq, Ord)

data Instr
  = U Datum -- something unifiable
  | 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
  | Cut -- remove all alternative clauses of the current goal
  deriving (Show)

type Code = [Instr]

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

data Cho =
  Cho
    { hed :: Code -- head pointer
    , gol :: Code -- goal pointer
    , stk :: [Code] -- remaining "and" goals
    , cut :: [Cho] -- snapshot of choicepoints
    }
  deriving (Show)

data Interp =
  Interp
    { defs :: Defs -- global definitions for lookup
    , cur :: Cho -- the choice that is being evaluated right now
    , cho :: [Cho] -- remaining choice points
    }
  deriving (Show)

prove :: Code -> Defs -> Either (Interp, String) Bool
prove g ds =
  let i0 =
        Interp
          {defs = ds, cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}, cho = []}
      run (Left x) = x
      run (Right x) = run $ proveStep Right Left x
   in run (Right i0)

{- this gonna need Either String Bool for errors later -}
proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
proveStep c f i = go i
  where
    ifail msg = f $ Left (i, msg)
    withDef fn
      | Just d <- defs i M.!? fn = ($ d)
      | otherwise = const $ ifail $ "no definition: " ++ show fn
    {- Backtracking -}
    backtrack i@Interp {cho = chos}
      {- if available, restore the easiest choicepoint -}
      | (cho:chos) <- chos = c i {cur = cho, cho = chos}
      {- if there's no other choice, answer no -}
      | otherwise = f (Right False)
    {- Unification -}
    go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
     = unify a b
      where
        uok = c i {cur = cur {hed = hs, gol = gs}}
        unify (Atom a) (Atom b)
          | a == b = uok
        unify (Struct a) (Struct b)
          | a == b = uok
        unify _ _ = backtrack i
    {- Resulution -}
    go i@Interp {cur = cur@Cho {hed = hed, gol = gol, stk = stk}, cho = chos}
      {- top-level success -}
      | [NoGoal] <- hed
      , [LastCall] <- gol
      , [] <- stk = f (Right True)
      {- succeed and return to caller -}
      | [NoGoal] <- hed
      , [LastCall] <- gol
      , (Goal:U (Struct fn):gs):ss <- stk =
        withDef fn $ \(hs:ohs) ->
          c
            i
              { cur = cur {hed = hs, gol = gs, stk = ss}
              , cho = [Cho oh gs ss chos | oh <- ohs] ++ chos
              }
      {- start matching next goal -}
      | [NoGoal] <- hed
      , (Call:Goal:U (Struct fn):gs) <- gol =
        withDef fn $ \(hs:ohs) ->
          c
            i
              { cur = cur {hed = hs, gol = gs}
              , cho = [Cho oh gs stk chos | oh <- ohs] ++ chos
              }
      {- goal head matching succeeded, make a normal call -}
      | (Goal:U (Struct fn):ngs) <- hed
      , (Call:gs) <- gol =
        withDef fn $ \(hs:ohs) ->
          c
            i
              { cur = cur {hed = hs, gol = ngs, stk = gs : stk}
              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
              }
    {- R: Successful match continued by tail call -}
      | (Goal:U (Struct fn):ngs) <- hed
      , [LastCall] <- gol =
        withDef fn $ \(hs:ohs) ->
          c
            i
              { cur = cur {hed = hs, gol = ngs}
              , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
              }
    {- The End -}
    go _ = ifail "impossible instruction combo"