@@ -34,7 +34,6 @@ import System.FilePath
34import qualified Text.Parser.Char as Chr
34import qualified Text.Parser.Char as Chr
35import Text.Parser.LookAhead
35import Text.Parser.LookAhead
36import qualified Text.Parser.Token as Tok
36import qualified Text.Parser.Token as Tok
37−import qualified Text.Parser.Token.Highlight as Hi
38import qualified Text.PrettyPrint.ANSI.Leijen as PP
37import qualified Text.PrettyPrint.ANSI.Leijen as PP
39import Text.Trifecta ((<?>))
38import Text.Trifecta ((<?>))
40import qualified Text.Trifecta as P
39import qualified Text.Trifecta as P
@@ -255,23 +254,22 @@ float = do f <- Tok.double
256{- * Symbols, identifiers, names and operators -}
255{- * Symbols, identifiers, names and operators -}
258−
257+reservedIdentifiers :: HS.HashSet String
259−-- | Idris Style for parsing identifiers/reserved keywords
258+reservedIdentifiers = HS.fromList
260−idrisStyle :: MonadicParsing m => P.IdentifierStyle m
259+ [ "Type"
261−idrisStyle = P.IdentifierStyle {
260+ , "abstract", "case", "class", "codata", "constructor", "corecord", "data"
262− P._styleName = "Idris"
261+ , "do", "dsl", "else", "export", "if", "implementation", "implicit"
263− , P._styleStart = P.satisfy isAlpha <|> P.oneOf "_"
264− , P._styleLetter = P.satisfy isAlphaNum <|> P.oneOf "_'."
265− , P._styleReserved = HS.fromList
266− ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",
267− "import", "impossible", "case", "of", "total", "partial", "mutual",
268− "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",
262+ , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"
269− "proof", "postulate", "using", "namespace", "class", "instance",
270− "interface", "implementation", "parameters", "public", "private",
263+ , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"
271− "export", "abstract", "implicit", "quoteGoal", "constructor", "if",
264+ , "postulate", "private", "proof", "public", "quoteGoal", "record"
272− "then", "else"]
265+ , "rewrite", "syntax", "then", "total", "using", "where", "with"
273− , P._styleHighlight = Hi.Identifier
266+ ]
274− , P._styleReservedHighlight = Hi.ReservedIdentifier }
267+
268+identifierOrReserved :: MonadicParsing m => m String
269+identifierOrReserved = P.token $ P.try $ do
270+ c <- P.satisfy isAlpha <|> P.oneOf "_"
271+ cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")
276char :: MonadicParsing m => Char -> m Char
274char :: MonadicParsing m => Char -> m Char
277char = Chr.char
275char = Chr.char
@@ -300,7 +298,9 @@ symbolFC str = do (FC file (l, c) _) <- getFC
301-- | Parses a reserved identifier
299-- | Parses a reserved identifier
302reserved :: MonadicParsing m => String -> m ()
300reserved :: MonadicParsing m => String -> m ()
303−reserved = Tok.reserve idrisStyle
301+reserved name = P.token $ P.try $ do
303+ P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
305-- | Parses a reserved identifier, computing its span. Assumes that
305-- | Parses a reserved identifier, computing its span. Assumes that
306-- reserved identifiers never contain line breaks.
306-- reserved identifiers never contain line breaks.
@@ -318,7 +318,7 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword
318reservedOp :: MonadicParsing m => String -> m ()
318reservedOp :: MonadicParsing m => String -> m ()
319reservedOp name = P.token $ P.try $
319reservedOp name = P.token $ P.try $
320 do string name
320 do string name
321− P.notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
321+ P.notFollowedBy operatorLetter <?> ("end of " ++ show name)
323reservedOpFC :: MonadicParsing m => String -> m FC
323reservedOpFC :: MonadicParsing m => String -> m FC
324reservedOpFC name = do (FC f (l, c) _) <- getFC
324reservedOpFC name = do (FC f (l, c) _) <- getFC
@@ -327,12 +327,12 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC
328-- | Parses an identifier as a token
328-- | Parses an identifier as a token
329identifier :: (MonadicParsing m) => m (String, FC)
329identifier :: (MonadicParsing m) => m (String, FC)
330−identifier = P.try(do (i, fc) <-
330+identifier = P.try $ do
331− P.token $ do (FC f (l, c) _) <- getFC
331+ (FC f (l, c) _) <- getFC
332− i <- Tok.ident idrisStyle
332+ ident <- identifierOrReserved
333− return (i, FC f (l, c) (l, c + length i))
333+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident
334− when (i == "_") $ P.unexpected "wildcard"
334+ when (ident == "_") $ P.unexpected "wildcard"
335− return (i, fc))
335+ return (ident, FC f (l, c) (l, c + length ident))
337-- | Parses an identifier with possible namespace as a name
337-- | Parses an identifier with possible namespace as a name
338iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)
338iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)