on master help sign in
Merge pull request #90 from raichoo/parser

Some parser patches

commit809c28311e77be01164ee26064dea07a021a11d2 authorEdwin Brady <edwin.brady@gmail.com> dateTue 20 Nov 2012, 16:12 (14 years ago) parentab3931a92f3139
2 files changed+20−21
src/Idris/AbsSyntaxTree.hs+5−1 src/Idris/Parser.hs+15−20
src/Idris/AbsSyntaxTree.hs+5−1
@@ -231,7 +231,11 @@ instance Show Fixity where
231231 show (PrefixN i) = "prefix " ++ show i
232232
233233data FixDecl = Fix Fixity String
234− deriving (Show, Eq)
234+ deriving Eq
235+
236+instance Show FixDecl where
237+ show (Fix f s) = show f ++ " " ++ s
238+
235239{-!
236240deriving instance Binary FixDecl
237241!-}
src/Idris/Parser.hs+15−20
@@ -154,12 +154,6 @@ parseTac i = runParser (do t <- pTactic defaultSyntax
154154 eof
155155 return t) i "(proof)"
156156
157−iShowError fname err = let ln = sourceLine (errorPos err)
158− clm = sourceColumn (errorPos err)
159− msg = map messageString (errorMessages err) in
160− fname ++ ":" ++ show ln ++ ":parse error"
161− ++ " at column " ++ show clm -- ++ " with error:\n\t" ++ show msg
162−
163157parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
164158parseImports fname input
165159 = do i <- get
@@ -169,7 +163,7 @@ parseImports fname input
169163 rest <- getInput
170164 pos <- getPosition
171165 return ((mname, ps, rest, pos), i)) i fname input of
172− Left err -> fail (iShowError fname err)
166+ Left err -> fail (show err)
173167 Right (x, i) -> do put i
174168 return x
175169
@@ -212,14 +206,13 @@ openBlock = do lchar '{'
212206closeBlock :: IParser ()
213207closeBlock = do ist <- getState
214208 bs <- case brace_stack ist of
215− Nothing : xs -> do lchar '}'
216− return xs
217− Just lvl : xs -> do i <- indent
218− inp <- getInput
209+ Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
210+ Just lvl : xs -> (do i <- indent
211+ inp <- getInput
219212-- trace (show (take 10 inp, i, lvl)) $
220− if i >= lvl && take 1 inp /= ")"
221− then fail "Not end of block"
222− else return xs
213+ if i >= lvl && take 1 inp /= ")"
214+ then fail "Not end of block"
215+ else return xs) <|> (eof >> return [])
223216 setState (ist { brace_stack = bs })
224217
225218pTerminator = do lchar ';'; popIndent
@@ -286,7 +279,7 @@ parseProg syn fname input pos
286279 eof
287280 i' <- getState
288281 return (concat ps, i')) i fname input of
289− Left err -> fail (iShowError fname err)
282+ Left err -> fail (show err)
290283 Right (x, i) -> do put i
291284 return (collect x)
292285
@@ -357,10 +350,10 @@ pFunDecl syn
357350pDecl' :: SyntaxInfo -> IParser PDecl
358351pDecl' syn
359352 = try pFixity
360− <|> pFunDecl' syn
353+ <|> try (pFunDecl' syn)
361354 <|> try (pData syn)
362355 <|> try (pRecord syn)
363− <|> pSyntaxDecl syn
356+ <|> try (pSyntaxDecl syn)
364357
365358pSyntaxDecl :: SyntaxInfo -> IParser PDecl
366359pSyntaxDecl syn
@@ -492,14 +485,16 @@ pFixity = do pushIndent
492485 istate <- getState
493486 let infixes = idris_infixes istate
494487 let fs = map (Fix (f prec)) ops
495− let redecl = map (alreadyDeclared infixes) fs
496− if False `notElem` map checkValidity redecl
488+ let redecls = map (alreadyDeclared infixes) fs
489+ let ill = filter (not . checkValidity) redecls
490+ if null ill
497491 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
498492 , ibc_write = map IBCFix fs ++ ibc_write istate
499493 })
500494 fc <- pfc
501495 return (PFix fc (f prec) ops)
502− else fail "Illegal redeclaration of fixity"
496+ else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity: \""
497+ ++ show f ++ "\" overrides \"" ++ show x ++ "\"\n") ill
503498 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
504499 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
505500