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