f52eafd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix for name shadowing in evaluator

f52eafdEdwin Brady13 years ago

src/Idris/Core/Evaluate.hs+7−5

compare with master

unifiedsplit

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

257 return $ VBind True n (Let t' v') (\x -> return sc')

258 ev ntimes stk top env (Bind n b sc)

259 = do b' <- vbind env b

260− let n' = uniqueName n (map fst env)

260+ let n' = uniqueName n (map fst genv ++ map fst env)

261 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)

263 where vbind env t

264 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

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

@@ -536,8 +536,10 @@ convEq ctxt holes = ceq [] where

536 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

537 | n == n' = ceq ps x y

538 ceq ps (V x) (V y) = return (x == y)

539+ ceq ps (V x) (P _ y _) = return (fst (ps!!x) == y)

540+ ceq ps (P _ x _) (V y) = return (x == snd (ps!!y))

539− ceq ps (Bind _ xb xs) (Bind _ yb ys)

541+ ceq ps (Bind n xb xs) (Bind n' yb ys)

540− = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)

542+ = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

541 where

543 where

542 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

544 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

543 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

545 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

549 return True

551 return True

550 ceq ps Erased _ = return True

552 ceq ps Erased _ = return True

551 ceq ps _ Erased = return True

553 ceq ps _ Erased = return True

552− ceq ps _ _ = return False

554+ ceq ps x y = return False

553

555

554 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'

556 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'

555 where

557 where

src/Idris/Core/Unify.hs+21−16

@@ -37,11 +37,12 @@ data UResult a = UOK a

37match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

38 TC [(Name, TT Name)]

39match_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

41 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))

42 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))

42 res ->

43 res ->

43− let topxn = normalise ctxt env topx

44+ let topxn = renameBindersTm env (normalise ctxt env topx)

44− topyn = normalise ctxt env topy in

45+ topyn = renameBindersTm env (normalise ctxt env topy) in

45 case runStateT (un [] topxn topyn)

46 case runStateT (un [] topxn topyn)

46 (UI 0 []) of

47 (UI 0 []) of

47 OK (v, UI _ fails) ->

48 OK (v, UI _ fails) ->

@@ -147,17 +148,20 @@ match_unify ctxt env topx topy inj holes =

147 App (Bind y (Lam ty) (bind (i-1) ns tm))

148 App (Bind y (Lam ty) (bind (i-1) ns tm))

148 (P Bound x ty)

149 (P Bound x ty)

149

150

151+renameBinders env (x, t) = (x, renameBindersTm env t)

152+

150−renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)

153+renameBindersTm :: Env -> TT Name -> TT Name

151−renameBinders env (x, tm) = (x, uniqueBinders tm)

154+renameBindersTm env tm = uniqueBinders (map fst env) tm

152 where

155 where

153− uniqueBinders (Bind n b sc)

156+ uniqueBinders env (Bind n b sc)

154− | n `elem` map fst env

157+ | n `elem` env

155− = let n' = uniqueName n (map fst env) in

158+ = let n' = uniqueName n env in

156− Bind n' (fmap uniqueBinders b)

159+ Bind n' (fmap (uniqueBinders env) b)

157− (uniqueBinders (rename n n' sc))

160+ (uniqueBinders (n':env) (rename n n' sc))

158− | otherwise = Bind n (fmap uniqueBinders b) (uniqueBinders sc)

161+ | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

162+ (uniqueBinders (n:env) sc)

159− uniqueBinders (App f a) = App (uniqueBinders f) (uniqueBinders a)

163+ uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

160− uniqueBinders t = t

164+ uniqueBinders env t = t

161

165

162 rename n n' (P nt x ty) | n == x = P nt n' ty

166 rename n n' (P nt x ty) | n == x = P nt n' ty

163 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)

167 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] ->

189unify ctxt env topx topy inj holes =

193unify ctxt env topx topy inj holes =

190-- trace ("Unifying " ++ show (topx, topy)) $

194-- trace ("Unifying " ++ show (topx, topy)) $

191 -- don't bother if topx and topy are different at the head

195 -- 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

193 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),

198 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),

194 [])

199 [])

195 res ->

200 res ->

196− let topxn = normalise ctxt env topx

201+ let topxn = renameBindersTm env (normalise ctxt env topx)

197− topyn = normalise ctxt env topy in

202+ topyn = renameBindersTm env (normalise ctxt env topy) in

198-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

203-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

199 case runStateT (un False [] topxn topyn)

204 case runStateT (un False [] topxn topyn)

200 (UI 0 []) of

205 (UI 0 []) of