module Main where

{- TODO:
  profiling
  write tests
-}


import           Paths_Delta_Lambda          (version)
import           Control.Monad
import           Control.Applicative
import           Control.Monad.Except
import           Control.Monad.Reader
import           Data.Version
import           Data.Word                   (Word64)
import           Data.Char                   (isSpace, isNumber)
import           Data.ByteString             (writeFile, readFile)
import           Data.Text                   (Text, pack)
import           Data.Text.IO
import           Prelude                     hiding (getContents, putStrLn)
import           System.IO                   (Handle, IOMode (ReadMode, ReadWriteMode), withFile)

import           Data.Serialize
import           Options
import           System.FilePath             hiding ((</>))
import           System.Console.Haskeline
import           Text.Megaparsec             (SourcePos(..))

import AST
import Reduction
import Check
import Parser
import Printer                               ()

data ReplOptions = ReplOptions
  { interactive  :: Bool
  , writeHistory :: Bool
  , historyFileN :: String
  , noHelpPrompt :: Bool
  }

data FileOptions = FileOptions
  { usePreprocessor     :: Bool
  , compileToByteCode   :: Bool
  , saveMetadata        :: Bool
  , preprocessorOptions :: [String]
  }

data MainOptions = MainOptions
  { inFile              :: String
  , echoType            :: Bool
  , useExtension        :: [String]
  , replOptions         :: ReplOptions
  , fileOptions         :: FileOptions
  }

fileGroup :: Maybe Group
fileGroup = Just $ group "file" "file commands" "commands that only affect files"

replGroup :: Maybe Group
replGroup = Just $ group "repl" "repl commands" "commands that only affect the repl"

fileAndReplGroup :: Maybe Group
fileAndReplGroup = Just $ group "file-and-repl" "file and repl commands" "commands that both the file compiler and the repl interpreter share"

instance Options ReplOptions where
  defineOptions = pure ReplOptions
    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["interactive"]
          , optionDefault = False
          , optionShortFlags = ['n']
          , optionDescription = "start repl"
          , optionGroup = replGroup
          })

    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["write-history"]
          , optionDefault = True
          , optionShortFlags = ['w']
          , optionDescription = "enable writing to the history file"
          , optionGroup = replGroup
          })

    <*> defineOption optionType_string (\o -> o
          { optionLongFlags = ["history-file"]
          , optionDefault = "~/.delta-lambda"
          , optionShortFlags = ['f']
          , optionDescription = "set the history file name and location"
          , optionGroup = replGroup
          })

    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["no-help-prompt"]
          , optionDefault = False
          , optionShortFlags = ['k']
          , optionDescription = "dont issue help prompt on initial repl load"
          , optionGroup = replGroup
          })

instance Options FileOptions where
  defineOptions = pure FileOptions
    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["use-preprocessor"]
          , optionDefault = True
          , optionShortFlags = ['p']
          , optionDescription = "enable the preprocessor"
          , optionGroup = fileGroup
          })
    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["compile"]
          , optionDefault = False
          , optionShortFlags = ['o']
          , optionDescription = "enable compilation to bytecode"
          , optionGroup = fileGroup
          })
    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["without-metadata"]
          , optionDefault = False
          , optionShortFlags = ['s']
          , optionDescription = "save metadata during compilation to bytecode"
          , optionGroup = fileGroup
          })
    <*> defineOption (optionType_list ',' optionType_string) (\o -> o
          { optionLongFlags = ["preprocessor-flags"]
          , optionDefault = []
          , optionShortFlags = ['c']
          , optionDescription = "passes the proceeding flags to the preprocessor"
          , optionGroup = fileGroup
          })

instance Options MainOptions where
  defineOptions = pure MainOptions
    <*> defineOption optionType_string (\o -> o
          { optionLongFlags = ["in-file"]
          , optionDefault = "stdin"
          , optionShortFlags = ['i']
          , optionDescription =
              "input file usable extension must be one of "
              ++ "(*.dl, *.cdl). note that if the \"-n\""
              ++ " or \"--interactive\" flags are not used"
              ++ " in combination with this option, the compiler"
              ++ " will not load the file."
          , optionGroup = fileAndReplGroup
          })
    <*> defineOption optionType_bool (\o -> o
          { optionLongFlags = ["echo-type"]
          , optionDefault = True
          , optionShortFlags = ['e']
          , optionDescription = "enable echoing the type of a term after checking"
          , optionGroup = fileAndReplGroup
          })
    <*> defineOption (optionType_list ',' optionType_string) (\o -> o
          { optionLongFlags = ["use-extensions"]
          , optionDefault = []
          , optionShortFlags = ['x']
          , optionDescription =
              "enables a set of extensions"
          , optionGroup = fileAndReplGroup
          })
    <*> defineOptions
    <*> defineOptions

--version :: Version
--version = Version
--  { versionBranch = [0,3,0,0]
--  , versionTags = [] -- depreciated, but showVersion throws an exception without it
--  }

replPrompt :: Version -> String
replPrompt vers = Prelude.unlines
  [ "    /\\         /\\"
  , "   /  \\       /  \\"
  , "  / /\\ \\     / /\\ \\"
  , " / /__\\ \\   / /  \\ \\"
  , "/________\\ /_/    \\_\\"
  , "Welcome to Delta-Lambda, the 1000 line[s of haskell] theorem prover!"
  , "This is apha level software! no documentation currently, and dragons galore!"
  , "version: " ++ showVersion vers
  ]

helpPrompt :: String
helpPrompt = Prelude.unlines
  [ "/-----------------------------------------------------------------------------\\"
  , "| command | parameters | description                                          |"
  , "| :c      | input term | check that the input term is correct                 |"
  , "| :e      | posn, term | add a term to the context at the position            |"
  , "| :f      | input term | provide the final type of the input term             |"
  , "| :g      | position   | get the type of a term name (or position) in context |"
  , "| :h      |            | display this table                                   |"
  , "| :o      | file name  | open a file and load it                              |"
  , "| :q      |            | quit this repl                                       |"
  , "| :r      | input term | provide the normal form of the input term            |"
  , "| :t      | input term | provide the type of the input term                   |"
  , "| :s      | input flag | set a flag, restart the repl                         |"
  , "| :?      |            | syntax and semantics tutorial (not implemented)      |"
  , "\\-----------------------------------------------------------------------------/"
  ]

data ReplState = ReplState
  { replContext :: Context SourcePos Text Word64
  , replTerm    :: Maybe (Term SourcePos Text Word64)
  , replOpts    :: MainOptions
  }

-- I _*really*_ dislike the code following this comment
-- it basically is a bunch of shenanigans dealing with somewhat non-composible
-- MONADS. maybe I should just bite the bullet, and use exceptions in IO...


main :: IO ()
main = runCommand $ \opts _ ->
  if interactive $ replOptions opts then
    repl opts
  else
    if takeExtension (inFile opts) == ".dl" then
      withFile (inFile opts) ReadMode $ parseCheckAndType opts
    else
      if takeExtension (inFile opts) == ".cdl" then
        putStrLn . pack $ "cannot open binary file in non interactive mode!"
      else
        putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile opts)

preprocess :: MainOptions -> Text -> IO (Either String Text)
preprocess options fileContents =
  if usePreprocessor $ fileOptions options then
    preprocessor (preprocessorOptions $ fileOptions options) (inFile options) fileContents
  else return $ Right fileContents

compile :: (Serialize m , Serialize v, Serialize i) => Term m v i -> MainOptions -> IO ()
compile val options
  | not (saveMetadata $ fileOptions options) = Data.ByteString.writeFile compiledFilename (encode file)
  | otherwise =  Data.ByteString.writeFile compiledFilename (encode cleaned)
  where header = DecompiledFileHeader
          { compiledFileName = pack $ inFile options
          , interpreterVersion = version
          , extensionsUsed = map pack $ useExtension options
          }

        file = DecompiledFile
          { decompiledFileHeader = header
          , decompiledTerm = val
          }

        cleaned = transpile (const ()) id id file

        compiledFilename = dropExtension (inFile options) -<.> ".cdl"


checkAndType :: (Enum i, Show v, BetaEq (PseudoTerm SourcePos) v i) => Term SourcePos v i -> MainOptions -> Context SourcePos v i -> IO (Maybe ())
checkAndType term options context =
  case runReaderT (termCorrect term) context of
    Left err -> do
      putStrLn $ pack err
      return Nothing
    Right _
      | echoType options ->
        case runReaderT (typeSynth term) context of
          Left err -> do
            putStrLn $ pack err
            return Nothing
          Right val -> do
            putStrLn . pack $ show val
            return $ Just ()
      | otherwise -> return $ Just ()

-- touch, peel, and stand anyone?
parseCheckAndType :: MainOptions -> Handle -> IO ()
parseCheckAndType options file = do
  input <- Data.Text.IO.hGetContents file
  input' <- preprocess options input
  case input' of
    Left pperr -> putStrLn $ pack pperr
    Right ppval ->
      case parseInput ppval of
        Left perr -> putStrLn $ pack perr
        Right pval -> do
          checked <- checkAndType pval options []
          case checked of
            Nothing -> return ()
            Just _ ->
              when (compileToByteCode $ fileOptions options) $
                compile pval options

-- halp. much blegh. very not DRY. super wet.

repl :: MainOptions -> IO ()
repl options = do
  Data.Text.IO.putStr $ pack (replPrompt version)
  unless (noHelpPrompt (replOptions options)) $ Data.Text.IO.putStr (pack helpPrompt)
  if inFile options == "stdin" then
    runInputT replSettings $ loop (initReplState Nothing options)
    else
    if takeExtension (inFile options) == ".dl" then
      withFile (inFile options) ReadWriteMode $ \h -> do
        input <- Data.Text.IO.hGetContents h
        input' <- preprocess options input
        case input' of
          Left pperr -> putStrLn $ pack pperr
          Right ppval ->
            case parseInput ppval of
              Left perr -> putStrLn $ pack perr
              Right pval -> do
                checked <- checkAndType pval options []
                case checked of
                  Nothing -> return ()
                  Just _ -> runInputT replSettings $ loop (initReplState (Just pval) options)
    else
      if takeExtension (inFile options) == ".cdl" then do
        fileCont <- Data.ByteString.readFile (inFile options)
        case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
          Left perr -> putStrLn $ pack perr
          Right pval -> do
            let fvers = interpreterVersion (decompiledFileHeader pval)
            if fvers < version then
              putStrLn . pack $ "cannot load file \"" ++ inFile options ++ "\n" ++
              "compiler version of file:   " ++ showVersion fvers ++ "\n" ++
              "compiler version of system: " ++ showVersion version
              else do
                let val = decompiledTerm pval
                runInputT replSettings $ loop (initReplState (Just val) options)
      else
        putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile options)

  where replSettings = defaultSettings
          { historyFile = Just $ historyFileN (replOptions options)
          , autoAddHistory = writeHistory (replOptions options)
          }

initReplState term options = ReplState
  { replContext = []
  , replTerm = term
  , replOpts = options
  }

-- dragons. you where warned!

loop :: ReplState -> InputT IO ()
loop state = do
  let count = Prelude.length (replContext state)
  input <- getInputLine $ if count == 0 then "|- " else show count ++ " |- "
  case input of
    Nothing -> loop state
    Just (':':'c':' ':rest) ->
      case parseInput (pack rest) of
        Left perr -> do
          outputStrLn perr
          loop state
        Right pval -> do
          lift $ checkAndType pval (replOpts state) (replContext state)
          loop state
    Just (':':'e':' ':rest) -> do
      let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
      let termStr = dropWhile (\x -> not (isSpace x) && isNumber x) rest
      if null positionStr then do
        outputStrLn "please enter a non-negative number"
        loop state
        else do
          let position :: Int = read positionStr
          case parseInput $ pack termStr of
            Left perr -> do
              outputStrLn perr
              loop state
            Right pval -> do
              checked <- lift $ checkAndType pval (replOpts state) (replContext state)
              case checked of
                Nothing -> loop state
                Just _ -> do
                  let (before, after) = splitAt position (replContext state)
                  let pval' = bindContext (replContext state) 1 pval
                  loop (state { replContext = before ++ [pval'] ++ after })

    Just (':':'f':' ':rest) ->
      case parseInput (pack rest) of
        Left perr -> do
          outputStrLn perr
          loop state
        Right pval -> do
          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
          case checked of
            Nothing -> loop state
            Just _ ->
              case runReaderT (fTypeSynth pval) (replContext state) of
                Left err -> do
                  outputStrLn err
                  loop state
                Right val -> do
                  outputStrLn $ show val
                  loop state
    Just (':':'g':' ':rest) -> do
      let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
      if null positionStr then do
        outputStrLn "please enter a non-negative number"
        loop state
        else do
          let position :: Int = read positionStr
          if position > Prelude.length (replContext state) then do
            outputStrLn "position of term in context cannot be outside of context"
            loop state
            else do
            let term = replContext state !! (position - 1)
            outputStrLn $ show term
            loop state
    Just (':':'h':       _) -> do
      outputStrLn helpPrompt
      loop state
    Just (':':'o':' ':rest)
      | takeExtension rest == ".dl" -> do
        loaded <- lift $ withFile rest ReadWriteMode $ \h -> do
          input <- Data.Text.IO.hGetContents h
          input' <- preprocess (replOpts state) input
          case input' of
            Left pperr -> do
              putStrLn $ pack pperr
              return Nothing
            Right ppval ->
              case parseInput ppval of
                Left perr -> do
                  putStrLn $ pack perr
                  return Nothing
                Right pval -> do
                  checked <- checkAndType pval (replOpts state) []
                  case checked of
                    Nothing -> return Nothing
                    Just _ -> return $ Just pval
        case loaded of
          Nothing -> loop state
          Just val -> loop (state{ replTerm = Just val, replContext = [] })
      | takeExtension rest == ".cdl" -> do
          fileCont <- lift $ Data.ByteString.readFile rest
          case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
            Left perr -> do
              outputStrLn perr
              loop state
            Right pval -> do
              let fvers = interpreterVersion (decompiledFileHeader pval)
              if fvers < version then do
                outputStrLn $ "cannot load file \"" ++ rest ++ "\n" ++
                  "compiler version of file:   " ++ showVersion fvers ++ "\n" ++
                  "compiler version of system: " ++ showVersion version
                loop state
                else do
                  let val = decompiledTerm pval
                  loop (state { replTerm = Just val, replContext = [] })
      | otherwise -> do
          outputStrLn $ "extension not recognized: " ++ rest
          loop state
    Just (':':'q':       _) -> return ()
    Just (':':'r':' ':rest) ->
      case parseInput (pack rest) of
        Left perr -> do
          outputStrLn perr
          loop state
        Right pval -> do
          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
          case checked of
            Nothing -> loop state
            Just _ -> do
              outputStrLn $ show . nfTerm $ pval
              loop state
    Just (':':'t':' ':rest) ->
      case parseInput (pack rest) of
        Left perr -> do
          outputStrLn perr
          loop state
        Right pval -> do
          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
          case checked of
            Nothing -> loop state
            Just _ ->
              case runReaderT (typeSynth pval) (replContext state) of
                Left err -> do
                  outputStrLn err
                  loop state
                Right val -> do
                  outputStrLn $ show val
                  loop state
    Just (':':'s':' ':rest) -> do
      let pOpts = Options.parseOptions (split rest " ")
      case parsedOptions pOpts of
        Nothing ->
          case parsedError pOpts of
            Nothing -> do
              outputStrLn $ "an unknow error occured during proccessing of the options: "
                ++ "\n" ++ rest
              loop state
            Just err -> do
              outputStrLn err
              loop state
        Just opts -> loop (state {replOpts = opts})
    Just (':':'?':_) -> do
      outputStrLn "the turorial is under construction!"
      loop state
    Just input -> do
      outputStrLn $ "input : " ++ input ++ "\n not recognised"
      loop state

split :: String -> String -> [String]
split str pat = helper str pat [] [] where
    helper :: String -> String -> String -> String -> [String]
    helper [] _  n _ = [n]
    helper xs [] n _ = n : split xs pat
    helper (x:xs) (y:ys) n m
        | x /= y = helper xs pat ((n++m)++[x]) m
        | otherwise = helper xs ys n (m++[y])