@@ -34,7 +34,6 @@ import System.FilePath
3434import qualified Text.Parser.Char as Chr
3535import Text.Parser.LookAhead
3636import qualified Text.Parser.Token as Tok
37−import qualified Text.Parser.Token.Highlight as Hi
3837import qualified Text.PrettyPrint.ANSI.Leijen as PP
3938import Text.Trifecta ((<?>))
4039import qualified Text.Trifecta as P
@@ -255,23 +254,22 @@ float = do f <- Tok.double
255254
256255{- * Symbols, identifiers, names and operators -}
257256
258−
259−-- | Idris Style for parsing identifiers/reserved keywords
260−idrisStyle :: MonadicParsing m => P.IdentifierStyle m
261−idrisStyle = P.IdentifierStyle {
262− P._styleName = "Idris"
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",
269− "proof", "postulate", "using", "namespace", "class", "instance",
270− "interface", "implementation", "parameters", "public", "private",
271− "export", "abstract", "implicit", "quoteGoal", "constructor", "if",
272− "then", "else"]
273− , P._styleHighlight = Hi.Identifier
274− , P._styleReservedHighlight = Hi.ReservedIdentifier }
257+reservedIdentifiers :: HS.HashSet String
258+reservedIdentifiers = HS.fromList
259+ [ "Type"
260+ , "abstract", "case", "class", "codata", "constructor", "corecord", "data"
261+ , "do", "dsl", "else", "export", "if", "implementation", "implicit"
262+ , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"
263+ , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"
264+ , "postulate", "private", "proof", "public", "quoteGoal", "record"
265+ , "rewrite", "syntax", "then", "total", "using", "where", "with"
266+ ]
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 "_'.")
272+ return $ c : cs
275273
276274char :: MonadicParsing m => Char -> m Char
277275char = Chr.char
@@ -300,7 +298,9 @@ symbolFC str = do (FC file (l, c) _) <- getFC
300298
301299-- | Parses a reserved identifier
302300reserved :: MonadicParsing m => String -> m ()
303−reserved = Tok.reserve idrisStyle
301+reserved name = P.token $ P.try $ do
302+ P.string name
303+ P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
304304
305305-- | Parses a reserved identifier, computing its span. Assumes that
306306-- reserved identifiers never contain line breaks.
@@ -318,7 +318,7 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword
318318reservedOp :: MonadicParsing m => String -> m ()
319319reservedOp name = P.token $ P.try $
320320 do string name
321− P.notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
321+ P.notFollowedBy operatorLetter <?> ("end of " ++ show name)
322322
323323reservedOpFC :: MonadicParsing m => String -> m FC
324324reservedOpFC name = do (FC f (l, c) _) <- getFC
@@ -327,12 +327,12 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC
327327
328328-- | Parses an identifier as a token
329329identifier :: (MonadicParsing m) => m (String, FC)
330−identifier = P.try(do (i, fc) <-
331− P.token $ do (FC f (l, c) _) <- getFC
332− i <- Tok.ident idrisStyle
333− return (i, FC f (l, c) (l, c + length i))
334− when (i == "_") $ P.unexpected "wildcard"
335− return (i, fc))
330+identifier = P.try $ do
331+ (FC f (l, c) _) <- getFC
332+ ident <- identifierOrReserved
333+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident
334+ when (ident == "_") $ P.unexpected "wildcard"
335+ return (ident, FC f (l, c) (l, c + length ident))
336336
337337-- | Parses an identifier with possible namespace as a name
338338iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)