{-|
Module      : Idris.Parser.Helpers
Description : Utilities for Idris' parser.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}
module Idris.Parser.Helpers
  ( module Idris.Parser.Stack
    -- * The parser
  , IdrisParser
  , parseErrorDoc
    -- * Space
  , whiteSpace
  , someSpace
  , eol
  , isEol
    -- * Basic parsers
  , char
  , symbol
  , string
  , lookAheadMatches
    -- * Terminals
  , lchar
  , reserved
  , docComment
  , token
  , natural
  , charLiteral
  , stringLiteral
  , float
    -- * Names
  , bindList
  , maybeWithNS
  , iName
  , name
  , identifier
  , identifierWithExtraChars
  , packageName
    -- * Access
  , accessibility
  , accData
  , addAcc
    -- * Warnings and errors
  , fixErrorMsg
  , parserWarning
  , clearParserWarnings
  , reportParserWarnings
    -- * Highlighting
  , highlight
  , keyword
    -- * Indentation
  , pushIndent
  , popIndent
  , indentGt
  , notOpenBraces
    -- * Indented blocks
  , openBlock
  , closeBlock
  , terminator
  , notEndBlock
  , indentedBlock
  , indentedBlock1
  , indentedBlockS
  , indented
    -- * Miscellaneous
  , notEndApp
  , commaSeparated
  )
where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate (pprintErr)
import Idris.Docstrings
import Idris.Options
import Idris.Output (iWarn)
import Idris.Parser.Stack

import Prelude hiding (pi)

import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import Data.Char
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P
import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
import qualified Text.PrettyPrint.ANSI.Leijen as PP


-- | Idris parser with state used during parsing
type IdrisParser = Parser IState

parseErrorDoc :: ParseError -> PP.Doc
parseErrorDoc = PP.string . prettyError

someSpace :: Parsing m => m ()
someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

token :: Parsing m => m a -> m a
token p = trackExtent p <* whiteSpace

highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a
highlight annot p = do
  (result, fc) <- withExtent p
  modify $ \ist -> ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }
  return result

-- | Parse a reserved identfier, highlighting it as a keyword
keyword :: (Parsing m, MonadState IState m) => String -> m ()
keyword str = highlight AnnKeyword (reserved str)

clearParserWarnings :: Idris ()
clearParserWarnings = do ist <- getIState
                         putIState ist { parserWarnings = [] }

reportParserWarnings :: Idris ()
reportParserWarnings = do ist <- getIState
                          mapM_ (uncurry iWarn)
                                (map (\ (fc, err) -> (fc, pprintErr ist err)) .
                                 reverse .
                                 nubBy (\(fc, err) (fc', err') ->
                                         FC' fc == FC' fc' && err == err') $
                                 parserWarnings ist)
                          clearParserWarnings


parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning fc warnOpt warnErr = do
  ist <- get
  let cmdline = opt_cmdline (idris_options ist)
  unless (maybe False (`elem` cmdline) warnOpt) $
    put ist { parserWarnings = (fc, warnErr) : parserWarnings ist }

{- * Space, comments and literals (token/lexing like parsers) -}

-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
simpleWhiteSpace :: Parsing m => m ()
simpleWhiteSpace = () <$ P.satisfy isSpace

-- | Checks if a charcter is end of line
isEol :: Char -> Bool
isEol '\n' = True
isEol  _   = False

-- | A parser that succeeds at the end of the line
eol :: Parsing m => m ()
eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"

{- | Consumes a single-line comment

@
     SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
@
 -}
singleLineComment :: Parsing m => m ()
singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)) *> eol)

{- | Consumes a multi-line comment

@
  MultiLineComment_t ::=
     '{ -- }'
   | '{ -' InCommentChars_t
  ;
@

@
  InCommentChars_t ::=
   '- }'
   | MultiLineComment_t InCommentChars_t
   | ~'- }'+ InCommentChars_t
  ;
@
-}
multiLineComment :: Parsing m => m ()
multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())
                              <|> string "{-" *> inCommentChars
  where inCommentChars :: Parsing m => m ()
        inCommentChars =     string "-}" *> pure ()
                         <|> P.try (multiLineComment) *> inCommentChars
                         <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars
                         <|> P.skipSome (P.noneOf startEnd) *> inCommentChars
                         <|> P.oneOf startEnd *> inCommentChars
                         <?> "end of comment"
        startEnd :: String
        startEnd = "{}-"

{-| Parses a documentation comment

@
  DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;

  DocCommentLine ::= '|||' ~EOL_t* EOL_t ;
  ArgCommentLine ::= '|||' '@' ~EOL_t* EOL_t ;
@
 -}
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
docComment = do dc <- pushIndent *> docCommentLine
                rest <- many (indented docCommentLine)
                args <- many $ do (name, first) <- indented argDocCommentLine
                                  rest <- many (indented docCommentLine)
                                  return (name, concat (intersperse "\n" (first:rest)))
                popIndent
                return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),
                        map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

  where docCommentLine :: Parsing m => m String
        docCommentLine = P.hidden $ P.try $ do
                           string "|||"
                           many (P.satisfy (==' '))
                           contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))
                                                       res <- many (P.satisfy (not . isEol))
                                                       return $ first:res)
                           eol ; someSpace
                           return contents

        argDocCommentLine :: IdrisParser (Name, String)
        argDocCommentLine = do P.string "|||"
                               P.many (P.satisfy isSpace)
                               P.char '@'
                               P.many (P.satisfy isSpace)
                               n <- name
                               P.many (P.satisfy isSpace)
                               docs <- P.many (P.satisfy (not . isEol))
                               P.eol ; someSpace
                               return (n, docs)

-- | Parses some white space
whiteSpace :: Parsing m => m ()
whiteSpace = someSpace <|> pure ()

-- | Parses a string literal
stringLiteral :: Parsing m => m String
stringLiteral = token . P.try $ P.char '"' *> P.manyTill P.charLiteral (P.char '"')

-- | Parses a char literal
charLiteral :: Parsing m => m Char
charLiteral = token . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''

-- | Parses a natural number
natural :: Parsing m => m Integer
natural = token (    P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)
                 <|> P.try (P.char '0' *> P.char' 'o' *> P.octal)
                 <|> P.try P.decimal)

-- | Parses a floating point number
float :: Parsing m => m Double
float = token . P.try $ P.float

{- * Symbols, identifiers, names and operators -}

reservedIdentifiers :: HS.HashSet String
reservedIdentifiers = HS.fromList
  [ "Type"
  , "case", "class", "codata", "constructor", "corecord", "data"
  , "do", "dsl", "else", "export", "if", "implementation", "implicit"
  , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"
  , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"
  , "postulate", "private", "proof", "public", "quoteGoal", "record"
  , "rewrite", "syntax", "then", "total", "using", "where", "with"
  ]

identifierOrReservedWithExtraChars :: Parsing m => String -> m String
identifierOrReservedWithExtraChars extraChars = token $ P.try $ do
  c <- P.satisfy isAlpha <|> P.oneOf "_"
  cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf extraChars)
  return $ c : cs

char :: Parsing m => Char -> m Char
char = P.char

string :: Parsing m => String -> m String
string = P.string

-- | Parses a character as a token
lchar :: Parsing m => Char -> m Char
lchar = token . P.char

symbol :: Parsing m => String -> m ()
symbol = void . token . P.string

-- | Parses a reserved identifier
reserved :: Parsing m => String -> m ()
reserved name = token $ P.try $ do
  P.string name
  P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

-- | Parses an identifier as a token
identifierWithExtraChars :: Parsing m => String -> m String
identifierWithExtraChars extraChars = P.try $ do
  ident <- identifierOrReservedWithExtraChars extraChars
  when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident
  when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"
  return ident

identifier :: Parsing m => m String
identifier = identifierWithExtraChars "_'."

-- | Parses an identifier with possible namespace as a name
iName :: Parsing m => [String] -> m Name
iName bad = maybeWithNS identifier bad <?> "name"

-- | Parses an string possibly prefixed by a namespace
maybeWithNS :: Parsing m => m String -> [String] -> m Name
maybeWithNS parser bad = do
  i <- P.option "" (P.lookAhead identifier)
  when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"
  mkName <$> P.choice (reverse (parserNoNS parser : parsersNS parser i))
  where parserNoNS :: Parsing m => m String -> m (String, String)
        parserNoNS = fmap (\x -> (x, ""))
        parserNS   :: Parsing m => m String -> String -> m (String, String)
        parserNS   parser ns = do xs <- trackExtent (string ns)
                                  lchar '.'
                                  x <- parser
                                  return (x, xs)
        parsersNS  :: Parsing m => m String -> String -> [m (String, String)]
        parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

-- | Parses a name
name :: (Parsing m, MonadState IState m) => m Name
name = do
    keywords <- syntax_keywords <$> get
    aliases  <- module_aliases  <$> get
    n <- iName keywords
    return (unalias aliases n)
   <?> "name"
  where
    unalias :: M.Map [T.Text] [T.Text] -> Name -> Name
    unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'
    unalias aliases name = name

{- | List of all initial segments in ascending order of a list.  Every
such initial segment ends right before an element satisfying the given
condition.
-}
initsEndAt :: (a -> Bool) -> [a] -> [[a]]
initsEndAt p [] = []
initsEndAt p (x:xs) | p x = [] : x_inits_xs
                    | otherwise = x_inits_xs
  where x_inits_xs = [x : cs | cs <- initsEndAt p xs]


{- | Create a `Name' from a pair of strings representing a base name and its
 namespace.
-}
mkName :: (String, String) -> Name
mkName (n, "") = sUN n
mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))
  where parseNS x = case span (/= '.') x of
                      (x, "")    -> [x]
                      (x, '.':y) -> x : parseNS y

-- | Parse a package name
packageName :: Parsing m => m String
packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)
  where firstChars = ['a'..'z'] ++ ['A'..'Z']
        remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

{- * Position helpers -}

{-* Syntax helpers-}
-- | Bind constraints to term
bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList b []                 sc = sc
bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

{- | @commaSeparated p@ parses one or more occurences of `p`,
     separated by commas and optional whitespace. -}
commaSeparated :: Parsing m => m a -> m [a]
commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)

{- * Layout helpers -}

-- | Push indentation to stack
pushIndent :: IdrisParser ()
pushIndent = do columnNumber <- indent
                ist <- get
                put (ist { indent_stack = columnNumber : indent_stack ist })

-- | Pops indentation from stack
popIndent :: IdrisParser ()
popIndent = do ist <- get
               case indent_stack ist of
                 [] -> error "The impossible happened! Tried to pop an indentation level where none was pushed (underflow)."
                 (x : xs) -> put (ist { indent_stack = xs })


-- | Gets current indentation
indent :: Parsing m => m Int
indent = P.unPos . P.sourceColumn <$> P.getSourcePos

-- | Gets last indentation
lastIndent :: (MonadState IState m) => m Int
lastIndent = do ist <- get
                case indent_stack ist of
                  (x : xs) -> return x
                  _        -> return 1

-- | Applies parser in an indented position
indented :: IdrisParser a -> IdrisParser a
indented p = notEndBlock *> p <* keepTerminator

-- | Applies parser to get a block (which has possibly indented statements)
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock p = do openBlock
                     pushIndent
                     res <- many (indented p)
                     popIndent
                     closeBlock
                     return res

-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 p = do openBlock
                      pushIndent
                      res <- some (indented p)
                      popIndent
                      closeBlock
                      return res

-- | Applies parser to get a block with exactly one (possibly indented) statement
indentedBlockS :: IdrisParser a -> IdrisParser a
indentedBlockS p = do openBlock
                      pushIndent
                      res <- indented p
                      popIndent
                      closeBlock
                      return res


-- | Checks if the following character matches provided parser
lookAheadMatches :: Parsing m => m a -> m Bool
lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)

-- | Parses a start of block
openBlock :: IdrisParser ()
openBlock =     do lchar '{'
                   ist <- get
                   put (ist { brace_stack = Nothing : brace_stack ist })
            <|> do ist <- get
                   lvl' <- indent
                    -- if we're not indented further, it's an empty block, so
                    -- increment lvl to ensure we get to the end
                   let lvl = case brace_stack ist of
                                   Just lvl_old : _ ->
                                       if lvl' <= lvl_old then lvl_old+1
                                                          else lvl'
                                   [] -> if lvl' == 1 then 2 else lvl'
                                   _ -> lvl'
                   put (ist { brace_stack = Just lvl : brace_stack ist })
            <?> "start of block"

-- | Parses an end of block
closeBlock :: IdrisParser ()
closeBlock = do ist <- get
                bs <- case brace_stack ist of
                        []  -> [] <$ P.eof
                        Nothing : xs -> lchar '}' >> return xs <?> "end of block"
                        Just lvl : xs -> (do i   <- indent
                                             isParen <- lookAheadMatches (char ')')
                                             isIn <- lookAheadMatches (reserved "in")
                                             if i >= lvl && not (isParen || isIn)
                                                then fail "not end of block"
                                                else return xs)
                                          <|> (do notOpenBraces
                                                  P.eof
                                                  return [])
                put (ist { brace_stack = bs })

-- | Parses a terminator
terminator :: IdrisParser ()
terminator =     do lchar ';'; popIndent
             <|> do c <- indent; l <- lastIndent
                    if c <= l then popIndent else fail "not a terminator"
             <|> do isParen <- lookAheadMatches (P.oneOf ")}")
                    if isParen then popIndent else fail "not a terminator"
             <|> P.lookAhead P.eof

-- | Parses and keeps a terminator
keepTerminator :: IdrisParser ()
keepTerminator =  () <$ lchar ';'
              <|> do c <- indent; l <- lastIndent
                     unless (c <= l) $ fail "not a terminator"
              <|> do isParen <- lookAheadMatches (P.oneOf ")}|")
                     isIn <- lookAheadMatches (reserved "in")
                     unless (isIn || isParen) $ fail "not a terminator"
              <|> P.lookAhead P.eof

-- | Checks if application expression does not end
notEndApp :: IdrisParser ()
notEndApp = do c <- indent; l <- lastIndent
               when (c <= l) (fail "terminator")

-- | Checks that it is not end of block
notEndBlock :: IdrisParser ()
notEndBlock = do ist <- get
                 case brace_stack ist of
                      Just lvl : xs -> do i <- indent
                                          isParen <- lookAheadMatches (P.char ')')
                                          when (i < lvl || isParen) (fail "end of block")
                      _ -> return ()

indentGt :: (Parsing m, MonadState IState m) => m ()
indentGt = do
  li <- lastIndent
  i <- indent
  when (i <= li) $ fail "Wrong indention: should be greater than context indentation"

-- | Checks that there are no braces that are not closed
notOpenBraces :: IdrisParser ()
notOpenBraces = do ist <- get
                   when (hasNothing $ brace_stack ist) $ fail "end of input"
  where hasNothing :: [Maybe a] -> Bool
        hasNothing = any isNothing

{- | Parses an accessibilty modifier (e.g. public, private) -}
accessibility' :: IdrisParser Accessibility
accessibility' = Public  <$ reserved "public" <* reserved "export"
             <|> Frozen  <$ reserved "export"
             <|> Private <$ reserved "private"
             <?> "accessibility modifier"

accessibility :: IdrisParser Accessibility
accessibility = do acc <- optional accessibility'
                   case acc of
                        Just a -> return a
                        Nothing -> do ist <- get
                                      return (default_access ist)

-- | Adds accessibility option for function
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc n a = do i <- get
                put (i { hide_list = addDef n a (hide_list i) })

{- | Add accessbility option for data declarations
 (works for interfaces too - 'abstract' means the data/interface is visible but members not) -}
accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions
                         mapM_ (\n -> addAcc n Private) ns -- so that they are invisible
accData a n ns = do addAcc n a
                    mapM_ (`addAcc` a) ns


{- * Error reporting helpers -}
{- | Error message with possible fixes list -}
fixErrorMsg :: String -> [String] -> String
fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)