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