git.iko.soy/Idris-dev
on 4efeda8 help sign in
Idris-dev/src/Idris/Parser/Stack.hs
147 lines 4.6 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 err
61 Right v -> Right $ fst v
63{- * Parse errors -}
65newtype ParseError = ParseError { unParseError :: P.ParseErrorBundle String Void }
67parseError :: ParseError -> P.ParseError String Void
68parseError = NonEmpty.head . P.bundleErrors . unParseError
70parseErrorPosState :: ParseError -> P.PosState String
71parseErrorPosState = P.bundlePosState . unParseError
73parseErrorOffset :: ParseError -> Int
74parseErrorOffset = P.errorOffset . parseError
76instance Message ParseError where
77 messageExtent err = sourcePositionFC pos
78 where
79 (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
80 messageText = PP.text . init . P.parseErrorTextPretty . parseError
81 messageSource err = Just sline
82 where
83 (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
85-- | A fully formatted parse error, with caret and bar, etc.
86prettyError :: ParseError -> String
87prettyError = P.errorBundlePretty . unParseError
89{- * Mark and restore -}
91type Mark = P.State String
93-- | Retrieve the parser state so we can restart from this point later.
94mark :: Parsing m => m Mark
95mark = P.getParserState
97restore :: Parsing m => Mark -> m ()
98restore = P.setParserState
100{- * Tracking the extent of productions -}
102sourcePositionFC :: P.SourcePos -> FC
103sourcePositionFC (P.SourcePos name line column) =
104 FC f (lineNumber, columnNumber) (lineNumber, columnNumber)
105 where
106 lineNumber = P.unPos line
107 columnNumber = P.unPos column
108 (dir, file) = splitFileName name
109 f = if dir == addTrailingPathSeparator "."
110 then file
111 else name
113-- | Get the current parse position.
114--
115-- This is useful when the position is needed in a way unrelated to the
116-- heirarchy of parsers. Prefer using @withExtent@ and friends.
117getFC :: Parsing m => m FC
118getFC = sourcePositionFC <$> P.getSourcePos
120-- | Add an extent (widen) our current parsing context.
121addExtent :: MonadWriter FC m => FC -> m ()
122addExtent = tell
124-- | Run a parser and track its extent.
125--
126-- Wrap bare Megaparsec parsers with this to make them "visible" in error
127-- messages. Do not wrap whitespace or comment parsers. If you find an
128-- extent is taking trailing whitespace, it's likely there's a double-wrapped
129-- parser (usually via @Idris.Parser.Helpers.token@).
130trackExtent :: Parsing m => m a -> m a
131trackExtent p = do ~(FC f (sr, sc) _) <- getFC
132 result <- p
133 ~(FC f _ (er, ec)) <- getFC
134 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
135 return result
137-- | Run a parser, discard its value, and return its extent.
138extent :: MonadWriter FC m => m a -> m FC
139extent = fmap snd . withExtent
141-- | Run a parser and return its value and extent.
142withExtent :: MonadWriter FC m => m a -> m (a, FC)
143withExtent = listen
145-- | Run a parser and inject the extent after via function application.
146appExtent :: MonadWriter FC m => m (FC -> a) -> m a
147appExtent = fmap app . withExtent