git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/src/Core/CoreParser.hs
575 lines 19 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4 idrisLexer, maybeWithNS, pDocComment, opChars) where
6import Core.TT
8import Text.ParserCombinators.Parsec
9import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Language
11import Text.ParserCombinators.Parsec.Prim
12import Text.ParserCombinators.Parsec.Char
13import Text.ParserCombinators.Parsec.Combinator
14import qualified Text.ParserCombinators.Parsec.Token as PTok
16import Control.Monad.State
17import Control.Monad.Identity
18import Data.Char
19import Data.List
20import Debug.Trace
22type TokenParser a = PTok.TokenParser a
24idrisDef = haskellDef {
25 opStart = iOpStart,
26 opLetter = iOpLetter,
27 identLetter = identLetter haskellDef <|> lchar '.',
28 reservedOpNames
29 = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
30 reservedNames
31 = ["let", "in", "data", "codata", "record", "Type",
32 "do", "dsl", "import", "impossible",
33 "case", "of", "total", "partial", "mutual",
34 "infix", "infixl", "infixr", "rewrite",
35 "where", "with", "syntax", "proof", "postulate",
36 "using", "namespace", "class", "instance",
37 "public", "private", "abstract", "implicit",
38 "quoteGoal"]
39 }
41-- | The characters allowed in operator names
42opChars = ":!#$%&*+./<=>?@\\^|-~"
44iOpStart = oneOf opChars
45iOpLetter = oneOf opChars
46-- <|> letter
48idrisLexer :: TokenParser a
49idrisLexer = idrisMakeTokenParser idrisDef
51lexer = idrisLexer
53-- Taken from Parsec source code
54lexWS = do i <- getInput
55 skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
56 where
58 simpleSpace = skipMany1 (satisfy isSpace)
59 oneLineComment =
60 try (void $ string "--\n") <|>
61 do try (do string "--"
62 satisfy (\x -> x /= '|' && x /= '^'))
63 skipMany (satisfy (/= '\n'))
64 multiLineComment =
65 try (void $ string "{--}") <|>
66 do try (do string "{-"
67 satisfy (\x -> x /= '|' && x /= '^'))
68 inCommentMulti
70 inCommentMulti
71 = do{ try (string "-}") ; return () }
72 <|> do{ multiLineComment ; inCommentMulti }
73 <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }
74 <|> do{ oneOf startEnd ; inCommentMulti }
75 <?> "end of comment"
76 where
77 startEnd = "-}{"
79whiteSpace= PTok.whiteSpace lexer
80lexeme = PTok.lexeme lexer
81symbol = PTok.symbol lexer
82natural = PTok.natural lexer
83parens = PTok.parens lexer
84semi = PTok.semi lexer
85comma = PTok.comma lexer
86identifier= PTok.identifier lexer
87reserved = PTok.reserved lexer
88operator = PTok.operator lexer
89reservedOp= PTok.reservedOp lexer
90strlit = PTok.stringLiteral lexer
91lchar = lexeme.char
93type CParser a = GenParser Char a
95parseFile = runParser pTestFile () "(input)"
96parseDef = runParser pDef () "(input)"
97parseTerm = runParser pTerm () "(input)"
99pTestFile :: CParser a RProgram
100pTestFile = do p <- many1 pDef ; eof
101 return p
103iName :: [String] -> CParser a Name
104iName bad = maybeWithNS identifier False bad
106-- Enhances a given parser to accept an optional namespace. All possible
107-- namespace prefixes are tried in ascending / descending order, and
108-- identifiers of a given list fail.
109maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
110maybeWithNS parser ascend bad = do
111 i <- option "" (lookAhead identifier)
112 when (i `elem` bad) $ fail "Reserved identifier"
113 let transf = if ascend then id else reverse
114 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
115 return $ mkName (x, xs)
116 where
117 parserNoNS = do x <- parser; return (x, "")
118 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
119 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
121-- List of all initial segments in ascending order of a list. Every such
122-- initial segment ends right before an element satisfying the given
123-- condition.
124initsEndAt :: (a -> Bool) -> [a] -> [[a]]
125initsEndAt p [] = []
126initsEndAt p (x:xs) | p x = [] : x_inits_xs
127 | otherwise = x_inits_xs
128 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
130-- Create a `Name' from a pair of strings representing a base name and its
131-- namespace.
132mkName :: (String, String) -> Name
133mkName (n, "") = UN n
134mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
135 where parseNS x = case span (/= '.') x of
136 (x, "") -> [x]
137 (x, '.':y) -> x : parseNS y
139pDocComment :: Char -> CParser a String
140pDocComment c
141 = try (do string ("--")
142 char c
143 skipMany simpleSpace
144 i <- getInput
145 let (doc, rest) = span (/='\n') i
146 setInput rest
147 whiteSpace
148 return doc)
149 <|> try (do string ("{-")
150 char c
151 skipMany simpleSpace
152 i <- getInput
153 -- read to '-}'
154 let (doc, rest) = spanComment "" i
155 setInput rest
156 whiteSpace
157 return doc)
158 where spanComment acc ('-':'}':xs) = (reverse acc, xs)
159 spanComment acc (x:xs) = spanComment (x : acc) xs
160 spanComment acc [] = (acc, [])
161 simpleSpace = skipMany1 (satisfy isSpace)
163pDef :: CParser a (Name, RDef)
164pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
165 lchar '='
166 tm <- pTerm
167 lchar ';'
168 return (x, RFunction (RawFun ty tm)))
169 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
170 return (x, RConst ty)
171 <|> do (x, d) <- pData; lchar ';'
172 return (x, RData d)
174app :: CParser a (Raw -> Raw -> Raw)
175app = do whiteSpace ; return RApp
177arrow :: CParser a (Raw -> Raw -> Raw)
178arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
180pTerm :: CParser a Raw
181pTerm = try (do chainl1 pNoApp app)
182 <|> pNoApp
184pNoApp :: CParser a Raw
185pNoApp = try (chainr1 pExp arrow)
186 <|> pExp
187pExp :: CParser a Raw
188pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
189 symbol "=>";
190 sc <- pTerm
191 return (RBind x (Lam ty) sc)
192 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
193 lchar '.';
194 sc <- pTerm
195 return (RBind x (Hole ty) sc))
196 <|> try (do lchar '(';
197 x <- iName []; lchar ':'; ty <- pTerm
198 lchar ')';
199 symbol "->";
200 sc <- pTerm
201 return (RBind x (Pi ty) sc))
202 <|> try (do lchar '(';
203 t <- pTerm
204 lchar ')'
205 return t)
206 <|> try (do symbol "??";
207 x <- iName []; lchar ':'; ty <- pTerm
208 lchar '=';
209 val <- pTerm
210 sc <- pTerm
211 return (RBind x (Guess ty val) sc))
212 <|> try (do reserved "let";
213 x <- iName []; lchar ':'; ty <- pTerm
214 lchar '=';
215 val <- pTerm
216 reserved "in";
217 sc <- pTerm
218 return (RBind x (Let ty val) sc))
219 <|> try (do lchar '_';
220 x <- iName []; lchar ':'; ty <- pTerm
221 lchar '.';
222 sc <- pTerm
223 return (RBind x (PVar ty) sc))
224 <|> try (do reserved "Type"
225 return RType)
226 <|> try (do x <- iName []
227 return (Var x))
229pData :: CParser a (Name, RawDatatype)
230pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
231 cs <- many pConstructor
232 return (x, RDatatype x ty cs)
234pConstructor :: CParser a (Name, Raw)
235pConstructor = do lchar '|'
236 c <- iName []; lchar ':'; ty <- pTerm
237 return (c, ty)
239------ borrowed from Parsec
240-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
242idrisMakeTokenParser languageDef
243 = PTok.TokenParser{
244 PTok.identifier = identifier
245 , PTok.reserved = reserved
246 , PTok.operator = operator
247 , PTok.reservedOp = reservedOp
249 , PTok.charLiteral = charLiteral
250 , PTok.stringLiteral = stringLiteral
251 , PTok.natural = natural
252 , PTok.integer = integer
253 , PTok.float = float
254 , PTok.naturalOrFloat = naturalOrFloat
255 , PTok.decimal = decimal
256 , PTok.hexadecimal = hexadecimal
257 , PTok.octal = octal
259 , PTok.symbol = symbol
260 , PTok.lexeme = lexeme
261 , PTok.whiteSpace = lexWS
263 , PTok.parens = parens
264 , PTok.braces = braces
265 , PTok.angles = angles
266 , PTok.brackets = brackets
267 , PTok.squares = brackets
268 , PTok.semi = semi
269 , PTok.comma = comma
270 , PTok.colon = colon
271 , PTok.dot = dot
272 , PTok.semiSep = semiSep
273 , PTok.semiSep1 = semiSep1
274 , PTok.commaSep = commaSep
275 , PTok.commaSep1 = commaSep1
276 }
277 where
279 -----------------------------------------------------------
280 -- Bracketing
281 -----------------------------------------------------------
282 parens p = between (symbol "(") (symbol ")") p
283 braces p = between (symbol "{") (symbol "}") p
284 angles p = between (symbol "<") (symbol ">") p
285 brackets p = between (symbol "[") (symbol "]") p
287 semi = symbol ";"
288 comma = symbol ","
289 dot = symbol "."
290 colon = symbol ":"
292 commaSep p = sepBy p comma
293 semiSep p = sepBy p semi
295 commaSep1 p = sepBy1 p comma
296 semiSep1 p = sepBy1 p semi
299 -----------------------------------------------------------
300 -- Chars & Strings
301 -----------------------------------------------------------
302 charLiteral = lexeme (between (char '\'')
303 (char '\'' <?> "end of character")
304 characterChar )
305 <?> "character"
307 characterChar = charLetter <|> charEscape
308 <?> "literal character"
310 charEscape = do{ char '\\'; escapeCode }
311 charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
315 stringLiteral = lexeme (
316 do{ str <- between (char '"')
317 (char '"' <?> "end of string")
318 (many stringChar)
319 ; return (foldr (maybe id (:)) "" str)
320 }
321 <?> "literal string")
323 stringChar = do{ c <- stringLetter; return (Just c) }
324 <|> stringEscape
325 <?> "string character"
327 stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
329 stringEscape = do{ char '\\'
330 ; do{ escapeGap ; return Nothing }
331 <|> do{ escapeEmpty; return Nothing }
332 <|> do{ esc <- escapeCode; return (Just esc) }
333 }
335 escapeEmpty = char '&'
336 escapeGap = do{ many1 space
337 ; char '\\' <?> "end of string gap"
338 }
342 -- escape codes
343 escapeCode = charEsc <|> charNum <|> charAscii <|> charControl
344 <?> "escape code"
346 charControl = do{ char '^'
347 ; code <- upper
348 ; return (toEnum (fromEnum code - fromEnum 'A'))
349 }
351 charNum = do{ code <- decimal
352 <|> do{ char 'o'; number 8 octDigit }
353 <|> do{ char 'x'; number 16 hexDigit }
354 ; return (toEnum (fromInteger code))
355 }
357 charEsc = choice (map parseEsc escMap)
358 where
359 parseEsc (c,code) = do{ char c; return code }
361 charAscii = choice (map parseAscii asciiMap)
362 where
363 parseAscii (asc,code) = try (do{ string asc; return code })
366 -- escape code tables
367 escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
368 asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
370 ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",
371 "FS","GS","RS","US","SP"]
372 ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",
373 "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",
374 "CAN","SUB","ESC","DEL"]
376 ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',
377 '\EM','\FS','\GS','\RS','\US','\SP']
378 ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',
379 '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',
380 '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']
383 -----------------------------------------------------------
384 -- Numbers
385 -----------------------------------------------------------
386 naturalOrFloat = lexeme (natFloat) <?> "number"
388 float = lexeme floating <?> "float"
389 integer = lexeme int <?> "integer"
390 natural = lexeme nat <?> "natural"
393 -- floats
394 floating = do{ n <- decimal
395 ; fractExponent n
396 }
399 natFloat = do{ char '0'
400 ; zeroNumFloat
401 }
402 <|> decimalFloat
404 zeroNumFloat = do{ n <- hexadecimal <|> octal
405 ; return (Left n)
406 }
407 <|> decimalFloat
408 <|> fractFloat 0
409 <|> return (Left 0)
411 decimalFloat = do{ n <- decimal
412 ; option (Left n)
413 (fractFloat n)
414 }
416 fractFloat n = do{ f <- fractExponent n
417 ; return (Right f)
418 }
420 fractExponent n = do{ fract <- fraction
421 ; expo <- option 1.0 exponent'
422 ; return ((fromInteger n + fract)*expo)
423 }
424 <|>
425 do{ expo <- exponent'
426 ; return ((fromInteger n)*expo)
427 }
429 fraction = do{ char '.'
430 ; digits <- many1 digit <?> "fraction"
431 ; return (foldr op 0.0 digits)
432 }
433 <?> "fraction"
434 where
435 op d f = (f + fromIntegral (digitToInt d))/10.0
437 exponent' = do{ oneOf "eE"
438 ; f <- sign
439 ; e <- decimal <?> "exponent"
440 ; return (power (f e))
441 }
442 <?> "exponent"
443 where
444 power e | e < 0 = 1.0/power(-e)
445 | otherwise = fromInteger (10^e)
448 -- integers and naturals
449 int = do{ f <- lexeme sign
450 ; n <- nat
451 ; return (f n)
452 }
454 sign = (char '-' >> return negate)
455 <|> (char '+' >> return id)
456 <|> return id
458 nat = zeroNumber <|> decimal
460 zeroNumber = do{ char '0'
461 ; hexadecimal <|> octal <|> decimal <|> return 0
462 }
463 <?> ""
465 decimal = number 10 digit
466 hexadecimal = do{ oneOf "xX"; number 16 hexDigit }
467 octal = do{ oneOf "oO"; number 8 octDigit }
469 number base baseDigit
470 = do{ digits <- many1 baseDigit
471 ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits
472 ; seq n (return n)
473 }
475 -----------------------------------------------------------
476 -- Operators & reserved ops
477 -----------------------------------------------------------
478 reservedOp name =
479 lexeme $ try $
480 do{ string name
481 ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
482 }
484 operator =
485 lexeme $ try $
486 do{ name <- oper
487 ; if (isReservedOp name)
488 then unexpected ("reserved operator " ++ show name)
489 else return name
490 }
492 oper =
493 do{ c <- (opStart languageDef)
494 ; cs <- many (opLetter languageDef)
495 ; return (c:cs)
496 }
497 <?> "operator"
499 isReservedOp name =
500 isReserved (sort (reservedOpNames languageDef)) name
503 -----------------------------------------------------------
504 -- Identifiers & Reserved words
505 -----------------------------------------------------------
506 reserved name =
507 lexeme $ try $
508 do{ caseString name
509 ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
510 }
512 caseString name
513 | caseSensitive languageDef = string name
514 | otherwise = do{ walk name; return name }
515 where
516 walk [] = return ()
517 walk (c:cs) = do{ caseChar c <?> msg; walk cs }
519 caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)
520 | otherwise = char c
522 msg = show name
525 identifier =
526 lexeme $ try $
527 do{ name <- ident
528 ; if (isReservedName name)
529 then unexpected ("reserved word " ++ show name)
530 else return name
531 }
534 ident
535 = do{ c <- identStart languageDef
536 ; cs <- many (identLetter languageDef)
537 ; return (c:cs)
538 }
539 <?> "identifier"
541 isReservedName name
542 = isReserved theReservedNames caseName
543 where
544 caseName | caseSensitive languageDef = name
545 | otherwise = map toLower name
548 isReserved names name
549 = scan names
550 where
551 scan [] = False
552 scan (r:rs) = case (compare r name) of
553 LT -> scan rs
554 EQ -> True
555 GT -> False
557 theReservedNames
558 | caseSensitive languageDef = sortedNames
559 | otherwise = map (map toLower) sortedNames
560 where
561 sortedNames = sort (reservedNames languageDef)
565 -----------------------------------------------------------
566 -- White space & symbols
567 -----------------------------------------------------------
568 symbol name
569 = lexeme (string name)
571 lexeme p
572 = do{ x <- p; whiteSpace; return x }
574 --whiteSpace
575 whiteSpace = lexWS