git.iko.soy/Idris-dev
on master help sign in
Fix let scope leakage bug
commitfa8059147ac6af2f9cee6d0c09abf93577a41c64 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 26 Jul 2013, 19:42 (13 years ago) parent6f88ecd
5 files changed+41−5
compare with master
unifiedsplit
src/Core/Elaborate.hs+8 src/Core/ProofState.hs+14 src/Core/TT.hs+1−1 src/Core/Unify.hs+13−3 src/Idris/ElabTerm.hs+5−1
src/Core/Elaborate.hs+8
@@ -263,6 +263,9 @@ regret = processTactic' Regret
263263compute :: Elab' aux ()
264264compute = processTactic' Compute
265265
266+simplify :: Elab' aux ()
267+simplify = processTactic' Simplify
268+
266269hnf_compute :: Elab' aux ()
267270hnf_compute = processTactic' HNF_Compute
268271
@@ -284,6 +287,9 @@ forall n t = processTactic' (Forall n t)
284287letbind :: Name -> Raw -> Raw -> Elab' aux ()
285288letbind n t v = processTactic' (LetBind n t v)
286289
290+expandLet :: Name -> Term -> Elab' aux ()
291+expandLet n v = processTactic' (ExpandLet n v)
292+
287293rewrite :: Raw -> Elab' aux ()
288294rewrite tm = processTactic' (Rewrite tm)
289295
@@ -392,6 +398,8 @@ match_apply = apply' match_fill
392398apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]
393399apply' fillt fn imps =
394400 do args <- prepare_apply fn (map fst imps)
401+ env <- get_env
402+ g <- goal
395403 fillt (raw_apply fn (map Var args))
396404 -- _Don't_ solve the arguments we're specifying by hand.
397405 -- (remove from unified list before calling end_unify)
src/Core/ProofState.hs+14
@@ -58,6 +58,7 @@ data Tactic = Attack
5858 | StartUnify Name
5959 | EndUnify
6060 | Compute
61+ | Simplify
6162 | HNF_Compute
6263 | EvalIn Raw
6364 | CheckIn Raw
@@ -65,6 +66,7 @@ data Tactic = Attack
6566 | IntroTy Raw (Maybe Name)
6667 | Forall Name Raw
6768 | LetBind Name Raw Raw
69+ | ExpandLet Name Term
6870 | Rewrite Raw
6971 | Equiv Raw
7072 | PatVar Name
@@ -504,6 +506,10 @@ letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
504506 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
505507letbind n ty val ctxt env _ = fail "Can't let bind here"
506508
509+expandLet :: Name -> Term -> RunTactic
510+expandLet n v ctxt env tm =
511+ return $ subst n v tm
512+
507513rewrite :: Raw -> RunTactic
508514rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
509515 do (tmv, tmt) <- lift $ check ctxt env tm
@@ -570,6 +576,12 @@ hnf_compute ctxt env (Bind x (Hole ty) sc) =
570576 return $ Bind x (Hole ty') sc
571577hnf_compute ctxt env t = return t
572578
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+
573585check_in :: Raw -> RunTactic
574586check_in t ctxt env tm =
575587 do (val, valty) <- lift $ check ctxt env t
@@ -726,11 +738,13 @@ process t h = tactic (Just h) (mktac t)
726738 mktac Solve = solve
727739 mktac (StartUnify n) = start_unify n
728740 mktac Compute = compute
741+ mktac Simplify = Core.ProofState.simplify
729742 mktac HNF_Compute = hnf_compute
730743 mktac (Intro n) = intro n
731744 mktac (IntroTy ty n) = introTy ty n
732745 mktac (Forall n t) = forall n t
733746 mktac (LetBind n t v) = letbind n t v
747+ mktac (ExpandLet n b) = expandLet n b
734748 mktac (Rewrite t) = rewrite t
735749 mktac (Equiv t) = equiv t
736750 mktac (PatVar n) = patvar n
src/Core/TT.hs+1−1
@@ -605,7 +605,7 @@ pToV' n i (P _ x _) | n == x = V i
605605pToV' n i (Bind x b sc)
606606-- We can assume the inner scope has been pToVed already, so continue to
607607-- 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
609609 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
610610pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)
611611pToV' 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] ->
3434 TC [(Name, TT Name)]
3535match_unify ctxt env topx topy dont holes =
3636-- trace ("Matching " ++ show (topx, topy)) $
37− case runStateT (un [] topx topy) (UI 0 []) of
37+ case runStateT (un [] topx topy) (UI 0 []) of
3838 OK (v, UI _ []) -> return (filter notTrivial v)
3939 res ->
4040 let topxn = normalise ctxt env topx
@@ -100,6 +100,14 @@ match_unify ctxt env topx topy dont holes =
100100notTrivial (x, P _ x' _) = x /= x'
101101notTrivial _ = True
102102
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+
103111
104112unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
105113 TC ([(Name, TT Name)], Fails)
@@ -107,7 +115,8 @@ unify ctxt env topx topy dont holes =
107115-- trace ("Unifying " ++ show (topx, topy)) $
108116 -- don't bother if topx and topy are different at the head
109117 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+ [])
111120 res ->
112121 let topxn = normalise ctxt env topx
113122 topyn = normalise ctxt env topy in
@@ -115,7 +124,8 @@ unify ctxt env topx topy dont holes =
115124 case runStateT (un False [] topxn topyn)
116125 (UI 0 []) of
117126 OK (v, UI _ fails) ->
118− return (filter notTrivial v, reverse fails)
127+ return (filter notTrivial v,
128+ reverse fails)
119129-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
120130 Error e -> tfail e
121131 where
src/Idris/ElabTerm.hs+5−1
@@ -285,8 +285,12 @@ elab ist info pattern tcgen fn tm
285285 elabE (True, a) ty
286286 focus valn
287287 elabE (True, a) val
288+ env <- get_env
288289 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)
290294 solve
291295 elab' ina tm@(PApp fc (PInferRef _ f) args) = do
292296 rty <- goal