module Frontend where

import Builtins
import Code (Interp(..))
import CodeLens
import Control.Monad (when)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Except (except, runExceptT)
import Control.Monad.Trans.State.Lazy (evalStateT)
import qualified Data.Map as M
import Env (PrlgEnv)
import qualified IR
import qualified Interpreter as I
import Lens.Micro.Mtl
import Load
  ( compile
  , intern
  , loadExpansion
  , processInput
  , queryExpansion
  , shunt
  )
import System.Console.Haskeline

-- the signature of this is too ugly to include here
handleError m = do
  res <- runExceptT m
  case res of
    Left err -> do
      lift $ outputStrLn err
      cmdq .= []
    _ -> (pure () :: PrlgEnv ()) --prevents ambiguity

processCmd precompileHook ast' = do
  ast <- shunt ast'
  source <- lift $ intern ast >>= precompileHook
  compile source >>= lift . I.prove >>= except

interpreterStart :: PrlgEnv ()
interpreterStart = do
  addPrelude
  interpreterLoop True

interpreterLoop :: Bool -> PrlgEnv ()
interpreterLoop queryMode = do
  q <- use cmdq
  case q of
    [] -> do
      minput <-
        lift $
        getInputLine
          (if queryMode
             then "prlg? "
             else "prlg |- ")
      case minput of
        Nothing -> return ()
        Just "." -> interpreterLoop (not queryMode)
        Just input -> do
          handleError $ processInput "<user input>" queryMode input
          interpreterLoop queryMode
    ((mode, ast):asts) -> do
      cmdq .= asts
      handleError $ do
        resOK <-
          processCmd
            (if mode
               then queryExpansion
               else loadExpansion)
            ast
        finished <- lift $ null <$> use cmdq
        when finished . lift . lift . outputStrLn $
          case (resOK, queryMode) of
            (True, True) -> "yes."
            (False, True) -> "no proof."
            (True, False) -> "ok."
            (False, False) -> "rejected."
      interpreterLoop queryMode

interpreter :: InputT IO ()
interpreter =
  evalStateT
    interpreterStart
    (Interp
       { _defs = M.empty
       , _cur = error "no cur"
       , _cho = []
       , _ops = []
       , _opstash = []
       , _macrostash = []
       , _strtable = IR.emptystrtable
       , _cmdq = []
       })