@@ -37,22 +37,22 @@ type IParser = GenParser Char IState
3737lexer :: TokenParser IState
3838lexer = PTok.makeTokenParser idrisDef
3939
40−whiteSpace= PTok.whiteSpace lexer
41−lexeme = PTok.lexeme lexer
42−symbol = PTok.symbol lexer
43−natural = PTok.natural lexer
44−parens = PTok.parens lexer
45−semi = PTok.semi lexer
46−comma = PTok.comma lexer
47−identifier= PTok.identifier lexer
48−reserved = PTok.reserved lexer
49−operator = PTok.operator lexer
50−reservedOp= PTok.reservedOp lexer
51−integer = PTok.integer lexer
52−float = PTok.float lexer
53−strlit = PTok.stringLiteral lexer
54−chlit = PTok.charLiteral lexer
55−lchar = lexeme.char
40+whiteSpace = PTok.whiteSpace lexer
41+lexeme = PTok.lexeme lexer
42+symbol = PTok.symbol lexer
43+natural = PTok.natural lexer
44+parens = PTok.parens lexer
45+semi = PTok.semi lexer
46+comma = PTok.comma lexer
47+identifier = PTok.identifier lexer
48+reserved = PTok.reserved lexer
49+operator = PTok.operator lexer
50+reservedOp = PTok.reservedOp lexer
51+integer = PTok.integer lexer
52+float = PTok.float lexer
53+strlit = PTok.stringLiteral lexer
54+chlit = PTok.charLiteral lexer
55+lchar = lexeme.char
5656
5757-- Loading modules
5858
@@ -62,7 +62,7 @@ loadModule f
6262 ibcsd <- valIBCSubDir i
6363 ids <- allImportDirs i
6464 fp <- liftIO $ findImport ids ibcsd f
65− if (f `elem` imported i)
65+ if f `elem` imported i
6666 then iLOG $ "Already read " ++ f
6767 else do putIState (i { imported = f : imported i })
6868 case fp of
@@ -91,7 +91,7 @@ loadSource lidr f
9191 putIState (i { default_access = Hidden })
9292 mapM_ loadModule modules
9393 clearIBC -- start a new .ibc file
94− mapM_ (\m -> addIBC (IBCImport m)) modules
94+ mapM_ (addIBC . IBCImport) modules
9595 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
9696 f rest pos
9797 let ds = namespaces mname ds'
@@ -126,10 +126,10 @@ addHides :: [(Name, Maybe Accessibility)] -> Idris ()
126126addHides xs = do i <- getIState
127127 let defh = default_access i
128128 let (hs, as) = partition isNothing xs
129− if null as then return ()
130− else mapM_ doHide
131− (map (\ (n, _) -> (n, defh)) hs ++
132− map (\ (n, Just a) -> (n, a)) as)
129+ unless (null as) $
130+ mapM_ doHide
131+ (map (\ (n, _) -> (n, defh)) hs ++
132+ map (\ (n, Just a) -> (n, a)) as)
133133 where isNothing (_, Nothing) = True
134134 isNothing _ = False
135135
@@ -141,123 +141,121 @@ parseTac i = runParser (do t <- pTactic defaultSyntax
141141 eof
142142 return t) i "(proof)"
143143
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
149+
144150parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
145151parseImports fname input
146152 = do i <- get
147− case (runParser (do whiteSpace
148− mname <- pHeader
149− ps <- many pImport
150− rest <- getInput
151− pos <- getPosition
152− return ((mname, ps, rest, pos), i)) i fname input) of
153− Left err -> fail (show err)
154− Right (x, i) -> do put i
155− return x
156− where ishow err = let ln = sourceLine (errorPos err) in
157− fname ++ ":" ++ show ln ++ ":parse error"
158−-- ++ show (map messageString (errorMessages err))
153+ case runParser (do whiteSpace
154+ mname <- pHeader
155+ ps <- many pImport
156+ rest <- getInput
157+ pos <- getPosition
158+ return ((mname, ps, rest, pos), i)) i fname input of
159+ Left err -> fail (iShowError fname err)
160+ Right (x, i) -> do put i
161+ return x
159162
160163pHeader :: IParser [String]
161164pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
162165 return (parseName i))
163166 <|> return []
164167 where parseName x = case span (/='.') x of
165− (x, "") -> [x]
166− (x, '.':y) -> x : parseName y
168+ (x, "") -> [x]
169+ (x, '.':y) -> x : parseName y
167170
168−push_indent :: IParser ()
169−push_indent = do pos <- getPosition
170− ist <- getState
171− setState (ist { indent_stack = sourceColumn pos :
171+pushIndent :: IParser ()
172+pushIndent = do pos <- getPosition
173+ ist <- getState
174+ setState (ist { indent_stack = sourceColumn pos :
172175 indent_stack ist })
173176
174−last_indent :: IParser Int
175−last_indent = do ist <- getState
176− case indent_stack ist of
177− (x : xs) -> return x
178− _ -> return 1
177+lastIndent :: IParser Int
178+lastIndent = do ist <- getState
179+ case indent_stack ist of
180+ (x : xs) -> return x
181+ _ -> return 1
179182
180183indent :: IParser Int
181−indent = do pos <- getPosition
182− return (sourceColumn pos)
184+indent = liftM sourceColumn getPosition
183185
184−pop_indent :: IParser ()
185−pop_indent = do ist <- getState
186− let (x : xs) = indent_stack ist
187− setState (ist { indent_stack = xs })
186+popIndent :: IParser ()
187+popIndent = do ist <- getState
188+ let (x : xs) = indent_stack ist
189+ setState (ist { indent_stack = xs })
188190
189−open_block :: IParser ()
190−open_block = do lchar '{'
191− ist <- getState
192− setState (ist { brace_stack = Nothing : brace_stack ist })
191+openBlock :: IParser ()
192+openBlock = do lchar '{'
193+ ist <- getState
194+ setState (ist { brace_stack = Nothing : brace_stack ist })
193195 <|> do ist <- getState
194196 lvl <- indent
195197 setState (ist { brace_stack = Just lvl : brace_stack ist })
196198
197−close_block :: IParser ()
198−close_block = do ist <- getState
199− bs <- case brace_stack ist of
200− Nothing : xs -> do lchar '}'
201− return xs
202− Just lvl : xs -> do i <- indent
203− inp <- getInput
199+closeBlock :: IParser ()
200+closeBlock = do ist <- getState
201+ bs <- case brace_stack ist of
202+ Nothing : xs -> do lchar '}'
203+ return xs
204+ Just lvl : xs -> do i <- indent
205+ inp <- getInput
204206-- trace (show (take 10 inp, i, lvl)) $
205− if (i >= lvl && take 1 inp /= ")")
206− then fail "Not end of block"
207− else return xs
208− setState (ist { brace_stack = bs })
209−
210−pTerminator = do lchar ';'; pop_indent
211− <|> do c <- indent; l <- last_indent
212− if (c <= l) then pop_indent
213− else fail "Not a terminator"
214− <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
215− else fail "Not a terminator"
207+ if i >= lvl && take 1 inp /= ")"
208+ then fail "Not end of block"
209+ else return xs
210+ setState (ist { brace_stack = bs })
211+
212+pTerminator = do lchar ';'; popIndent
213+ <|> do c <- indent; l <- lastIndent
214+ if c <= l
215+ then popIndent
216+ else fail "Not a terminator"
217+ <|> do i <- getInput
218+ if "}" `isPrefixOf` i || ")" `isPrefixOf` i
219+ then popIndent
220+ else fail "Not a terminator"
216221 <|> lookAhead eof
217222
218223pBarTerminator
219224 = do lchar '|'; return ()
220− <|> do c <- indent; l <- last_indent
221− if (c <= l) then return ()
222− else fail "Not a terminator"
225+ <|> do c <- indent; l <- lastIndent
226+ unless (c <= l) $ fail "Not a terminator"
223227 <|> lookAhead eof
224228
225229pKeepTerminator
226230 = do lchar ';'; return ()
227− <|> do c <- indent; l <- last_indent
228− if (c <= l) then return ()
229− else fail "Not a terminator"
230− <|> do i <- getInput; let h = take 1 i
231− if (h == "}" || h == ")" || h == "|") then return ()
232− else fail "Not a terminator"
231+ <|> do c <- indent; l <- lastIndent
232+ unless (c <= l) $ fail "Not a terminator"
233+ <|> do i <- getInput
234+ let h = take 1 i
235+ unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
233236 <|> lookAhead eof
234237
235−notEndApp = do c <- indent; l <- last_indent
238+notEndApp = do c <- indent; l <- lastIndent
236239 i <- getInput
237− if (c <= l) then fail "Terminator"
238− else return ()
240+ when (c <= l) $ fail "Terminator"
239241
240242notEndBlock = do ist <- getState
241243 case brace_stack ist of
242− Just lvl : xs -> do i <- indent
244+ Just lvl : xs -> do i <- indent
243245 inp <- getInput
244− if (i < lvl || take 1 inp == ")")
245− then fail "End of block"
246− else return ()
247− _ -> return ()
246+ when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
247+ _ -> return ()
248248
249249pfc :: IParser FC
250250pfc = do s <- getPosition
251251 let (dir, file) = splitFileName (sourceName s)
252252 let f = case dir of
253− "./" -> file
254− _ -> sourceName s
253+ "./" -> file
254+ _ -> sourceName s
255255 return $ FC f (sourceLine s)
256256
257257pImport :: IParser String
258−pImport = do reserved "import"
259− f <- identifier
260− option ';' (lchar ';')
258+pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
261259 return (map dot f)
262260 where dot '.' = '/'
263261 dot c = c
@@ -265,19 +263,15 @@ pImport = do reserved "import"
265263parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
266264parseProg syn fname input pos
267265 = do i <- get
268− case (runParser (do setPosition pos
269− whiteSpace
270− ps <- many (pDecl syn)
271− eof
272− i' <- getState
273− return (concat ps, i')) i fname input) of
274− Left err -> fail (ishow err)
266+ case runParser (do setPosition pos
267+ whiteSpace
268+ ps <- many (pDecl syn)
269+ eof
270+ i' <- getState
271+ return (concat ps, i')) i fname input of
272+ Left err -> fail (iShowError fname err)
275273 Right (x, i) -> do put i
276274 return (collect x)
277− where ishow err = let ln = sourceLine (errorPos err) in
278− fname ++ ":" ++ show ln ++ ":parse error"
279− ++ " at column " ++ show (sourceColumn (errorPos err))
280−-- show (map messageString (errorMessages err))
281275
282276-- Collect PClauses with the same function name
283277
@@ -323,8 +317,7 @@ pDecl syn = do notEndBlock
323317 <|> pInstance syn
324318 <|> do d <- pDSL syn; return [d]
325319 <|> pDirective
326− <|> try (do reserved "import"
327− fp <- identifier
320+ <|> try (do reserved "import"; fp <- identifier
328321 fail "imports must be at the top of file")
329322
330323pFunDecl :: SyntaxInfo -> IParser [PDecl]
@@ -366,7 +359,7 @@ pSyntaxDecl syn
366359
367360pSyntaxRule :: SyntaxInfo -> IParser Syntax
368361pSyntaxRule syn
369− = do push_indent
362+ = do pushIndent
370363 sty <- option AnySyntax (do reserved "term"; return TermSyntax
371364 <|> do reserved "pattern"; return PatternSyntax)
372365 reserved "syntax"
@@ -406,7 +399,7 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
406399 return (Symbol sym)
407400
408401pFunDecl' :: SyntaxInfo -> IParser PDecl
409−pFunDecl' syn = try (do push_indent
402+pFunDecl' syn = try (do pushIndent
410403 opts <- pFnOpts
411404 acc <- pAccessibility
412405 opts' <- pFnOpts
@@ -422,22 +415,16 @@ pFunDecl' syn = try (do push_indent
422415
423416pUsing :: SyntaxInfo -> IParser [PDecl]
424417pUsing syn =
425− do reserved "using";
426− lchar '('
427− ns <- tyDeclList syn
428− lchar ')'
429− open_block
418+ do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'
419+ openBlock
430420 let uvars = using syn
431421 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
432− close_block
422+ closeBlock
433423 return (concat ds)
434424
435425pParams :: SyntaxInfo -> IParser [PDecl]
436426pParams syn =
437− do reserved "params";
438− lchar '('
439− ns <- tyDeclList syn
440− lchar ')'
427+ do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'
441428 lchar '{'
442429 let pvars = syn_params syn
443430 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
@@ -447,17 +434,16 @@ pParams syn =
447434
448435pNamespace :: SyntaxInfo -> IParser [PDecl]
449436pNamespace syn =
450− do reserved "namespace";
451− n <- identifier
452− open_block
437+ do reserved "namespace"; n <- identifier;
438+ openBlock
453439 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
454− close_block
440+ closeBlock
455441 return [PNamespace n (concat ds)]
456442
457443--------- Fixity ---------
458444
459445pFixity :: IParser PDecl
460−pFixity = do push_indent
446+pFixity = do pushIndent
461447 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
462448 pTerminator
463449 let prec = fromInteger i
@@ -479,14 +465,12 @@ fixity = try (do reserved "infixl"; return Infixl)
479465
480466pClass :: SyntaxInfo -> IParser [PDecl]
481467pClass syn = do acc <- pAccessibility
482− reserved "class"
483− fc <- pfc
484− cons <- pConstList syn
485− n_in <- pName; let n = expandNS syn n_in
468+ reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
469+ let n = expandNS syn n_in
486470 cs <- many1 carg
487− reserved "where"; open_block
471+ reserved "where"; openBlock
488472 ds <- many $ pFunDecl syn
489− close_block
473+ closeBlock
490474 let allDs = concat ds
491475 accData acc n (concatMap declared allDs)
492476 return [PClass syn fc cons n cs allDs]
@@ -497,8 +481,7 @@ pClass syn = do acc <- pAccessibility
497481 return (i, PSet)
498482
499483pInstance :: SyntaxInfo -> IParser [PDecl]
500−pInstance syn = do reserved "instance"
501− fc <- pfc
484+pInstance syn = do reserved "instance"; fc <- pfc
502485 en <- option Nothing
503486 (do lchar '['; n_in <- pfName; lchar ']'
504487 let n = expandNS syn n_in
@@ -508,9 +491,9 @@ pInstance syn = do reserved "instance"
508491 args <- many1 (pSimpleExpr syn)
509492 let sc = PApp fc (PRef fc cn) (map pexp args)
510493 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
511− reserved "where"; open_block
494+ reserved "where"; openBlock
512495 ds <- many $ pFunDecl syn
513− close_block
496+ closeBlock
514497 return [PInstance syn fc cs cn args t en (concat ds)]
515498
516499--------- Expressions ---------
@@ -535,7 +518,7 @@ pSimpleExtExpr syn = do i <- getState
535518 simple (Rule (SimpleExpr x:xs) _ _) = False
536519 simple (Rule [Keyword _] _ _) = True
537520 simple (Rule [Symbol _] _ _) = True
538− simple (Rule (_:xs) _ _) = case (last xs) of
521+ simple (Rule (_:xs) _ _) = case last xs of
539522 Keyword _ -> True
540523 Symbol _ -> True
541524 _ -> False
@@ -552,7 +535,7 @@ pNoExtExpr syn =
552535 <|> pComprehension syn
553536
554537pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
555−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))
556539 where
557540 valid (Rule _ _ AnySyntax) = True
558541 valid (Rule _ _ PatternSyntax) = inPattern syn
@@ -649,41 +632,56 @@ addAcc :: Name -> Maybe Accessibility -> IParser ()
649632addAcc n a = do i <- getState
650633 setState (i { hide_list = (n, a) : hide_list i })
651634
635+pCaseExpr syn = do
636+ reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
637+ openBlock
638+ pushIndent
639+ opts <- many1 (do notEndBlock
640+ x <- pCaseOpt syn
641+ pKeepTerminator
642+ return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
643+ popIndent
644+ closeBlock
645+ return (PCase fc scr opts)
646+
647+pProofExpr syn = do
648+ reserved "proof"; lchar '{'
649+ ts <- endBy (pTactic syn) (lchar ';')
650+ lchar '}'
651+ return (PProof ts)
652+
653+pTacticsExpr syn = do
654+ reserved "tactics"; lchar '{'
655+ ts <- endBy (pTactic syn) (lchar ';')
656+ lchar '}'
657+ return (PTactics ts)
658+
652659pSimpleExpr syn =
653− try (do symbol "!["; t <- pTerm; lchar ']'
654− return $ PQuote t)
660+ try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
655661 <|> do lchar '?'; x <- pName; return (PMetavar x)
656662 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
657663-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
658− <|> do reserved "proof"; lchar '{';
659− ts <- endBy (pTactic syn) (lchar ';')
660− lchar '}'
661− return (PProof ts)
662− <|> do reserved "tactics"; lchar '{';
663− ts <- endBy (pTactic syn) (lchar ';')
664− lchar '}'
665− return (PTactics ts)
666− <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
667− open_block
668− push_indent
669− opts <- many1 (do notEndBlock
670− x <- pCaseOpt syn
671− pKeepTerminator
672− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
673− pop_indent
674− close_block
675− return (PCase fc scr opts)
676− <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
664+ <|> pProofExpr syn
665+ <|> pTacticsExpr syn
666+ <|> pCaseExpr syn
667+ <|> try (do x <- pfName
668+ fc <- pfc
669+ return (PRef fc x))
677670 <|> try (pList syn)
678671 <|> try (pAlt syn)
679672 <|> try (pIdiom syn)
680− <|> try (do lchar '('; bracketed (noImp syn))
681− <|> try (do c <- pConstant; fc <- pfc
673+ <|> try (do lchar '('
674+ bracketed (noImp syn))
675+ <|> try (do c <- pConstant
676+ fc <- pfc
682677 return (modifyConst syn fc (PConstant c)))
683678 <|> do reserved "Set"; return PSet
684−-- <|> do symbol "*"; return PSet
685− <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
686− <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
679+ <|> try (do symbol "()"
680+ fc <- pfc
681+ return (PTrue fc))
682+ <|> try (do symbol "_|_"
683+ fc <- pfc
684+ return (PFalse fc))
687685 <|> do lchar '_'; return Placeholder
688686 <|> pSimpleExtExpr syn
689687
@@ -703,8 +701,7 @@ bracketed syn =
703701 pexp (PRef fc (MN 0 "x"))]))
704702
705703pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
706−pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
707− rhs <- pExpr syn
704+pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn
708705 return (lhs, rhs)
709706
710707modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
@@ -714,8 +711,7 @@ modifyConst syn fc (PConstant (I x))
714711 | otherwise = PConstant (I x)
715712modifyConst syn fc x = x
716713
717−pList syn = do lchar '['; fc <- pfc
718− xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
714+pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
719715 return (mkList fc xs)
720716 where
721717 mkList fc [] = PRef fc (UN "Nil")
@@ -731,10 +727,12 @@ pPair syn = try (do l <- pExpr syn
731727 <|> try (do x <- ntuple
732728 lchar ')'
733729 return x)
734− <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
735− reservedOp "**";
730+ <|> do ln <- pName; lchar ':'
731+ lty <- pExpr syn
732+ reservedOp "**"
736733 fc <- pfc
737− r <- pExpr syn; lchar ')';
734+ r <- pExpr syn
735+ lchar ')'
738736 return (PDPair fc (PRef fc ln) lty r)
739737 where
740738 restTuple = do lchar ')'; return []
@@ -753,9 +751,7 @@ pPair syn = try (do l <- pExpr syn
753751 r <- pExpr syn
754752 return (PPair fc l r))
755753
756−pAlt syn = do symbol "(|";
757− alts <- sepBy1 (pExpr' syn) (lchar ',')
758− symbol "|)"
754+pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
759755 return (PAlternative False alts)
760756
761757pHSimpleExpr syn
@@ -782,13 +778,17 @@ pArg syn = try (pImplicitArg syn)
782778 <|> do e <- pSimpleExpr syn
783779 return (pexp e)
784780
785−pImplicitArg syn = do lchar '{'; n <- pName
781+pImplicitArg syn = do lchar '{'
782+ n <- pName
786783 fc <- pfc
787− v <- option (PRef fc n) (do lchar '='; pExpr syn)
784+ v <- option (PRef fc n) (do lchar '='
785+ pExpr syn)
788786 lchar '}'
789787 return (pimp n v)
790788
791−pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
789+pConstraintArg syn = do symbol "@{"
790+ e <- pExpr syn
791+ symbol "}"
792792 return (pconst e)
793793
794794pRecordSet syn
@@ -797,13 +797,15 @@ pRecordSet syn
797797 fields <- sepBy1 pFieldSet (lchar ',')
798798 lchar '}'
799799 fc <- pfc
800− rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))
800+ rec <- option Nothing (do e <- pSimpleExpr syn
801+ return (Just e))
801802 case rec of
802803 Nothing ->
803804 return (PLam (MN 0 "fldx") Placeholder
804805 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
805806 Just v -> return (applyAll fc fields v)
806− where pFieldSet = do n <- pfName; lchar '='
807+ where pFieldSet = do n <- pfName
808+ lchar '='
807809 e <- pExpr syn
808810 return (n, e)
809811 applyAll fc [] x = x
@@ -823,10 +825,10 @@ pTSig syn = do lchar ':'
823825 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
824826
825827pLambda syn = do lchar '\\'
826− (try (do xt <- tyOptDeclList syn
827− symbol "=>"
828− sc <- pExpr syn
829− return (bindList PLam xt sc))
828+ try (do xt <- tyOptDeclList syn
829+ symbol "=>"
830+ sc <- pExpr syn
831+ return (bindList PLam xt sc)
830832 <|> (do ps <- sepBy (do fc <- pfc
831833 e <- pSimpleExpr syn
832834 return (fc, e)) (lchar ',')
@@ -837,11 +839,12 @@ pLambda syn = do lchar '\\'
837839 pmList ((i, (fc, x)) : xs) sc
838840 = PLam (MN i "lamp") Placeholder
839841 (PCase fc (PRef fc (MN i "lamp"))
840− [(x, (pmList xs sc))])
842+ [(x, pmList xs sc)])
841843
842844pLet syn = try (do reserved "let"; n <- pName;
843845 ty <- option Placeholder (do lchar ':'; pExpr' syn)
844− lchar '='; v <- pExpr syn
846+ lchar '='
847+ v <- pExpr syn
845848 reserved "in"; sc <- pExpr syn
846849 return (PLet n ty v sc))
847850 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
@@ -856,27 +859,36 @@ pPi syn =
856859 symbol "->"
857860 sc <- pExpr syn
858861 return (bindList (PPi (Exp lazy st)) xt sc))
859− <|> try (if implicitAllowed syn then
860− do lazy <- option False (do lchar '|'; return True)
861− st <- pStatic
862− lchar '{'; xt <- tyDeclList syn; lchar '}'
863− symbol "->"
864− sc <- pExpr syn
865− return (bindList (PPi (Imp lazy st)) xt sc)
862+ <|> try (if implicitAllowed syn
863+ then do lazy <- option False (do lchar '|'
864+ return True)
865+ st <- pStatic
866+ lchar '{'
867+ xt <- tyDeclList syn
868+ lchar '}'
869+ symbol "->"
870+ sc <- pExpr syn
871+ return (bindList (PPi (Imp lazy st)) xt sc)
866872 else fail "No implicit arguments allowed here")
867− <|> try (do lchar '{'; reserved "auto"
868− xt <- tyDeclList syn; lchar '}'
873+ <|> try (do lchar '{'
874+ reserved "auto"
875+ xt <- tyDeclList syn
876+ lchar '}'
869877 symbol "->"
870878 sc <- pExpr syn
871879 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
872− <|> try (do lchar '{'; reserved "default"
880+ <|> try (do lchar '{'
881+ reserved "default"
873882 script <- pSimpleExpr syn
874− xt <- tyDeclList syn; lchar '}'
883+ xt <- tyDeclList syn
884+ lchar '}'
875885 symbol "->"
876886 sc <- pExpr syn
877887 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
878888 <|> do --lazy <- option False (do lchar '|'; return True)
879− lchar '{'; reserved "static"; lchar '}'
889+ lchar '{'
890+ reserved "static"
891+ lchar '}'
880892 t <- pExpr' syn
881893 symbol "->"
882894 sc <- pExpr syn
@@ -893,7 +905,9 @@ pConstList syn = try (do lchar '('
893905 return [t])
894906 <|> return []
895907
896−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)
910+ return (x,t))
897911 (lchar ','))
898912 <|> do ns <- sepBy1 pName (lchar ',')
899913 t <- pTSig (noImp syn)
@@ -909,8 +923,12 @@ bindList b [] sc = sc
909923bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
910924
911925pComprehension syn
912− = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
913− qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';
926+ = do lchar '['
927+ fc <- pfc
928+ pat <- pExpr syn
929+ lchar '|'
930+ qs <- sepBy1 (pDo syn) (lchar ',')
931+ lchar ']'
914932 return (PDoBlock (map addGuard qs ++
915933 [DoExp fc (PApp fc (PRef fc (UN "return"))
916934 [pexp pat])]))
@@ -919,34 +937,51 @@ pComprehension syn
919937 addGuard x = x
920938
921939pDoBlock syn
922− = do reserved "do"; open_block
923− push_indent
940+ = do reserved "do"
941+ openBlock
942+ pushIndent
924943 ds <- many1 (do notEndBlock
925− x <- pDo syn; pKeepTerminator; return x)
926− pop_indent
927− close_block
944+ x <- pDo syn
945+ pKeepTerminator
946+ return x)
947+ popIndent
948+ closeBlock
928949 return (PDoBlock ds)
929950
930951pDo syn
931− = try (do reserved "let"; i <- pName;
932− ty <- option Placeholder (do lchar ':'; pExpr' syn)
933− reservedOp "="; fc <- pfc
952+ = try (do reserved "let"
953+ i <- pName;
954+ ty <- option Placeholder (do lchar ':'
955+ pExpr' syn)
956+ reservedOp "="
957+ fc <- pfc
934958 e <- pExpr syn
935959 return (DoLet fc i ty e))
936− <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
960+ <|> try (do reserved "let"
961+ i <- pExpr' syn
962+ reservedOp "="
963+ fc <- pfc
937964 sc <- pExpr syn
938965 return (DoLetP fc i sc))
939− <|> try (do i <- pName; symbol "<-"; fc <- pfc
966+ <|> try (do i <- pName
967+ symbol "<-"
968+ fc <- pfc
940969 e <- pExpr syn;
941970 return (DoBind fc i e))
942− <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
971+ <|> try (do i <- pExpr' syn
972+ symbol "<-"
973+ fc <- pfc
943974 e <- pExpr syn;
944975 return (DoBindP fc i e))
945− <|> try (do e <- pExpr syn; fc <- pfc
976+ <|> try (do e <- pExpr syn
977+ fc <- pfc
946978 return (DoExp fc e))
947979
948980pIdiom syn
949− = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
981+ = do symbol "[|"
982+ fc <- pfc
983+ e <- pExpr syn
984+ symbol "|]"
950985 return (PIdiom fc e)
951986
952987pConstant :: IParser Const
@@ -963,7 +998,9 @@ pConstant = do reserved "Integer";return BIType
963998 <|> try (do c <- chlit; return $ Ch c)
964999
9651000pStatic :: IParser Static
966−pStatic = do lchar '['; reserved "static"; lchar ']';
1001+pStatic = do lchar '['
1002+ reserved "static"
1003+ lchar ']';
9671004 return Static
9681005 <|> return Dynamic
9691006
@@ -972,7 +1009,7 @@ table fixes
9721009 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
9731010 ++ toTable (reverse fixes) ++
9741011 [[backtick],
975− [binary "=" (\fc x y -> PEq fc x y) AssocLeft],
1012+ [binary "=" PEq AssocLeft],
9761013 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
9771014
9781015toTable fs = map (map toBin)
@@ -985,11 +1022,14 @@ toTable fs = map (map toBin)
9851022 assoc (Infixr _) = AssocRight
9861023 assoc (InfixN _) = AssocNone
9871024
988−binary name f assoc = Infix (do reservedOp name; fc <- pfc;
989− return (f fc)) assoc
990−prefix name f = Prefix (do reservedOp name; fc <- pfc;
1025+binary name f = Infix (do reservedOp name
1026+ fc <- pfc;
1027+ return (f fc))
1028+prefix name f = Prefix (do reservedOp name
1029+ fc <- pfc;
9911030 return (f fc))
992−backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
1031+backtick = Infix (do lchar '`'; n <- pfName
1032+ lchar '`'
9931033 fc <- pfc
9941034 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
9951035
@@ -999,20 +1039,23 @@ backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
9991039accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
10001040accData (Just Frozen) n ns = do addAcc n (Just Frozen)
10011041 mapM_ (\n -> addAcc n (Just Hidden)) ns
1002−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
10031044
10041045pRecord :: SyntaxInfo -> IParser PDecl
10051046pRecord syn = do acc <- pAccessibility
1006− reserved "record"; fc <- pfc
1007− tyn_in <- pfName; ty <- pTSig (impOK syn)
1047+ reserved "record"
1048+ fc <- pfc
1049+ tyn_in <- pfName
1050+ ty <- pTSig (impOK syn)
10081051 let tyn = expandNS syn tyn_in
10091052 reserved "where"
1010− open_block
1011− push_indent
1053+ openBlock
1054+ pushIndent
10121055 (cn, cty, _) <- pConstructor syn
10131056 pKeepTerminator
1014− pop_indent
1015− close_block
1057+ popIndent
1058+ closeBlock
10161059 accData acc tyn [cn]
10171060 let rsyn = syn { syn_namespace = show (nsroot tyn) :
10181061 syn_namespace syn }
@@ -1029,30 +1072,34 @@ pRecord syn = do acc <- pAccessibility
10291072
10301073pData :: SyntaxInfo -> IParser PDecl
10311074pData syn = try (do acc <- pAccessibility
1032− reserved "data"; fc <- pfc
1033− tyn_in <- pfName; ty <- pTSig (impOK syn)
1075+ reserved "data"
1076+ fc <- pfc
1077+ tyn_in <- pfName
1078+ ty <- pTSig (impOK syn)
10341079 let tyn = expandNS syn tyn_in
10351080 reserved "where"
1036− open_block
1037− push_indent
1081+ openBlock
1082+ pushIndent
10381083 cons <- many (do notEndBlock
10391084 c <- pConstructor syn
10401085 pKeepTerminator
10411086 return c) -- (lchar '|')
1042− pop_indent
1043− close_block
1087+ popIndent
1088+ closeBlock
10441089 accData acc tyn (map (\ (n, _, _) -> n) cons)
10451090 return $ PData syn fc (PDatadecl tyn ty cons))
1046− <|> try (do push_indent
1091+ <|> try (do pushIndent
10471092 acc <- pAccessibility
1048− reserved "data"; fc <- pfc
1049− tyn_in <- pfName; args <- many pName
1093+ reserved "data"
1094+ fc <- pfc
1095+ tyn_in <- pfName
1096+ args <- many pName
10501097 let tyn = expandNS syn tyn_in
10511098 lchar '='
10521099 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
10531100 pTerminator
10541101 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1055− let ty = bindArgs (map (\a -> PSet) args) PSet
1102+ let ty = bindArgs (map (const PSet) args) PSet
10561103 cons' <- mapM (\ (x, cargs, cfc) ->
10571104 do let cty = bindArgs cargs conty
10581105 return (x, cty, cfc)) cons
@@ -1063,8 +1110,7 @@ pData syn = try (do acc <- pAccessibility
10631110 mkPApp fc t xs = PApp fc t (map pexp xs)
10641111
10651112bindArgs :: [PTerm] -> PTerm -> PTerm
1066−bindArgs [] t = t
1067−bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
1113+bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
10681114
10691115pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
10701116pConstructor syn
@@ -1087,13 +1133,15 @@ pSimpleCon syn
10871133--------- DSL syntax overloading ---------
10881134
10891135pDSL :: SyntaxInfo -> IParser PDecl
1090−pDSL syn = do reserved "dsl"; n <- pfName
1091− open_block; push_indent
1136+pDSL syn = do reserved "dsl"
1137+ n <- pfName
1138+ openBlock
1139+ pushIndent
10921140 bs <- many1 (do notEndBlock
10931141 b <- pOverload syn
10941142 pKeepTerminator
10951143 return b)
1096− pop_indent; close_block
1144+ popIndent; closeBlock
10971145 let dsl = mkDSL bs (dsl_info syn)
10981146 checkDSL dsl
10991147 i <- getState
@@ -1114,8 +1162,9 @@ checkDSL :: DSL -> IParser ()
11141162checkDSL dsl = return ()
11151163
11161164pOverload :: SyntaxInfo -> IParser (String, PTerm)
1117−pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1118− if (not (o `elem` overloadable))
1165+pOverload syn = do o <- identifier <|> do reserved "let"
1166+ return "let"
1167+ if o `notElem` overloadable
11191168 then fail $ show o ++ " is not an overloading"
11201169 else do
11211170 lchar '='
@@ -1144,7 +1193,7 @@ pRHS syn n = do lchar '='; pExpr syn
11441193
11451194pClause :: SyntaxInfo -> IParser PClause
11461195pClause syn
1147− = try (do push_indent
1196+ = try (do pushIndent
11481197 n_in <- pfName; let n = expandNS syn n_in
11491198 cargs <- many (pConstraintArg syn)
11501199 iargs <- many (pImplicitArg syn)
@@ -1156,7 +1205,7 @@ pClause syn
11561205 let ctxt = tt_ctxt ist
11571206 let wsyn = syn { syn_namespace = [] }
11581207 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1159− pop_indent
1208+ popIndent
11601209 return x,
11611210 do pTerminator
11621211 return ([], [])]
@@ -1165,7 +1214,7 @@ pClause syn
11651214 ist <- getState
11661215 setState (ist { lastParse = Just n })
11671216 return $ PClause fc n capp wargs rhs wheres)
1168− <|> try (do push_indent
1217+ <|> try (do pushIndent
11691218 wargs <- many1 (pWExpr syn)
11701219 ist <- getState
11711220 n <- case lastParse ist of
@@ -1176,13 +1225,13 @@ pClause syn
11761225 let ctxt = tt_ctxt ist
11771226 let wsyn = syn { syn_namespace = [] }
11781227 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1179− pop_indent
1228+ popIndent
11801229 return x,
11811230 do pTerminator
11821231 return ([], [])]
11831232 return $ PClauseR fc wargs rhs wheres)
11841233
1185− <|> try (do push_indent
1234+ <|> try (do pushIndent
11861235 n_in <- pfName; let n = expandNS syn n_in
11871236 cargs <- many (pConstraintArg syn)
11881237 iargs <- many (pImplicitArg syn)
@@ -1195,24 +1244,24 @@ pClause syn
11951244 setState (ist { lastParse = Just n })
11961245 reserved "with"
11971246 wval <- pSimpleExpr syn
1198− open_block
1247+ openBlock
11991248 ds <- many1 $ pFunDecl syn
12001249 let withs = map (fillLHSD n capp wargs) $ concat ds
1201− close_block
1202− pop_indent
1250+ closeBlock
1251+ popIndent
12031252 return $ PWith fc n capp wargs wval withs)
12041253
12051254 <|> try (do wargs <- many1 (pWExpr syn)
12061255 fc <- pfc
12071256 reserved "with"
12081257 wval <- pSimpleExpr syn
1209− open_block
1258+ openBlock
12101259 ds <- many1 $ pFunDecl syn
12111260 let withs = concat ds
1212− close_block
1261+ closeBlock
12131262 return $ PWithR fc wargs wval withs)
12141263
1215− <|> do push_indent
1264+ <|> do pushIndent
12161265 l <- pArgExpr syn
12171266 op <- operator
12181267 let n = expandNS syn (UN op)
@@ -1222,7 +1271,7 @@ pClause syn
12221271 rhs <- pRHS syn n
12231272 let wsyn = syn { syn_namespace = [] }
12241273 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1225− pop_indent
1274+ popIndent
12261275 return x,
12271276 do pTerminator
12281277 return ([], [])]
@@ -1239,9 +1288,9 @@ pClause syn
12391288 wargs <- many (pWExpr syn)
12401289 reserved "with"
12411290 wval <- pSimpleExpr syn
1242− open_block
1291+ openBlock
12431292 ds <- many1 $ pFunDecl syn
1244− close_block
1293+ closeBlock
12451294 ist <- getState
12461295 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
12471296 let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1259,14 +1308,15 @@ pClause syn
12591308 fillLHSD n c a x = x
12601309
12611310pWExpr :: SyntaxInfo -> IParser PTerm
1262−pWExpr syn = do lchar '|'; pExpr' syn
1311+pWExpr syn = do lchar '|'
1312+ pExpr' syn
12631313
12641314pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
12651315pWhereblock n syn
1266− = do reserved "where"; open_block
1316+ = do reserved "where"; openBlock
12671317 ds <- many1 $ pFunDecl syn
12681318 let dns = concatMap (concatMap declared) ds
1269− close_block
1319+ closeBlock
12701320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
12711321
12721322pDirective :: IParser [PDecl]
@@ -1274,7 +1324,7 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
12741324 return [PDirective (do addLib lib
12751325 addIBC (IBCLib lib))])
12761326 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1277− return [PDirective (do datadir <- liftIO $ getDataDir
1327+ return [PDirective (do datadir <- liftIO getDataDir
12781328 o <- liftIO $ findInPath [".", datadir] obj
12791329 addIBC (IBCObj o)
12801330 addObjectFile o)])