git.iko.soy/Idris-dev
on 496cf41 help sign in
Idris-dev/src/Core/CoreParser.hs
574 lines 20 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4 idrisLexer, maybeWithNS, pDocComment) 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",
35 "where", "with", "syntax", "proof", "postulate",
36 "using", "namespace", "class", "instance",
37 "public", "private", "abstract",
38 "Int", "Integer", "Float", "Char", "String", "Ptr",
39 "Word8", "Word16"]
40 }
42iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
43iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
44-- <|> letter
46idrisLexer :: TokenParser a
47idrisLexer = idrisMakeTokenParser idrisDef
49lexer = idrisLexer
51-- Taken from Parsec source code
52lexWS = do i <- getInput
53 skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
54 where
56 simpleSpace = skipMany1 (satisfy isSpace)
57 oneLineComment = do try (do string ("--")
58 skipMany simpleSpace
59 satisfy (\x -> x /= '|' && x /= '^'))
60 skipMany (satisfy (/= '\n'))
61 return ()
62 multiLineComment = do try (do string "{-"
63 skipMany simpleSpace
64 satisfy (\x -> x /= '|' && x /= '^'))
65 inCommentMulti
67 inCommentMulti
68 = do{ try (string "-}") ; return () }
69 <|> do{ multiLineComment ; inCommentMulti }
70 <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }
71 <|> do{ oneOf startEnd ; inCommentMulti }
72 <?> "end of comment"
73 where
74 startEnd = "-}{"
76whiteSpace= PTok.whiteSpace lexer
77lexeme = PTok.lexeme lexer
78symbol = PTok.symbol lexer
79natural = PTok.natural lexer
80parens = PTok.parens lexer
81semi = PTok.semi lexer
82comma = PTok.comma lexer
83identifier= PTok.identifier lexer
84reserved = PTok.reserved lexer
85operator = PTok.operator lexer
86reservedOp= PTok.reservedOp lexer
87strlit = PTok.stringLiteral lexer
88lchar = lexeme.char
90type CParser a = GenParser Char a
92parseFile = runParser pTestFile () "(input)"
93parseDef = runParser pDef () "(input)"
94parseTerm = runParser pTerm () "(input)"
96pTestFile :: CParser a RProgram
97pTestFile = do p <- many1 pDef ; eof
98 return p
100iName :: [String] -> CParser a Name
101iName bad = maybeWithNS identifier False bad
103-- Enhances a given parser to accept an optional namespace. All possible
104-- namespace prefixes are tried in ascending / descending order, and
105-- identifiers of a given list fail.
106maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
107maybeWithNS parser ascend bad = do
108 i <- option "" (lookAhead identifier)
109 when (i `elem` bad) $ fail "Reserved identifier"
110 let transf = if ascend then id else reverse
111 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
112 return $ mkName (x, xs)
113 where
114 parserNoNS = do x <- parser; return (x, "")
115 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
116 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
118-- List of all initial segments in ascending order of a list. Every such
119-- initial segment ends right before an element satisfying the given
120-- condition.
121initsEndAt :: (a -> Bool) -> [a] -> [[a]]
122initsEndAt p [] = []
123initsEndAt p (x:xs) | p x = [] : x_inits_xs
124 | otherwise = x_inits_xs
125 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
127-- Create a `Name' from a pair of strings representing a base name and its
128-- namespace.
129mkName :: (String, String) -> Name
130mkName (n, "") = UN n
131mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
132 where parseNS x = case span (/= '.') x of
133 (x, "") -> [x]
134 (x, '.':y) -> x : parseNS y
136pDocComment :: Char -> CParser a String
137pDocComment c
138 = try (do string ("--")
139 option ' ' (lchar ' ')
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 option ' ' (lchar ' ')
149 char c
150 skipMany simpleSpace
151 i <- getInput
152 -- read to '-}'
153 let (doc, rest) = spanComment "" i
154 setInput rest
155 whiteSpace
156 return doc)
157 where spanComment acc ('-':'}':xs) = (reverse acc, xs)
158 spanComment acc (x:xs) = spanComment (x : acc) xs
159 spanComment acc [] = (acc, [])
160 simpleSpace = skipMany1 (satisfy isSpace)
162pDef :: CParser a (Name, RDef)
163pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
164 lchar '='
165 tm <- pTerm
166 lchar ';'
167 return (x, RFunction (RawFun ty tm)))
168 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
169 return (x, RConst ty)
170 <|> do (x, d) <- pData; lchar ';'
171 return (x, RData d)
173app :: CParser a (Raw -> Raw -> Raw)
174app = do whiteSpace ; return RApp
176arrow :: CParser a (Raw -> Raw -> Raw)
177arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
179pTerm :: CParser a Raw
180pTerm = try (do chainl1 pNoApp app)
181 <|> pNoApp
183pNoApp :: CParser a Raw
184pNoApp = try (chainr1 pExp arrow)
185 <|> pExp
186pExp :: CParser a Raw
187pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
188 symbol "=>";
189 sc <- pTerm
190 return (RBind x (Lam ty) sc)
191 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
192 lchar '.';
193 sc <- pTerm
194 return (RBind x (Hole ty) sc))
195 <|> try (do lchar '(';
196 x <- iName []; lchar ':'; ty <- pTerm
197 lchar ')';
198 symbol "->";
199 sc <- pTerm
200 return (RBind x (Pi ty) sc))
201 <|> try (do lchar '(';
202 t <- pTerm
203 lchar ')'
204 return t)
205 <|> try (do symbol "??";
206 x <- iName []; lchar ':'; ty <- pTerm
207 lchar '=';
208 val <- pTerm
209 sc <- pTerm
210 return (RBind x (Guess ty val) sc))
211 <|> try (do reserved "let";
212 x <- iName []; lchar ':'; ty <- pTerm
213 lchar '=';
214 val <- pTerm
215 reserved "in";
216 sc <- pTerm
217 return (RBind x (Let ty val) sc))
218 <|> try (do lchar '_';
219 x <- iName []; lchar ':'; ty <- pTerm
220 lchar '.';
221 sc <- pTerm
222 return (RBind x (PVar ty) sc))
223 <|> try (do reserved "Type"
224 return RType)
225 <|> try (do x <- iName []
226 return (Var x))
228pData :: CParser a (Name, RawDatatype)
229pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
230 cs <- many pConstructor
231 return (x, RDatatype x ty cs)
233pConstructor :: CParser a (Name, Raw)
234pConstructor = do lchar '|'
235 c <- iName []; lchar ':'; ty <- pTerm
236 return (c, ty)
238------ borrowed from Parsec
239-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
241idrisMakeTokenParser languageDef
242 = PTok.TokenParser{
243 PTok.identifier = identifier
244 , PTok.reserved = reserved
245 , PTok.operator = operator
246 , PTok.reservedOp = reservedOp
248 , PTok.charLiteral = charLiteral
249 , PTok.stringLiteral = stringLiteral
250 , PTok.natural = natural
251 , PTok.integer = integer
252 , PTok.float = float
253 , PTok.naturalOrFloat = naturalOrFloat
254 , PTok.decimal = decimal
255 , PTok.hexadecimal = hexadecimal
256 , PTok.octal = octal
258 , PTok.symbol = symbol
259 , PTok.lexeme = lexeme
260 , PTok.whiteSpace = lexWS
262 , PTok.parens = parens
263 , PTok.braces = braces
264 , PTok.angles = angles
265 , PTok.brackets = brackets
266 , PTok.squares = brackets
267 , PTok.semi = semi
268 , PTok.comma = comma
269 , PTok.colon = colon
270 , PTok.dot = dot
271 , PTok.semiSep = semiSep
272 , PTok.semiSep1 = semiSep1
273 , PTok.commaSep = commaSep
274 , PTok.commaSep1 = commaSep1
275 }
276 where
278 -----------------------------------------------------------
279 -- Bracketing
280 -----------------------------------------------------------
281 parens p = between (symbol "(") (symbol ")") p
282 braces p = between (symbol "{") (symbol "}") p
283 angles p = between (symbol "<") (symbol ">") p
284 brackets p = between (symbol "[") (symbol "]") p
286 semi = symbol ";"
287 comma = symbol ","
288 dot = symbol "."
289 colon = symbol ":"
291 commaSep p = sepBy p comma
292 semiSep p = sepBy p semi
294 commaSep1 p = sepBy1 p comma
295 semiSep1 p = sepBy1 p semi
298 -----------------------------------------------------------
299 -- Chars & Strings
300 -----------------------------------------------------------
301 charLiteral = lexeme (between (char '\'')
302 (char '\'' <?> "end of character")
303 characterChar )
304 <?> "character"
306 characterChar = charLetter <|> charEscape
307 <?> "literal character"
309 charEscape = do{ char '\\'; escapeCode }
310 charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
314 stringLiteral = lexeme (
315 do{ str <- between (char '"')
316 (char '"' <?> "end of string")
317 (many stringChar)
318 ; return (foldr (maybe id (:)) "" str)
319 }
320 <?> "literal string")
322 stringChar = do{ c <- stringLetter; return (Just c) }
323 <|> stringEscape
324 <?> "string character"
326 stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
328 stringEscape = do{ char '\\'
329 ; do{ escapeGap ; return Nothing }
330 <|> do{ escapeEmpty; return Nothing }
331 <|> do{ esc <- escapeCode; return (Just esc) }
332 }
334 escapeEmpty = char '&'
335 escapeGap = do{ many1 space
336 ; char '\\' <?> "end of string gap"
337 }
341 -- escape codes
342 escapeCode = charEsc <|> charNum <|> charAscii <|> charControl
343 <?> "escape code"
345 charControl = do{ char '^'
346 ; code <- upper
347 ; return (toEnum (fromEnum code - fromEnum 'A'))
348 }
350 charNum = do{ code <- decimal
351 <|> do{ char 'o'; number 8 octDigit }
352 <|> do{ char 'x'; number 16 hexDigit }
353 ; return (toEnum (fromInteger code))
354 }
356 charEsc = choice (map parseEsc escMap)
357 where
358 parseEsc (c,code) = do{ char c; return code }
360 charAscii = choice (map parseAscii asciiMap)
361 where
362 parseAscii (asc,code) = try (do{ string asc; return code })
365 -- escape code tables
366 escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
367 asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
369 ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",
370 "FS","GS","RS","US","SP"]
371 ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",
372 "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",
373 "CAN","SUB","ESC","DEL"]
375 ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',
376 '\EM','\FS','\GS','\RS','\US','\SP']
377 ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',
378 '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',
379 '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']
382 -----------------------------------------------------------
383 -- Numbers
384 -----------------------------------------------------------
385 naturalOrFloat = lexeme (natFloat) <?> "number"
387 float = lexeme floating <?> "float"
388 integer = lexeme int <?> "integer"
389 natural = lexeme nat <?> "natural"
392 -- floats
393 floating = do{ n <- decimal
394 ; fractExponent n
395 }
398 natFloat = do{ char '0'
399 ; zeroNumFloat
400 }
401 <|> decimalFloat
403 zeroNumFloat = do{ n <- hexadecimal <|> octal
404 ; return (Left n)
405 }
406 <|> decimalFloat
407 <|> fractFloat 0
408 <|> return (Left 0)
410 decimalFloat = do{ n <- decimal
411 ; option (Left n)
412 (fractFloat n)
413 }
415 fractFloat n = do{ f <- fractExponent n
416 ; return (Right f)
417 }
419 fractExponent n = do{ fract <- fraction
420 ; expo <- option 1.0 exponent'
421 ; return ((fromInteger n + fract)*expo)
422 }
423 <|>
424 do{ expo <- exponent'
425 ; return ((fromInteger n)*expo)
426 }
428 fraction = do{ char '.'
429 ; digits <- many1 digit <?> "fraction"
430 ; return (foldr op 0.0 digits)
431 }
432 <?> "fraction"
433 where
434 op d f = (f + fromIntegral (digitToInt d))/10.0
436 exponent' = do{ oneOf "eE"
437 ; f <- sign
438 ; e <- decimal <?> "exponent"
439 ; return (power (f e))
440 }
441 <?> "exponent"
442 where
443 power e | e < 0 = 1.0/power(-e)
444 | otherwise = fromInteger (10^e)
447 -- integers and naturals
448 int = do{ f <- lexeme sign
449 ; n <- nat
450 ; return (f n)
451 }
453 sign = (char '-' >> return negate)
454 <|> (char '+' >> return id)
455 <|> return id
457 nat = zeroNumber <|> decimal
459 zeroNumber = do{ char '0'
460 ; hexadecimal <|> octal <|> decimal <|> return 0
461 }
462 <?> ""
464 decimal = number 10 digit
465 hexadecimal = do{ oneOf "xX"; number 16 hexDigit }
466 octal = do{ oneOf "oO"; number 8 octDigit }
468 number base baseDigit
469 = do{ digits <- many1 baseDigit
470 ; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits
471 ; seq n (return n)
472 }
474 -----------------------------------------------------------
475 -- Operators & reserved ops
476 -----------------------------------------------------------
477 reservedOp name =
478 lexeme $ try $
479 do{ string name
480 ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
481 }
483 operator =
484 lexeme $ try $
485 do{ name <- oper
486 ; if (isReservedOp name)
487 then unexpected ("reserved operator " ++ show name)
488 else return name
489 }
491 oper =
492 do{ c <- (opStart languageDef)
493 ; cs <- many (opLetter languageDef)
494 ; return (c:cs)
495 }
496 <?> "operator"
498 isReservedOp name =
499 isReserved (sort (reservedOpNames languageDef)) name
502 -----------------------------------------------------------
503 -- Identifiers & Reserved words
504 -----------------------------------------------------------
505 reserved name =
506 lexeme $ try $
507 do{ caseString name
508 ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
509 }
511 caseString name
512 | caseSensitive languageDef = string name
513 | otherwise = do{ walk name; return name }
514 where
515 walk [] = return ()
516 walk (c:cs) = do{ caseChar c <?> msg; walk cs }
518 caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)
519 | otherwise = char c
521 msg = show name
524 identifier =
525 lexeme $ try $
526 do{ name <- ident
527 ; if (isReservedName name)
528 then unexpected ("reserved word " ++ show name)
529 else return name
530 }
533 ident
534 = do{ c <- identStart languageDef
535 ; cs <- many (identLetter languageDef)
536 ; return (c:cs)
537 }
538 <?> "identifier"
540 isReservedName name
541 = isReserved theReservedNames caseName
542 where
543 caseName | caseSensitive languageDef = name
544 | otherwise = map toLower name
547 isReserved names name
548 = scan names
549 where
550 scan [] = False
551 scan (r:rs) = case (compare r name) of
552 LT -> scan rs
553 EQ -> True
554 GT -> False
556 theReservedNames
557 | caseSensitive languageDef = sortedNames
558 | otherwise = map (map toLower) sortedNames
559 where
560 sortedNames = sort (reservedNames languageDef)
564 -----------------------------------------------------------
565 -- White space & symbols
566 -----------------------------------------------------------
567 symbol name
568 = lexeme (string name)
570 lexeme p
571 = do{ x <- p; whiteSpace; return x }
573 --whiteSpace
574 whiteSpace = lexWS