module Frontend where

import qualified Compiler as C
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Lazy
import Data.Foldable (traverse_)
import qualified Data.Map as M
import qualified Interpreter as I
import qualified Parser as P
import System.Console.Haskeline
import qualified Text.Megaparsec as MP
import Text.Pretty.Simple

data PrlgState =
  PrlgState
    { defs :: I.Defs
    , ops :: P.Ops
    , strtable :: I.StrTable
    }
  deriving (Show)

type PrlgEnv a = StateT PrlgState (InputT IO) a

ppr :: Show a => a -> PrlgEnv ()
ppr x =
  liftIO $
  pPrintOpt
    CheckColorTty
    defaultOutputOptionsDarkBg
      { outputOptionsCompactParens = True
      , outputOptionsIndentAmount = 2
      , outputOptionsPageWidth = 80
      }
    x

withStrTable :: (I.StrTable -> (I.StrTable, a)) -> PrlgEnv a
withStrTable f = do
  st <- gets strtable
  let (st', x) = f st
  modify (\s -> s {strtable = st'})
  return x

findStruct :: String -> Int -> PrlgEnv I.Id
findStruct str arity = do
  stri <- findAtom str
  return I.Id {I.str = stri, I.arity = arity}

findAtom :: String -> PrlgEnv Int
findAtom = withStrTable . flip I.strtablize

interpret :: String -> PrlgEnv Bool
interpret = (>> return True) . lex
  where
    lex input = do
      case MP.parse P.lexPrlg "-" input of
        Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
        Right toks -> parse toks
    parse toks = do
      case MP.parse P.parsePrlg "-" toks of
        Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
        Right asts -> traverse_ prologize asts
    prologize ast = do
      o <- gets ops
      case P.ast2prlg o ast of
        Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
        Right prlg -> intern prlg
    intern prlgs = do
      prlgi <-
        withStrTable $ \st -> C.strtablizePrlg (C.varnames prlgs) st prlgs
      compile prlgi
    compile prlgi
      {- TODO: switch between prove goal/compile clause here -}
     = do
      commaId <- findStruct "," 2
      let code = C.seqGoals $ C.compileGoals commaId prlgi
      execute code
    execute code = do
      ds <- gets defs
      let (_, res) = I.prove code ds
      case res of
        Left err -> liftIO $ putStrLn err
        Right res ->
          liftIO $
          putStrLn $
          if res
            then "yes."
            else "no proof."

addBuiltins = do
  a1 <- findStruct "a" 1
  a <- findAtom "a"
  b <- findAtom "b"
  c <- findAtom "c"
  b0 <- findStruct "b" 0
  any <- findStruct "any" 1
  eq <- findStruct "=" 2
  modify $ \s ->
    s
      { defs =
          M.fromList
            [ (eq, [[I.U (I.LocalRef 0),I.U (I.LocalRef 0), I.NoGoal]])
            , (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
            , ( b0
              , [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
                , [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
                ])
            , (any, [[I.U I.VoidRef, I.NoGoal]])
            ]
      , ops =
        [ (",", P.Op 1000 $ P.Infix P.X P.Y)
        , ("=", P.Op 700 $ P.Infix P.X P.X)
        ]
      }

interpreterStart :: PrlgEnv ()
interpreterStart = do
  addBuiltins
  interpreterLoop

interpreterLoop :: PrlgEnv ()
interpreterLoop = do
  minput <- lift $ getInputLine "prlg> "
  case minput of
    Nothing -> return ()
    Just input -> do
      continue <- interpret input
      if continue
        then interpreterLoop
        else return ()

interpreter :: InputT IO ()
interpreter =
  evalStateT
    interpreterStart
    (PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable})