809c283 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #90 from raichoo/parser

809c283Edwin Brady14 years ago

src/Idris/AbsSyntaxTree.hs+5−1

compare with master

unifiedsplit

@@ -231,7 +231,11 @@ instance Show Fixity where

231 show (PrefixN i) = "prefix " ++ show i

232

233data 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+

235{-!

239{-!

236deriving instance Binary FixDecl

240deriving instance Binary FixDecl

237!-}

241!-}

src/Idris/Parser.hs+15−20

@@ -154,12 +154,6 @@ parseTac i = runParser (do t <- pTactic defaultSyntax

154 eof

155 return t) i "(proof)"

156

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−

163parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)

157parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)

164parseImports fname input

158parseImports fname input

165 = do i <- get

159 = do i <- get

@@ -169,7 +163,7 @@ parseImports fname input

169 rest <- getInput

163 rest <- getInput

170 pos <- getPosition

164 pos <- getPosition

171 return ((mname, ps, rest, pos), i)) i fname input of

165 return ((mname, ps, rest, pos), i)) i fname input of

172− Left err -> fail (iShowError fname err)

166+ Left err -> fail (show err)

173 Right (x, i) -> do put i

167 Right (x, i) -> do put i

174 return x

168 return x

175

169

@@ -212,14 +206,13 @@ openBlock = do lchar '{'

212closeBlock :: IParser ()

206closeBlock :: IParser ()

213closeBlock = do ist <- getState

207closeBlock = do ist <- getState

214 bs <- case brace_stack ist of

208 bs <- case brace_stack ist of

215− Nothing : xs -> do lchar '}'

209+ Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])

216− return xs

217− Just lvl : xs -> do i <- indent

210+ Just lvl : xs -> (do i <- indent

218− inp <- getInput

211+ inp <- getInput

219-- trace (show (take 10 inp, i, lvl)) $

212-- trace (show (take 10 inp, i, lvl)) $

220− if i >= lvl && take 1 inp /= ")"

213+ if i >= lvl && take 1 inp /= ")"

221− then fail "Not end of block"

214+ then fail "Not end of block"

222− else return xs

215+ else return xs) <|> (eof >> return [])

223 setState (ist { brace_stack = bs })

216 setState (ist { brace_stack = bs })

224

217

225pTerminator = do lchar ';'; popIndent

218pTerminator = do lchar ';'; popIndent

@@ -286,7 +279,7 @@ parseProg syn fname input pos

286 eof

279 eof

287 i' <- getState

280 i' <- getState

288 return (concat ps, i')) i fname input of

281 return (concat ps, i')) i fname input of

289− Left err -> fail (iShowError fname err)

282+ Left err -> fail (show err)

290 Right (x, i) -> do put i

283 Right (x, i) -> do put i

291 return (collect x)

284 return (collect x)

292

285

@@ -357,10 +350,10 @@ pFunDecl syn

357pDecl' :: SyntaxInfo -> IParser PDecl

350pDecl' :: SyntaxInfo -> IParser PDecl

358pDecl' syn

351pDecl' syn

359 = try pFixity

352 = try pFixity

360− <|> pFunDecl' syn

353+ <|> try (pFunDecl' syn)

361 <|> try (pData syn)

354 <|> try (pData syn)

362 <|> try (pRecord syn)

355 <|> try (pRecord syn)

363− <|> pSyntaxDecl syn

356+ <|> try (pSyntaxDecl syn)

364

357

365pSyntaxDecl :: SyntaxInfo -> IParser PDecl

358pSyntaxDecl :: SyntaxInfo -> IParser PDecl

366pSyntaxDecl syn

359pSyntaxDecl syn

@@ -492,14 +485,16 @@ pFixity = do pushIndent

492 istate <- getState

485 istate <- getState

493 let infixes = idris_infixes istate

486 let infixes = idris_infixes istate

494 let fs = map (Fix (f prec)) ops

487 let fs = map (Fix (f prec)) ops

495− let redecl = map (alreadyDeclared infixes) fs

488+ let redecls = map (alreadyDeclared infixes) fs

496− if False `notElem` map checkValidity redecl

489+ let ill = filter (not . checkValidity) redecls

490+ if null ill

497 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)

491 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)

498 , ibc_write = map IBCFix fs ++ ibc_write istate

492 , ibc_write = map IBCFix fs ++ ibc_write istate

499 })

493 })

500 fc <- pfc

494 fc <- pfc

501 return (PFix fc (f prec) ops)

495 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

503 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

498 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

504 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

499 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

505

500