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