module Frontend where

import Builtins
import Code (Interp(..))
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 Env
import qualified IR
import qualified Interpreter as I
import qualified Parser as P
import System.Console.Haskeline
import qualified Text.Megaparsec as MP
import Text.Pretty.Simple

ppr :: Show a => a -> PrlgEnv ()
ppr x =
  liftIO $
  pPrintOpt
    CheckColorTty
    defaultOutputOptionsDarkBg
      { outputOptionsCompactParens = True
      , outputOptionsIndentAmount = 2
      , 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 -> C.internPrlg st prlgs
      underscore <- findAtom "_"
      prlgv <-
        withStrTable $ \st ->
          (st, C.variablizePrlg underscore (C.varIds st prlgi) prlgi)
      compile prlgv
    compile prlgv = do
      commaId <- findStruct "," 2
      -- TODO cut
      let code = C.seqGoals $ C.compileGoals commaId 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
  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
    (Interp
       { defs = M.empty
       , ops = []
       , strtable = IR.emptystrtable
       , cur = error "no cur"
       , cho = []
       })