4447a4d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed structure of parser such that it correctly overloads

4447a4dAhmad Salim Al-Sibahi13 years ago

src/Idris/Parser.hs+28−25

compare with master

unifiedsplit

@@ -4,7 +4,7 @@ module Idris.Parser where

4import Prelude hiding (pi)

6import Text.Trifecta.Delta

7−import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)

7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

8import Text.Parser.LookAhead

9import Text.Parser.Expression

10import qualified Text.Parser.Token as Tok

@@ -56,15 +56,18 @@ import System.FilePath

58-- | Idris parser with state used during parsing

59−type IdrisParser = StateT IState Parser

59+type IdrisParser = StateT IState IdrisInnerParser

60+

61+newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

62+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)

63+

64+instance TokenParsing IdrisInnerParser where

65+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

61-- | Generalized monadic parsing constraint type

67-- | Generalized monadic parsing constraint type

62type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

68type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

64{- * Space, comments and literals (token/lexing like parsers) -}

70{- * Space, comments and literals (token/lexing like parsers) -}

65−-- | Parses a token by applying parser and then consuming all following whiteSpace

66−lexeme :: MonadicParsing m => m a -> m a

67−lexeme p = p <* whiteSpace

69-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

72-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

70simpleWhiteSpace :: MonadicParsing m => m ()

73simpleWhiteSpace :: MonadicParsing m => m ()

@@ -135,29 +138,29 @@ docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; ret

135 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")

138 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")

136 <?> ""

139 <?> ""

137

140

138−-- | Consumes whitespace (and comments)

141+-- | Parses some white space

139whiteSpace :: MonadicParsing m => m ()

142whiteSpace :: MonadicParsing m => m ()

140−whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

143+whiteSpace = Tok.whiteSpace

141

144

142-- | Parses a string literal

145-- | Parses a string literal

143stringLiteral :: MonadicParsing m => m String

146stringLiteral :: MonadicParsing m => m String

144−stringLiteral = lexeme $ Tok.stringLiteral

147+stringLiteral = Tok.stringLiteral

145

148

146-- | Parses a char literal

149-- | Parses a char literal

147charLiteral :: MonadicParsing m => m Char

150charLiteral :: MonadicParsing m => m Char

148−charLiteral = lexeme $ Tok.charLiteral

151+charLiteral = Tok.charLiteral

149

152

150-- | Parses a natural number

153-- | Parses a natural number

151natural :: MonadicParsing m => m Integer

154natural :: MonadicParsing m => m Integer

152−natural = lexeme $ Tok.natural

155+natural = Tok.natural

153

156

154-- | Parses an integral number

157-- | Parses an integral number

155integer :: MonadicParsing m => m Integer

158integer :: MonadicParsing m => m Integer

156−integer = lexeme $ Tok.integer

159+integer = Tok.integer

157

160

158-- | Parses a floating point number

161-- | Parses a floating point number

159float :: MonadicParsing m => m Double

162float :: MonadicParsing m => m Double

160−float = lexeme $ Tok.double

163+float = Tok.double

161

164

162{- * Symbols, identifiers, names and operators -}

165{- * Symbols, identifiers, names and operators -}

163

166

@@ -186,28 +189,28 @@ char = Chr.char

186string :: MonadicParsing m => String -> m String

189string :: MonadicParsing m => String -> m String

187string = Chr.string

190string = Chr.string

188

191

189−-- | Parses a character as a lexeme

192+-- | Parses a character as a token

190lchar :: MonadicParsing m => Char -> m Char

193lchar :: MonadicParsing m => Char -> m Char

191−lchar = lexeme . char

194+lchar = token . char

192

195

193−-- | Parses string as a lexeme

196+-- | Parses string as a token

194symbol :: MonadicParsing m => String -> m String

197symbol :: MonadicParsing m => String -> m String

195−symbol = lexeme . Tok.symbol

198+symbol = Tok.symbol

196

199

197-- | Parses a reserved identifier

200-- | Parses a reserved identifier

198reserved :: MonadicParsing m => String -> m ()

201reserved :: MonadicParsing m => String -> m ()

199−reserved = lexeme . Tok.reserve idrisStyle

202+reserved = Tok.reserve idrisStyle

200

203

201-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

204-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

202-- | Parses a reserved operator

205-- | Parses a reserved operator

203reservedOp :: MonadicParsing m => String -> m ()

206reservedOp :: MonadicParsing m => String -> m ()

204−reservedOp name = lexeme $ try $

207+reservedOp name = token $ try $

205 do string name

208 do string name

206 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

209 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

207

210

208−-- | Parses an identifier as a lexeme

211+-- | Parses an identifier as a token

209identifier :: MonadicParsing m => m String

212identifier :: MonadicParsing m => m String

210−identifier = lexeme $ Tok.ident idrisStyle

213+identifier = token $ Tok.ident idrisStyle

211

214

212-- | Parses an identifier with possible namespace as a name

215-- | Parses an identifier with possible namespace as a name

213iName :: MonadicParsing m => [String] -> m Name

216iName :: MonadicParsing m => [String] -> m Name

@@ -261,7 +264,7 @@ operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

261

264

262-- | Parses an operator

265-- | Parses an operator

263operator :: MonadicParsing m => m String

266operator :: MonadicParsing m => m String

264−operator = do op <- lexeme . some $ operatorLetter

267+operator = do op <- token . some $ operatorLetter

265 when (op == ":") $ fail "(:) is not a valid operator"

268 when (op == ":") $ fail "(:) is not a valid operator"

266 return op

269 return op

267

270

@@ -2536,17 +2539,17 @@ fullTactic syn = do t <- tactic syn

2536{- * Loading and parsing -}

2539{- * Loading and parsing -}

2537{- | Parses an expression from input -}

2540{- | Parses an expression from input -}

2538parseExpr :: IState -> String -> Result PTerm

2541parseExpr :: IState -> String -> Result PTerm

2539−parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)

2542+parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)

2540

2543

2541{- | Parses a tactic from input -}

2544{- | Parses a tactic from input -}

2542parseTactic :: IState -> String -> Result PTactic

2545parseTactic :: IState -> String -> Result PTactic

2543−parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)

2546+parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)

2544

2547

2545-- | Parse module header and imports

2548-- | Parse module header and imports

2546parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

2549parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

2547parseImports fname input

2550parseImports fname input

2548 = do i <- getIState

2551 = do i <- getIState

2549− case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of

2552+ case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

2550 Failure err -> fail (show err)

2553 Failure err -> fail (show err)

2551 Success (x, i) -> do -- Discard state updates (there should be

2554 Success (x, i) -> do -- Discard state updates (there should be

2552 -- none anyway)

2555 -- none anyway)

@@ -2570,7 +2573,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

2570 Idris [PDecl]

2573 Idris [PDecl]

2571parseProg syn fname input mrk

2574parseProg syn fname input mrk

2572 = do i <- getIState

2575 = do i <- getIState

2573− case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of

2576+ case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

2574 Failure doc -> do iputStrLn (show doc)

2577 Failure doc -> do iputStrLn (show doc)

2575 -- FIXME: Get error location from trifecta

2578 -- FIXME: Get error location from trifecta

2576 --let errl = sourceLine (errorPos err)

2579 --let errl = sourceLine (errorPos err)

src/Idris/REPLParser.hs+1−1

@@ -23,7 +23,7 @@ import Data.Char(toLower)

23import qualified Data.ByteString.UTF8 as UTF8

25parseCmd :: IState -> String -> String -> Result Command

26−parseCmd i inputname = parseString (evalStateT pCmd i) (Directed (UTF8.fromString inputname) 0 0 0 0)

26+parseCmd i inputname = parseString (P.runInnerParser (evalStateT pCmd i)) (Directed (UTF8.fromString inputname) 0 0 0 0)

28cmd :: [String] -> P.IdrisParser ()

29cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)