git.iko.soy/Idris-dev
on master help sign in
When collecting implicit args in wheres, ignore names bound in above scope
commit5e92c7000e77ef6bf4237526a1787e877a6d326f authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 11:38 (15 years ago) parentbf368ab
3 files changed+17−3
compare with master
unifiedsplit
src/Core/TT.hs+4 src/Idris/AbsSyntax.hs+3−2 src/Idris/Parser.hs+10−1
src/Core/TT.hs+4
@@ -280,6 +280,10 @@ bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
280280bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
281281bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
282282
283+getArgTys :: TT n -> [(n, TT n)]
284+getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
285+getArgTys _ = []
286+
283287type Term = TT Name
284288type Type = Term
285289
src/Idris/AbsSyntax.hs+3−2
@@ -215,10 +215,11 @@ initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
215215
216216data SyntaxInfo = Syn { using :: [(Name, PTerm)],
217217 syn_params :: [(Name, PTerm)],
218+ no_imp :: [Name],
218219 dsl_info :: DSL }
219220 deriving Show
220221
221−defaultSyntax = Syn [] [] initDSL
222+defaultSyntax = Syn [] [] [] initDSL
222223
223224--- Pretty printing declarations and terms
224225
@@ -398,7 +399,7 @@ implicitise syn ist tm
398399 = let uvars = using syn
399400 pvars = syn_params syn
400401 (declimps, ns') = execState (imps True [] tm) ([], [])
401− ns = ns' \\ map fst pvars in
402+ ns = ns' \\ (map fst pvars ++ no_imp syn) in
402403 if null ns
403404 then (tm, reverse declimps)
404405 else implicitise syn ist (pibind uvars ns tm)
src/Idris/Parser.hs+10−1
@@ -7,6 +7,7 @@ import Idris.ElabDecls
77
88import Core.CoreParser
99import Core.TT
10+import Core.Evaluate
1011
1112import Text.ParserCombinators.Parsec
1213import Text.ParserCombinators.Parsec.Expr
@@ -486,6 +487,11 @@ pPattern syn = do fc <- pfc
486487 clause <- pClause syn
487488 return (PClauses fc (MN 2 "_") [clause]) -- collect together later
488489
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+
489495pClause :: SyntaxInfo -> IParser PClause
490496pClause syn
491497 = try (do n <- pfName
@@ -495,7 +501,10 @@ pClause syn
495501 wargs <- many (pWExpr syn)
496502 lchar '='
497503 rhs <- pExpr syn
498− wheres <- choice [pWhereblock syn, do lchar ';'; return []]
504+ ist <- getState
505+ let ctxt = tt_ctxt ist
506+ let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)
507+ wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]
499508 return $ PClause n (PApp fc (PRef fc n)
500509 (iargs ++ map PExp args)) wargs rhs wheres)
501510 <|> try (do n <- pfName