git.iko.soy/Idris-dev
on e65d0fa help sign in
Idris-dev/src/Idris/Parser/Stack.hs
136 lines 4.2 kB history raw
1{-|
2Module : Idris.Parser.Stack
3Description : Idris parser stack and its primitives.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}
9module Idris.Parser.Stack
10 ( -- * Parsing
11 Parser(..)
12 , Parsing(..)
13 , runparser
14 -- * Parse errors
15 , ParseError
16 , prettyError
17 -- * Mark and restore
18 , Mark
19 , mark
20 , restore
22 -- * Tracking the extent of productions
23 --
24 -- The parser stack automatically builds up the extent of any parse from
25 -- the extents of sub-parsers wrapped with @trackExtent@.
26 , getFC
27 , addExtent
28 , trackExtent
29 , extent
30 , withExtent
31 , appExtent
32 )
33where
35import Idris.Core.TT (FC(..))
36import Idris.Output (Message(..))
38import Control.Arrow (app)
39import Control.Monad.State.Strict (StateT(..), evalStateT)
40import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,
41 runWriterT, tell)
42import qualified Data.List.NonEmpty as NonEmpty
43import Data.Void (Void(..))
44import System.FilePath (addTrailingPathSeparator, splitFileName)
45import qualified Text.Megaparsec as P
46import qualified Util.Pretty as PP
48{- * Parsing -}
50-- | Our parser stack with state of type @s@
51type Parser s = StateT s (WriterT FC (P.Parsec Void String))
53-- | A constraint for parsing without state
54type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)
56-- | Run the Idris parser stack
57runparser :: Parser st res -> st -> String -> String -> Either ParseError res
58runparser p i inputname s =
59 case P.parse (runWriterT (evalStateT p i)) inputname s of
60 Left err -> Left $ ParseError s err
61 Right v -> Right $ fst v
63{- * Parse errors -}
65data ParseError = ParseError String (P.ParseError (P.Token String) Void)
67instance Message ParseError where
68 messageExtent (ParseError _ err) = sourcePositionFC pos
69 where
70 (pos NonEmpty.:| _) = P.errorPos err
71 messageText (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err
72 messageSource (ParseError src _) = Just src
74-- | A fully formatted parse error, with caret and bar, etc.
75prettyError :: ParseError -> String
76prettyError (ParseError s err) = P.parseErrorPretty' s err
78{- * Mark and restore -}
80type Mark = P.State String
82-- | Retrieve the parser state so we can restart from this point later.
83mark :: Parsing m => m Mark
84mark = P.getParserState
86restore :: Parsing m => Mark -> m ()
87restore = P.setParserState
89{- * Tracking the extent of productions -}
91sourcePositionFC :: P.SourcePos -> FC
92sourcePositionFC (P.SourcePos name line column) =
93 FC f (lineNumber, columnNumber) (lineNumber, columnNumber)
94 where
95 lineNumber = P.unPos line
96 columnNumber = P.unPos column
97 (dir, file) = splitFileName name
98 f = if dir == addTrailingPathSeparator "."
99 then file
100 else name
102-- | Get the current parse position.
103--
104-- This is useful when the position is needed in a way unrelated to the
105-- heirarchy of parsers. Prefer using @withExtent@ and friends.
106getFC :: Parsing m => m FC
107getFC = sourcePositionFC <$> P.getPosition
109-- | Add an extent (widen) our current parsing context.
110addExtent :: MonadWriter FC m => FC -> m ()
111addExtent = tell
113-- | Run a parser and track its extent.
114--
115-- Wrap bare Megaparsec parsers with this to make them "visible" in error
116-- messages. Do not wrap whitespace or comment parsers. If you find an
117-- extent is taking trailing whitespace, it's likely there's a double-wrapped
118-- parser (usually via @Idris.Parser.Helpers.token@).
119trackExtent :: Parsing m => m a -> m a
120trackExtent p = do (FC f (sr, sc) _) <- getFC
121 result <- p
122 (FC f _ (er, ec)) <- getFC
123 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
124 return result
126-- | Run a parser, discard its value, and return its extent.
127extent :: MonadWriter FC m => m a -> m FC
128extent = fmap snd . withExtent
130-- | Run a parser and return its value and extent.
131withExtent :: MonadWriter FC m => m a -> m (a, FC)
132withExtent = listen
134-- | Run a parser and inject the extent after via function application.
135appExtent :: MonadWriter FC m => m (FC -> a) -> m a
136appExtent = fmap app . withExtent