8697358 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix scope error when shadowing

commit869735872efb5caead0a80d9713f5b53a3230134 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 21 Feb 2015, 18:20 (12 years ago) parent6d6c81b

4 files changed+19−8

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−1 src/Idris/Core/Evaluate.hs+3−3 src/Idris/Elab/Clause.hs+3−3 src/Idris/ElabTerm.hs+9−1

src/Idris/AbsSyntax.hs+4−1

@@ -1978,8 +1978,11 @@ shadow :: Name -> Name -> PTerm -> PTerm

19781978shadow n n' t = sm t where

19791979 sm (PRef fc x) | n == x = PRef fc n'

19801980 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)

1981− sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)

1981+ | otherwise = PLam fc x (sm t) sc

1982+ sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)

1983+ | otherwise = PPi p x (sm t) sc

19821984 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

1985+ | otherwise = PLet fc x (sm t) (sm v) sc

19831986 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

19841987 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

19851988 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

src/Idris/Core/Evaluate.hs+3−3

@@ -286,17 +286,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

286286 -- block reduction immediately under codata (and not forced)

287287 ev ntimes stk top env

288288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289− | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

289+ | dly == txt "Delay" && lco == txt "LazyCodata" -- && not simpl

290290 = do let (f, _) = unApply arg

291291 let ntimes' = case f of

292292 P _ fn _ -> (fn, 0) : ntimes

293293 _ -> ntimes

294− when spec $ setBlock True

294+ when (spec || simpl) $ setBlock True

295295 d' <- ev ntimes' stk False env d

296296 l' <- ev ntimes' stk False env l

297297 t' <- ev ntimes' stk False env t

298298 arg' <- ev ntimes' stk False env arg

299− when spec $ setBlock False

299+ when (spec || simpl) $ setBlock False

300300 evApply ntimes' stk top env [l',t',arg'] d'

301301 -- Treat "assert_total" specially, as long as it's defined!

302302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)

src/Idris/Elab/Clause.hs+3−3

@@ -648,9 +648,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

648648 -- Now build the RHS, using the type of the LHS as the goal.

649649 i <- getIState -- new implicits from where block

650650 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

651− let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

651+ let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)

652652 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

653− logLvl 2 $ "RHS: " ++ showTmImpls rhs

653+ logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

654654 ctxt <- getContext -- new context with where block added

655655 logLvl 5 "STARTING CHECK"

656656 ((rhs', defer, is, probs), _) <-

@@ -673,7 +673,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

673673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

674674

675675 logLvl 5 "DONE CHECK"

676− logLvl 2 $ "---> " ++ show rhs'

676+ logLvl 4 $ "---> " ++ show rhs'

677677 when (not (null defer)) $ iLOG $ "DEFERRED " ++

678678 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

679679 def' <- checkDef fc defer

src/Idris/ElabTerm.hs+9−1

@@ -893,9 +893,17 @@ elab ist info emode opts fn tm

893893 -- Drop the unique arguments used in the term already

894894 -- and in the scrutinee (since it's

895895 -- not valid to use them again anyway)

896+ --

897+ -- Also drop unique arguments which don't appear explicitly

898+ -- in either case branch so they don't count as used

899+ -- unnecessarily (can only do this for unique things, since we

900+ -- assume they don't appear implicitly in types)

896901 ptm <- get_term

902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

903+

897904 let argsDropped = filter (isUnique envU)

898− (nub $ allNamesIn scr ++ inApp ptm)

905+ (nub $ allNamesIn scr ++ inApp ptm ++

906+ inOpts)

899907

900908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

901909