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