{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ViewPatterns #-}

module Minilang.REPL.Types where

import Control.Exception (Exception)
import Data.Aeson (FromJSON, ToJSON)
import Data.Text as Text hiding (replicate)
import GHC.Generics
import Minilang.Lambda.Eval (Env, Term, newEnv)
import Minilang.Lambda.Infer (Context, newContext)
import Minilang.Lambda.Parser (AST)
import Minilang.Lambda.Unify (Type)
import Text.Read (readMaybe)

class Monad m => MonadREPL m where
  -- | Returns the current environment for this session
  -- Environment is made of an `Env`ironment binding names to `Decl`arations
  -- and typing `Context` binding names to `Value`s denoting evaluated types.
  getEnv :: m REPLEnv

  -- | Updates the current environment for this session.
  setEnv :: REPLEnv -> m ()

  -- | Handle some input, parsing, typechecking and possibly evaluating it.
  input :: m In

  -- | Produces some output
  output :: Out -> m ()

  -- | Prompt for some input
  prompt :: m ()

  -- | Read given file
  load :: Text -> m (Either REPLError Text)

-- | Possible error in REPL interactions
data REPLError
  = FileError IOError
  | REPLError Text
  deriving (Eq, Show)

instance Exception REPLError

-- | REPL state
data REPLEnv = REPLEnv
  { env :: Env
  , context :: Context
  , curIndent :: Int
  , stepTypeCheck :: Bool
  , debugParser :: Bool
  , language :: Language
  , evaluator :: Evaluator
  }

initialREPL :: REPLEnv
initialREPL = REPLEnv newEnv newContext 0 False False Untyped DeBruijn

-- | Input
data In
  = EOF
  | In Text
  | Com Command
  deriving (Eq, Show, Generic, ToJSON, FromJSON)

data Command
  = ClearEnv
  | DumpEnv
  | Set Flag
  | Load Content
  | Help
  deriving (Eq, Show, Generic, ToJSON, FromJSON)

data Content
  = File Text
  | Data Text
  deriving (Eq, Show, Generic, ToJSON, FromJSON)

data Out
  = Defined Text (Maybe Type)
  | Evaluated AST Term (Maybe Type)
  | CurrentEnv Env Context Language
  | Msg Text
  | Bye
  deriving (Eq, Show, Generic, ToJSON, FromJSON)

data Flag
  = StepTypeChecker Bool
  | DebugParser Bool
  | SelectLanguage Language
  | SelectEvaluator Evaluator
  deriving (Eq, Show, Generic, ToJSON, FromJSON)

data Language = Untyped | Typed
  deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)

-- | Which reduction strategy to use.
--
-- * 'DeBruijn' — call-by-value head reduction on De Bruijn-indexed terms
--   (the original evaluator).
-- * 'NbE' — Normalisation by Evaluation: eval to a 'Value' semantic domain,
--   then read back to a 'Term'.  Reduces under lambda binders and therefore
--   produces fully-normalised terms.
data Evaluator = DeBruijn | NbE
  deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)

-- | "Parse" given `Text` into some input for the REPL
interpret ::
  Text -> In
interpret ":q" = EOF
interpret ":quit" = EOF
interpret ":h" = Com Help
interpret ":help" = Com Help
interpret ":e" = Com DumpEnv
interpret ":env" = Com DumpEnv
interpret ":c" = Com ClearEnv
interpret ":clear" = Com ClearEnv
interpret ":set step" = Com $ Set $ StepTypeChecker True
interpret ":unset step" = Com $ Set $ StepTypeChecker False
interpret ":set debug" = Com $ Set $ DebugParser True
interpret ":unset debug" = Com $ Set $ DebugParser False
interpret (unpack -> (':' : 'l' : ' ' : file)) = Com $ Load $ File $ strip $ pack file
interpret (unpack -> (':' : 'l' : 'o' : 'a' : 'd' : ' ' : file)) = Com $ Load $ File $ strip $ pack file
interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
  case readMaybe lang of
    Nothing -> Com Help
    Just l -> Com $ Set $ SelectLanguage l
interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) =
  case readMaybe ev of
    Nothing -> Com Help
    Just e -> Com $ Set $ SelectEvaluator e
interpret t = In t

helpText :: Text
helpText =
  Text.unlines
    [ "REPL Commands Help:"
    , "   :h(elp)          : Display this help"
    , "   :q(uit)          : Exit the interpreter"
    , "   :e(nv)           : Displays the current interpreter's environment"
    , "                      This dumps both the Environment, where values are defined,"
    , "                      and the typing Context, where types are defined. "
    , "   :c(lear)         : Clear the current interpreter's environment"
    , "   :set <option>    : Set an option modifying the interpreter's behaviour"
    , "   :unset <option>  : Remove an option that's been set previously"
    , "   :l(oad) <file>   : load content of <file> into the interpreter, parsing and type-checking it"
    , "   :lang <Language> : Switch type-checking language (Untyped | Typed)"
    , "   :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)"
    , ""
    , "Options: "
    , "   step             : Run the typechecker step-by-step, pausing at each rule application and"
    , "                      waiting for user to hit <enter> key to continue"
    , "   debug            : Debug parser, displaying the trail of rules tried and triggered"
    ]