@@ -8,10 +8,15 @@ import Core.TT
88import Text.ParserCombinators.Parsec
99import Text.ParserCombinators.Parsec.Expr
1010import Text.ParserCombinators.Parsec.Language
11+import Text.ParserCombinators.Parsec.Prim
12+import Text.ParserCombinators.Parsec.Char
13+import Text.ParserCombinators.Parsec.Combinator
1114import qualified Text.ParserCombinators.Parsec.Token as PTok
1215
1316import Control.Monad.State
17+import Control.Monad.Identity
1418import Data.Char
19+import Data.List
1520import Debug.Trace
1621
1722type TokenParser a = PTok.TokenParser a
@@ -38,21 +43,22 @@ iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
3843-- <|> letter
3944
4045idrisLexer :: TokenParser a
41−idrisLexer = (PTok.makeTokenParser idrisDef) { PTok.whiteSpace = lexWS }
46+idrisLexer = idrisMakeTokenParser idrisDef
4247
4348lexer = idrisLexer
4449
4550-- Taken from Parsec source code
46−lexWS = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
51+lexWS = do i <- getInput
52+ skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
4753 where
4854
4955 simpleSpace = skipMany1 (satisfy isSpace)
50− oneLineComment = do try (string ("--"))
51− satisfy (/= '|')
56+ oneLineComment = do try (do string ("--")
57+ satisfy (\x -> x /= '|' && x /= '^'))
5258 skipMany (satisfy (/= '\n'))
5359 return ()
54− multiLineComment = do try (string "{-")
55− satisfy (/= '|')
60+ multiLineComment = do try (do string "{-"
61+ satisfy (\x -> x /= '|' && x /= '^'))
5662 inCommentMulti
5763
5864 inCommentMulti
@@ -75,6 +81,7 @@ identifier= PTok.identifier lexer
7581reserved = PTok.reserved lexer
7682operator = PTok.operator lexer
7783reservedOp= PTok.reservedOp lexer
84+strlit = PTok.stringLiteral lexer
7885lchar = lexeme.char
7986
8087type CParser a = GenParser Char a
@@ -124,13 +131,23 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
124131 (x, '.':y) -> x : parseNS y
125132
126133pDocComment :: Char -> CParser a String
127−pDocComment c
128− = do string "--"
129− char c
130− i <- getInput
131− let (doc, rest) = span (/='\n') i
132− setInput rest
133− return doc
134+pDocComment 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, [])
134151
135152pDef :: CParser a (Name, RDef)
136153pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
@@ -208,3 +225,340 @@ pConstructor = do lchar '|'
208225 c <- iName []; lchar ':'; ty <- pTerm
209226 return (c, ty)
210227
228+------ borrowed from Parsec
229+-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
230+
231+idrisMakeTokenParser languageDef
232+ = PTok.TokenParser{
233+ PTok.identifier = identifier
234+ , PTok.reserved = reserved
235+ , PTok.operator = operator
236+ , PTok.reservedOp = reservedOp
237+
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
247+
248+ , PTok.symbol = symbol
249+ , PTok.lexeme = lexeme
250+ , PTok.whiteSpace = lexWS
251+
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
267+
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
275+
276+ semi = symbol ";"
277+ comma = symbol ","
278+ dot = symbol "."
279+ colon = symbol ":"
280+
281+ commaSep p = sepBy p comma
282+ semiSep p = sepBy p semi
283+
284+ commaSep1 p = sepBy1 p comma
285+ semiSep1 p = sepBy1 p semi
286+
287+
288+ -----------------------------------------------------------
289+ -- Chars & Strings
290+ -----------------------------------------------------------
291+ charLiteral = lexeme (between (char '\'')
292+ (char '\'' <?> "end of character")
293+ characterChar )
294+ <?> "character"
295+
296+ characterChar = charLetter <|> charEscape
297+ <?> "literal character"
298+
299+ charEscape = do{ char '\\'; escapeCode }
300+ charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))
301+
302+
303+
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")
311+
312+ stringChar = do{ c <- stringLetter; return (Just c) }
313+ <|> stringEscape
314+ <?> "string character"
315+
316+ stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))
317+
318+ stringEscape = do{ char '\\'
319+ ; do{ escapeGap ; return Nothing }
320+ <|> do{ escapeEmpty; return Nothing }
321+ <|> do{ esc <- escapeCode; return (Just esc) }
322+ }
323+
324+ escapeEmpty = char '&'
325+ escapeGap = do{ many1 space
326+ ; char '\\' <?> "end of string gap"
327+ }
328+
329+
330+
331+ -- escape codes
332+ escapeCode = charEsc <|> charNum <|> charAscii <|> charControl
333+ <?> "escape code"
334+
335+ charControl = do{ char '^'
336+ ; code <- upper
337+ ; return (toEnum (fromEnum code - fromEnum 'A'))
338+ }
339+
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+ }
345+
346+ charEsc = choice (map parseEsc escMap)
347+ where
348+ parseEsc (c,code) = do{ char c; return code }
349+
350+ charAscii = choice (map parseAscii asciiMap)
351+ where
352+ parseAscii (asc,code) = try (do{ string asc; return code })
353+
354+
355+ -- escape code tables
356+ escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")
357+ asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)
358+
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"]
364+
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']
370+
371+
372+ -----------------------------------------------------------
373+ -- Numbers
374+ -----------------------------------------------------------
375+ naturalOrFloat = lexeme (natFloat) <?> "number"
376+
377+ float = lexeme floating <?> "float"
378+ integer = lexeme int <?> "integer"
379+ natural = lexeme nat <?> "natural"
380+
381+
382+ -- floats
383+ floating = do{ n <- decimal
384+ ; fractExponent n
385+ }
386+
387+
388+ natFloat = do{ char '0'
389+ ; zeroNumFloat
390+ }
391+ <|> decimalFloat
392+
393+ zeroNumFloat = do{ n <- hexadecimal <|> octal
394+ ; return (Left n)
395+ }
396+ <|> decimalFloat
397+ <|> fractFloat 0
398+ <|> return (Left 0)
399+
400+ decimalFloat = do{ n <- decimal
401+ ; option (Left n)
402+ (fractFloat n)
403+ }
404+
405+ fractFloat n = do{ f <- fractExponent n
406+ ; return (Right f)
407+ }
408+
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+ }
417+
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
425+
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)
435+
436+
437+ -- integers and naturals
438+ int = do{ f <- lexeme sign
439+ ; n <- nat
440+ ; return (f n)
441+ }
442+
443+ sign = (char '-' >> return negate)
444+ <|> (char '+' >> return id)
445+ <|> return id
446+
447+ nat = zeroNumber <|> decimal
448+
449+ zeroNumber = do{ char '0'
450+ ; hexadecimal <|> octal <|> decimal <|> return 0
451+ }
452+ <?> ""
453+
454+ decimal = number 10 digit
455+ hexadecimal = do{ oneOf "xX"; number 16 hexDigit }
456+ octal = do{ oneOf "oO"; number 8 octDigit }
457+
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+ }
463+
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+ }
472+
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+ }
480+
481+ oper =
482+ do{ c <- (opStart languageDef)
483+ ; cs <- many (opLetter languageDef)
484+ ; return (c:cs)
485+ }
486+ <?> "operator"
487+
488+ isReservedOp name =
489+ isReserved (sort (reservedOpNames languageDef)) name
490+
491+
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+ }
500+
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 }
507+
508+ caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)
509+ | otherwise = char c
510+
511+ msg = show name
512+
513+
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+ }
521+
522+
523+ ident
524+ = do{ c <- identStart languageDef
525+ ; cs <- many (identLetter languageDef)
526+ ; return (c:cs)
527+ }
528+ <?> "identifier"
529+
530+ isReservedName name
531+ = isReserved theReservedNames caseName
532+ where
533+ caseName | caseSensitive languageDef = name
534+ | otherwise = map toLower name
535+
536+
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
545+
546+ theReservedNames
547+ | caseSensitive languageDef = sortedNames
548+ | otherwise = map (map toLower) sortedNames
549+ where
550+ sortedNames = sort (reservedNames languageDef)
551+
552+
553+
554+ -----------------------------------------------------------
555+ -- White space & symbols
556+ -----------------------------------------------------------
557+ symbol name
558+ = lexeme (string name)
559+
560+ lexeme p
561+ = do{ x <- p; whiteSpace; return x }
562+
563+ --whiteSpace
564+ whiteSpace = lexWS