{-|
Module      : Idris.REPL.Parser
Description : Parser for the REPL commands.
License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts #-}
module Idris.REPL.Parser (
    parseCmd
  , help
  , allHelp
  , setOptions
  ) where

import Idris.AbsSyntax
import Idris.Colours
import Idris.Core.TT
import Idris.Help
import Idris.Imports
import Idris.Options
import qualified Idris.Parser as IP
import qualified Idris.Parser.Expr as IP
import qualified Idris.Parser.Helpers as IP
import qualified Idris.Parser.Ops as IP

import Idris.REPL.Commands

import Control.Applicative
import Control.Monad.State.Strict
import Data.Char (isSpace, toLower)
import Data.List
import Data.List.Split (splitOn)
import System.Console.ANSI (Color(..))
import System.FilePath ((</>))
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P

parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)
parseCmd i inputname = IP.runparser pCmd i inputname . trim
    where trim = f . f
              where f = reverse . dropWhile isSpace

type CommandTable = [ ( [String], CmdArg, String
                    , String -> IP.IdrisParser (Either String Command) ) ]

setOptions :: [(String, Opt)]
setOptions = [("errorcontext", ErrContext),
              ("showimplicits", ShowImpl),
              ("originalerrors", ShowOrigErr),
              ("autosolve", AutoSolve),
              ("nobanner", NoBanner),
              ("warnreach", WarnReach),
              ("evaltypes", EvalTypes),
              ("desugarnats", DesugarNats)]

help :: [([String], CmdArg, String)]
help = (["<expr>"], NoArg, "Evaluate an expression") :
  [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

allHelp :: [([String], CmdArg, String)]
allHelp = [ (map (':' :) names, args, text)
          | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]

parserCommandsForHelp :: CommandTable
parserCommandsForHelp =
  [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
  , exprArgCmd ["core"] Core "View the core language representation of a term"
  , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
  , (["doc"], NameArg, "Show internal documentation", cmd_doc)
  , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"
    , genArg "namespace" (P.many P.anyChar) MakeDoc)
  , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"
    , cmd_apropos)
  , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg
    , " Search for values by type", cmd_search)
  , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"
  , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"
  , namespaceArgCmd ["browse"] Browse "List the contents of some namespace"
  , nameArgCmd ["total"] TotCheck "Check the totality of a name"
  , noArgCmd ["r", "reload"] Reload "Reload current file"
  , noArgCmd ["w", "watch"] Watch "Watch the current file for changes"
  , (["l", "load"], FileArg, "Load a new file"
    , strArg (\f -> Load f Nothing))
  , (["!"], ShellCommandArg, "Run a shell command", strArg RunShellCommand)
  , (["cd"], FileArg, "Change working directory"
    , strArg ChangeDirectory)
  , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons
  , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"
  , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables or holes)"
  , (["p", "prove"], MetaVarArg, "Prove a metavariable"
    , nameArg (Prove False))
  , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell"
    , nameArg (Prove True))
  , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)
  , (["rmproof"], NameArg, "Remove proof from proof stack"
    , nameArg RmProof)
  , (["showproof"], NameArg, "Show proof"
    , nameArg ShowProof)
  , noArgCmd ["proofs"] Proofs "Show available proofs"
  , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"
  , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)
  , (["exec", "execute"], OptionalArg ExprArg, "Compile to an executable and run", cmd_execute)
  , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)
  , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)
  , noArgCmd ["?", "h", "help"] Help "Display this help text"
  , optArgCmd ["set"] SetOpt $ "Set an option (" ++ optionsList ++ ")"
  , optArgCmd ["unset"] UnsetOpt "Unset an option"
  , (["color", "colour"], ColourArg
    , "Turn REPL colours on or off; set a specific colour"
    , cmd_colour)
  , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)
  , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth)
  , noArgCmd ["q", "quit"] Quit "Exit the Idris system"
  , noArgCmd ["version"] ShowVersion "Display the Idris version"
  , noArgCmd ["warranty"] Warranty "Displays warranty information"
  , (["let"], ManyArgs DeclArg
    , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"
    , cmd_let)
  , (["unlet", "undefine"], ManyArgs NameArg
    , "Remove the listed repl definitions, or all repl definitions if no names given"
    , cmd_unlet)
  , nameArgCmd ["printdef"] PrintDef "Show the definition of a function"
  , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg))
    , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."
    , cmd_pprint)
  , (["verbosity"], NumberArg, "Set verbosity level", cmd_verb)
  ]
  where optionsList = intercalate ", " $ map fst setOptions


parserCommands :: CommandTable
parserCommands =
  [ noArgCmd ["u", "universes"] Universes "Display universe constraints"
  , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"

  , nameArgCmd ["d", "def"] Defn "Display a name's internal definitions"
  , nameArgCmd ["transinfo"] TransformInfo "Show relevant transformation rules for a name"
  , nameArgCmd ["di", "dbginfo"] DebugInfo "Show debugging information for a name"

  , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression"
  , exprArgCmd ["spec"] Spec "?"
  , exprArgCmd ["whnf"] WHNF "(Debugging) Show weak head normal form of an expression"
  , exprArgCmd ["inline"] TestInline "?"
  , proofArgCmd ["cs", "casesplit"] CaseSplitAt
      ":cs <line> <name> splits the pattern variable on the line"
  , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom
      ":apc <line> <name> adds a pattern-matching proof clause to name on line"
  , proofArgCmd ["ac", "addclause"] AddClauseFrom
      ":ac <line> <name> adds a clause for the definition of the name on the line"
  , proofArgCmd ["am", "addmissing"] AddMissing
      ":am <line> <name> adds all missing pattern matches for the name on the line"
  , proofArgCmd ["mw", "makewith"] MakeWith
      ":mw <line> <name> adds a with clause for the definition of the name on the line"
  , proofArgCmd ["mc", "makecase"] MakeCase
      ":mc <line> <name> adds a case block for the definition of the metavariable on the line"
  , proofArgCmd ["ml", "makelemma"] MakeLemma "?"
  , (["log"], NumberArg, "Set logging level", cmd_log)
  , ( ["logcats"]
    , ManyArgs NameArg
    , "Set logging categories"
    , cmd_cats)
  , (["lto", "loadto"], SeqArgs NumberArg FileArg
    , "Load file up to line number", cmd_loadto)
  , (["ps", "proofsearch"], NoArg
    , ":ps <line> <name> <names> does proof search for name on line, with names as hints"
    , cmd_proofsearch)
  , (["ref", "refine"], NoArg
    , ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"
    , cmd_refine)
  , (["debugunify"], SeqArgs ExprArg ExprArg
    , "(Debugging) Try to unify two expressions", const $ do
       l <- IP.simpleExpr defaultSyntax
       r <- IP.simpleExpr defaultSyntax
       P.eof
       return (Right (DebugUnify l r))
    )
  ]

noArgCmd names command doc =
  (names, NoArg, doc, noArgs command)
nameArgCmd names command doc =
  (names, NameArg, doc, fnNameArg command)
namespaceArgCmd names command doc =
  (names, NamespaceArg, doc, namespaceArg command)
exprArgCmd names command doc =
  (names, ExprArg, doc, exprArg command)
optArgCmd names command doc =
  (names, OptionArg, doc, optArg command)
proofArgCmd names command doc =
  (names, NoArg, doc, proofArg command)

pCmd :: IP.IdrisParser (Either String Command)
pCmd = P.choice [ do c <- cmd names; parser c
                | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]
     <|> unrecognized
     <|> nop
     <|> eval
    where nop = do P.eof; return (Right NOP)
          unrecognized = do
              IP.lchar ':'
              cmd <- P.many P.anyChar
              let cmd' = takeWhile (/=' ') cmd
              return (Left $ "Unrecognized command: " ++ cmd')

cmd :: [String] -> IP.IdrisParser String
cmd xs = P.try $ do
    IP.lchar ':'
    docmd sorted_xs

    where docmd [] = fail "Could not parse command"
          docmd (x:xs) = P.try (IP.reserved x >> return x) <|> docmd xs

          sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs


noArgs :: Command -> String -> IP.IdrisParser (Either String Command)
noArgs cmd name = do
    let emptyArgs = do
          P.eof
          return (Right cmd)

    let failure = return (Left $ ":" ++ name ++ " takes no arguments")

    emptyArgs <|> failure

eval :: IP.IdrisParser (Either String Command)
eval = do
  t <- IP.fullExpr defaultSyntax
  return $ Right (Eval t)

exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)
exprArg cmd name = do
    let noArg = do
          P.eof
          return $ Left ("Usage is :" ++ name ++ " <expression>")

    let justOperator = do
          (op, fc) <- IP.withExtent IP.symbolicOperator
          P.eof
          return $ Right $ cmd (PRef fc [] (sUN op))

    let properArg = do
          t <- IP.fullExpr defaultSyntax
          return $ Right (cmd t)
    P.try noArg <|> P.try justOperator <|> properArg

genArg :: String -> IP.IdrisParser a -> (a -> Command)
           -> String -> IP.IdrisParser (Either String Command)
genArg argName argParser cmd name = do
    let emptyArgs = do P.eof; failure
        oneArg = do arg <- argParser
                    P.eof
                    return (Right (cmd arg))
    P.try emptyArgs <|> oneArg <|> failure
    where
    failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)
nameArg = genArg "name" IP.name
fnNameArg = genArg "functionname" IP.fnName

strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)
strArg = genArg "string" (P.many P.anyChar)

moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)
moduleArg = genArg "module" (fmap toPath IP.identifier)
  where
    toPath n = foldl1' (</>) $ splitOn "." n

namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)
namespaceArg = genArg "namespace" (fmap toNS IP.identifier)
  where
    toNS  = splitOn "."

optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)
optArg cmd name = do
    let emptyArgs = do
            P.eof
            return $ Left ("Usage is :" ++ name ++ " <option>")

    let oneArg = do
          o <- pOption
          IP.whiteSpace
          P.eof
          return (Right (cmd o))

    let failure = return $ Left "Unrecognized setting"

    P.try emptyArgs <|> oneArg <|> failure

    where
        pOption :: IP.IdrisParser Opt
        pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions

proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)
proofArg cmd name = do
    upd <- P.option False $ do
        IP.lchar '!'
        return True
    l <- IP.natural
    n <- IP.name
    return (Right (cmd upd (fromInteger l) n))

cmd_doc :: String -> IP.IdrisParser (Either String Command)
cmd_doc name = do
    let constant = do
          c <- IP.constant
          P.eof
          return $ Right (DocStr (Right c) FullDocs)

    let pType = do
          IP.reserved "Type"
          P.eof
          return $ Right (DocStr (Left $ sUN "Type") FullDocs)

    let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

    P.try constant <|> pType <|> fnName

cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)
cmd_consolewidth name = do
    w <- pConsoleWidth
    return (Right (SetConsoleWidth w))

    where
        pConsoleWidth :: IP.IdrisParser ConsoleWidth
        pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth
                    <|> do discard (IP.symbol "infinite"); return InfinitelyWide
                    <|> do n <- fromInteger <$> IP.natural
                           return (ColsWide n)

cmd_printdepth :: String -> IP.IdrisParser (Either String Command)
cmd_printdepth _ = do d <- optional (fromInteger <$> IP.natural)
                      return (Right $ SetPrinterDepth d)

cmd_execute :: String -> IP.IdrisParser (Either String Command)
cmd_execute name = do
    tm <- P.option maintm (IP.fullExpr defaultSyntax)
    return (Right (Execute tm))
  where
    maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

cmd_dynamic :: String -> IP.IdrisParser (Either String Command)
cmd_dynamic name = do
    let optArg = do l <- P.many P.anyChar
                    if (l /= "")
                        then return $ Right (DynamicLink l)
                        else return $ Right ListDynamic
    let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
    P.try optArg <|> failure

cmd_pprint :: String -> IP.IdrisParser (Either String Command)
cmd_pprint name = do
     fmt <- ppFormat
     IP.whiteSpace
     n <- fromInteger <$> IP.natural
     IP.whiteSpace
     t <- IP.fullExpr defaultSyntax
     return (Right (PPrint fmt n t))

    where
        ppFormat :: IP.IdrisParser OutputFmt
        ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)
               <|> (discard (IP.symbol "latex") >> return LaTeXOutput)

cmd_compile :: String -> IP.IdrisParser (Either String Command)
cmd_compile name = do
    let defaultCodegen = Via IBCFormat "c"

    let codegenOption :: IP.IdrisParser Codegen
        codegenOption = do
            let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode
                viaCodegen = do x <- IP.identifier
                                return (Via IBCFormat (map toLower x))
            bytecodeCodegen <|> viaCodegen

    let hasOneArg = do
          i <- get
          f <- IP.identifier
          P.eof
          return $ Right (Compile defaultCodegen f)

    let hasTwoArgs = do
          i <- get
          codegen <- codegenOption
          f <- IP.identifier
          P.eof
          return $ Right (Compile codegen f)

    let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
    P.try hasTwoArgs <|> P.try hasOneArg <|> failure

cmd_addproof :: String -> IP.IdrisParser (Either String Command)
cmd_addproof name = do
    n <- P.option Nothing $ do
        x <- IP.name
        return (Just x)
    P.eof
    return (Right (AddProof n))

cmd_log :: String -> IP.IdrisParser (Either String Command)
cmd_log name = do
    i <- fromIntegral <$> IP.natural
    P.eof
    return (Right (LogLvl i))

cmd_verb :: String -> IP.IdrisParser (Either String Command)
cmd_verb name = do
    i <- fromIntegral <$> IP.natural
    P.eof
    return (Right (Verbosity i))

cmd_cats :: String -> IP.IdrisParser (Either String Command)
cmd_cats name = do
    cs <- P.sepBy pLogCats (IP.whiteSpace)
    P.eof
    return $ Right $ LogCategory (concat cs)
  where
    badCat = do
      c <- IP.identifier
      fail $ "Category: " ++ c ++ " is not recognised."

    pLogCats :: IP.IdrisParser [LogCat]
    pLogCats = P.try (parserCats  <$ IP.symbol (strLogCat IParse))
           <|> P.try (elabCats    <$ IP.symbol (strLogCat IElab))
           <|> P.try (codegenCats <$ IP.symbol (strLogCat ICodeGen))
           <|> P.try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))
           <|> P.try ([IIBC]      <$ IP.symbol (strLogCat IIBC))
           <|> P.try ([IErasure]  <$ IP.symbol (strLogCat IErasure))
           <|> badCat

cmd_let :: String -> IP.IdrisParser (Either String Command)
cmd_let name = do
    defn <- concat <$> P.many (IP.decl defaultSyntax)
    return (Right (NewDefn defn))

cmd_unlet :: String -> IP.IdrisParser (Either String Command)
cmd_unlet name = Right . Undefine <$> P.many IP.name

cmd_loadto :: String -> IP.IdrisParser (Either String Command)
cmd_loadto name = do
    toline <- fromInteger <$> IP.natural
    f <- P.many P.anyChar
    return (Right (Load f (Just toline)))

cmd_colour :: String -> IP.IdrisParser (Either String Command)
cmd_colour name = fmap Right pSetColourCmd

    where
        colours :: [(String, Maybe Color)]
        colours = [ ("black", Just Black)
                  , ("red", Just Red)
                  , ("green", Just Green)
                  , ("yellow", Just Yellow)
                  , ("blue", Just Blue)
                  , ("magenta", Just Magenta)
                  , ("cyan", Just Cyan)
                  , ("white", Just White)
                  , ("default", Nothing)
                  ]

        pSetColourCmd :: IP.IdrisParser Command
        pSetColourCmd = (do c <- pColourType
                            let defaultColour = IdrisColour Nothing True False False False
                            opts <- P.sepBy pColourMod (IP.whiteSpace)
                            let colour = foldr ($) defaultColour $ reverse opts
                            return $ SetColour c colour)
                    <|> P.try (IP.symbol "on" >> return ColourOn)
                    <|> P.try (IP.symbol "off" >> return ColourOff)

        pColour :: IP.IdrisParser (Maybe Color)
        pColour = doColour colours
            where doColour [] = fail "Unknown colour"
                  doColour ((s, c):cs) = (P.try (IP.symbol s) >> return c) <|> doColour cs

        pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)
        pColourMod = P.try (doVivid <$ IP.symbol "vivid")
                 <|> P.try (doDull <$ IP.symbol "dull")
                 <|> P.try (doUnderline <$ IP.symbol "underline")
                 <|> P.try (doNoUnderline <$ IP.symbol "nounderline")
                 <|> P.try (doBold <$ IP.symbol "bold")
                 <|> P.try (doNoBold <$ IP.symbol "nobold")
                 <|> P.try (doItalic <$ IP.symbol "italic")
                 <|> P.try (doNoItalic <$ IP.symbol "noitalic")
                 <|> P.try (pColour >>= return . doSetColour)
            where doVivid i       = i { vivid = True }
                  doDull i        = i { vivid = False }
                  doUnderline i   = i { underline = True }
                  doNoUnderline i = i { underline = False }
                  doBold i        = i { bold = True }
                  doNoBold i      = i { bold = False }
                  doItalic i      = i { italic = True }
                  doNoItalic i    = i { italic = False }
                  doSetColour c i = i { colour = c }

        -- | Generate the colour type names using the default Show instance.
        colourTypes :: [(String, ColourType)]
        colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
                      enumFromTo minBound maxBound

        pColourType :: IP.IdrisParser ColourType
        pColourType = doColourType colourTypes
            where doColourType [] = fail $ "Unknown colour category. Options: " ++
                                           (concat . intersperse ", " . map fst) colourTypes
                  doColourType ((s,ct):cts) = (P.try (IP.symbol s) >> return ct) <|> doColourType cts

idChar = P.oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

cmd_apropos :: String -> IP.IdrisParser (Either String Command)
cmd_apropos = packageBasedCmd (some idChar) Apropos

packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)
                -> String -> IP.IdrisParser (Either String Command)
packageBasedCmd valParser cmd name =
  P.try (do IP.lchar '('
            pkgs <- P.sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')
            IP.lchar ')'
            val <- valParser
            return (Right (cmd pkgs val)))
   <|> do val <- valParser
          return (Right (cmd [] val))
  where
    pkg = either fail pure . pkgName =<< IP.packageName

cmd_search :: String -> IP.IdrisParser (Either String Command)
cmd_search = packageBasedCmd
  (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search

cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)
cmd_proofsearch name = do
    upd <- P.option False (True <$ IP.lchar '!')
    l <- fromInteger <$> IP.natural; n <- IP.name
    hints <- P.many IP.fnName
    return (Right (DoProofSearch upd True l n hints))

cmd_refine :: String -> IP.IdrisParser (Either String Command)
cmd_refine name = do
   upd <- P.option False (do IP.lchar '!'; return True)
   l <- fromInteger <$> IP.natural; n <- IP.name
   hint <- IP.fnName
   return (Right (DoProofSearch upd False l n [hint]))