@@ -17,11 +17,12 @@ import Core.CoreParser
17import Core.TT
17import Core.TT
18import Core.Evaluate
18import Core.Evaluate
20−import Text.ParserCombinators.Parsec
20+import Text.Parsec
21−import Text.ParserCombinators.Parsec.Error
21+import Text.Parsec.Error
22−import Text.ParserCombinators.Parsec.Expr
22+import Text.Parsec.Expr
23−import Text.ParserCombinators.Parsec.Language
23+import Text.Parsec.Language
24+import Text.Parsec.String
24−import qualified Text.ParserCombinators.Parsec.Token as PTok
25+import qualified Text.Parsec.Token as PTok
26import Data.List
27import Data.List
27import Control.Monad.State
28import Control.Monad.State
@@ -36,22 +37,22 @@ type IParser = GenParser Char IState
36lexer :: TokenParser IState
37lexer :: TokenParser IState
37lexer = PTok.makeTokenParser idrisDef
38lexer = PTok.makeTokenParser idrisDef
39−whiteSpace= PTok.whiteSpace lexer
40+whiteSpace = PTok.whiteSpace lexer
40−lexeme = PTok.lexeme lexer
41+lexeme = PTok.lexeme lexer
41−symbol = PTok.symbol lexer
42+symbol = PTok.symbol lexer
42−natural = PTok.natural lexer
43+natural = PTok.natural lexer
43−parens = PTok.parens lexer
44+parens = PTok.parens lexer
44−semi = PTok.semi lexer
45+semi = PTok.semi lexer
45−comma = PTok.comma lexer
46+comma = PTok.comma lexer
46−identifier= PTok.identifier lexer
47+identifier = PTok.identifier lexer
47−reserved = PTok.reserved lexer
48+reserved = PTok.reserved lexer
48−operator = PTok.operator lexer
49+operator = PTok.operator lexer
49−reservedOp= PTok.reservedOp lexer
50+reservedOp = PTok.reservedOp lexer
50−integer = PTok.integer lexer
51+integer = PTok.integer lexer
51−float = PTok.float lexer
52+float = PTok.float lexer
52−strlit = PTok.stringLiteral lexer
53+strlit = PTok.stringLiteral lexer
53−chlit = PTok.charLiteral lexer
54+chlit = PTok.charLiteral lexer
54−lchar = lexeme.char
55+lchar = lexeme.char
56-- Loading modules
57-- Loading modules
@@ -61,7 +62,7 @@ loadModule f
61 ibcsd <- valIBCSubDir i
62 ibcsd <- valIBCSubDir i
62 ids <- allImportDirs i
63 ids <- allImportDirs i
63 fp <- liftIO $ findImport ids ibcsd f
64 fp <- liftIO $ findImport ids ibcsd f
64− if (f `elem` imported i)
65+ if f `elem` imported i
65 then iLOG $ "Already read " ++ f
66 then iLOG $ "Already read " ++ f
66 else do putIState (i { imported = f : imported i })
67 else do putIState (i { imported = f : imported i })
67 case fp of
68 case fp of
@@ -90,7 +91,7 @@ loadSource lidr f
90 putIState (i { default_access = Hidden })
91 putIState (i { default_access = Hidden })
91 mapM_ loadModule modules
92 mapM_ loadModule modules
92 clearIBC -- start a new .ibc file
93 clearIBC -- start a new .ibc file
93− mapM_ (\m -> addIBC (IBCImport m)) modules
94+ mapM_ (addIBC . IBCImport) modules
94 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
95 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
95 f rest pos
96 f rest pos
96 let ds = namespaces mname ds'
97 let ds = namespaces mname ds'
@@ -125,10 +126,10 @@ addHides :: [(Name, Maybe Accessibility)] -> Idris ()
125addHides xs = do i <- getIState
126addHides xs = do i <- getIState
126 let defh = default_access i
127 let defh = default_access i
127 let (hs, as) = partition isNothing xs
128 let (hs, as) = partition isNothing xs
128− if null as then return ()
129+ unless (null as) $
129− else mapM_ doHide
130+ mapM_ doHide
130− (map (\ (n, _) -> (n, defh)) hs ++
131+ (map (\ (n, _) -> (n, defh)) hs ++
131− map (\ (n, Just a) -> (n, a)) as)
132+ map (\ (n, Just a) -> (n, a)) as)
132 where isNothing (_, Nothing) = True
133 where isNothing (_, Nothing) = True
133 isNothing _ = False
134 isNothing _ = False
@@ -140,123 +141,121 @@ parseTac i = runParser (do t <- pTactic defaultSyntax
141 return t) i "(proof)"
142 return t) i "(proof)"
144+iShowError fname err = let ln = sourceLine (errorPos err)
145+ clm = sourceColumn (errorPos err)
146+ msg = map messageString (errorMessages err) in
147+ fname ++ ":" ++ show ln ++ ":parse error"
148+ ++ " at column " ++ show clm -- ++ " with error:\n\t" ++ show msg
143parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
150parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
144parseImports fname input
151parseImports fname input
145 = do i <- get
152 = do i <- get
146− case (runParser (do whiteSpace
153+ case runParser (do whiteSpace
147− mname <- pHeader
154+ mname <- pHeader
148− ps <- many pImport
155+ ps <- many pImport
149− rest <- getInput
156+ rest <- getInput
150− pos <- getPosition
157+ pos <- getPosition
151− return ((mname, ps, rest, pos), i)) i fname input) of
158+ return ((mname, ps, rest, pos), i)) i fname input of
152− Left err -> fail (show err)
159+ Left err -> fail (iShowError fname err)
153− Right (x, i) -> do put i
160+ Right (x, i) -> do put i
154− return x
161+ return x
155− where ishow err = let ln = sourceLine (errorPos err) in
156− fname ++ ":" ++ show ln ++ ":parse error"
157−-- ++ show (map messageString (errorMessages err))
159pHeader :: IParser [String]
163pHeader :: IParser [String]
160pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
164pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
161 return (parseName i))
165 return (parseName i))
162 <|> return []
166 <|> return []
163 where parseName x = case span (/='.') x of
167 where parseName x = case span (/='.') x of
164− (x, "") -> [x]
168+ (x, "") -> [x]
165− (x, '.':y) -> x : parseName y
169+ (x, '.':y) -> x : parseName y
167−push_indent :: IParser ()
171+pushIndent :: IParser ()
168−push_indent = do pos <- getPosition
172+pushIndent = do pos <- getPosition
169− ist <- getState
173+ ist <- getState
170− setState (ist { indent_stack = sourceColumn pos :
174+ setState (ist { indent_stack = sourceColumn pos :
171 indent_stack ist })
175 indent_stack ist })
173−last_indent :: IParser Int
177+lastIndent :: IParser Int
174−last_indent = do ist <- getState
178+lastIndent = do ist <- getState
175− case indent_stack ist of
179+ case indent_stack ist of
176− (x : xs) -> return x
180+ (x : xs) -> return x
177− _ -> return 1
181+ _ -> return 1
179indent :: IParser Int
183indent :: IParser Int
180−indent = do pos <- getPosition
184+indent = liftM sourceColumn getPosition
181− return (sourceColumn pos)
183−pop_indent :: IParser ()
186+popIndent :: IParser ()
184−pop_indent = do ist <- getState
187+popIndent = do ist <- getState
185− let (x : xs) = indent_stack ist
188+ let (x : xs) = indent_stack ist
186− setState (ist { indent_stack = xs })
189+ setState (ist { indent_stack = xs })
188−open_block :: IParser ()
191+openBlock :: IParser ()
189−open_block = do lchar '{'
192+openBlock = do lchar '{'
190− ist <- getState
193+ ist <- getState
191− setState (ist { brace_stack = Nothing : brace_stack ist })
194+ setState (ist { brace_stack = Nothing : brace_stack ist })
192 <|> do ist <- getState
195 <|> do ist <- getState
193 lvl <- indent
196 lvl <- indent
194 setState (ist { brace_stack = Just lvl : brace_stack ist })
197 setState (ist { brace_stack = Just lvl : brace_stack ist })
196−close_block :: IParser ()
199+closeBlock :: IParser ()
197−close_block = do ist <- getState
200+closeBlock = do ist <- getState
198− bs <- case brace_stack ist of
201+ bs <- case brace_stack ist of
199− Nothing : xs -> do lchar '}'
202+ Nothing : xs -> do lchar '}'
200− return xs
203+ return xs
201− Just lvl : xs -> do i <- indent
204+ Just lvl : xs -> do i <- indent
202− inp <- getInput
205+ inp <- getInput
203-- trace (show (take 10 inp, i, lvl)) $
206-- trace (show (take 10 inp, i, lvl)) $
204− if (i >= lvl && take 1 inp /= ")")
207+ if i >= lvl && take 1 inp /= ")"
205− then fail "Not end of block"
208+ then fail "Not end of block"
206− else return xs
209+ else return xs
207− setState (ist { brace_stack = bs })
210+ setState (ist { brace_stack = bs })
209−pTerminator = do lchar ';'; pop_indent
212+pTerminator = do lchar ';'; popIndent
210− <|> do c <- indent; l <- last_indent
213+ <|> do c <- indent; l <- lastIndent
211− if (c <= l) then pop_indent
214+ if c <= l
212− else fail "Not a terminator"
216+ else fail "Not a terminator"
213− <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
217+ <|> do i <- getInput
218+ if "}" `isPrefixOf` i || ")" `isPrefixOf` i
214− else fail "Not a terminator"
220+ else fail "Not a terminator"
215 <|> lookAhead eof
221 <|> lookAhead eof
217pBarTerminator
223pBarTerminator
218 = do lchar '|'; return ()
224 = do lchar '|'; return ()
219− <|> do c <- indent; l <- last_indent
225+ <|> do c <- indent; l <- lastIndent
220− if (c <= l) then return ()
221− else fail "Not a terminator"
226+ unless (c <= l) $ fail "Not a terminator"
222 <|> lookAhead eof
227 <|> lookAhead eof
224pKeepTerminator
229pKeepTerminator
225 = do lchar ';'; return ()
230 = do lchar ';'; return ()
226− <|> do c <- indent; l <- last_indent
231+ <|> do c <- indent; l <- lastIndent
227− if (c <= l) then return ()
228− else fail "Not a terminator"
232+ unless (c <= l) $ fail "Not a terminator"
229− <|> do i <- getInput; let h = take 1 i
233+ <|> do i <- getInput
230− if (h == "}" || h == ")" || h == "|") then return ()
234+ let h = take 1 i
231− else fail "Not a terminator"
235+ unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
232 <|> lookAhead eof
236 <|> lookAhead eof
234−notEndApp = do c <- indent; l <- last_indent
238+notEndApp = do c <- indent; l <- lastIndent
235 i <- getInput
239 i <- getInput
236− if (c <= l) then fail "Terminator"
240+ when (c <= l) $ fail "Terminator"
239notEndBlock = do ist <- getState
242notEndBlock = do ist <- getState
240 case brace_stack ist of
243 case brace_stack ist of
241− Just lvl : xs -> do i <- indent
244+ Just lvl : xs -> do i <- indent
242 inp <- getInput
245 inp <- getInput
243− if (i < lvl || take 1 inp == ")")
244− then fail "End of block"
246+ when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
246− _ -> return ()
247+ _ -> return ()
248pfc :: IParser FC
249pfc :: IParser FC
249pfc = do s <- getPosition
250pfc = do s <- getPosition
250 let (dir, file) = splitFileName (sourceName s)
251 let (dir, file) = splitFileName (sourceName s)
251 let f = case dir of
252 let f = case dir of
252− "./" -> file
253+ "./" -> file
253− _ -> sourceName s
254+ _ -> sourceName s
254 return $ FC f (sourceLine s)
255 return $ FC f (sourceLine s)
256pImport :: IParser String
257pImport :: IParser String
257−pImport = do reserved "import"
258+pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
259− option ';' (lchar ';')
260 return (map dot f)
259 return (map dot f)
261 where dot '.' = '/'
260 where dot '.' = '/'
262 dot c = c
261 dot c = c
@@ -264,19 +263,15 @@ pImport = do reserved "import"
264parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
263parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
265parseProg syn fname input pos
264parseProg syn fname input pos
266 = do i <- get
265 = do i <- get
267− case (runParser (do setPosition pos
266+ case runParser (do setPosition pos
268− whiteSpace
267+ whiteSpace
269− ps <- many (pDecl syn)
268+ ps <- many (pDecl syn)
271− i' <- getState
270+ i' <- getState
272− return (concat ps, i')) i fname input) of
271+ return (concat ps, i')) i fname input of
273− Left err -> fail (ishow err)
272+ Left err -> fail (iShowError fname err)
274 Right (x, i) -> do put i
273 Right (x, i) -> do put i
275 return (collect x)
274 return (collect x)
276− where ishow err = let ln = sourceLine (errorPos err) in
277− fname ++ ":" ++ show ln ++ ":parse error"
278− ++ " at column " ++ show (sourceColumn (errorPos err))
279−-- show (map messageString (errorMessages err))
281-- Collect PClauses with the same function name
276-- Collect PClauses with the same function name
@@ -322,8 +317,7 @@ pDecl syn = do notEndBlock
322 <|> pInstance syn
317 <|> pInstance syn
323 <|> do d <- pDSL syn; return [d]
318 <|> do d <- pDSL syn; return [d]
324 <|> pDirective
319 <|> pDirective
325− <|> try (do reserved "import"
320+ <|> try (do reserved "import"; fp <- identifier
327 fail "imports must be at the top of file")
321 fail "imports must be at the top of file")
329pFunDecl :: SyntaxInfo -> IParser [PDecl]
323pFunDecl :: SyntaxInfo -> IParser [PDecl]
@@ -365,7 +359,7 @@ pSyntaxDecl syn
366pSyntaxRule :: SyntaxInfo -> IParser Syntax
360pSyntaxRule :: SyntaxInfo -> IParser Syntax
367pSyntaxRule syn
361pSyntaxRule syn
368− = do push_indent
362+ = do pushIndent
369 sty <- option AnySyntax (do reserved "term"; return TermSyntax
363 sty <- option AnySyntax (do reserved "term"; return TermSyntax
370 <|> do reserved "pattern"; return PatternSyntax)
364 <|> do reserved "pattern"; return PatternSyntax)
371 reserved "syntax"
365 reserved "syntax"
@@ -405,7 +399,7 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
405 return (Symbol sym)
399 return (Symbol sym)
407pFunDecl' :: SyntaxInfo -> IParser PDecl
401pFunDecl' :: SyntaxInfo -> IParser PDecl
408−pFunDecl' syn = try (do push_indent
402+pFunDecl' syn = try (do pushIndent
409 opts <- pFnOpts
403 opts <- pFnOpts
410 acc <- pAccessibility
404 acc <- pAccessibility
411 opts' <- pFnOpts
405 opts' <- pFnOpts
@@ -421,22 +415,16 @@ pFunDecl' syn = try (do push_indent
422pUsing :: SyntaxInfo -> IParser [PDecl]
416pUsing :: SyntaxInfo -> IParser [PDecl]
423pUsing syn =
417pUsing syn =
424− do reserved "using";
418+ do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'
425− lchar '('
419+ openBlock
426− ns <- tyDeclList syn
429 let uvars = using syn
420 let uvars = using syn
430 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
421 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
431− close_block
422+ closeBlock
432 return (concat ds)
423 return (concat ds)
434pParams :: SyntaxInfo -> IParser [PDecl]
425pParams :: SyntaxInfo -> IParser [PDecl]
435pParams syn =
426pParams syn =
436− do reserved "params";
427+ do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'
438− ns <- tyDeclList syn
440 lchar '{'
428 lchar '{'
441 let pvars = syn_params syn
429 let pvars = syn_params syn
442 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
430 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
@@ -446,17 +434,16 @@ pParams syn =
447pNamespace :: SyntaxInfo -> IParser [PDecl]
435pNamespace :: SyntaxInfo -> IParser [PDecl]
448pNamespace syn =
436pNamespace syn =
449− do reserved "namespace";
437+ do reserved "namespace"; n <- identifier;
450− n <- identifier
438+ openBlock
452 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
439 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
453− close_block
440+ closeBlock
454 return [PNamespace n (concat ds)]
441 return [PNamespace n (concat ds)]
456--------- Fixity ---------
443--------- Fixity ---------
458pFixity :: IParser PDecl
445pFixity :: IParser PDecl
459−pFixity = do push_indent
446+pFixity = do pushIndent
460 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
447 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
461 pTerminator
448 pTerminator
462 let prec = fromInteger i
449 let prec = fromInteger i
@@ -478,14 +465,12 @@ fixity = try (do reserved "infixl"; return Infixl)
479pClass :: SyntaxInfo -> IParser [PDecl]
466pClass :: SyntaxInfo -> IParser [PDecl]
480pClass syn = do acc <- pAccessibility
467pClass syn = do acc <- pAccessibility
483− cons <- pConstList syn
468+ reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
484− n_in <- pName; let n = expandNS syn n_in
469+ let n = expandNS syn n_in
485 cs <- many1 carg
470 cs <- many1 carg
486− reserved "where"; open_block
471+ reserved "where"; openBlock
487 ds <- many $ pFunDecl syn
472 ds <- many $ pFunDecl syn
488− close_block
473+ closeBlock
489 let allDs = concat ds
474 let allDs = concat ds
490 accData acc n (concatMap declared allDs)
475 accData acc n (concatMap declared allDs)
491 return [PClass syn fc cons n cs allDs]
476 return [PClass syn fc cons n cs allDs]
@@ -496,8 +481,7 @@ pClass syn = do acc <- pAccessibility
496 return (i, PSet)
481 return (i, PSet)
498pInstance :: SyntaxInfo -> IParser [PDecl]
483pInstance :: SyntaxInfo -> IParser [PDecl]
499−pInstance syn = do reserved "instance"
484+pInstance syn = do reserved "instance"; fc <- pfc
501 en <- option Nothing
485 en <- option Nothing
502 (do lchar '['; n_in <- pfName; lchar ']'
486 (do lchar '['; n_in <- pfName; lchar ']'
503 let n = expandNS syn n_in
487 let n = expandNS syn n_in
@@ -507,9 +491,9 @@ pInstance syn = do reserved "instance"
507 args <- many1 (pSimpleExpr syn)
491 args <- many1 (pSimpleExpr syn)
508 let sc = PApp fc (PRef fc cn) (map pexp args)
492 let sc = PApp fc (PRef fc cn) (map pexp args)
509 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
493 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
510− reserved "where"; open_block
494+ reserved "where"; openBlock
511 ds <- many $ pFunDecl syn
495 ds <- many $ pFunDecl syn
512− close_block
496+ closeBlock
513 return [PInstance syn fc cs cn args t en (concat ds)]
497 return [PInstance syn fc cs cn args t en (concat ds)]
515--------- Expressions ---------
499--------- Expressions ---------
@@ -534,7 +518,7 @@ pSimpleExtExpr syn = do i <- getState
534 simple (Rule (SimpleExpr x:xs) _ _) = False
518 simple (Rule (SimpleExpr x:xs) _ _) = False
535 simple (Rule [Keyword _] _ _) = True
519 simple (Rule [Keyword _] _ _) = True
536 simple (Rule [Symbol _] _ _) = True
520 simple (Rule [Symbol _] _ _) = True
537− simple (Rule (_:xs) _ _) = case (last xs) of
521+ simple (Rule (_:xs) _ _) = case last xs of
538 Keyword _ -> True
522 Keyword _ -> True
539 Symbol _ -> True
523 Symbol _ -> True
540 _ -> False
524 _ -> False
@@ -551,7 +535,7 @@ pNoExtExpr syn =
551 <|> pComprehension syn
535 <|> pComprehension syn
553pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
537pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
554−pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
538+pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
556 valid (Rule _ _ AnySyntax) = True
540 valid (Rule _ _ AnySyntax) = True
557 valid (Rule _ _ PatternSyntax) = inPattern syn
541 valid (Rule _ _ PatternSyntax) = inPattern syn
@@ -648,41 +632,56 @@ addAcc :: Name -> Maybe Accessibility -> IParser ()
648addAcc n a = do i <- getState
632addAcc n a = do i <- getState
649 setState (i { hide_list = (n, a) : hide_list i })
633 setState (i { hide_list = (n, a) : hide_list i })
636+ reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
639+ opts <- many1 (do notEndBlock
642+ return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
645+ return (PCase fc scr opts)
648+ reserved "proof"; lchar '{'
649+ ts <- endBy (pTactic syn) (lchar ';')
653+pTacticsExpr syn = do
654+ reserved "tactics"; lchar '{'
655+ ts <- endBy (pTactic syn) (lchar ';')
657+ return (PTactics ts)
651pSimpleExpr syn =
659pSimpleExpr syn =
652− try (do symbol "!["; t <- pTerm; lchar ']'
660+ try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
654 <|> do lchar '?'; x <- pName; return (PMetavar x)
661 <|> do lchar '?'; x <- pName; return (PMetavar x)
655 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
662 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
656-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
663-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
657− <|> do reserved "proof"; lchar '{';
664+ <|> pProofExpr syn
658− ts <- endBy (pTactic syn) (lchar ';')
665+ <|> pTacticsExpr syn
659− lchar '}'
666+ <|> pCaseExpr syn
660− return (PProof ts)
667+ <|> try (do x <- pfName
661− <|> do reserved "tactics"; lchar '{';
668+ fc <- pfc
662− ts <- endBy (pTactic syn) (lchar ';')
664− return (PTactics ts)
665− <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
668− opts <- many1 (do notEndBlock
671− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
674− return (PCase fc scr opts)
675− <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
669+ return (PRef fc x))
676 <|> try (pList syn)
670 <|> try (pList syn)
677 <|> try (pAlt syn)
671 <|> try (pAlt syn)
678 <|> try (pIdiom syn)
672 <|> try (pIdiom syn)
673+ <|> try (do lchar '('
679− <|> try (do lchar '('; bracketed (noImp syn))
674+ bracketed (noImp syn))
680− <|> try (do c <- pConstant; fc <- pfc
675+ <|> try (do c <- pConstant
681 return (modifyConst syn fc (PConstant c)))
677 return (modifyConst syn fc (PConstant c)))
682 <|> do reserved "Set"; return PSet
678 <|> do reserved "Set"; return PSet
683−-- <|> do symbol "*"; return PSet
679+ <|> try (do symbol "()"
684− <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
681+ return (PTrue fc))
682+ <|> try (do symbol "_|_"
685− <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
684+ return (PFalse fc))
686 <|> do lchar '_'; return Placeholder
685 <|> do lchar '_'; return Placeholder
687 <|> pSimpleExtExpr syn
686 <|> pSimpleExtExpr syn
@@ -702,8 +701,7 @@ bracketed syn =
702 pexp (PRef fc (MN 0 "x"))]))
701 pexp (PRef fc (MN 0 "x"))]))
704pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
703pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
705−pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
704+pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn
707 return (lhs, rhs)
705 return (lhs, rhs)
709modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
707modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
@@ -713,8 +711,7 @@ modifyConst syn fc (PConstant (I x))
713 | otherwise = PConstant (I x)
711 | otherwise = PConstant (I x)
714modifyConst syn fc x = x
712modifyConst syn fc x = x
716−pList syn = do lchar '['; fc <- pfc
717− xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
714+pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
718 return (mkList fc xs)
715 return (mkList fc xs)
720 mkList fc [] = PRef fc (UN "Nil")
717 mkList fc [] = PRef fc (UN "Nil")
@@ -730,10 +727,12 @@ pPair syn = try (do l <- pExpr syn
730 <|> try (do x <- ntuple
727 <|> try (do x <- ntuple
731 lchar ')'
728 lchar ')'
732 return x)
729 return x)
733− <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
730+ <|> do ln <- pName; lchar ':'
734− reservedOp "**";
732+ reservedOp "**"
735 fc <- pfc
733 fc <- pfc
736− r <- pExpr syn; lchar ')';
734+ r <- pExpr syn
737 return (PDPair fc (PRef fc ln) lty r)
736 return (PDPair fc (PRef fc ln) lty r)
739 restTuple = do lchar ')'; return []
738 restTuple = do lchar ')'; return []
@@ -752,9 +751,7 @@ pPair syn = try (do l <- pExpr syn
752 r <- pExpr syn
751 r <- pExpr syn
753 return (PPair fc l r))
752 return (PPair fc l r))
755−pAlt syn = do symbol "(|";
756− alts <- sepBy1 (pExpr' syn) (lchar ',')
754+pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
758 return (PAlternative False alts)
755 return (PAlternative False alts)
760pHSimpleExpr syn
757pHSimpleExpr syn
@@ -781,13 +778,17 @@ pArg syn = try (pImplicitArg syn)
781 <|> do e <- pSimpleExpr syn
778 <|> do e <- pSimpleExpr syn
782 return (pexp e)
779 return (pexp e)
784−pImplicitArg syn = do lchar '{'; n <- pName
781+pImplicitArg syn = do lchar '{'
785 fc <- pfc
783 fc <- pfc
786− v <- option (PRef fc n) (do lchar '='; pExpr syn)
784+ v <- option (PRef fc n) (do lchar '='
787 lchar '}'
786 lchar '}'
788 return (pimp n v)
787 return (pimp n v)
790−pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
789+pConstraintArg syn = do symbol "@{"
791 return (pconst e)
792 return (pconst e)
793pRecordSet syn
794pRecordSet syn
@@ -796,13 +797,15 @@ pRecordSet syn
796 fields <- sepBy1 pFieldSet (lchar ',')
797 fields <- sepBy1 pFieldSet (lchar ',')
797 lchar '}'
798 lchar '}'
798 fc <- pfc
799 fc <- pfc
799− rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))
800+ rec <- option Nothing (do e <- pSimpleExpr syn
800 case rec of
802 case rec of
801 Nothing ->
803 Nothing ->
802 return (PLam (MN 0 "fldx") Placeholder
804 return (PLam (MN 0 "fldx") Placeholder
803 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
805 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
804 Just v -> return (applyAll fc fields v)
806 Just v -> return (applyAll fc fields v)
805− where pFieldSet = do n <- pfName; lchar '='
807+ where pFieldSet = do n <- pfName
806 e <- pExpr syn
809 e <- pExpr syn
807 return (n, e)
810 return (n, e)
808 applyAll fc [] x = x
811 applyAll fc [] x = x
@@ -822,10 +825,10 @@ pTSig syn = do lchar ':'
822 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
825 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
824pLambda syn = do lchar '\\'
827pLambda syn = do lchar '\\'
825− (try (do xt <- tyOptDeclList syn
828+ try (do xt <- tyOptDeclList syn
826− symbol "=>"
829+ symbol "=>"
827− sc <- pExpr syn
830+ sc <- pExpr syn
828− return (bindList PLam xt sc))
831+ return (bindList PLam xt sc)
829 <|> (do ps <- sepBy (do fc <- pfc
832 <|> (do ps <- sepBy (do fc <- pfc
830 e <- pSimpleExpr syn
833 e <- pSimpleExpr syn
831 return (fc, e)) (lchar ',')
834 return (fc, e)) (lchar ',')
@@ -836,11 +839,12 @@ pLambda syn = do lchar '\\'
836 pmList ((i, (fc, x)) : xs) sc
839 pmList ((i, (fc, x)) : xs) sc
837 = PLam (MN i "lamp") Placeholder
840 = PLam (MN i "lamp") Placeholder
838 (PCase fc (PRef fc (MN i "lamp"))
841 (PCase fc (PRef fc (MN i "lamp"))
839− [(x, (pmList xs sc))])
842+ [(x, pmList xs sc)])
841pLet syn = try (do reserved "let"; n <- pName;
844pLet syn = try (do reserved "let"; n <- pName;
842 ty <- option Placeholder (do lchar ':'; pExpr' syn)
845 ty <- option Placeholder (do lchar ':'; pExpr' syn)
843− lchar '='; v <- pExpr syn
847+ v <- pExpr syn
844 reserved "in"; sc <- pExpr syn
848 reserved "in"; sc <- pExpr syn
845 return (PLet n ty v sc))
849 return (PLet n ty v sc))
846 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
850 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
@@ -855,27 +859,36 @@ pPi syn =
855 symbol "->"
859 symbol "->"
856 sc <- pExpr syn
860 sc <- pExpr syn
857 return (bindList (PPi (Exp lazy st)) xt sc))
861 return (bindList (PPi (Exp lazy st)) xt sc))
858− <|> try (if implicitAllowed syn then
862+ <|> try (if implicitAllowed syn
859− do lazy <- option False (do lchar '|'; return True)
863+ then do lazy <- option False (do lchar '|'
860− st <- pStatic
865+ st <- pStatic
861− lchar '{'; xt <- tyDeclList syn; lchar '}'
867+ xt <- tyDeclList syn
862− symbol "->"
869+ symbol "->"
863− sc <- pExpr syn
870+ sc <- pExpr syn
864− return (bindList (PPi (Imp lazy st)) xt sc)
871+ return (bindList (PPi (Imp lazy st)) xt sc)
865 else fail "No implicit arguments allowed here")
872 else fail "No implicit arguments allowed here")
873+ <|> try (do lchar '{'
866− <|> try (do lchar '{'; reserved "auto"
874+ reserved "auto"
867− xt <- tyDeclList syn; lchar '}'
875+ xt <- tyDeclList syn
868 symbol "->"
877 symbol "->"
869 sc <- pExpr syn
878 sc <- pExpr syn
870 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
879 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
880+ <|> try (do lchar '{'
871− <|> try (do lchar '{'; reserved "default"
881+ reserved "default"
872 script <- pSimpleExpr syn
882 script <- pSimpleExpr syn
873− xt <- tyDeclList syn; lchar '}'
883+ xt <- tyDeclList syn
874 symbol "->"
885 symbol "->"
875 sc <- pExpr syn
886 sc <- pExpr syn
876 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
887 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
877 <|> do --lazy <- option False (do lchar '|'; return True)
888 <|> do --lazy <- option False (do lchar '|'; return True)
878− lchar '{'; reserved "static"; lchar '}'
890+ reserved "static"
879 t <- pExpr' syn
892 t <- pExpr' syn
880 symbol "->"
893 symbol "->"
881 sc <- pExpr syn
894 sc <- pExpr syn
@@ -892,7 +905,9 @@ pConstList syn = try (do lchar '('
892 return [t])
905 return [t])
893 <|> return []
906 <|> return []
895−tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig (noImp syn); return (x,t))
908+tyDeclList syn = try (sepBy1 (do x <- pfName
909+ t <- pTSig (noImp syn)
896 (lchar ','))
911 (lchar ','))
897 <|> do ns <- sepBy1 pName (lchar ',')
912 <|> do ns <- sepBy1 pName (lchar ',')
898 t <- pTSig (noImp syn)
913 t <- pTSig (noImp syn)
@@ -908,8 +923,12 @@ bindList b [] sc = sc
908bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
923bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
910pComprehension syn
925pComprehension syn
911− = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
928+ pat <- pExpr syn
912− qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';
930+ qs <- sepBy1 (pDo syn) (lchar ',')
913 return (PDoBlock (map addGuard qs ++
932 return (PDoBlock (map addGuard qs ++
914 [DoExp fc (PApp fc (PRef fc (UN "return"))
933 [DoExp fc (PApp fc (PRef fc (UN "return"))
915 [pexp pat])]))
934 [pexp pat])]))
@@ -918,34 +937,51 @@ pComprehension syn
918 addGuard x = x
937 addGuard x = x
920pDoBlock syn
939pDoBlock syn
921− = do reserved "do"; open_block
940+ = do reserved "do"
922− push_indent
941+ openBlock
923 ds <- many1 (do notEndBlock
943 ds <- many1 (do notEndBlock
924− x <- pDo syn; pKeepTerminator; return x)
945+ pKeepTerminator
925− pop_indent
946+ return x)
926− close_block
947+ popIndent
927 return (PDoBlock ds)
949 return (PDoBlock ds)
930− = try (do reserved "let"; i <- pName;
952+ = try (do reserved "let"
931− ty <- option Placeholder (do lchar ':'; pExpr' syn)
954+ ty <- option Placeholder (do lchar ':'
932− reservedOp "="; fc <- pfc
956+ reservedOp "="
933 e <- pExpr syn
958 e <- pExpr syn
934 return (DoLet fc i ty e))
959 return (DoLet fc i ty e))
935− <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
960+ <|> try (do reserved "let"
936 sc <- pExpr syn
964 sc <- pExpr syn
937 return (DoLetP fc i sc))
965 return (DoLetP fc i sc))
938− <|> try (do i <- pName; symbol "<-"; fc <- pfc
966+ <|> try (do i <- pName
939 e <- pExpr syn;
969 e <- pExpr syn;
940 return (DoBind fc i e))
970 return (DoBind fc i e))
941− <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
971+ <|> try (do i <- pExpr' syn
942 e <- pExpr syn;
974 e <- pExpr syn;
943 return (DoBindP fc i e))
975 return (DoBindP fc i e))
944− <|> try (do e <- pExpr syn; fc <- pfc
976+ <|> try (do e <- pExpr syn
945 return (DoExp fc e))
978 return (DoExp fc e))
947pIdiom syn
980pIdiom syn
948− = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
983+ e <- pExpr syn
949 return (PIdiom fc e)
985 return (PIdiom fc e)
951pConstant :: IParser Const
987pConstant :: IParser Const
@@ -962,7 +998,9 @@ pConstant = do reserved "Integer";return BIType
962 <|> try (do c <- chlit; return $ Ch c)
998 <|> try (do c <- chlit; return $ Ch c)
964pStatic :: IParser Static
1000pStatic :: IParser Static
965−pStatic = do lchar '['; reserved "static"; lchar ']';
1001+pStatic = do lchar '['
966 return Static
1004 return Static
967 <|> return Dynamic
1005 <|> return Dynamic
@@ -971,7 +1009,7 @@ table fixes
971 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1009 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
972 ++ toTable (reverse fixes) ++
1010 ++ toTable (reverse fixes) ++
973 [[backtick],
1011 [[backtick],
974− [binary "=" (\fc x y -> PEq fc x y) AssocLeft],
1012+ [binary "=" PEq AssocLeft],
975 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1013 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
977toTable fs = map (map toBin)
1015toTable fs = map (map toBin)
@@ -984,11 +1022,14 @@ toTable fs = map (map toBin)
984 assoc (Infixr _) = AssocRight
1022 assoc (Infixr _) = AssocRight
985 assoc (InfixN _) = AssocNone
1023 assoc (InfixN _) = AssocNone
987−binary name f assoc = Infix (do reservedOp name; fc <- pfc;
1025+binary name f = Infix (do reservedOp name
988− return (f fc)) assoc
1027+ return (f fc))
989−prefix name f = Prefix (do reservedOp name; fc <- pfc;
1028+prefix name f = Prefix (do reservedOp name
990 return (f fc))
1030 return (f fc))
991−backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
1031+backtick = Infix (do lchar '`'; n <- pfName
992 fc <- pfc
1033 fc <- pfc
993 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1034 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
@@ -998,20 +1039,23 @@ backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
998accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1039accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
999accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1040accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1000 mapM_ (\n -> addAcc n (Just Hidden)) ns
1041 mapM_ (\n -> addAcc n (Just Hidden)) ns
1001−accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
1042+accData a n ns = do addAcc n a
1043+ mapM_ (`addAcc` a) ns
1003pRecord :: SyntaxInfo -> IParser PDecl
1045pRecord :: SyntaxInfo -> IParser PDecl
1004pRecord syn = do acc <- pAccessibility
1046pRecord syn = do acc <- pAccessibility
1005− reserved "record"; fc <- pfc
1047+ reserved "record"
1006− tyn_in <- pfName; ty <- pTSig (impOK syn)
1050+ ty <- pTSig (impOK syn)
1007 let tyn = expandNS syn tyn_in
1051 let tyn = expandNS syn tyn_in
1008 reserved "where"
1052 reserved "where"
1009− open_block
1053+ openBlock
1010− push_indent
1054+ pushIndent
1011 (cn, cty, _) <- pConstructor syn
1055 (cn, cty, _) <- pConstructor syn
1012 pKeepTerminator
1056 pKeepTerminator
1013− pop_indent
1057+ popIndent
1014− close_block
1058+ closeBlock
1015 accData acc tyn [cn]
1059 accData acc tyn [cn]
1016 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1060 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1017 syn_namespace syn }
1061 syn_namespace syn }
@@ -1028,30 +1072,34 @@ pRecord syn = do acc <- pAccessibility
1029pData :: SyntaxInfo -> IParser PDecl
1073pData :: SyntaxInfo -> IParser PDecl
1030pData syn = try (do acc <- pAccessibility
1074pData syn = try (do acc <- pAccessibility
1031− reserved "data"; fc <- pfc
1075+ reserved "data"
1032− tyn_in <- pfName; ty <- pTSig (impOK syn)
1078+ ty <- pTSig (impOK syn)
1033 let tyn = expandNS syn tyn_in
1079 let tyn = expandNS syn tyn_in
1034 reserved "where"
1080 reserved "where"
1035− open_block
1081+ openBlock
1036− push_indent
1082+ pushIndent
1037 cons <- many (do notEndBlock
1083 cons <- many (do notEndBlock
1038 c <- pConstructor syn
1084 c <- pConstructor syn
1039 pKeepTerminator
1085 pKeepTerminator
1040 return c) -- (lchar '|')
1086 return c) -- (lchar '|')
1041− pop_indent
1087+ popIndent
1042− close_block
1088+ closeBlock
1043 accData acc tyn (map (\ (n, _, _) -> n) cons)
1089 accData acc tyn (map (\ (n, _, _) -> n) cons)
1044 return $ PData syn fc (PDatadecl tyn ty cons))
1090 return $ PData syn fc (PDatadecl tyn ty cons))
1045− <|> try (do push_indent
1091+ <|> try (do pushIndent
1046 acc <- pAccessibility
1092 acc <- pAccessibility
1047− reserved "data"; fc <- pfc
1093+ reserved "data"
1048− tyn_in <- pfName; args <- many pName
1096+ args <- many pName
1049 let tyn = expandNS syn tyn_in
1097 let tyn = expandNS syn tyn_in
1050 lchar '='
1098 lchar '='
1051 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1099 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1052 pTerminator
1100 pTerminator
1053 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1101 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1054− let ty = bindArgs (map (\a -> PSet) args) PSet
1102+ let ty = bindArgs (map (const PSet) args) PSet
1055 cons' <- mapM (\ (x, cargs, cfc) ->
1103 cons' <- mapM (\ (x, cargs, cfc) ->
1056 do let cty = bindArgs cargs conty
1104 do let cty = bindArgs cargs conty
1057 return (x, cty, cfc)) cons
1105 return (x, cty, cfc)) cons
@@ -1062,8 +1110,7 @@ pData syn = try (do acc <- pAccessibility
1062 mkPApp fc t xs = PApp fc t (map pexp xs)
1110 mkPApp fc t xs = PApp fc t (map pexp xs)
1064bindArgs :: [PTerm] -> PTerm -> PTerm
1112bindArgs :: [PTerm] -> PTerm -> PTerm
1065−bindArgs [] t = t
1113+bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1066−bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
1068pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1115pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1069pConstructor syn
1116pConstructor syn
@@ -1086,13 +1133,15 @@ pSimpleCon syn
1086--------- DSL syntax overloading ---------
1133--------- DSL syntax overloading ---------
1088pDSL :: SyntaxInfo -> IParser PDecl
1135pDSL :: SyntaxInfo -> IParser PDecl
1089−pDSL syn = do reserved "dsl"; n <- pfName
1136+pDSL syn = do reserved "dsl"
1090− open_block; push_indent
1137+ n <- pfName
1091 bs <- many1 (do notEndBlock
1140 bs <- many1 (do notEndBlock
1092 b <- pOverload syn
1141 b <- pOverload syn
1093 pKeepTerminator
1142 pKeepTerminator
1094 return b)
1143 return b)
1095− pop_indent; close_block
1144+ popIndent; closeBlock
1096 let dsl = mkDSL bs (dsl_info syn)
1145 let dsl = mkDSL bs (dsl_info syn)
1097 checkDSL dsl
1146 checkDSL dsl
1098 i <- getState
1147 i <- getState
@@ -1113,8 +1162,9 @@ checkDSL :: DSL -> IParser ()
1113checkDSL dsl = return ()
1162checkDSL dsl = return ()
1115pOverload :: SyntaxInfo -> IParser (String, PTerm)
1164pOverload :: SyntaxInfo -> IParser (String, PTerm)
1116−pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1165+pOverload syn = do o <- identifier <|> do reserved "let"
1117− if (not (o `elem` overloadable))
1167+ if o `notElem` overloadable
1118 then fail $ show o ++ " is not an overloading"
1168 then fail $ show o ++ " is not an overloading"
1120 lchar '='
1170 lchar '='
@@ -1143,7 +1193,7 @@ pRHS syn n = do lchar '='; pExpr syn
1144pClause :: SyntaxInfo -> IParser PClause
1194pClause :: SyntaxInfo -> IParser PClause
1145pClause syn
1195pClause syn
1146− = try (do push_indent
1196+ = try (do pushIndent
1147 n_in <- pfName; let n = expandNS syn n_in
1197 n_in <- pfName; let n = expandNS syn n_in
1148 cargs <- many (pConstraintArg syn)
1198 cargs <- many (pConstraintArg syn)
1149 iargs <- many (pImplicitArg syn)
1199 iargs <- many (pImplicitArg syn)
@@ -1155,7 +1205,7 @@ pClause syn
1155 let ctxt = tt_ctxt ist
1205 let ctxt = tt_ctxt ist
1156 let wsyn = syn { syn_namespace = [] }
1206 let wsyn = syn { syn_namespace = [] }
1157 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1207 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1158− pop_indent
1208+ popIndent
1159 return x,
1209 return x,
1160 do pTerminator
1210 do pTerminator
1161 return ([], [])]
1211 return ([], [])]
@@ -1164,7 +1214,7 @@ pClause syn
1164 ist <- getState
1214 ist <- getState
1165 setState (ist { lastParse = Just n })
1215 setState (ist { lastParse = Just n })
1166 return $ PClause fc n capp wargs rhs wheres)
1216 return $ PClause fc n capp wargs rhs wheres)
1167− <|> try (do push_indent
1217+ <|> try (do pushIndent
1168 wargs <- many1 (pWExpr syn)
1218 wargs <- many1 (pWExpr syn)
1169 ist <- getState
1219 ist <- getState
1170 n <- case lastParse ist of
1220 n <- case lastParse ist of
@@ -1175,13 +1225,13 @@ pClause syn
1175 let ctxt = tt_ctxt ist
1225 let ctxt = tt_ctxt ist
1176 let wsyn = syn { syn_namespace = [] }
1226 let wsyn = syn { syn_namespace = [] }
1177 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1227 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1178− pop_indent
1228+ popIndent
1179 return x,
1229 return x,
1180 do pTerminator
1230 do pTerminator
1181 return ([], [])]
1231 return ([], [])]
1182 return $ PClauseR fc wargs rhs wheres)
1232 return $ PClauseR fc wargs rhs wheres)
1184− <|> try (do push_indent
1234+ <|> try (do pushIndent
1185 n_in <- pfName; let n = expandNS syn n_in
1235 n_in <- pfName; let n = expandNS syn n_in
1186 cargs <- many (pConstraintArg syn)
1236 cargs <- many (pConstraintArg syn)
1187 iargs <- many (pImplicitArg syn)
1237 iargs <- many (pImplicitArg syn)
@@ -1194,24 +1244,24 @@ pClause syn
1194 setState (ist { lastParse = Just n })
1244 setState (ist { lastParse = Just n })
1195 reserved "with"
1245 reserved "with"
1196 wval <- pSimpleExpr syn
1246 wval <- pSimpleExpr syn
1197− open_block
1247+ openBlock
1198 ds <- many1 $ pFunDecl syn
1248 ds <- many1 $ pFunDecl syn
1199 let withs = map (fillLHSD n capp wargs) $ concat ds
1249 let withs = map (fillLHSD n capp wargs) $ concat ds
1200− close_block
1250+ closeBlock
1201− pop_indent
1251+ popIndent
1202 return $ PWith fc n capp wargs wval withs)
1252 return $ PWith fc n capp wargs wval withs)
1204 <|> try (do wargs <- many1 (pWExpr syn)
1254 <|> try (do wargs <- many1 (pWExpr syn)
1205 fc <- pfc
1255 fc <- pfc
1206 reserved "with"
1256 reserved "with"
1207 wval <- pSimpleExpr syn
1257 wval <- pSimpleExpr syn
1208− open_block
1258+ openBlock
1209 ds <- many1 $ pFunDecl syn
1259 ds <- many1 $ pFunDecl syn
1210 let withs = concat ds
1260 let withs = concat ds
1211− close_block
1261+ closeBlock
1212 return $ PWithR fc wargs wval withs)
1262 return $ PWithR fc wargs wval withs)
1214− <|> do push_indent
1264+ <|> do pushIndent
1215 l <- pArgExpr syn
1265 l <- pArgExpr syn
1216 op <- operator
1266 op <- operator
1217 let n = expandNS syn (UN op)
1267 let n = expandNS syn (UN op)
@@ -1221,7 +1271,7 @@ pClause syn
1221 rhs <- pRHS syn n
1271 rhs <- pRHS syn n
1222 let wsyn = syn { syn_namespace = [] }
1272 let wsyn = syn { syn_namespace = [] }
1223 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1273 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1224− pop_indent
1274+ popIndent
1225 return x,
1275 return x,
1226 do pTerminator
1276 do pTerminator
1227 return ([], [])]
1277 return ([], [])]
@@ -1238,9 +1288,9 @@ pClause syn
1238 wargs <- many (pWExpr syn)
1288 wargs <- many (pWExpr syn)
1239 reserved "with"
1289 reserved "with"
1240 wval <- pSimpleExpr syn
1290 wval <- pSimpleExpr syn
1241− open_block
1291+ openBlock
1242 ds <- many1 $ pFunDecl syn
1292 ds <- many1 $ pFunDecl syn
1243− close_block
1293+ closeBlock
1244 ist <- getState
1294 ist <- getState
1245 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1295 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1246 let withs = map (fillLHSD n capp wargs) $ concat ds
1296 let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1258,14 +1308,15 @@ pClause syn
1258 fillLHSD n c a x = x
1308 fillLHSD n c a x = x
1260pWExpr :: SyntaxInfo -> IParser PTerm
1310pWExpr :: SyntaxInfo -> IParser PTerm
1261−pWExpr syn = do lchar '|'; pExpr' syn
1311+pWExpr syn = do lchar '|'
1263pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1314pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1264pWhereblock n syn
1315pWhereblock n syn
1265− = do reserved "where"; open_block
1316+ = do reserved "where"; openBlock
1266 ds <- many1 $ pFunDecl syn
1317 ds <- many1 $ pFunDecl syn
1267 let dns = concatMap (concatMap declared) ds
1318 let dns = concatMap (concatMap declared) ds
1268− close_block
1319+ closeBlock
1269 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1271pDirective :: IParser [PDecl]
1322pDirective :: IParser [PDecl]
@@ -1273,7 +1324,7 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1273 return [PDirective (do addLib lib
1324 return [PDirective (do addLib lib
1274 addIBC (IBCLib lib))])
1325 addIBC (IBCLib lib))])
1275 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1326 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1276− return [PDirective (do datadir <- liftIO $ getDataDir
1327+ return [PDirective (do datadir <- liftIO getDataDir
1277 o <- liftIO $ findInPath [".", datadir] obj
1328 o <- liftIO $ findInPath [".", datadir] obj
1278 addIBC (IBCObj o)
1329 addIBC (IBCObj o)
1279 addObjectFile o)])
1330 addObjectFile o)])