{-|
Module      : Idris.Parser.Stack
Description : Idris parser stack and its primitives.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP, ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}
module Idris.Parser.Stack
  ( -- * Parsing
    Parser(..)
  , Parsing(..)
  , runparser
    -- * Parse errors
  , ParseError
  , prettyError
    -- * Mark and restore
  , Mark
  , mark
  , restore

    -- * Tracking the extent of productions
    --
    -- The parser stack automatically builds up the extent of any parse from
    -- the extents of sub-parsers wrapped with @trackExtent@.
  , getFC
  , addExtent
  , trackExtent
  , extent
  , withExtent
  , appExtent
  )
where

import Idris.Core.TT (FC(..))
import Idris.Output (Message(..))

import Control.Arrow (app)
import qualified Control.Monad.Fail as Fail
import Control.Monad.State.Strict (StateT(..), evalStateT)
import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,
                                    runWriterT, tell)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Void (Void(..))
import System.FilePath (addTrailingPathSeparator, splitFileName)
import qualified Text.Megaparsec as P
import qualified Util.Pretty as PP

{- * Parsing -}

-- | Our parser stack with state of type @s@
type Parser s = StateT s (WriterT FC (P.Parsec Void String))

-- | A constraint for parsing without state
type Parsing m = (Fail.MonadFail m, P.MonadParsec Void String m, MonadWriter FC m)

-- | Run the Idris parser stack
runparser :: Parser st res -> st -> String -> String -> Either ParseError res
runparser p i inputname s =
  case P.parse (runWriterT (evalStateT p i)) inputname s of
    Left err -> Left $ ParseError err
    Right v  -> Right $ fst v

{- * Parse errors -}

newtype ParseError = ParseError { unParseError :: P.ParseErrorBundle String Void }

parseError :: ParseError -> P.ParseError String Void
parseError = NonEmpty.head . P.bundleErrors . unParseError

parseErrorPosState :: ParseError -> P.PosState String
parseErrorPosState = P.bundlePosState . unParseError

parseErrorOffset :: ParseError -> Int
parseErrorOffset = P.errorOffset . parseError

instance Message ParseError where
  messageExtent err = sourcePositionFC pos
    where
#if MIN_VERSION_megaparsec(8,0,0)
      P.PosState {P.pstateSourcePos = pos} =
        P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
#else
      (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
#endif
  messageText = PP.text . init . P.parseErrorTextPretty . parseError
#if MIN_VERSION_megaparsec(9,0,0)
  messageSource err = sline
#else
  messageSource err = Just sline
#endif
    where
#if MIN_VERSION_megaparsec(8,0,0)
      (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
#else
      (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
#endif

-- | A fully formatted parse error, with caret and bar, etc.
prettyError :: ParseError -> String
prettyError =  P.errorBundlePretty . unParseError

{- * Mark and restore -}

#if MIN_VERSION_megaparsec(8,0,0)
type Mark = P.State String Void
#else
type Mark = P.State String
#endif

-- | Retrieve the parser state so we can restart from this point later.
mark :: Parsing m => m Mark
mark = P.getParserState

restore :: Parsing m => Mark -> m ()
restore = P.setParserState

{- * Tracking the extent of productions -}

sourcePositionFC :: P.SourcePos -> FC
sourcePositionFC (P.SourcePos name line column) =
  FC f (lineNumber, columnNumber) (lineNumber, columnNumber)
  where
    lineNumber = P.unPos line
    columnNumber = P.unPos column
    (dir, file) = splitFileName name
    f = if dir == addTrailingPathSeparator "."
        then file
        else name

-- | Get the current parse position.
--
-- This is useful when the position is needed in a way unrelated to the
-- heirarchy of parsers.  Prefer using @withExtent@ and friends.
getFC :: Parsing m => m FC
getFC = sourcePositionFC <$> P.getSourcePos

-- | Add an extent (widen) our current parsing context.
addExtent :: MonadWriter FC m => FC -> m ()
addExtent = tell

-- | Run a parser and track its extent.
--
-- Wrap bare Megaparsec parsers with this to make them "visible" in error
-- messages.  Do not wrap whitespace or comment parsers.  If you find an
-- extent is taking trailing whitespace, it's likely there's a double-wrapped
-- parser (usually via @Idris.Parser.Helpers.token@).
trackExtent :: Parsing m => m a -> m a
trackExtent p = do ~(FC f (sr, sc) _) <- getFC
                   result <- p
                   ~(FC f _ (er, ec)) <- getFC
                   addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
                   return result

-- | Run a parser, discard its value, and return its extent.
extent :: MonadWriter FC m => m a -> m FC
extent = fmap snd . withExtent

-- | Run a parser and return its value and extent.
withExtent :: MonadWriter FC m => m a -> m (a, FC)
withExtent = listen

-- | Run a parser and inject the extent after via function application.
appExtent :: MonadWriter FC m => m (FC -> a) -> m a
appExtent = fmap app . withExtent