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