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