git.iko.soy/Idris-dev
on master help sign in
Fix for name shadowing in evaluator

Things are much easier if we have unique names everywhere, but we didn't quite have it right in the evaluator (it wasn't checking the outer environment when evaluating in a surrounding environment). Fixes #642

commitf52eafd3e11fea798ff7cb0e4ba55fd994dac245 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 6 Mar 2014, 00:12 (13 years ago) parent1519d88
2 files changed+28−21
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+7−5 src/Idris/Core/Unify.hs+21−16
src/Idris/Core/Evaluate.hs+7−5
@@ -257,9 +257,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
257257 return $ VBind True n (Let t' v') (\x -> return sc')
258258 ev ntimes stk top env (Bind n b sc)
259259 = do b' <- vbind env b
260− let n' = uniqueName n (map fst env)
260+ let n' = uniqueName n (map fst genv ++ map fst env)
261261 return $ VBind True -- (vinstances 0 sc < 2)
262− n' b' (\x -> ev ntimes stk False ((n, x):env) sc)
262+ n' b' (\x -> ev ntimes stk False ((n', x):env) sc)
263263 where vbind env t
264264 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
265265 -- Treat "assert_total" specially, as long as it's defined!
@@ -536,8 +536,10 @@ convEq ctxt holes = ceq [] where
536536 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y
537537 | n == n' = ceq ps x y
538538 ceq ps (V x) (V y) = return (x == y)
539− ceq ps (Bind _ xb xs) (Bind _ yb ys)
540− = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
539+ ceq ps (V x) (P _ y _) = return (fst (ps!!x) == y)
540+ ceq ps (P _ x _) (V y) = return (x == snd (ps!!y))
541+ ceq ps (Bind n xb xs) (Bind n' yb ys)
542+ = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)
541543 where
542544 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
543545 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
@@ -549,7 +551,7 @@ convEq ctxt holes = ceq [] where
549551 return True
550552 ceq ps Erased _ = return True
551553 ceq ps _ Erased = return True
552− ceq ps _ _ = return False
554+ ceq ps x y = return False
553555
554556 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
555557 where
src/Idris/Core/Unify.hs+21−16
@@ -37,11 +37,12 @@ data UResult a = UOK a
3737match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
3838 TC [(Name, TT Name)]
3939match_unify ctxt env topx topy inj holes =
40− case runStateT (un [] topx topy) (UI 0 []) of
40+ case runStateT (un [] (renameBindersTm env topx)
41+ (renameBindersTm env topy)) (UI 0 []) of
4142 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
4243 res ->
43− let topxn = normalise ctxt env topx
44− topyn = normalise ctxt env topy in
44+ let topxn = renameBindersTm env (normalise ctxt env topx)
45+ topyn = renameBindersTm env (normalise ctxt env topy) in
4546 case runStateT (un [] topxn topyn)
4647 (UI 0 []) of
4748 OK (v, UI _ fails) ->
@@ -147,17 +148,20 @@ match_unify ctxt env topx topy inj holes =
147148 App (Bind y (Lam ty) (bind (i-1) ns tm))
148149 (P Bound x ty)
149150
150−renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)
151−renameBinders env (x, tm) = (x, uniqueBinders tm)
151+renameBinders env (x, t) = (x, renameBindersTm env t)
152+
153+renameBindersTm :: Env -> TT Name -> TT Name
154+renameBindersTm env tm = uniqueBinders (map fst env) tm
152155 where
153− uniqueBinders (Bind n b sc)
154− | n `elem` map fst env
155− = let n' = uniqueName n (map fst env) in
156− Bind n' (fmap uniqueBinders b)
157− (uniqueBinders (rename n n' sc))
158− | otherwise = Bind n (fmap uniqueBinders b) (uniqueBinders sc)
159− uniqueBinders (App f a) = App (uniqueBinders f) (uniqueBinders a)
160− uniqueBinders t = t
156+ uniqueBinders env (Bind n b sc)
157+ | n `elem` env
158+ = let n' = uniqueName n env in
159+ Bind n' (fmap (uniqueBinders env) b)
160+ (uniqueBinders (n':env) (rename n n' sc))
161+ | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
162+ (uniqueBinders (n:env) sc)
163+ uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)
164+ uniqueBinders env t = t
161165
162166 rename n n' (P nt x ty) | n == x = P nt n' ty
163167 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
@@ -189,12 +193,13 @@ unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
189193unify ctxt env topx topy inj holes =
190194-- trace ("Unifying " ++ show (topx, topy)) $
191195 -- don't bother if topx and topy are different at the head
192− case runStateT (un False [] topx topy) (UI 0 []) of
196+ case runStateT (un False [] (renameBindersTm env topx)
197+ (renameBindersTm env topy)) (UI 0 []) of
193198 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
194199 [])
195200 res ->
196− let topxn = normalise ctxt env topx
197− topyn = normalise ctxt env topy in
201+ let topxn = renameBindersTm env (normalise ctxt env topx)
202+ topyn = renameBindersTm env (normalise ctxt env topy) in
198203-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
199204 case runStateT (un False [] topxn topyn)
200205 (UI 0 []) of