fa80591 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix let scope leakage bug

fa80591Edwin Brady13 years ago

src/Core/Elaborate.hs+8

compare with master

unifiedsplit

@@ -263,6 +263,9 @@ regret = processTactic' Regret

263compute :: Elab' aux ()

264compute = processTactic' Compute

265

266+simplify :: Elab' aux ()

267+simplify = processTactic' Simplify

268+

266hnf_compute :: Elab' aux ()

269hnf_compute :: Elab' aux ()

267hnf_compute = processTactic' HNF_Compute

270hnf_compute = processTactic' HNF_Compute

268

271

@@ -284,6 +287,9 @@ forall n t = processTactic' (Forall n t)

284letbind :: Name -> Raw -> Raw -> Elab' aux ()

287letbind :: Name -> Raw -> Raw -> Elab' aux ()

285letbind n t v = processTactic' (LetBind n t v)

288letbind n t v = processTactic' (LetBind n t v)

286

289

290+expandLet :: Name -> Term -> Elab' aux ()

291+expandLet n v = processTactic' (ExpandLet n v)

292+

287rewrite :: Raw -> Elab' aux ()

293rewrite :: Raw -> Elab' aux ()

288rewrite tm = processTactic' (Rewrite tm)

294rewrite tm = processTactic' (Rewrite tm)

289

295

@@ -392,6 +398,8 @@ match_apply = apply' match_fill

392apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

398apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

393apply' fillt fn imps =

399apply' fillt fn imps =

394 do args <- prepare_apply fn (map fst imps)

400 do args <- prepare_apply fn (map fst imps)

401+ env <- get_env

402+ g <- goal

395 fillt (raw_apply fn (map Var args))

403 fillt (raw_apply fn (map Var args))

396 -- _Don't_ solve the arguments we're specifying by hand.

404 -- _Don't_ solve the arguments we're specifying by hand.

397 -- (remove from unified list before calling end_unify)

405 -- (remove from unified list before calling end_unify)

src/Core/ProofState.hs+14

@@ -58,6 +58,7 @@ data Tactic = Attack

58 | StartUnify Name

59 | EndUnify

60 | Compute

61+ | Simplify

61 | HNF_Compute

62 | HNF_Compute

62 | EvalIn Raw

63 | EvalIn Raw

63 | CheckIn Raw

64 | CheckIn Raw

@@ -65,6 +66,7 @@ data Tactic = Attack

65 | IntroTy Raw (Maybe Name)

66 | IntroTy Raw (Maybe Name)

66 | Forall Name Raw

67 | Forall Name Raw

67 | LetBind Name Raw Raw

68 | LetBind Name Raw Raw

69+ | ExpandLet Name Term

68 | Rewrite Raw

70 | Rewrite Raw

69 | Equiv Raw

71 | Equiv Raw

70 | PatVar Name

72 | PatVar Name

@@ -504,6 +506,10 @@ letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

504 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

506 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

505letbind n ty val ctxt env _ = fail "Can't let bind here"

507letbind n ty val ctxt env _ = fail "Can't let bind here"

506

508

509+expandLet :: Name -> Term -> RunTactic

510+expandLet n v ctxt env tm =

511+ return $ subst n v tm

512+

507rewrite :: Raw -> RunTactic

513rewrite :: Raw -> RunTactic

508rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

514rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

509 do (tmv, tmt) <- lift $ check ctxt env tm

515 do (tmv, tmt) <- lift $ check ctxt env tm

@@ -570,6 +576,12 @@ hnf_compute ctxt env (Bind x (Hole ty) sc) =

570 return $ Bind x (Hole ty') sc

576 return $ Bind x (Hole ty') sc

571hnf_compute ctxt env t = return t

577hnf_compute ctxt env t = return t

572

578

579+-- reduce let bindings only

580+simplify :: RunTactic

581+simplify ctxt env (Bind x (Hole ty) sc) =

582+ do return $ Bind x (Hole (specialise ctxt env [] ty)) sc

583+simplify ctxt env t = return t

584+

573check_in :: Raw -> RunTactic

585check_in :: Raw -> RunTactic

574check_in t ctxt env tm =

586check_in t ctxt env tm =

575 do (val, valty) <- lift $ check ctxt env t

587 do (val, valty) <- lift $ check ctxt env t

@@ -726,11 +738,13 @@ process t h = tactic (Just h) (mktac t)

726 mktac Solve = solve

738 mktac Solve = solve

727 mktac (StartUnify n) = start_unify n

739 mktac (StartUnify n) = start_unify n

728 mktac Compute = compute

740 mktac Compute = compute

741+ mktac Simplify = Core.ProofState.simplify

729 mktac HNF_Compute = hnf_compute

742 mktac HNF_Compute = hnf_compute

730 mktac (Intro n) = intro n

743 mktac (Intro n) = intro n

731 mktac (IntroTy ty n) = introTy ty n

744 mktac (IntroTy ty n) = introTy ty n

732 mktac (Forall n t) = forall n t

745 mktac (Forall n t) = forall n t

733 mktac (LetBind n t v) = letbind n t v

746 mktac (LetBind n t v) = letbind n t v

747+ mktac (ExpandLet n b) = expandLet n b

734 mktac (Rewrite t) = rewrite t

748 mktac (Rewrite t) = rewrite t

735 mktac (Equiv t) = equiv t

749 mktac (Equiv t) = equiv t

736 mktac (PatVar n) = patvar n

750 mktac (PatVar n) = patvar n

src/Core/TT.hs+1−1

@@ -605,7 +605,7 @@ pToV' n i (P _ x _) | n == x = V i

605pToV' n i (Bind x b sc)

606-- We can assume the inner scope has been pToVed already, so continue to

607-- resolve names from the *outer* scope which may happen to have the same id.

608−-- | n == x = Bind x (fmap (pToV' n i) b) sc

608+ | n == x = Bind x (fmap (pToV' n i) b) sc

609 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

610pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

611pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

src/Core/Unify.hs+13−3

@@ -34,7 +34,7 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

34 TC [(Name, TT Name)]

35match_unify ctxt env topx topy dont holes =

36-- trace ("Matching " ++ show (topx, topy)) $

37− case runStateT (un [] topx topy) (UI 0 []) of

37+ case runStateT (un [] topx topy) (UI 0 []) of

38 OK (v, UI _ []) -> return (filter notTrivial v)

39 res ->

40 let topxn = normalise ctxt env topx

@@ -100,6 +100,14 @@ match_unify ctxt env topx topy dont holes =

100notTrivial (x, P _ x' _) = x /= x'

101notTrivial _ = True

102

103+expandLets env (x, tm) = (x, doSubst (reverse env) tm)

104+ where

105+ doSubst [] tm = tm

106+ doSubst ((n, Let v t) : env) tm

107+ = doSubst env (subst n v tm)

108+ doSubst (_ : env) tm

109+ = doSubst env tm

110+

103

111

104unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

112unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

105 TC ([(Name, TT Name)], Fails)

113 TC ([(Name, TT Name)], Fails)

@@ -107,7 +115,8 @@ unify ctxt env topx topy dont holes =

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

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

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

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

109 case runStateT (un False [] topx topy) (UI 0 []) of

117 case runStateT (un False [] topx topy) (UI 0 []) of

110− OK (v, UI _ []) -> return (filter notTrivial v, [])

118+ OK (v, UI _ []) -> return (filter notTrivial v,

119+ [])

111 res ->

120 res ->

112 let topxn = normalise ctxt env topx

121 let topxn = normalise ctxt env topx

113 topyn = normalise ctxt env topy in

122 topyn = normalise ctxt env topy in

@@ -115,7 +124,8 @@ unify ctxt env topx topy dont holes =

115 case runStateT (un False [] topxn topyn)

124 case runStateT (un False [] topxn topyn)

116 (UI 0 []) of

125 (UI 0 []) of

117 OK (v, UI _ fails) ->

126 OK (v, UI _ fails) ->

118− return (filter notTrivial v, reverse fails)

127+ return (filter notTrivial v,

128+ reverse fails)

119-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

129-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

120 Error e -> tfail e

130 Error e -> tfail e

121 where

131 where

src/Idris/ElabTerm.hs+5−1

@@ -285,8 +285,12 @@ elab ist info pattern tcgen fn tm

285 elabE (True, a) ty

286 focus valn

287 elabE (True, a) val

288+ env <- get_env

288 elabE (True, a) sc

289 elabE (True, a) sc

289− ptm <- get_term

290+ -- HACK: If the name leaks into its type, it may leak out of

291+ -- scope outside, so substitute in the outer scope.

292+ expandLet n (case lookup n env of

293+ Just (Let t v) -> v)

290 solve

294 solve

291 elab' ina tm@(PApp fc (PInferRef _ f) args) = do

295 elab' ina tm@(PApp fc (PInferRef _ f) args) = do

292 rty <- goal

296 rty <- goal