#if !(MIN_VERSION_base(4,8,0))
#endif
module Idris.Parser.Helpers where
import Prelude hiding (pi)
import Text.Trifecta.Delta
import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)
import Text.Parser.LookAhead
import Text.Parser.Expression
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Char as Chr
import qualified Text.Parser.Token.Highlight as Hi
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Delaborate (pprintErr)
import Idris.Docstrings
import Idris.Output (iWarn)
import qualified Util.Pretty as Pretty (text)
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import Data.Maybe
import qualified Data.List.Split as Spl
import Data.List
import Data.Monoid
import Data.Char
import qualified Data.Map as M
import qualified Data.HashSet as HS
import qualified Data.Text as T
import qualified Data.ByteString.UTF8 as UTF8
import System.FilePath
import Debug.Trace
type IdrisParser = StateT IState IdrisInnerParser
newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
  deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)
deriving instance Parsing IdrisInnerParser
#if MIN_VERSION_base(4,8,0)
instance  TokenParsing IdrisParser where
#else
instance TokenParsing IdrisParser where
#endif
  someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
  token p = do s <- get
               (FC fn (sl, sc) _) <- getFC 
                                           
               r <- p
               (FC fn _ (el, ec)) <- getFC
               whiteSpace
               put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })
               return r
type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
class HasLastTokenSpan m where
  getLastTokenSpan :: m (Maybe FC)
instance HasLastTokenSpan IdrisParser where
  getLastTokenSpan = lastTokenSpan <$> get
runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res
runparser p i inputname =
  parseString (runInnerParser (evalStateT p i))
              (Directed (UTF8.fromString inputname) 0 0 0 0)
highlightP :: FC -> OutputAnnotation -> IdrisParser ()
highlightP fc annot = do ist <- get
                         put ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist}
noDocCommentHere :: String -> IdrisParser ()
noDocCommentHere msg =
  optional (do fc <- getFC
               docComment
               ist <- get
               put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>
  pure ()
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 }
simpleWhiteSpace :: MonadicParsing m => m ()
simpleWhiteSpace = satisfy isSpace *> pure ()
isEol :: Char -> Bool
isEol '\n' = True
isEol  _   = False
eol :: MonadicParsing m => m ()
eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
singleLineComment :: MonadicParsing m => m ()
singleLineComment = (string "--" *>
                     many (satisfy (not . isEol)) *>
                     eol *> pure ())
                    <?> ""
multiLineComment :: MonadicParsing m => m ()
multiLineComment =     try (string "{-" *> (string "-}") *> pure ())
                   <|> string "{-" *> inCommentChars
                   <?> ""
  where inCommentChars :: MonadicParsing m => m ()
        inCommentChars =     string "-}" *> pure ()
                         <|> try (multiLineComment) *> inCommentChars
                         <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars
                         <|> skipSome (noneOf startEnd) *> inCommentChars
                         <|> oneOf startEnd *> inCommentChars
                         <?> "end of comment"
        startEnd :: String
        startEnd = "{}-"
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 :: MonadicParsing m => m String
        docCommentLine = try (do string "|||"
                                 many (satisfy (==' '))
                                 contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))
                                                           res <- many (satisfy (not . isEol))
                                                           return $ first:res)
                                 eol ; someSpace
                                 return contents)
                        <?> ""
        argDocCommentLine = do string "|||"
                               many (satisfy isSpace)
                               char '@'
                               many (satisfy isSpace)
                               n <- fst <$> name
                               many (satisfy isSpace)
                               docs <- many (satisfy (not . isEol))
                               eol ; someSpace
                               return (n, docs)
whiteSpace :: MonadicParsing m => m ()
whiteSpace = Tok.whiteSpace
stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)
stringLiteral = do str <- Tok.stringLiteral
                   fc <- getLastTokenSpan
                   return (str, fromMaybe NoFC fc)
charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)
charLiteral = do ch <- Tok.charLiteral
                 fc <- getLastTokenSpan
                 return (ch, fromMaybe NoFC fc)
natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)
natural = do n <- Tok.natural
             fc <- getLastTokenSpan
             return (n, fromMaybe NoFC fc)
integer :: MonadicParsing m => m Integer
integer = Tok.integer
float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)
float = do f <- Tok.double
           fc <- getLastTokenSpan
           return (f, fromMaybe NoFC fc)
idrisStyle :: MonadicParsing m => IdentifierStyle m
idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
  where _styleName = "Idris"
        _styleStart = satisfy isAlpha <|> oneOf "_"
        _styleLetter = satisfy isAlphaNum <|> oneOf "_'."
        _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "corecord", "Type",
                                      "do", "dsl", "import", "impossible",
                                      "case", "of", "total", "partial", "mutual",
                                      "infix", "infixl", "infixr", "rewrite",
                                      "where", "with", "syntax", "proof", "postulate",
                                      "using", "namespace", "class", "instance",
                                      "interface", "implementation", "parameters",
                                      "public", "private", "export", "abstract", "implicit",
                                      "quoteGoal", "constructor",
                                      "if", "then", "else"]
char :: MonadicParsing m => Char -> m Char
char = Chr.char
string :: MonadicParsing m => String -> m String
string = Chr.string
lchar :: MonadicParsing m => Char -> m Char
lchar = token . char
lcharFC :: MonadicParsing m => Char -> m FC
lcharFC ch = do (FC file (l, c) _) <- getFC
                _ <- token (char ch)
                return $ FC file (l, c) (l, c+1)
symbol :: MonadicParsing m => String -> m String
symbol = Tok.symbol
symbolFC :: MonadicParsing m => String -> m FC
symbolFC str = do (FC file (l, c) _) <- getFC
                  Tok.symbol str
                  return $ FC file (l, c) (l, c + length str)
reserved :: MonadicParsing m => String -> m ()
reserved = Tok.reserve idrisStyle
reservedFC :: MonadicParsing m => String -> m FC
reservedFC str = do (FC file (l, c) _) <- getFC
                    Tok.reserve idrisStyle str
                    return $ FC file (l, c) (l, c + length str)
reservedHL :: String -> IdrisParser ()
reservedHL str = reservedFC str >>= flip highlightP AnnKeyword
reservedOp :: MonadicParsing m => String -> m ()
reservedOp name = token $ try $
  do string name
     notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
reservedOpFC :: MonadicParsing m => String -> m FC
reservedOpFC name = token $ try $ do (FC f (l, c) _) <- getFC
                                     string name
                                     notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
                                     return (FC f (l, c) (l, c + length name))
identifier :: (MonadicParsing m) => m (String, FC)
identifier = try(do (i, fc) <-
                      token $ do (FC f (l, c) _) <- getFC
                                 i <- Tok.ident idrisStyle
                                 return (i, FC f (l, c) (l, c + length i))
                    when (i == "_") $ unexpected "wildcard"
                    return (i, fc))
iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)
iName bad = do (n, fc) <- maybeWithNS identifier False bad
               return (n, fc)
            <?> "name"
maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)
maybeWithNS parser ascend bad = do
  fc <- getFC
  i <- option "" (lookAhead (fst <$> identifier))
  when (i `elem` bad) $ unexpected "reserved identifier"
  let transf = if ascend then id else reverse
  (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))
  return (mkName (x, xs), fc)
  where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)
        parserNoNS parser = do startFC <- getFC
                               (x, nameFC) <- parser
                               return (x, "", spanFC startFC nameFC)
        parserNS   :: MonadicParsing m => m (String, FC) -> String -> m (String, String, FC)
        parserNS   parser ns = do startFC <- getFC
                                  xs <- string ns
                                  lchar '.';  (x, nameFC) <- parser
                                  return (x, xs, spanFC startFC nameFC)
        parsersNS  :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]
        parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
name :: IdrisParser (Name, FC)
name = (<?> "name") $ do
    keywords <- syntax_keywords <$> get
    aliases  <- module_aliases  <$> get
    (n, fc) <- iName keywords
    return (unalias aliases n, fc)
  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
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]
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
opChars :: String
opChars = ":!#$%&*+./<=>?@\\^|-~"
operatorLetter :: MonadicParsing m => m Char
operatorLetter = oneOf opChars
commentMarkers :: [String]
commentMarkers = [ "--", "|||" ]
invalidOperators :: [String]
invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
operator :: MonadicParsing m => m String
operator = do op <- token . some $ operatorLetter
              when (op `elem` (invalidOperators ++ commentMarkers)) $
                   fail $ op ++ " is not a valid operator"
              return op
operatorFC :: MonadicParsing m => m (String, FC)
operatorFC = do (op, fc) <- token $ do (FC f (l, c) _) <- getFC
                                       op <- some operatorLetter
                                       return (op, FC f (l, c) (l, c + length op))
                when (op `elem` (invalidOperators ++ commentMarkers)) $
                     fail $ op ++ " is not a valid operator"
                return (op, fc)
fileName :: Delta -> String
fileName (Directed fn _ _ _ _) = UTF8.toString fn
fileName _                     = "(interactive)"
lineNum :: Delta -> Int
lineNum (Lines l _ _ _)      = fromIntegral l + 1
lineNum (Directed _ l _ _ _) = fromIntegral l + 1
lineNum _ = 0
columnNum :: Delta -> Int
columnNum pos = fromIntegral (column pos) + 1
getFC :: MonadicParsing m => m FC
getFC = do s <- position
           let (dir, file) = splitFileName (fileName s)
           let f = if dir == addTrailingPathSeparator "." then file else fileName s
           return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) 
           
           
bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm
bindList b []              sc = sc
bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)
commaSeparated :: MonadicParsing m => m a -> m [a]
commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)
pushIndent :: IdrisParser ()
pushIndent = do pos <- position
                ist <- get
                put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
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 })
indent :: IdrisParser Int
indent = liftM ((+1) . fromIntegral . column) position
lastIndent :: IdrisParser Int
lastIndent = do ist <- get
                case indent_stack ist of
                  (x : xs) -> return x
                  _        -> return 1
indented :: IdrisParser a -> IdrisParser a
indented p = notEndBlock *> p <* keepTerminator
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock p = do openBlock
                     pushIndent
                     res <- many (indented p)
                     popIndent
                     closeBlock
                     return res
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 p = do openBlock
                      pushIndent
                      res <- some (indented p)
                      popIndent
                      closeBlock
                      return res
indentedBlockS :: IdrisParser a -> IdrisParser a
indentedBlockS p = do openBlock
                      pushIndent
                      res <- indented p
                      popIndent
                      closeBlock
                      return res
lookAheadMatches :: MonadicParsing m => m a -> m Bool
lookAheadMatches p = do match <- lookAhead (optional p)
                        return $ isJust match
openBlock :: IdrisParser ()
openBlock =     do lchar '{'
                   ist <- get
                   put (ist { brace_stack = Nothing : brace_stack ist })
            <|> do ist <- get
                   lvl' <- indent
                    
                    
                   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"
closeBlock :: IdrisParser ()
closeBlock = do ist <- get
                bs <- case brace_stack ist of
                        []  -> eof >> return []
                        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
                                                  eof
                                                  return [])
                put (ist { brace_stack = bs })
terminator :: IdrisParser ()
terminator =     do lchar ';'; popIndent
             <|> do c <- indent; l <- lastIndent
                    if c <= l then popIndent else fail "not a terminator"
             <|> do isParen <- lookAheadMatches (oneOf ")}")
                    if isParen then popIndent else fail "not a terminator"
             <|> lookAhead eof
keepTerminator :: IdrisParser ()
keepTerminator =  do lchar ';'; return ()
              <|> do c <- indent; l <- lastIndent
                     unless (c <= l) $ fail "not a terminator"
              <|> do isParen <- lookAheadMatches (oneOf ")}|")
                     isIn <- lookAheadMatches (reserved "in")
                     unless (isIn || isParen) $ fail "not a terminator"
              <|> lookAhead eof
notEndApp :: IdrisParser ()
notEndApp = do c <- indent; l <- lastIndent
               when (c <= l) (fail "terminator")
notEndBlock :: IdrisParser ()
notEndBlock = do ist <- get
                 case brace_stack ist of
                      Just lvl : xs -> do i <- indent
                                          isParen <- lookAheadMatches (char ')')
                                          when (i < lvl || isParen) (fail "end of block")
                      _ -> return ()
data IndentProperty = IndentProperty (Int -> Int -> Bool) String
indentPropHolds :: IndentProperty -> IdrisParser ()
indentPropHolds (IndentProperty op msg) = do
  li <- lastIndent
  i <- indent
  when (not $ op i li) $ fail ("Wrong indention: " ++ msg)
gtProp :: IndentProperty
gtProp = IndentProperty (>) "should be greater than context indentation"
gteProp :: IndentProperty
gteProp = IndentProperty (>=) "should be greater than or equal context indentation"
eqProp :: IndentProperty
eqProp = IndentProperty (==) "should be equal to context indentation"
ltProp :: IndentProperty
ltProp = IndentProperty (<) "should be less than context indentation"
lteProp :: IndentProperty
lteProp = IndentProperty (<=) "should be less than or equal to context indentation"
notOpenBraces :: IdrisParser ()
notOpenBraces = do ist <- get
                   when (hasNothing $ brace_stack ist) $ fail "end of input"
  where hasNothing :: [Maybe a] -> Bool
        hasNothing = any isNothing
accessibility' :: IdrisParser Accessibility
accessibility'
              = do reserved "public";
                   gotexp <- optional (reserved "export")
                   case gotexp of
                        Just _ -> return ()
                        Nothing -> do
                           ist <- get
                           fc <- getFC
                           put ist { parserWarnings =
                              (fc, Msg "'public' is deprecated. Use 'public export' instead.")
                                   : parserWarnings ist }
                   return Public
            <|> do reserved "abstract";
                   ist <- get
                   fc <- getFC
                   put ist { parserWarnings =
                      (fc, Msg "The 'abstract' keyword is deprecated. Use 'export' instead.")
                           : parserWarnings ist }
                   return Frozen
            <|> do reserved "export"; return Frozen
            <|> do reserved "private";  return 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)
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc n a = do i <- get
                put (i { hide_list = addDef n a (hide_list i) })
accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
accData Frozen n ns = do addAcc n Public 
                         mapM_ (\n -> addAcc n Private) ns 
accData a n ns = do addAcc n a
                    mapM_ (`addAcc` a) ns
fixErrorMsg :: String -> [String] -> String
fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
collect :: [PDecl] -> [PDecl]
collect (c@(PClauses _ o _ _) : ds)
    = clauses (cname c) [] (c : ds)
  where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
        clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
           | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
        clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)
           | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds
        clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
        clauses Nothing acc (x:xs) = collect xs
        clauses Nothing acc [] = []
        cname :: PDecl -> Maybe Name
        cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
        cname (PClauses fc _ _ [PWith   _ n _ _ _ _ _]) = Just n
        cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
        cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing
        fcOf :: PDecl -> FC
        fcOf (PClauses fc _ _ _) = fc
collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')
    = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')
    = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'
collect (d : ds) = d : collect ds
collect [] = []