git.iko.soy/Idris-dev
on 308efea help sign in
Idris-dev/src/Core/CoreParser.hs
573 lines 20 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 "Int", "Integer", "Float", "Char", "String", "Ptr",
39 "Bits8", "Bits16", "Bits32", "Bits64"]
40 }
42-- | The characters allowed in operator names
43opChars = ":!#$%&*+./<=>?@\\^|-~"
45iOpStart = oneOf opChars
46iOpLetter = oneOf opChars
47-- <|> letter
49idrisLexer :: TokenParser a
50idrisLexer = idrisMakeTokenParser idrisDef
52lexer = idrisLexer
54-- Taken from Parsec source code
55lexWS = do i <- getInput
56 skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
57 where
59 simpleSpace = skipMany1 (satisfy isSpace)
60 oneLineComment = do try (do string ("--")
61 satisfy (\x -> x /= '|' && x /= '^'))
62 skipMany (satisfy (/= '\n'))
63 return ()
64 multiLineComment = do try (do string "{-"
65 satisfy (\x -> x /= '|' && x /= '^'))
66 inCommentMulti
68 inCommentMulti
69 = do{ try (string "-}") ; return () }
70 <|> do{ multiLineComment ; inCommentMulti }
71 <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }
72 <|> do{ oneOf startEnd ; inCommentMulti }
73 <?> "end of comment"
74 where
75 startEnd = "-}{"
77whiteSpace= PTok.whiteSpace lexer
78lexeme = PTok.lexeme lexer
79symbol = PTok.symbol lexer
80natural = PTok.natural lexer
81parens = PTok.parens lexer
82semi = PTok.semi lexer
83comma = PTok.comma lexer
84identifier= PTok.identifier lexer
85reserved = PTok.reserved lexer
86operator = PTok.operator lexer
87reservedOp= PTok.reservedOp lexer
88strlit = PTok.stringLiteral lexer
89lchar = lexeme.char
91type CParser a = GenParser Char a
93parseFile = runParser pTestFile () "(input)"
94parseDef = runParser pDef () "(input)"
95parseTerm = runParser pTerm () "(input)"
97pTestFile :: CParser a RProgram
98pTestFile = do p <- many1 pDef ; eof
99 return p
101iName :: [String] -> CParser a Name
102iName bad = maybeWithNS identifier False bad
104-- Enhances a given parser to accept an optional namespace. All possible
105-- namespace prefixes are tried in ascending / descending order, and
106-- identifiers of a given list fail.
107maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
108maybeWithNS parser ascend bad = do
109 i <- option "" (lookAhead identifier)
110 when (i `elem` bad) $ fail "Reserved identifier"
111 let transf = if ascend then id else reverse
112 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
113 return $ mkName (x, xs)
114 where
115 parserNoNS = do x <- parser; return (x, "")
116 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
117 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
119-- List of all initial segments in ascending order of a list. Every such
120-- initial segment ends right before an element satisfying the given
121-- condition.
122initsEndAt :: (a -> Bool) -> [a] -> [[a]]
123initsEndAt p [] = []
124initsEndAt p (x:xs) | p x = [] : x_inits_xs
125 | otherwise = x_inits_xs
126 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
128-- Create a `Name' from a pair of strings representing a base name and its
129-- namespace.
130mkName :: (String, String) -> Name
131mkName (n, "") = UN n
132mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
133 where parseNS x = case span (/= '.') x of
134 (x, "") -> [x]
135 (x, '.':y) -> x : parseNS y
137pDocComment :: Char -> CParser a String
138pDocComment c
139 = try (do string ("--")
140 char c
141 skipMany simpleSpace
142 i <- getInput
143 let (doc, rest) = span (/='\n') i
144 setInput rest
145 whiteSpace
146 return doc)
147 <|> try (do string ("{-")
148 char c
149 skipMany simpleSpace
150 i <- getInput
151 -- read to '-}'
152 let (doc, rest) = spanComment "" i
153 setInput rest
154 whiteSpace
155 return doc)
156 where spanComment acc ('-':'}':xs) = (reverse acc, xs)
157 spanComment acc (x:xs) = spanComment (x : acc) xs
158 spanComment acc [] = (acc, [])
159 simpleSpace = skipMany1 (satisfy isSpace)
161pDef :: CParser a (Name, RDef)
162pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
163 lchar '='
164 tm <- pTerm
165 lchar ';'
166 return (x, RFunction (RawFun ty tm)))
167 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
168 return (x, RConst ty)
169 <|> do (x, d) <- pData; lchar ';'
170 return (x, RData d)
172app :: CParser a (Raw -> Raw -> Raw)
173app = do whiteSpace ; return RApp
175arrow :: CParser a (Raw -> Raw -> Raw)
176arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
178pTerm :: CParser a Raw
179pTerm = try (do chainl1 pNoApp app)
180 <|> pNoApp
182pNoApp :: CParser a Raw
183pNoApp = try (chainr1 pExp arrow)
184 <|> pExp
185pExp :: CParser a Raw
186pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
187 symbol "=>";
188 sc <- pTerm
189 return (RBind x (Lam ty) sc)
190 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
191 lchar '.';
192 sc <- pTerm
193 return (RBind x (Hole ty) sc))
194 <|> try (do lchar '(';
195 x <- iName []; lchar ':'; ty <- pTerm
196 lchar ')';
197 symbol "->";
198 sc <- pTerm
199 return (RBind x (Pi ty) sc))
200 <|> try (do lchar '(';
201 t <- pTerm
202 lchar ')'
203 return t)
204 <|> try (do symbol "??";
205 x <- iName []; lchar ':'; ty <- pTerm
206 lchar '=';
207 val <- pTerm
208 sc <- pTerm
209 return (RBind x (Guess ty val) sc))
210 <|> try (do reserved "let";
211 x <- iName []; lchar ':'; ty <- pTerm
212 lchar '=';
213 val <- pTerm
214 reserved "in";
215 sc <- pTerm
216 return (RBind x (Let ty val) sc))
217 <|> try (do lchar '_';
218 x <- iName []; lchar ':'; ty <- pTerm
219 lchar '.';
220 sc <- pTerm
221 return (RBind x (PVar ty) sc))
222 <|> try (do reserved "Type"
223 return RType)
224 <|> try (do x <- iName []
225 return (Var x))
227pData :: CParser a (Name, RawDatatype)
228pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
229 cs <- many pConstructor
230 return (x, RDatatype x ty cs)
232pConstructor :: CParser a (Name, Raw)
233pConstructor = do lchar '|'
234 c <- iName []; lchar ':'; ty <- pTerm
235 return (c, ty)
237------ borrowed from Parsec
238-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
240idrisMakeTokenParser languageDef
241 = PTok.TokenParser{
242 PTok.identifier = identifier
243 , PTok.reserved = reserved
244 , PTok.operator = operator
245 , PTok.reservedOp = reservedOp
247 , PTok.charLiteral = charLiteral
248 , PTok.stringLiteral = stringLiteral
249 , PTok.natural = natural
250 , PTok.integer = integer
251 , PTok.float = float
252 , PTok.naturalOrFloat = naturalOrFloat
253 , PTok.decimal = decimal
254 , PTok.hexadecimal = hexadecimal
255 , PTok.octal = octal
257 , PTok.symbol = symbol
258 , PTok.lexeme = lexeme
259 , PTok.whiteSpace = lexWS
261 , PTok.parens = parens
262 , PTok.braces = braces
263 , PTok.angles = angles
264 , PTok.brackets = brackets
265 , PTok.squares = brackets
266 , PTok.semi = semi
267 , PTok.comma = comma
268 , PTok.colon = colon
269 , PTok.dot = dot
270 , PTok.semiSep = semiSep
271 , PTok.semiSep1 = semiSep1
272 , PTok.commaSep = commaSep
273 , PTok.commaSep1 = commaSep1
274 }
275 where
277 -----------------------------------------------------------
278 -- Bracketing
279 -----------------------------------------------------------
280 parens p = between (symbol "(") (symbol ")") p
281 braces p = between (symbol "{") (symbol "}") p
282 angles p = between (symbol "<") (symbol ">") p
283 brackets p = between (symbol "[") (symbol "]") p
285 semi = symbol ";"
286 comma = symbol ","
287 dot = symbol "."
288 colon = symbol ":"
290 commaSep p = sepBy p comma
291 semiSep p = sepBy p semi
293 commaSep1 p = sepBy1 p comma
294 semiSep1 p = sepBy1 p semi
297 -----------------------------------------------------------
298 -- Chars & Strings
299 -----------------------------------------------------------
300 charLiteral = lexeme (between (char '\'')
301 (char '\'' <?> "end of character")
302 characterChar )
303 <?> "character"
305 characterChar = charLetter <|> charEscape
306 <?> "literal character"
308 charEscape = do{ char '\\'; escapeCode }
309 charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
313 stringLiteral = lexeme (
314 do{ str <- between (char '"')
315 (char '"' <?> "end of string")
316 (many stringChar)
317 ; return (foldr (maybe id (:)) "" str)
318 }
319 <?> "literal string")
321 stringChar = do{ c <- stringLetter; return (Just c) }
322 <|> stringEscape
323 <?> "string character"
325 stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
327 stringEscape = do{ char '\\'
328 ; do{ escapeGap ; return Nothing }
329 <|> do{ escapeEmpty; return Nothing }
330 <|> do{ esc <- escapeCode; return (Just esc) }
331 }
333 escapeEmpty = char '&'
334 escapeGap = do{ many1 space
335 ; char '\\' <?> "end of string gap"
336 }
340 -- escape codes
341 escapeCode = charEsc <|> charNum <|> charAscii <|> charControl
342 <?> "escape code"
344 charControl = do{ char '^'
345 ; code <- upper
346 ; return (toEnum (fromEnum code - fromEnum 'A'))
347 }
349 charNum = do{ code <- decimal
350 <|> do{ char 'o'; number 8 octDigit }
351 <|> do{ char 'x'; number 16 hexDigit }
352 ; return (toEnum (fromInteger code))
353 }
355 charEsc = choice (map parseEsc escMap)
356 where
357 parseEsc (c,code) = do{ char c; return code }
359 charAscii = choice (map parseAscii asciiMap)
360 where
361 parseAscii (asc,code) = try (do{ string asc; return code })
364 -- escape code tables
365 escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
366 asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
368 ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",
369 "FS","GS","RS","US","SP"]
370 ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",
371 "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",
372 "CAN","SUB","ESC","DEL"]
374 ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',
375 '\EM','\FS','\GS','\RS','\US','\SP']
376 ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',
377 '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',
378 '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']
381 -----------------------------------------------------------
382 -- Numbers
383 -----------------------------------------------------------
384 naturalOrFloat = lexeme (natFloat) <?> "number"
386 float = lexeme floating <?> "float"
387 integer = lexeme int <?> "integer"
388 natural = lexeme nat <?> "natural"
391 -- floats
392 floating = do{ n <- decimal
393 ; fractExponent n
394 }
397 natFloat = do{ char '0'
398 ; zeroNumFloat
399 }
400 <|> decimalFloat
402 zeroNumFloat = do{ n <- hexadecimal <|> octal
403 ; return (Left n)
404 }
405 <|> decimalFloat
406 <|> fractFloat 0
407 <|> return (Left 0)
409 decimalFloat = do{ n <- decimal
410 ; option (Left n)
411 (fractFloat n)
412 }
414 fractFloat n = do{ f <- fractExponent n
415 ; return (Right f)
416 }
418 fractExponent n = do{ fract <- fraction
419 ; expo <- option 1.0 exponent'
420 ; return ((fromInteger n + fract)*expo)
421 }
422 <|>
423 do{ expo <- exponent'
424 ; return ((fromInteger n)*expo)
425 }
427 fraction = do{ char '.'
428 ; digits <- many1 digit <?> "fraction"
429 ; return (foldr op 0.0 digits)
430 }
431 <?> "fraction"
432 where
433 op d f = (f + fromIntegral (digitToInt d))/10.0
435 exponent' = do{ oneOf "eE"
436 ; f <- sign
437 ; e <- decimal <?> "exponent"
438 ; return (power (f e))
439 }
440 <?> "exponent"
441 where
442 power e | e < 0 = 1.0/power(-e)
443 | otherwise = fromInteger (10^e)
446 -- integers and naturals
447 int = do{ f <- lexeme sign
448 ; n <- nat
449 ; return (f n)
450 }
452 sign = (char '-' >> return negate)
453 <|> (char '+' >> return id)
454 <|> return id
456 nat = zeroNumber <|> decimal
458 zeroNumber = do{ char '0'
459 ; hexadecimal <|> octal <|> decimal <|> return 0
460 }
461 <?> ""
463 decimal = number 10 digit
464 hexadecimal = do{ oneOf "xX"; number 16 hexDigit }
465 octal = do{ oneOf "oO"; number 8 octDigit }
467 number base baseDigit
468 = do{ digits <- many1 baseDigit
469 ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits
470 ; seq n (return n)
471 }
473 -----------------------------------------------------------
474 -- Operators & reserved ops
475 -----------------------------------------------------------
476 reservedOp name =
477 lexeme $ try $
478 do{ string name
479 ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
480 }
482 operator =
483 lexeme $ try $
484 do{ name <- oper
485 ; if (isReservedOp name)
486 then unexpected ("reserved operator " ++ show name)
487 else return name
488 }
490 oper =
491 do{ c <- (opStart languageDef)
492 ; cs <- many (opLetter languageDef)
493 ; return (c:cs)
494 }
495 <?> "operator"
497 isReservedOp name =
498 isReserved (sort (reservedOpNames languageDef)) name
501 -----------------------------------------------------------
502 -- Identifiers & Reserved words
503 -----------------------------------------------------------
504 reserved name =
505 lexeme $ try $
506 do{ caseString name
507 ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
508 }
510 caseString name
511 | caseSensitive languageDef = string name
512 | otherwise = do{ walk name; return name }
513 where
514 walk [] = return ()
515 walk (c:cs) = do{ caseChar c <?> msg; walk cs }
517 caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)
518 | otherwise = char c
520 msg = show name
523 identifier =
524 lexeme $ try $
525 do{ name <- ident
526 ; if (isReservedName name)
527 then unexpected ("reserved word " ++ show name)
528 else return name
529 }
532 ident
533 = do{ c <- identStart languageDef
534 ; cs <- many (identLetter languageDef)
535 ; return (c:cs)
536 }
537 <?> "identifier"
539 isReservedName name
540 = isReserved theReservedNames caseName
541 where
542 caseName | caseSensitive languageDef = name
543 | otherwise = map toLower name
546 isReserved names name
547 = scan names
548 where
549 scan [] = False
550 scan (r:rs) = case (compare r name) of
551 LT -> scan rs
552 EQ -> True
553 GT -> False
555 theReservedNames
556 | caseSensitive languageDef = sortedNames
557 | otherwise = map (map toLower) sortedNames
558 where
559 sortedNames = sort (reservedNames languageDef)
563 -----------------------------------------------------------
564 -- White space & symbols
565 -----------------------------------------------------------
566 symbol name
567 = lexeme (string name)
569 lexeme p
570 = do{ x <- p; whiteSpace; return x }
572 --whiteSpace
573 whiteSpace = lexWS