git.iko.soy/Idris-dev
on b3ee2df help sign in
Idris-dev/src/Idris/Parser/Stack.hs
139 lines 4.3 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 , errorExtent
17 , errorMessage
18 , prettyError
19 -- * Mark and restore
20 , Mark
21 , mark
22 , restore
24 -- * Tracking the extent of productions
25 --
26 -- The parser stack automatically builds up the extent of any parse from
27 -- the extents of sub-parsers wrapped with @trackExtent@.
28 , getFC
29 , addExtent
30 , trackExtent
31 , extent
32 , withExtent
33 , appExtent
34 )
35where
37import Idris.Core.TT (FC(..))
39import Control.Arrow (app)
40import Control.Monad.State.Strict (StateT(..), evalStateT)
41import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,
42 runWriterT, tell)
43import qualified Data.List.NonEmpty as NonEmpty
44import Data.Void (Void(..))
45import System.FilePath (addTrailingPathSeparator, splitFileName)
46import qualified Text.Megaparsec as P
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)
67-- | Retrieve a parse error's FC
68errorExtent :: ParseError -> FC
69errorExtent (ParseError _ err) = sourcePositionFC pos
70 where
71 (pos NonEmpty.:| _) = P.errorPos err
73-- | A single-line parse error message, including location.
74errorMessage :: ParseError -> String
75errorMessage (ParseError _ err) = P.parseErrorTextPretty err
77-- | A fully formatted parse error, with caret and bar, etc.
78prettyError :: ParseError -> String
79prettyError (ParseError s err) = P.parseErrorPretty' s err
81{- * Mark and restore -}
83type Mark = P.State String
85-- | Retrieve the parser state so we can restart from this point later.
86mark :: Parsing m => m Mark
87mark = P.getParserState
89restore :: Parsing m => Mark -> m ()
90restore = P.setParserState
92{- * Tracking the extent of productions -}
94sourcePositionFC :: P.SourcePos -> FC
95sourcePositionFC (P.SourcePos name line column) =
96 FC f (lineNumber, columnNumber) (lineNumber, columnNumber)
97 where
98 lineNumber = P.unPos line
99 columnNumber = P.unPos column
100 (dir, file) = splitFileName name
101 f = if dir == addTrailingPathSeparator "."
102 then file
103 else name
105-- | Get the current parse position.
106--
107-- This is useful when the position is needed in a way unrelated to the
108-- heirarchy of parsers. Prefer using @withExtent@ and friends.
109getFC :: Parsing m => m FC
110getFC = sourcePositionFC <$> P.getPosition
112-- | Add an extent (widen) our current parsing context.
113addExtent :: MonadWriter FC m => FC -> m ()
114addExtent = tell
116-- | Run a parser and track its extent.
117--
118-- Wrap bare Megaparsec parsers with this to make them "visible" in error
119-- messages. Do not wrap whitespace or comment parsers. If you find an
120-- extent is taking trailing whitespace, it's likely there's a double-wrapped
121-- parser (usually via @Idris.Parser.Helpers.token@).
122trackExtent :: Parsing m => m a -> m a
123trackExtent p = do (FC f (sr, sc) _) <- getFC
124 result <- p
125 (FC f _ (er, ec)) <- getFC
126 addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))
127 return result
129-- | Run a parser, discard its value, and return its extent.
130extent :: MonadWriter FC m => m a -> m FC
131extent = fmap snd . withExtent
133-- | Run a parser and return its value and extent.
134withExtent :: MonadWriter FC m => m a -> m (a, FC)
135withExtent = listen
137-- | Run a parser and inject the extent after via function application.
138appExtent :: MonadWriter FC m => m (FC -> a) -> m a
139appExtent = fmap app . withExtent