1c87b5e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Thread the fresh name counter through runElab

Before, recursive reflected elaborator invocations could lead to name capture, because each recursive invocation had its own fresh name counter. This made combining their results unsafe. Now, they share a counter, which makes it safe again.

commit1c87b5e26a364bcf98d6e030c19665c7fdba765b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Aug 2015, 22:36 (11 years ago) parent6ada023

1 file changed+7−3

compare with master

unifiedsplit

src/Idris/Elab/Term.hs+7−3

src/Idris/Elab/Term.hs+7−3

@@ -2157,10 +2157,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

21572157 datatypes <- get_datatypes

21582158 env <- get_env

21592159 (_, ES (p, aux') _ _) <-

2160− lift $ runElab aux (runElabAction ist fc [] script ns)

2161− (newProof recH ctxt datatypes goalTT)

2160+ do (ES (current_p, _) _ _) <- get

2161+ lift $ runElab aux (runElabAction ist fc [] script ns)

2162+ ((newProof recH ctxt datatypes goalTT)

2163+ { nextname = nextname current_p})

21622164 let tm_out = getProofTerm (pterm p)

2163− updateAux $ const aux'

2165+ do (ES (prf, _) s e) <- get

2166+ let p' = prf { nextname = nextname p }

2167+ put (ES (p', aux') s e)

21642168 env' <- get_env

21652169 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

21662170 let (tm', ty') = (reflect tm, reflect ty)