git.iko.soy/Idris-dev
on 436bf95 help sign in
Idris-dev/src/Core/CoreParser.hs
576 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 =
61 try (void $ string "--\n") <|>
62 do try (do string "--"
63 satisfy (\x -> x /= '|' && x /= '^'))
64 skipMany (satisfy (/= '\n'))
65 multiLineComment =
66 try (void $ string "{--}") <|>
67 do try (do string "{-"
68 satisfy (\x -> x /= '|' && x /= '^'))
69 inCommentMulti
71 inCommentMulti
72 = do{ try (string "-}") ; return () }
73 <|> do{ multiLineComment ; inCommentMulti }
74 <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }
75 <|> do{ oneOf startEnd ; inCommentMulti }
76 <?> "end of comment"
77 where
78 startEnd = "-}{"
80whiteSpace= PTok.whiteSpace lexer
81lexeme = PTok.lexeme lexer
82symbol = PTok.symbol lexer
83natural = PTok.natural lexer
84parens = PTok.parens lexer
85semi = PTok.semi lexer
86comma = PTok.comma lexer
87identifier= PTok.identifier lexer
88reserved = PTok.reserved lexer
89operator = PTok.operator lexer
90reservedOp= PTok.reservedOp lexer
91strlit = PTok.stringLiteral lexer
92lchar = lexeme.char
94type CParser a = GenParser Char a
96parseFile = runParser pTestFile () "(input)"
97parseDef = runParser pDef () "(input)"
98parseTerm = runParser pTerm () "(input)"
100pTestFile :: CParser a RProgram
101pTestFile = do p <- many1 pDef ; eof
102 return p
104iName :: [String] -> CParser a Name
105iName bad = maybeWithNS identifier False bad
107-- Enhances a given parser to accept an optional namespace. All possible
108-- namespace prefixes are tried in ascending / descending order, and
109-- identifiers of a given list fail.
110maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
111maybeWithNS parser ascend bad = do
112 i <- option "" (lookAhead identifier)
113 when (i `elem` bad) $ fail "Reserved identifier"
114 let transf = if ascend then id else reverse
115 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
116 return $ mkName (x, xs)
117 where
118 parserNoNS = do x <- parser; return (x, "")
119 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
120 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
122-- List of all initial segments in ascending order of a list. Every such
123-- initial segment ends right before an element satisfying the given
124-- condition.
125initsEndAt :: (a -> Bool) -> [a] -> [[a]]
126initsEndAt p [] = []
127initsEndAt p (x:xs) | p x = [] : x_inits_xs
128 | otherwise = x_inits_xs
129 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
131-- Create a `Name' from a pair of strings representing a base name and its
132-- namespace.
133mkName :: (String, String) -> Name
134mkName (n, "") = UN n
135mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
136 where parseNS x = case span (/= '.') x of
137 (x, "") -> [x]
138 (x, '.':y) -> x : parseNS y
140pDocComment :: Char -> CParser a String
141pDocComment c
142 = try (do string ("--")
143 char c
144 skipMany simpleSpace
145 i <- getInput
146 let (doc, rest) = span (/='\n') i
147 setInput rest
148 whiteSpace
149 return doc)
150 <|> try (do string ("{-")
151 char c
152 skipMany simpleSpace
153 i <- getInput
154 -- read to '-}'
155 let (doc, rest) = spanComment "" i
156 setInput rest
157 whiteSpace
158 return doc)
159 where spanComment acc ('-':'}':xs) = (reverse acc, xs)
160 spanComment acc (x:xs) = spanComment (x : acc) xs
161 spanComment acc [] = (acc, [])
162 simpleSpace = skipMany1 (satisfy isSpace)
164pDef :: CParser a (Name, RDef)
165pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
166 lchar '='
167 tm <- pTerm
168 lchar ';'
169 return (x, RFunction (RawFun ty tm)))
170 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
171 return (x, RConst ty)
172 <|> do (x, d) <- pData; lchar ';'
173 return (x, RData d)
175app :: CParser a (Raw -> Raw -> Raw)
176app = do whiteSpace ; return RApp
178arrow :: CParser a (Raw -> Raw -> Raw)
179arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
181pTerm :: CParser a Raw
182pTerm = try (do chainl1 pNoApp app)
183 <|> pNoApp
185pNoApp :: CParser a Raw
186pNoApp = try (chainr1 pExp arrow)
187 <|> pExp
188pExp :: CParser a Raw
189pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
190 symbol "=>";
191 sc <- pTerm
192 return (RBind x (Lam ty) sc)
193 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
194 lchar '.';
195 sc <- pTerm
196 return (RBind x (Hole ty) sc))
197 <|> try (do lchar '(';
198 x <- iName []; lchar ':'; ty <- pTerm
199 lchar ')';
200 symbol "->";
201 sc <- pTerm
202 return (RBind x (Pi ty) sc))
203 <|> try (do lchar '(';
204 t <- pTerm
205 lchar ')'
206 return t)
207 <|> try (do symbol "??";
208 x <- iName []; lchar ':'; ty <- pTerm
209 lchar '=';
210 val <- pTerm
211 sc <- pTerm
212 return (RBind x (Guess ty val) sc))
213 <|> try (do reserved "let";
214 x <- iName []; lchar ':'; ty <- pTerm
215 lchar '=';
216 val <- pTerm
217 reserved "in";
218 sc <- pTerm
219 return (RBind x (Let ty val) sc))
220 <|> try (do lchar '_';
221 x <- iName []; lchar ':'; ty <- pTerm
222 lchar '.';
223 sc <- pTerm
224 return (RBind x (PVar ty) sc))
225 <|> try (do reserved "Type"
226 return RType)
227 <|> try (do x <- iName []
228 return (Var x))
230pData :: CParser a (Name, RawDatatype)
231pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
232 cs <- many pConstructor
233 return (x, RDatatype x ty cs)
235pConstructor :: CParser a (Name, Raw)
236pConstructor = do lchar '|'
237 c <- iName []; lchar ':'; ty <- pTerm
238 return (c, ty)
240------ borrowed from Parsec
241-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
243idrisMakeTokenParser languageDef
244 = PTok.TokenParser{
245 PTok.identifier = identifier
246 , PTok.reserved = reserved
247 , PTok.operator = operator
248 , PTok.reservedOp = reservedOp
250 , PTok.charLiteral = charLiteral
251 , PTok.stringLiteral = stringLiteral
252 , PTok.natural = natural
253 , PTok.integer = integer
254 , PTok.float = float
255 , PTok.naturalOrFloat = naturalOrFloat
256 , PTok.decimal = decimal
257 , PTok.hexadecimal = hexadecimal
258 , PTok.octal = octal
260 , PTok.symbol = symbol
261 , PTok.lexeme = lexeme
262 , PTok.whiteSpace = lexWS
264 , PTok.parens = parens
265 , PTok.braces = braces
266 , PTok.angles = angles
267 , PTok.brackets = brackets
268 , PTok.squares = brackets
269 , PTok.semi = semi
270 , PTok.comma = comma
271 , PTok.colon = colon
272 , PTok.dot = dot
273 , PTok.semiSep = semiSep
274 , PTok.semiSep1 = semiSep1
275 , PTok.commaSep = commaSep
276 , PTok.commaSep1 = commaSep1
277 }
278 where
280 -----------------------------------------------------------
281 -- Bracketing
282 -----------------------------------------------------------
283 parens p = between (symbol "(") (symbol ")") p
284 braces p = between (symbol "{") (symbol "}") p
285 angles p = between (symbol "<") (symbol ">") p
286 brackets p = between (symbol "[") (symbol "]") p
288 semi = symbol ";"
289 comma = symbol ","
290 dot = symbol "."
291 colon = symbol ":"
293 commaSep p = sepBy p comma
294 semiSep p = sepBy p semi
296 commaSep1 p = sepBy1 p comma
297 semiSep1 p = sepBy1 p semi
300 -----------------------------------------------------------
301 -- Chars & Strings
302 -----------------------------------------------------------
303 charLiteral = lexeme (between (char '\'')
304 (char '\'' <?> "end of character")
305 characterChar )
306 <?> "character"
308 characterChar = charLetter <|> charEscape
309 <?> "literal character"
311 charEscape = do{ char '\\'; escapeCode }
312 charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
316 stringLiteral = lexeme (
317 do{ str <- between (char '"')
318 (char '"' <?> "end of string")
319 (many stringChar)
320 ; return (foldr (maybe id (:)) "" str)
321 }
322 <?> "literal string")
324 stringChar = do{ c <- stringLetter; return (Just c) }
325 <|> stringEscape
326 <?> "string character"
328 stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
330 stringEscape = do{ char '\\'
331 ; do{ escapeGap ; return Nothing }
332 <|> do{ escapeEmpty; return Nothing }
333 <|> do{ esc <- escapeCode; return (Just esc) }
334 }
336 escapeEmpty = char '&'
337 escapeGap = do{ many1 space
338 ; char '\\' <?> "end of string gap"
339 }
343 -- escape codes
344 escapeCode = charEsc <|> charNum <|> charAscii <|> charControl
345 <?> "escape code"
347 charControl = do{ char '^'
348 ; code <- upper
349 ; return (toEnum (fromEnum code - fromEnum 'A'))
350 }
352 charNum = do{ code <- decimal
353 <|> do{ char 'o'; number 8 octDigit }
354 <|> do{ char 'x'; number 16 hexDigit }
355 ; return (toEnum (fromInteger code))
356 }
358 charEsc = choice (map parseEsc escMap)
359 where
360 parseEsc (c,code) = do{ char c; return code }
362 charAscii = choice (map parseAscii asciiMap)
363 where
364 parseAscii (asc,code) = try (do{ string asc; return code })
367 -- escape code tables
368 escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
369 asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
371 ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",
372 "FS","GS","RS","US","SP"]
373 ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",
374 "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",
375 "CAN","SUB","ESC","DEL"]
377 ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',
378 '\EM','\FS','\GS','\RS','\US','\SP']
379 ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',
380 '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',
381 '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']
384 -----------------------------------------------------------
385 -- Numbers
386 -----------------------------------------------------------
387 naturalOrFloat = lexeme (natFloat) <?> "number"
389 float = lexeme floating <?> "float"
390 integer = lexeme int <?> "integer"
391 natural = lexeme nat <?> "natural"
394 -- floats
395 floating = do{ n <- decimal
396 ; fractExponent n
397 }
400 natFloat = do{ char '0'
401 ; zeroNumFloat
402 }
403 <|> decimalFloat
405 zeroNumFloat = do{ n <- hexadecimal <|> octal
406 ; return (Left n)
407 }
408 <|> decimalFloat
409 <|> fractFloat 0
410 <|> return (Left 0)
412 decimalFloat = do{ n <- decimal
413 ; option (Left n)
414 (fractFloat n)
415 }
417 fractFloat n = do{ f <- fractExponent n
418 ; return (Right f)
419 }
421 fractExponent n = do{ fract <- fraction
422 ; expo <- option 1.0 exponent'
423 ; return ((fromInteger n + fract)*expo)
424 }
425 <|>
426 do{ expo <- exponent'
427 ; return ((fromInteger n)*expo)
428 }
430 fraction = do{ char '.'
431 ; digits <- many1 digit <?> "fraction"
432 ; return (foldr op 0.0 digits)
433 }
434 <?> "fraction"
435 where
436 op d f = (f + fromIntegral (digitToInt d))/10.0
438 exponent' = do{ oneOf "eE"
439 ; f <- sign
440 ; e <- decimal <?> "exponent"
441 ; return (power (f e))
442 }
443 <?> "exponent"
444 where
445 power e | e < 0 = 1.0/power(-e)
446 | otherwise = fromInteger (10^e)
449 -- integers and naturals
450 int = do{ f <- lexeme sign
451 ; n <- nat
452 ; return (f n)
453 }
455 sign = (char '-' >> return negate)
456 <|> (char '+' >> return id)
457 <|> return id
459 nat = zeroNumber <|> decimal
461 zeroNumber = do{ char '0'
462 ; hexadecimal <|> octal <|> decimal <|> return 0
463 }
464 <?> ""
466 decimal = number 10 digit
467 hexadecimal = do{ oneOf "xX"; number 16 hexDigit }
468 octal = do{ oneOf "oO"; number 8 octDigit }
470 number base baseDigit
471 = do{ digits <- many1 baseDigit
472 ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits
473 ; seq n (return n)
474 }
476 -----------------------------------------------------------
477 -- Operators & reserved ops
478 -----------------------------------------------------------
479 reservedOp name =
480 lexeme $ try $
481 do{ string name
482 ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
483 }
485 operator =
486 lexeme $ try $
487 do{ name <- oper
488 ; if (isReservedOp name)
489 then unexpected ("reserved operator " ++ show name)
490 else return name
491 }
493 oper =
494 do{ c <- (opStart languageDef)
495 ; cs <- many (opLetter languageDef)
496 ; return (c:cs)
497 }
498 <?> "operator"
500 isReservedOp name =
501 isReserved (sort (reservedOpNames languageDef)) name
504 -----------------------------------------------------------
505 -- Identifiers & Reserved words
506 -----------------------------------------------------------
507 reserved name =
508 lexeme $ try $
509 do{ caseString name
510 ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
511 }
513 caseString name
514 | caseSensitive languageDef = string name
515 | otherwise = do{ walk name; return name }
516 where
517 walk [] = return ()
518 walk (c:cs) = do{ caseChar c <?> msg; walk cs }
520 caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)
521 | otherwise = char c
523 msg = show name
526 identifier =
527 lexeme $ try $
528 do{ name <- ident
529 ; if (isReservedName name)
530 then unexpected ("reserved word " ++ show name)
531 else return name
532 }
535 ident
536 = do{ c <- identStart languageDef
537 ; cs <- many (identLetter languageDef)
538 ; return (c:cs)
539 }
540 <?> "identifier"
542 isReservedName name
543 = isReserved theReservedNames caseName
544 where
545 caseName | caseSensitive languageDef = name
546 | otherwise = map toLower name
549 isReserved names name
550 = scan names
551 where
552 scan [] = False
553 scan (r:rs) = case (compare r name) of
554 LT -> scan rs
555 EQ -> True
556 GT -> False
558 theReservedNames
559 | caseSensitive languageDef = sortedNames
560 | otherwise = map (map toLower) sortedNames
561 where
562 sortedNames = sort (reservedNames languageDef)
566 -----------------------------------------------------------
567 -- White space & symbols
568 -----------------------------------------------------------
569 symbol name
570 = lexeme (string name)
572 lexeme p
573 = do{ x <- p; whiteSpace; return x }
575 --whiteSpace
576 whiteSpace = lexWS