-- | The interpreter REPL.
module Tempus.Interpreter (
    repl
) where


import Control.Arrow
import Control.Monad
import Control.Monad.Trans

import Data.Char
import Data.List
import Data.Maybe

import           System.Console.Haskeline
import           System.Directory
import           System.FilePath
import qualified System.IO.UTF8 as BU

import Tempus.Loc
import Tempus.Syntax
import Tempus.Parser
import Tempus.TypeCheck
import Tempus.Evaluation


version :: String
version = "0.1.0"

executableName :: String
executableName = "tempus"

-- | The state of the interpreter.
data IState = IState {
                  -- | The path of the file the current module was loaded from, or @Nothing@ if no
                  -- one is loaded.
                  modulePath :: Maybe FilePath,

                  -- TODO: merge typeEnv and evalEnv
                  -- | A list of all global variables from the currently loaded module and added
                  -- interactively with their corresponding inferred type.
                  typeEnv :: TypeEnv,

                  -- | A list of all type synonyms from the currently loaded module and added
                  -- interactively.
                  synEnv :: TypeSynEnv,

                  -- | Like @typeEnv@ but with the expressions of the variables.
                  evalEnv :: EvalEnv,

                  -- | A triple with the same lists as @typeEnv@, @synEnv@, and @evalEnv@ but only
                  -- including variables and types from the Prelude module.
                  preludeEnvs :: (TypeEnv, TypeSynEnv, EvalEnv)
              }

-- | Initial interpreter state with empty lists and no module path.
initIState :: IState
initIState = IState {
        modulePath = Nothing,
        typeEnv = [],
        synEnv  = [],
        evalEnv = [],
        preludeEnvs = ([], [], [])
    }

mergedTypeEnv st@IState { preludeEnvs = (vs, _, _) } = vs ++ typeEnv st
mergedSynEnv  st@IState { preludeEnvs = (_, ts, _) } = ts ++ synEnv st
mergedEvalEnv st@IState { preludeEnvs = (_, _, es) } = es ++ evalEnv st


-- TODO: Allow redeclaration of values/types
-- TODO: Catch Ctrl-C
-- | The main interpreter REPL loop with an optional path to a Prelude file that is loaded at
-- the start.
repl :: Maybe FilePath -> IO ()
repl preludePath = runInputT defaultSettings $ do
    outputStrLn $ "This is " ++ executableName ++ " version " ++ version

    mbInitSt <- maybe (return Nothing) (loadModule [] [] False) preludePath
    case mbInitSt of
        Nothing -> do
            outputStrLn "Warning: Loading the Prelude module failed!"
            loop initIState
        Just (vs, ts, es) -> do
            outputStrLn $ "Loaded Prelude module from file `" ++ fromJust preludePath ++ "'."
            loop $ initIState { preludeEnvs = (vs, ts, es) }

    where
      loop st = do
        let moduleName = maybe "" takeBaseName $ modulePath st
        input <- getInputLine $ moduleName ++ "> "
        case input >>= parseAction of
            Just (Command "?" _) -> do
                mapM_ outputStrLn helpLines
                loop st

            Just (Command "q" _) -> do
                outputStrLn $ "Leaving " ++ executableName ++ "."

            Just (Command "l" []) -> do
                outputStrLn $ "Unloading module."
                loop st { modulePath = Nothing, typeEnv = [], synEnv = [], evalEnv = [] }

            Just (Command "l" [path]) -> do
                let (tEnv, sEnv, _) = preludeEnvs st
                mbSt <- loadModule tEnv sEnv True path
                case mbSt of
                    Nothing           -> loop st
                    Just (vs, ts, es) -> loop st { modulePath = Just path,
                                                   typeEnv = vs,
                                                   synEnv  = ts,
                                                   evalEnv = es }

            Just (Command "v" []) -> do
                showEnvironments (typeEnv st, synEnv st, evalEnv st)
                loop st

            Just (Command "p" []) -> do
                showEnvironments $ preludeEnvs st
                loop st

            Just (Command "t" [s]) -> do
                case parseExpr s of
                    Left (Loc loc err) -> do
                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
                    Right expr -> do
                        case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of
                            Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err
                            Right t          -> do
                                outputStrLn $ "  " ++ show (SrcCode expr)
                                outputStrLn $ "    : " ++ show (SrcCode t)
                loop st

            Just (Expression s) -> do
                case parseExpr s of
                    Left (Loc loc err) -> do
                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
                    Right expr -> do
                        case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of
                            Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err
                            Right t          -> liftIO $ putStrLn $ show $
                                evalExpr (mergedSynEnv st) (mergedTypeEnv st) (mergedEvalEnv st) expr
                loop st

            Just (Declaration s) -> do
                case parseDecl s of
                    Left (Loc loc err) -> do
                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
                        loop st
                    Right decl -> do
                        let tEnv = mergedTypeEnv st
                            sEnv = mergedSynEnv st
                        case checkProgram tEnv sEnv [decl] of
                            Left (Loc loc err) -> do
                                outputStrLn $
                                    "*** type error: " ++ show loc ++ ": " ++ showTypeErr err
                                loop st
                            -- DeclVal
                            Right (vs@[(v, (_,t))], []) -> do
                                outputStrLn $ "  " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)
                                loop st { typeEnv = typeEnv st ++ vs,
                                          evalEnv = evalEnv st ++
                                                        [(v, let DeclVal _ _ e = decl in e )] }
                            -- DeclType
                            Right ([], ts@[_]) -> do
                                outputStrLn $ "  " ++ show (SrcCode decl)
                                loop st { synEnv = synEnv st ++ ts }

            _ -> do
                outputStrLn $ "Unknown command, try :? for help."
                loop st


-- | The list of lines to be displayed on @:?@.
helpLines :: [String]
helpLines = [
     -- "|                                                                              |"
        "  Available commands:", 
        "    :?                 Show this help",
        "    :q                 Quit",
        "    :l                 Unload the current loaded module",
        "    :l <file>          Load the module in file <file>",
        "    :v                 Show types of all currently loaded module variables",
        "    :p                 Show types of all Prelude variables",
        "    :t <expr>          Show the type of expression <expr>",
        "    <decl>             Depending on the declaration <decl>, bring a new value",
        "                       or type synonym into scope",
        "    <expr>             Evaluate the expression <expr>"
    ]

-- | Produces an error message string for the given context error.
showTypeErr :: ContextError -> String
showTypeErr err = case err of
    UndefinedVariable v -> "undefined variable `" ++ show (SrcCode v) ++ "'"
    DuplicateVariable v -> "variable `" ++ show (SrcCode v) ++ "' already defined"
    DuplicateType v -> "type `" ++ show (SrcCode v) ++ "' already defined"
    OccursCheck t1 t2 -> "cannot construct the infinite type " ++ show (SrcCode t1)
                              ++ " = " ++ show (SrcCode t2)
    SymbolClash t1 t2 -> "cannot match type " ++ show (SrcCode t1) ++ " with " ++ show (SrcCode t2)
    IncorrectVariances t -> "incorrect variances in type " ++ show (SrcCode t)
    UndefinedType v -> "undefiend type variable `" ++ show (SrcCode v) ++ "'"
    TypeArgsMismatch v -> "wrong number of arguments to type synonym `" ++ show (SrcCode v) ++ "'"
    NoMuType t -> "type " ++ show (SrcCode t) ++ " is not a mu type"
    NoNuType t -> "type " ++ show (SrcCode t) ++ " is not a nu type"
    NoRecType t -> "type " ++ show (SrcCode t) ++ " is neither a mu nor a nu type"


{- |
    Reads an UTF8 encoded file and returns the file content. This function prevents that a file
    is read lazily and is so being kept in a locked state if a parser error occurs before the
    complete file was processed.
-}
seqReadFile :: FilePath -> IO String
seqReadFile = fmap (\s -> length s `seq` s) . BU.readFile


{- |
    @loadModule tEnv sEnv verbose path@ reads a Tempus module from @path@ and parses and typechecks
    all definitions where the types from @tEnv@ and @tSyn@ can be used. The result are the lists
    of all variables with types, type synonyms and variables with expression from that module.
    If @verbose == True@ all type synonyms and variables with the inferred types are printed.
-}
loadModule :: TypeEnv -> TypeSynEnv -> Bool -> FilePath
           -> InputT IO (Maybe (TypeEnv, TypeSynEnv, EvalEnv))
loadModule tEnv sEnv verbose path = do
    exists <- liftIO $ doesFileExist path
    if exists
        then do
            s <- liftIO $ seqReadFile path
            case parseProgram s of
                Left (Loc loc err) -> do
                    outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
                    return Nothing

                Right prog -> case checkProgram tEnv sEnv prog of
                    Left (Loc loc err) -> do
                        outputStrLn $ "*** type error: " ++ show loc ++ ": " ++ showTypeErr err
                        return Nothing

                    Right (vs, ts) -> do
                        when verbose $ do
                            forM_ ts $ \(v, (vs, t)) ->
                                outputStrLn $ "  " ++ show (SrcCode $ DeclType (0,0) v vs t)
                            forM_ vs $ \(v, (_, t)) ->
                                outputStrLn $ "  " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)
                        return $ Just (vs, ts, zip (map fst vs) [e | DeclVal _ _ e <- prog])
        else do
            outputStrLn $ "File not found: " ++ path
            return Nothing

-- | Prints a list of type synonyms and variables with their types.
showEnvironments :: (TypeEnv, TypeSynEnv, EvalEnv) -> InputT IO ()
showEnvironments (tEnv, sEnv, eEnv) = do
    case zipWith (\(v, (_, t)) (_, e) -> (v, e, t)) tEnv eEnv of
        []  -> outputStrLn $ "No variables loaded."
        env -> do
            outputStrLn $ "Loaded variables: "
            forM_ env $ \(v, e, t) -> outputStrLn $
                "  " ++ show (SrcCode v) ++
                -- " = " ++ show (SrcCode e) ++
                " : " ++ show (SrcCode t)

    case sEnv of
        []  -> outputStrLn $ "No type synonyms loaded."
        env -> do
            outputStrLn $ "Loaded type synonyms: "
            forM_ env $ \(v, (vs, t)) -> outputStrLn $
                "  " ++ show (SrcCode $ DeclType (0,0) v vs t)
    
-- | An interpreter action.
data Action = Command String [String]
              -- ^ A generic command with the list of parameters.
            | Expression String
              -- ^ An expression.
            | Declaration String
              -- ^ A type or value definition.

-- TODO: parse filenames with spaces correctly
-- TODO: better type/value parsing
-- | Parses a string command to an interpreter action or returns @Nothing@ if the parsing failed.
parseAction :: String -> Maybe Action
parseAction (':':'t':c:cs)
    | isSpace c = Just $ Command "t" [cs]
parseAction (':':cmd) = case words cmd of
                            []     -> Nothing
                            (c:cs) -> Just $ Command c cs
parseAction s
    | "value " `isPrefixOf` s = Just $ Declaration s
    | "type " `isPrefixOf` s = Just $ Declaration s
parseAction s@(c:cs)
    | isSpace c = parseAction $ dropWhile isSpace cs
    | otherwise = Just $ Expression s
parseAction _ = Nothing