@@ -17,11 +17,12 @@ import Core.CoreParser
1717import Core.TT
1818import Core.Evaluate
1919
20−import Text.ParserCombinators.Parsec
21−import Text.ParserCombinators.Parsec.Error
22−import Text.ParserCombinators.Parsec.Expr
23−import Text.ParserCombinators.Parsec.Language
24−import qualified Text.ParserCombinators.Parsec.Token as PTok
20+import Text.Parsec
21+import Text.Parsec.Error
22+import Text.Parsec.Expr
23+import Text.Parsec.Language
24+import Text.Parsec.String
25+import qualified Text.Parsec.Token as PTok
2526
2627import Data.List
2728import Control.Monad.State
@@ -36,22 +37,22 @@ type IParser = GenParser Char IState
3637lexer :: TokenParser IState
3738lexer = PTok.makeTokenParser idrisDef
3839
39−whiteSpace= PTok.whiteSpace lexer
40−lexeme = PTok.lexeme lexer
41−symbol = PTok.symbol lexer
42−natural = PTok.natural lexer
43−parens = PTok.parens lexer
44−semi = PTok.semi lexer
45−comma = PTok.comma lexer
46−identifier= PTok.identifier lexer
47−reserved = PTok.reserved lexer
48−operator = PTok.operator lexer
49−reservedOp= PTok.reservedOp lexer
50−integer = PTok.integer lexer
51−float = PTok.float lexer
52−strlit = PTok.stringLiteral lexer
53−chlit = PTok.charLiteral lexer
54−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
5556
5657-- Loading modules
5758
@@ -61,7 +62,7 @@ loadModule f
6162 ibcsd <- valIBCSubDir i
6263 ids <- allImportDirs i
6364 fp <- liftIO $ findImport ids ibcsd f
64− if (f `elem` imported i)
65+ if f `elem` imported i
6566 then iLOG $ "Already read " ++ f
6667 else do putIState (i { imported = f : imported i })
6768 case fp of
@@ -90,7 +91,7 @@ loadSource lidr f
9091 putIState (i { default_access = Hidden })
9192 mapM_ loadModule modules
9293 clearIBC -- start a new .ibc file
93− mapM_ (\m -> addIBC (IBCImport m)) modules
94+ mapM_ (addIBC . IBCImport) modules
9495 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
9596 f rest pos
9697 let ds = namespaces mname ds'
@@ -125,10 +126,10 @@ addHides :: [(Name, Maybe Accessibility)] -> Idris ()
125126addHides xs = do i <- getIState
126127 let defh = default_access i
127128 let (hs, as) = partition isNothing xs
128− if null as then return ()
129− else mapM_ doHide
130− (map (\ (n, _) -> (n, defh)) hs ++
131− 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)
132133 where isNothing (_, Nothing) = True
133134 isNothing _ = False
134135
@@ -140,123 +141,121 @@ parseTac i = runParser (do t <- pTactic defaultSyntax
140141 eof
141142 return t) i "(proof)"
142143
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+
143150parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
144151parseImports fname input
145152 = do i <- get
146− case (runParser (do whiteSpace
147− mname <- pHeader
148− ps <- many pImport
149− rest <- getInput
150− pos <- getPosition
151− return ((mname, ps, rest, pos), i)) i fname input) of
152− Left err -> fail (show err)
153− Right (x, i) -> do put i
154− return x
155− where ishow err = let ln = sourceLine (errorPos err) in
156− fname ++ ":" ++ show ln ++ ":parse error"
157−-- ++ 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
158162
159163pHeader :: IParser [String]
160164pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
161165 return (parseName i))
162166 <|> return []
163167 where parseName x = case span (/='.') x of
164− (x, "") -> [x]
165− (x, '.':y) -> x : parseName y
168+ (x, "") -> [x]
169+ (x, '.':y) -> x : parseName y
166170
167−push_indent :: IParser ()
168−push_indent = do pos <- getPosition
169− ist <- getState
170− setState (ist { indent_stack = sourceColumn pos :
171+pushIndent :: IParser ()
172+pushIndent = do pos <- getPosition
173+ ist <- getState
174+ setState (ist { indent_stack = sourceColumn pos :
171175 indent_stack ist })
172176
173−last_indent :: IParser Int
174−last_indent = do ist <- getState
175− case indent_stack ist of
176− (x : xs) -> return x
177− _ -> 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
178182
179183indent :: IParser Int
180−indent = do pos <- getPosition
181− return (sourceColumn pos)
184+indent = liftM sourceColumn getPosition
182185
183−pop_indent :: IParser ()
184−pop_indent = do ist <- getState
185− let (x : xs) = indent_stack ist
186− 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 })
187190
188−open_block :: IParser ()
189−open_block = do lchar '{'
190− ist <- getState
191− 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 })
192195 <|> do ist <- getState
193196 lvl <- indent
194197 setState (ist { brace_stack = Just lvl : brace_stack ist })
195198
196−close_block :: IParser ()
197−close_block = do ist <- getState
198− bs <- case brace_stack ist of
199− Nothing : xs -> do lchar '}'
200− return xs
201− Just lvl : xs -> do i <- indent
202− 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
203206-- trace (show (take 10 inp, i, lvl)) $
204− if (i >= lvl && take 1 inp /= ")")
205− then fail "Not end of block"
206− else return xs
207− setState (ist { brace_stack = bs })
208−
209−pTerminator = do lchar ';'; pop_indent
210− <|> do c <- indent; l <- last_indent
211− if (c <= l) then pop_indent
212− else fail "Not a terminator"
213− <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
214− 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"
215221 <|> lookAhead eof
216222
217223pBarTerminator
218224 = do lchar '|'; return ()
219− <|> do c <- indent; l <- last_indent
220− if (c <= l) then return ()
221− else fail "Not a terminator"
225+ <|> do c <- indent; l <- lastIndent
226+ unless (c <= l) $ fail "Not a terminator"
222227 <|> lookAhead eof
223228
224229pKeepTerminator
225230 = do lchar ';'; return ()
226− <|> do c <- indent; l <- last_indent
227− if (c <= l) then return ()
228− else fail "Not a terminator"
229− <|> do i <- getInput; let h = take 1 i
230− if (h == "}" || h == ")" || h == "|") then return ()
231− 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"
232236 <|> lookAhead eof
233237
234−notEndApp = do c <- indent; l <- last_indent
238+notEndApp = do c <- indent; l <- lastIndent
235239 i <- getInput
236− if (c <= l) then fail "Terminator"
237− else return ()
240+ when (c <= l) $ fail "Terminator"
238241
239242notEndBlock = do ist <- getState
240243 case brace_stack ist of
241− Just lvl : xs -> do i <- indent
244+ Just lvl : xs -> do i <- indent
242245 inp <- getInput
243− if (i < lvl || take 1 inp == ")")
244− then fail "End of block"
245− else return ()
246− _ -> return ()
246+ when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
247+ _ -> return ()
247248
248249pfc :: IParser FC
249250pfc = do s <- getPosition
250251 let (dir, file) = splitFileName (sourceName s)
251252 let f = case dir of
252− "./" -> file
253− _ -> sourceName s
253+ "./" -> file
254+ _ -> sourceName s
254255 return $ FC f (sourceLine s)
255256
256257pImport :: IParser String
257−pImport = do reserved "import"
258− f <- identifier
259− option ';' (lchar ';')
258+pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
260259 return (map dot f)
261260 where dot '.' = '/'
262261 dot c = c
@@ -264,19 +263,15 @@ pImport = do reserved "import"
264263parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
265264parseProg syn fname input pos
266265 = do i <- get
267− case (runParser (do setPosition pos
268− whiteSpace
269− ps <- many (pDecl syn)
270− eof
271− i' <- getState
272− return (concat ps, i')) i fname input) of
273− 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)
274273 Right (x, i) -> do put i
275274 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))
280275
281276-- Collect PClauses with the same function name
282277
@@ -322,8 +317,7 @@ pDecl syn = do notEndBlock
322317 <|> pInstance syn
323318 <|> do d <- pDSL syn; return [d]
324319 <|> pDirective
325− <|> try (do reserved "import"
326− fp <- identifier
320+ <|> try (do reserved "import"; fp <- identifier
327321 fail "imports must be at the top of file")
328322
329323pFunDecl :: SyntaxInfo -> IParser [PDecl]
@@ -365,7 +359,7 @@ pSyntaxDecl syn
365359
366360pSyntaxRule :: SyntaxInfo -> IParser Syntax
367361pSyntaxRule syn
368− = do push_indent
362+ = do pushIndent
369363 sty <- option AnySyntax (do reserved "term"; return TermSyntax
370364 <|> do reserved "pattern"; return PatternSyntax)
371365 reserved "syntax"
@@ -405,7 +399,7 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
405399 return (Symbol sym)
406400
407401pFunDecl' :: SyntaxInfo -> IParser PDecl
408−pFunDecl' syn = try (do push_indent
402+pFunDecl' syn = try (do pushIndent
409403 opts <- pFnOpts
410404 acc <- pAccessibility
411405 opts' <- pFnOpts
@@ -421,22 +415,16 @@ pFunDecl' syn = try (do push_indent
421415
422416pUsing :: SyntaxInfo -> IParser [PDecl]
423417pUsing syn =
424− do reserved "using";
425− lchar '('
426− ns <- tyDeclList syn
427− lchar ')'
428− open_block
418+ do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'
419+ openBlock
429420 let uvars = using syn
430421 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
431− close_block
422+ closeBlock
432423 return (concat ds)
433424
434425pParams :: SyntaxInfo -> IParser [PDecl]
435426pParams syn =
436− do reserved "params";
437− lchar '('
438− ns <- tyDeclList syn
439− lchar ')'
427+ do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'
440428 lchar '{'
441429 let pvars = syn_params syn
442430 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
@@ -446,17 +434,16 @@ pParams syn =
446434
447435pNamespace :: SyntaxInfo -> IParser [PDecl]
448436pNamespace syn =
449− do reserved "namespace";
450− n <- identifier
451− open_block
437+ do reserved "namespace"; n <- identifier;
438+ openBlock
452439 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
453− close_block
440+ closeBlock
454441 return [PNamespace n (concat ds)]
455442
456443--------- Fixity ---------
457444
458445pFixity :: IParser PDecl
459−pFixity = do push_indent
446+pFixity = do pushIndent
460447 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
461448 pTerminator
462449 let prec = fromInteger i
@@ -478,14 +465,12 @@ fixity = try (do reserved "infixl"; return Infixl)
478465
479466pClass :: SyntaxInfo -> IParser [PDecl]
480467pClass syn = do acc <- pAccessibility
481− reserved "class"
482− fc <- pfc
483− cons <- pConstList syn
484− 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
485470 cs <- many1 carg
486− reserved "where"; open_block
471+ reserved "where"; openBlock
487472 ds <- many $ pFunDecl syn
488− close_block
473+ closeBlock
489474 let allDs = concat ds
490475 accData acc n (concatMap declared allDs)
491476 return [PClass syn fc cons n cs allDs]
@@ -496,8 +481,7 @@ pClass syn = do acc <- pAccessibility
496481 return (i, PSet)
497482
498483pInstance :: SyntaxInfo -> IParser [PDecl]
499−pInstance syn = do reserved "instance"
500− fc <- pfc
484+pInstance syn = do reserved "instance"; fc <- pfc
501485 en <- option Nothing
502486 (do lchar '['; n_in <- pfName; lchar ']'
503487 let n = expandNS syn n_in
@@ -507,9 +491,9 @@ pInstance syn = do reserved "instance"
507491 args <- many1 (pSimpleExpr syn)
508492 let sc = PApp fc (PRef fc cn) (map pexp args)
509493 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
510− reserved "where"; open_block
494+ reserved "where"; openBlock
511495 ds <- many $ pFunDecl syn
512− close_block
496+ closeBlock
513497 return [PInstance syn fc cs cn args t en (concat ds)]
514498
515499--------- Expressions ---------
@@ -534,7 +518,7 @@ pSimpleExtExpr syn = do i <- getState
534518 simple (Rule (SimpleExpr x:xs) _ _) = False
535519 simple (Rule [Keyword _] _ _) = True
536520 simple (Rule [Symbol _] _ _) = True
537− simple (Rule (_:xs) _ _) = case (last xs) of
521+ simple (Rule (_:xs) _ _) = case last xs of
538522 Keyword _ -> True
539523 Symbol _ -> True
540524 _ -> False
@@ -551,7 +535,7 @@ pNoExtExpr syn =
551535 <|> pComprehension syn
552536
553537pExtensions :: 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))
555539 where
556540 valid (Rule _ _ AnySyntax) = True
557541 valid (Rule _ _ PatternSyntax) = inPattern syn
@@ -648,41 +632,56 @@ addAcc :: Name -> Maybe Accessibility -> IParser ()
648632addAcc n a = do i <- getState
649633 setState (i { hide_list = (n, a) : hide_list i })
650634
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+
651659pSimpleExpr syn =
652− try (do symbol "!["; t <- pTerm; lchar ']'
653− return $ PQuote t)
660+ try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
654661 <|> do lchar '?'; x <- pName; return (PMetavar x)
655662 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
656663-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
657− <|> do reserved "proof"; lchar '{';
658− ts <- endBy (pTactic syn) (lchar ';')
659− lchar '}'
660− return (PProof ts)
661− <|> do reserved "tactics"; lchar '{';
662− ts <- endBy (pTactic syn) (lchar ';')
663− lchar '}'
664− return (PTactics ts)
665− <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
666− open_block
667− push_indent
668− opts <- many1 (do notEndBlock
669− x <- pCaseOpt syn
670− pKeepTerminator
671− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
672− pop_indent
673− close_block
674− return (PCase fc scr opts)
675− <|> 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))
676670 <|> try (pList syn)
677671 <|> try (pAlt syn)
678672 <|> try (pIdiom syn)
679− <|> try (do lchar '('; bracketed (noImp syn))
680− <|> try (do c <- pConstant; fc <- pfc
673+ <|> try (do lchar '('
674+ bracketed (noImp syn))
675+ <|> try (do c <- pConstant
676+ fc <- pfc
681677 return (modifyConst syn fc (PConstant c)))
682678 <|> do reserved "Set"; return PSet
683−-- <|> do symbol "*"; return PSet
684− <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
685− <|> 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))
686685 <|> do lchar '_'; return Placeholder
687686 <|> pSimpleExtExpr syn
688687
@@ -702,8 +701,7 @@ bracketed syn =
702701 pexp (PRef fc (MN 0 "x"))]))
703702
704703pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
705−pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
706− rhs <- pExpr syn
704+pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn
707705 return (lhs, rhs)
708706
709707modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
@@ -713,8 +711,7 @@ modifyConst syn fc (PConstant (I x))
713711 | otherwise = PConstant (I x)
714712modifyConst syn fc x = x
715713
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 ']'
718715 return (mkList fc xs)
719716 where
720717 mkList fc [] = PRef fc (UN "Nil")
@@ -730,10 +727,12 @@ pPair syn = try (do l <- pExpr syn
730727 <|> try (do x <- ntuple
731728 lchar ')'
732729 return x)
733− <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
734− reservedOp "**";
730+ <|> do ln <- pName; lchar ':'
731+ lty <- pExpr syn
732+ reservedOp "**"
735733 fc <- pfc
736− r <- pExpr syn; lchar ')';
734+ r <- pExpr syn
735+ lchar ')'
737736 return (PDPair fc (PRef fc ln) lty r)
738737 where
739738 restTuple = do lchar ')'; return []
@@ -752,9 +751,7 @@ pPair syn = try (do l <- pExpr syn
752751 r <- pExpr syn
753752 return (PPair fc l r))
754753
755−pAlt syn = do symbol "(|";
756− alts <- sepBy1 (pExpr' syn) (lchar ',')
757− symbol "|)"
754+pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
758755 return (PAlternative False alts)
759756
760757pHSimpleExpr syn
@@ -781,13 +778,17 @@ pArg syn = try (pImplicitArg syn)
781778 <|> do e <- pSimpleExpr syn
782779 return (pexp e)
783780
784−pImplicitArg syn = do lchar '{'; n <- pName
781+pImplicitArg syn = do lchar '{'
782+ n <- pName
785783 fc <- pfc
786− v <- option (PRef fc n) (do lchar '='; pExpr syn)
784+ v <- option (PRef fc n) (do lchar '='
785+ pExpr syn)
787786 lchar '}'
788787 return (pimp n v)
789788
790−pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
789+pConstraintArg syn = do symbol "@{"
790+ e <- pExpr syn
791+ symbol "}"
791792 return (pconst e)
792793
793794pRecordSet syn
@@ -796,13 +797,15 @@ pRecordSet syn
796797 fields <- sepBy1 pFieldSet (lchar ',')
797798 lchar '}'
798799 fc <- pfc
799− rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))
800+ rec <- option Nothing (do e <- pSimpleExpr syn
801+ return (Just e))
800802 case rec of
801803 Nothing ->
802804 return (PLam (MN 0 "fldx") Placeholder
803805 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
804806 Just v -> return (applyAll fc fields v)
805− where pFieldSet = do n <- pfName; lchar '='
807+ where pFieldSet = do n <- pfName
808+ lchar '='
806809 e <- pExpr syn
807810 return (n, e)
808811 applyAll fc [] x = x
@@ -822,10 +825,10 @@ pTSig syn = do lchar ':'
822825 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
823826
824827pLambda syn = do lchar '\\'
825− (try (do xt <- tyOptDeclList syn
826− symbol "=>"
827− sc <- pExpr syn
828− return (bindList PLam xt sc))
828+ try (do xt <- tyOptDeclList syn
829+ symbol "=>"
830+ sc <- pExpr syn
831+ return (bindList PLam xt sc)
829832 <|> (do ps <- sepBy (do fc <- pfc
830833 e <- pSimpleExpr syn
831834 return (fc, e)) (lchar ',')
@@ -836,11 +839,12 @@ pLambda syn = do lchar '\\'
836839 pmList ((i, (fc, x)) : xs) sc
837840 = PLam (MN i "lamp") Placeholder
838841 (PCase fc (PRef fc (MN i "lamp"))
839− [(x, (pmList xs sc))])
842+ [(x, pmList xs sc)])
840843
841844pLet syn = try (do reserved "let"; n <- pName;
842845 ty <- option Placeholder (do lchar ':'; pExpr' syn)
843− lchar '='; v <- pExpr syn
846+ lchar '='
847+ v <- pExpr syn
844848 reserved "in"; sc <- pExpr syn
845849 return (PLet n ty v sc))
846850 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
@@ -855,27 +859,36 @@ pPi syn =
855859 symbol "->"
856860 sc <- pExpr syn
857861 return (bindList (PPi (Exp lazy st)) xt sc))
858− <|> try (if implicitAllowed syn then
859− do lazy <- option False (do lchar '|'; return True)
860− st <- pStatic
861− lchar '{'; xt <- tyDeclList syn; lchar '}'
862− symbol "->"
863− sc <- pExpr syn
864− 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)
865872 else fail "No implicit arguments allowed here")
866− <|> try (do lchar '{'; reserved "auto"
867− xt <- tyDeclList syn; lchar '}'
873+ <|> try (do lchar '{'
874+ reserved "auto"
875+ xt <- tyDeclList syn
876+ lchar '}'
868877 symbol "->"
869878 sc <- pExpr syn
870879 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))
871− <|> try (do lchar '{'; reserved "default"
880+ <|> try (do lchar '{'
881+ reserved "default"
872882 script <- pSimpleExpr syn
873− xt <- tyDeclList syn; lchar '}'
883+ xt <- tyDeclList syn
884+ lchar '}'
874885 symbol "->"
875886 sc <- pExpr syn
876887 return (bindList (PPi (TacImp False Dynamic script)) xt sc))
877888 <|> do --lazy <- option False (do lchar '|'; return True)
878− lchar '{'; reserved "static"; lchar '}'
889+ lchar '{'
890+ reserved "static"
891+ lchar '}'
879892 t <- pExpr' syn
880893 symbol "->"
881894 sc <- pExpr syn
@@ -892,7 +905,9 @@ pConstList syn = try (do lchar '('
892905 return [t])
893906 <|> return []
894907
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)
910+ return (x,t))
896911 (lchar ','))
897912 <|> do ns <- sepBy1 pName (lchar ',')
898913 t <- pTSig (noImp syn)
@@ -908,8 +923,12 @@ bindList b [] sc = sc
908923bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
909924
910925pComprehension syn
911− = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
912− 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 ']'
913932 return (PDoBlock (map addGuard qs ++
914933 [DoExp fc (PApp fc (PRef fc (UN "return"))
915934 [pexp pat])]))
@@ -918,34 +937,51 @@ pComprehension syn
918937 addGuard x = x
919938
920939pDoBlock syn
921− = do reserved "do"; open_block
922− push_indent
940+ = do reserved "do"
941+ openBlock
942+ pushIndent
923943 ds <- many1 (do notEndBlock
924− x <- pDo syn; pKeepTerminator; return x)
925− pop_indent
926− close_block
944+ x <- pDo syn
945+ pKeepTerminator
946+ return x)
947+ popIndent
948+ closeBlock
927949 return (PDoBlock ds)
928950
929951pDo syn
930− = try (do reserved "let"; i <- pName;
931− ty <- option Placeholder (do lchar ':'; pExpr' syn)
932− 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
933958 e <- pExpr syn
934959 return (DoLet fc i ty e))
935− <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
960+ <|> try (do reserved "let"
961+ i <- pExpr' syn
962+ reservedOp "="
963+ fc <- pfc
936964 sc <- pExpr syn
937965 return (DoLetP fc i sc))
938− <|> try (do i <- pName; symbol "<-"; fc <- pfc
966+ <|> try (do i <- pName
967+ symbol "<-"
968+ fc <- pfc
939969 e <- pExpr syn;
940970 return (DoBind fc i e))
941− <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
971+ <|> try (do i <- pExpr' syn
972+ symbol "<-"
973+ fc <- pfc
942974 e <- pExpr syn;
943975 return (DoBindP fc i e))
944− <|> try (do e <- pExpr syn; fc <- pfc
976+ <|> try (do e <- pExpr syn
977+ fc <- pfc
945978 return (DoExp fc e))
946979
947980pIdiom syn
948− = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
981+ = do symbol "[|"
982+ fc <- pfc
983+ e <- pExpr syn
984+ symbol "|]"
949985 return (PIdiom fc e)
950986
951987pConstant :: IParser Const
@@ -962,7 +998,9 @@ pConstant = do reserved "Integer";return BIType
962998 <|> try (do c <- chlit; return $ Ch c)
963999
9641000pStatic :: IParser Static
965−pStatic = do lchar '['; reserved "static"; lchar ']';
1001+pStatic = do lchar '['
1002+ reserved "static"
1003+ lchar ']';
9661004 return Static
9671005 <|> return Dynamic
9681006
@@ -971,7 +1009,7 @@ table fixes
9711009 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
9721010 ++ toTable (reverse fixes) ++
9731011 [[backtick],
974− [binary "=" (\fc x y -> PEq fc x y) AssocLeft],
1012+ [binary "=" PEq AssocLeft],
9751013 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
9761014
9771015toTable fs = map (map toBin)
@@ -984,11 +1022,14 @@ toTable fs = map (map toBin)
9841022 assoc (Infixr _) = AssocRight
9851023 assoc (InfixN _) = AssocNone
9861024
987−binary name f assoc = Infix (do reservedOp name; fc <- pfc;
988− return (f fc)) assoc
989−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;
9901030 return (f fc))
991−backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
1031+backtick = Infix (do lchar '`'; n <- pfName
1032+ lchar '`'
9921033 fc <- pfc
9931034 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
9941035
@@ -998,20 +1039,23 @@ backtick = Infix (do lchar '`'; n <- pfName; lchar '`'
9981039accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
9991040accData (Just Frozen) n ns = do addAcc n (Just Frozen)
10001041 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
10021044
10031045pRecord :: SyntaxInfo -> IParser PDecl
10041046pRecord syn = do acc <- pAccessibility
1005− reserved "record"; fc <- pfc
1006− tyn_in <- pfName; ty <- pTSig (impOK syn)
1047+ reserved "record"
1048+ fc <- pfc
1049+ tyn_in <- pfName
1050+ ty <- pTSig (impOK syn)
10071051 let tyn = expandNS syn tyn_in
10081052 reserved "where"
1009− open_block
1010− push_indent
1053+ openBlock
1054+ pushIndent
10111055 (cn, cty, _) <- pConstructor syn
10121056 pKeepTerminator
1013− pop_indent
1014− close_block
1057+ popIndent
1058+ closeBlock
10151059 accData acc tyn [cn]
10161060 let rsyn = syn { syn_namespace = show (nsroot tyn) :
10171061 syn_namespace syn }
@@ -1028,30 +1072,34 @@ pRecord syn = do acc <- pAccessibility
10281072
10291073pData :: SyntaxInfo -> IParser PDecl
10301074pData syn = try (do acc <- pAccessibility
1031− reserved "data"; fc <- pfc
1032− tyn_in <- pfName; ty <- pTSig (impOK syn)
1075+ reserved "data"
1076+ fc <- pfc
1077+ tyn_in <- pfName
1078+ ty <- pTSig (impOK syn)
10331079 let tyn = expandNS syn tyn_in
10341080 reserved "where"
1035− open_block
1036− push_indent
1081+ openBlock
1082+ pushIndent
10371083 cons <- many (do notEndBlock
10381084 c <- pConstructor syn
10391085 pKeepTerminator
10401086 return c) -- (lchar '|')
1041− pop_indent
1042− close_block
1087+ popIndent
1088+ closeBlock
10431089 accData acc tyn (map (\ (n, _, _) -> n) cons)
10441090 return $ PData syn fc (PDatadecl tyn ty cons))
1045− <|> try (do push_indent
1091+ <|> try (do pushIndent
10461092 acc <- pAccessibility
1047− reserved "data"; fc <- pfc
1048− tyn_in <- pfName; args <- many pName
1093+ reserved "data"
1094+ fc <- pfc
1095+ tyn_in <- pfName
1096+ args <- many pName
10491097 let tyn = expandNS syn tyn_in
10501098 lchar '='
10511099 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
10521100 pTerminator
10531101 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
10551103 cons' <- mapM (\ (x, cargs, cfc) ->
10561104 do let cty = bindArgs cargs conty
10571105 return (x, cty, cfc)) cons
@@ -1062,8 +1110,7 @@ pData syn = try (do acc <- pAccessibility
10621110 mkPApp fc t xs = PApp fc t (map pexp xs)
10631111
10641112bindArgs :: [PTerm] -> PTerm -> PTerm
1065−bindArgs [] t = t
1066−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
10671114
10681115pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
10691116pConstructor syn
@@ -1086,13 +1133,15 @@ pSimpleCon syn
10861133--------- DSL syntax overloading ---------
10871134
10881135pDSL :: SyntaxInfo -> IParser PDecl
1089−pDSL syn = do reserved "dsl"; n <- pfName
1090− open_block; push_indent
1136+pDSL syn = do reserved "dsl"
1137+ n <- pfName
1138+ openBlock
1139+ pushIndent
10911140 bs <- many1 (do notEndBlock
10921141 b <- pOverload syn
10931142 pKeepTerminator
10941143 return b)
1095− pop_indent; close_block
1144+ popIndent; closeBlock
10961145 let dsl = mkDSL bs (dsl_info syn)
10971146 checkDSL dsl
10981147 i <- getState
@@ -1113,8 +1162,9 @@ checkDSL :: DSL -> IParser ()
11131162checkDSL dsl = return ()
11141163
11151164pOverload :: SyntaxInfo -> IParser (String, PTerm)
1116−pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1117− if (not (o `elem` overloadable))
1165+pOverload syn = do o <- identifier <|> do reserved "let"
1166+ return "let"
1167+ if o `notElem` overloadable
11181168 then fail $ show o ++ " is not an overloading"
11191169 else do
11201170 lchar '='
@@ -1143,7 +1193,7 @@ pRHS syn n = do lchar '='; pExpr syn
11431193
11441194pClause :: SyntaxInfo -> IParser PClause
11451195pClause syn
1146− = try (do push_indent
1196+ = try (do pushIndent
11471197 n_in <- pfName; let n = expandNS syn n_in
11481198 cargs <- many (pConstraintArg syn)
11491199 iargs <- many (pImplicitArg syn)
@@ -1155,7 +1205,7 @@ pClause syn
11551205 let ctxt = tt_ctxt ist
11561206 let wsyn = syn { syn_namespace = [] }
11571207 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1158− pop_indent
1208+ popIndent
11591209 return x,
11601210 do pTerminator
11611211 return ([], [])]
@@ -1164,7 +1214,7 @@ pClause syn
11641214 ist <- getState
11651215 setState (ist { lastParse = Just n })
11661216 return $ PClause fc n capp wargs rhs wheres)
1167− <|> try (do push_indent
1217+ <|> try (do pushIndent
11681218 wargs <- many1 (pWExpr syn)
11691219 ist <- getState
11701220 n <- case lastParse ist of
@@ -1175,13 +1225,13 @@ pClause syn
11751225 let ctxt = tt_ctxt ist
11761226 let wsyn = syn { syn_namespace = [] }
11771227 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1178− pop_indent
1228+ popIndent
11791229 return x,
11801230 do pTerminator
11811231 return ([], [])]
11821232 return $ PClauseR fc wargs rhs wheres)
11831233
1184− <|> try (do push_indent
1234+ <|> try (do pushIndent
11851235 n_in <- pfName; let n = expandNS syn n_in
11861236 cargs <- many (pConstraintArg syn)
11871237 iargs <- many (pImplicitArg syn)
@@ -1194,24 +1244,24 @@ pClause syn
11941244 setState (ist { lastParse = Just n })
11951245 reserved "with"
11961246 wval <- pSimpleExpr syn
1197− open_block
1247+ openBlock
11981248 ds <- many1 $ pFunDecl syn
11991249 let withs = map (fillLHSD n capp wargs) $ concat ds
1200− close_block
1201− pop_indent
1250+ closeBlock
1251+ popIndent
12021252 return $ PWith fc n capp wargs wval withs)
12031253
12041254 <|> try (do wargs <- many1 (pWExpr syn)
12051255 fc <- pfc
12061256 reserved "with"
12071257 wval <- pSimpleExpr syn
1208− open_block
1258+ openBlock
12091259 ds <- many1 $ pFunDecl syn
12101260 let withs = concat ds
1211− close_block
1261+ closeBlock
12121262 return $ PWithR fc wargs wval withs)
12131263
1214− <|> do push_indent
1264+ <|> do pushIndent
12151265 l <- pArgExpr syn
12161266 op <- operator
12171267 let n = expandNS syn (UN op)
@@ -1221,7 +1271,7 @@ pClause syn
12211271 rhs <- pRHS syn n
12221272 let wsyn = syn { syn_namespace = [] }
12231273 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1224− pop_indent
1274+ popIndent
12251275 return x,
12261276 do pTerminator
12271277 return ([], [])]
@@ -1238,9 +1288,9 @@ pClause syn
12381288 wargs <- many (pWExpr syn)
12391289 reserved "with"
12401290 wval <- pSimpleExpr syn
1241− open_block
1291+ openBlock
12421292 ds <- many1 $ pFunDecl syn
1243− close_block
1293+ closeBlock
12441294 ist <- getState
12451295 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
12461296 let withs = map (fillLHSD n capp wargs) $ concat ds
@@ -1258,14 +1308,15 @@ pClause syn
12581308 fillLHSD n c a x = x
12591309
12601310pWExpr :: SyntaxInfo -> IParser PTerm
1261−pWExpr syn = do lchar '|'; pExpr' syn
1311+pWExpr syn = do lchar '|'
1312+ pExpr' syn
12621313
12631314pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
12641315pWhereblock n syn
1265− = do reserved "where"; open_block
1316+ = do reserved "where"; openBlock
12661317 ds <- many1 $ pFunDecl syn
12671318 let dns = concatMap (concatMap declared) ds
1268− close_block
1319+ closeBlock
12691320 return (concat ds, map (\x -> (x, decoration syn x)) dns)
12701321
12711322pDirective :: IParser [PDecl]
@@ -1273,7 +1324,7 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
12731324 return [PDirective (do addLib lib
12741325 addIBC (IBCLib lib))])
12751326 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1276− return [PDirective (do datadir <- liftIO $ getDataDir
1327+ return [PDirective (do datadir <- liftIO getDataDir
12771328 o <- liftIO $ findInPath [".", datadir] obj
12781329 addIBC (IBCObj o)
12791330 addObjectFile o)])