{-|
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 :: forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser Parser st res
p st
i String
inputname String
s =
  case forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
P.parse (forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Parser st res
p st
i)) String
inputname String
s of
    Left ParseErrorBundle String Void
err -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ ParseErrorBundle String Void -> ParseError
ParseError ParseErrorBundle String Void
err
    Right (res, FC)
v  -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (res, FC)
v

{- * Parse errors -}

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

parseError :: ParseError -> P.ParseError String Void
parseError :: ParseError -> ParseError String Void
parseError = forall a. NonEmpty a -> a
NonEmpty.head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s e. ParseErrorBundle s e -> NonEmpty (ParseError s e)
P.bundleErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> ParseErrorBundle String Void
unParseError

parseErrorPosState :: ParseError -> P.PosState String
parseErrorPosState :: ParseError -> PosState String
parseErrorPosState = forall s e. ParseErrorBundle s e -> PosState s
P.bundlePosState forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> ParseErrorBundle String Void
unParseError

parseErrorOffset :: ParseError -> Int
parseErrorOffset :: ParseError -> Int
parseErrorOffset = forall s e. ParseError s e -> Int
P.errorOffset forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> ParseError String Void
parseError

instance Message ParseError where
  messageExtent :: ParseError -> FC
messageExtent ParseError
err = SourcePos -> FC
sourcePositionFC SourcePos
pos
    where
#if MIN_VERSION_megaparsec(8,0,0)
      P.PosState {pstateSourcePos :: forall s. PosState s -> SourcePos
P.pstateSourcePos = SourcePos
pos} =
        forall s. TraversableStream s => Int -> PosState s -> PosState s
P.reachOffsetNoLine (ParseError -> Int
parseErrorOffset ParseError
err) (ParseError -> PosState String
parseErrorPosState ParseError
err)
#else
      (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
#endif
  messageText :: ParseError -> OutputDoc
messageText = forall a. String -> Doc a
PP.text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
init forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s e.
(VisualStream s, ShowErrorComponent e) =>
ParseError s e -> String
P.parseErrorTextPretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> ParseError String Void
parseError
#if MIN_VERSION_megaparsec(9,0,0)
  messageSource :: ParseError -> Maybe String
messageSource ParseError
err = Maybe String
sline
#else
  messageSource err = Just sline
#endif
    where
#if MIN_VERSION_megaparsec(8,0,0)
      (Maybe String
sline, PosState String
_) = forall s.
TraversableStream s =>
Int -> PosState s -> (Maybe String, PosState s)
P.reachOffset (ParseError -> Int
parseErrorOffset ParseError
err) (ParseError -> PosState String
parseErrorPosState ParseError
err)
#else
      (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
#endif

-- | A fully formatted parse error, with caret and bar, etc.
prettyError :: ParseError -> String
prettyError :: ParseError -> String
prettyError =  forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
P.errorBundlePretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> ParseErrorBundle String Void
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 :: forall (m :: * -> *). Parsing m => m Mark
mark = forall e s (m :: * -> *). MonadParsec e s m => m (State s e)
P.getParserState

restore :: Parsing m => Mark -> m ()
restore :: forall (m :: * -> *). Parsing m => Mark -> m ()
restore = forall e s (m :: * -> *). MonadParsec e s m => State s e -> m ()
P.setParserState

{- * Tracking the extent of productions -}

sourcePositionFC :: P.SourcePos -> FC
sourcePositionFC :: SourcePos -> FC
sourcePositionFC (P.SourcePos String
name Pos
line Pos
column) =
  String -> (Int, Int) -> (Int, Int) -> FC
FC String
f (Int
lineNumber, Int
columnNumber) (Int
lineNumber, Int
columnNumber)
  where
    lineNumber :: Int
lineNumber = Pos -> Int
P.unPos Pos
line
    columnNumber :: Int
columnNumber = Pos -> Int
P.unPos Pos
column
    (String
dir, String
file) = String -> (String, String)
splitFileName String
name
    f :: String
f = if String
dir forall a. Eq a => a -> a -> Bool
== String -> String
addTrailingPathSeparator String
"."
        then String
file
        else String
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 :: forall (m :: * -> *). Parsing m => m FC
getFC = SourcePos -> FC
sourcePositionFC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
P.getSourcePos

-- | Add an extent (widen) our current parsing context.
addExtent :: MonadWriter FC m => FC -> m ()
addExtent :: forall (m :: * -> *). MonadWriter FC m => FC -> m ()
addExtent = forall w (m :: * -> *). MonadWriter w m => w -> m ()
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 :: forall (m :: * -> *) a. Parsing m => m a -> m a
trackExtent m a
p = do ~(FC String
f (Int
sr, Int
sc) (Int, Int)
_) <- forall (m :: * -> *). Parsing m => m FC
getFC
                   a
result <- m a
p
                   ~(FC String
f (Int, Int)
_ (Int
er, Int
ec)) <- forall (m :: * -> *). Parsing m => m FC
getFC
                   forall (m :: * -> *). MonadWriter FC m => FC -> m ()
addExtent (String -> (Int, Int) -> (Int, Int) -> FC
FC String
f (Int
sr, Int
sc) (Int
er, forall a. Ord a => a -> a -> a
max Int
1 (Int
ec forall a. Num a => a -> a -> a
- Int
1)))
                   forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Run a parser, discard its value, and return its extent.
extent :: MonadWriter FC m => m a -> m FC
extent :: forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent

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

-- | Run a parser and inject the extent after via function application.
appExtent :: MonadWriter FC m => m (FC -> a) -> m a
appExtent :: forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: * -> * -> *) b c. ArrowApply a => a (a b c, b) c
app forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent