module Frontend where

import Builtins
import Code (Interp(..))
import qualified Compiler as C
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Lazy (evalStateT, gets)
import Data.Foldable (traverse_)
import qualified Data.Map as M
import Env (PrlgEnv, findAtom, withStrTable)
import qualified IR
import qualified Interpreter as I
import qualified Parser as P
import System.Console.Haskeline
import qualified Text.Megaparsec as MP
import qualified Text.Pretty.Simple as Ppr

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

interpret :: String -> PrlgEnv Bool
interpret = (>> return True) . lex
  where
    lex input = do
      case MP.parse P.lexPrlg "-" input of
        Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
        Right toks -> parse toks
    parse toks = do
      case MP.parse P.parsePrlg "-" toks of
        Left bundle -> lift . outputStr $ MP.errorBundlePretty bundle
        Right asts -> traverse_ shunt asts
    shunt ast = do
      o <- gets ops
      case P.shuntPrlg o ast of
        Left err -> lift . outputStrLn $ "expression parsing: " ++ err
        Right prlg -> intern prlg
    intern prlgs = do
      prlgi <- withStrTable $ \st -> IR.internPrlg st prlgs
      underscore <- findAtom "_"
      list <- findAtom "[]"
      prlgv <-
        withStrTable $ \st ->
          ( st
          , C.squashVars $
            C.variablizePrlg underscore st $ C.desugarPrlg list prlgi)
      compile prlgv
    compile prlgv = do
      comma <- findAtom ","
      cut <- findAtom "!"
      let code = C.seqGoals $ C.compileGoals comma cut prlgv
      execute code
    execute code = do
      res <- I.prove code
      lift . outputStrLn $
        case res of
          Left err -> err
          Right res ->
            if res
              then "yes."
              else "no proof."

interpreterStart :: PrlgEnv ()
interpreterStart = do
  addPrelude
  interpreterLoop

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

interpreter :: InputT IO ()
interpreter =
  evalStateT
    interpreterStart
    (Interp
       { defs = M.empty
       , ops = []
       , opstash = []
       , strtable = IR.emptystrtable
       , cur = error "no cur"
       , cho = []
       })