5e92c70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

When collecting implicit args in wheres, ignore names bound in above scope

5e92c70Edwin Brady15 years ago

src/Core/TT.hs+4

compare with master

unifiedsplit

@@ -280,6 +280,10 @@ bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)

280bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n

281bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

282

283+getArgTys :: TT n -> [(n, TT n)]

284+getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc

285+getArgTys _ = []

286+

283type Term = TT Name

287type Term = TT Name

284type Type = Term

288type Type = Term

285

289

src/Idris/AbsSyntax.hs+3−2

@@ -215,10 +215,11 @@ initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])

215

216data SyntaxInfo = Syn { using :: [(Name, PTerm)],

217 syn_params :: [(Name, PTerm)],

218+ no_imp :: [Name],

218 dsl_info :: DSL }

219 dsl_info :: DSL }

219 deriving Show

220 deriving Show

220

221

221−defaultSyntax = Syn [] [] initDSL

222+defaultSyntax = Syn [] [] [] initDSL

222

223

223--- Pretty printing declarations and terms

224--- Pretty printing declarations and terms

224

225

@@ -398,7 +399,7 @@ implicitise syn ist tm

398 = let uvars = using syn

399 = let uvars = using syn

399 pvars = syn_params syn

400 pvars = syn_params syn

400 (declimps, ns') = execState (imps True [] tm) ([], [])

401 (declimps, ns') = execState (imps True [] tm) ([], [])

401− ns = ns' \\ map fst pvars in

402+ ns = ns' \\ (map fst pvars ++ no_imp syn) in

402 if null ns

403 if null ns

403 then (tm, reverse declimps)

404 then (tm, reverse declimps)

404 else implicitise syn ist (pibind uvars ns tm)

405 else implicitise syn ist (pibind uvars ns tm)

src/Idris/Parser.hs+10−1

@@ -7,6 +7,7 @@ import Idris.ElabDecls

8import Core.CoreParser

9import Core.TT

10+import Core.Evaluate

11import Text.ParserCombinators.Parsec

12import Text.ParserCombinators.Parsec

12import Text.ParserCombinators.Parsec.Expr

13import Text.ParserCombinators.Parsec.Expr

@@ -486,6 +487,11 @@ pPattern syn = do fc <- pfc

486 clause <- pClause syn

487 clause <- pClause syn

487 return (PClauses fc (MN 2 "_") [clause]) -- collect together later

488 return (PClauses fc (MN 2 "_") [clause]) -- collect together later

488

489

490+whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

491+whereSyn n syn args = let ns = concatMap allNamesIn args

492+ ni = no_imp syn in

493+ syn { no_imp = nub (ni ++ ns) }

494+

489pClause :: SyntaxInfo -> IParser PClause

495pClause :: SyntaxInfo -> IParser PClause

490pClause syn

496pClause syn

491 = try (do n <- pfName

497 = try (do n <- pfName

@@ -495,7 +501,10 @@ pClause syn

495 wargs <- many (pWExpr syn)

501 wargs <- many (pWExpr syn)

496 lchar '='

502 lchar '='

497 rhs <- pExpr syn

503 rhs <- pExpr syn

504+ ist <- getState

505+ let ctxt = tt_ctxt ist

506+ let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

498− wheres <- choice [pWhereblock syn, do lchar ';'; return []]

507+ wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]

499 return $ PClause n (PApp fc (PRef fc n)

508 return $ PClause n (PApp fc (PRef fc n)

500 (iargs ++ map PExp args)) wargs rhs wheres)

509 (iargs ++ map PExp args)) wargs rhs wheres)

501 <|> try (do n <- pfName

510 <|> try (do n <- pfName