max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/compiler/ir/rc): use updated ctx at addDecForAlt

Browse source 
Compiler was introducing unnecessary `dec` operations
This commit is contained in:
Leonardo de Moura 2019-05-24 19:20:20 -07:00
parent fa7e17c5bb
commit 4b896bc71c
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/compiler/ir/rc.lean
View file

@ -247,7 +247,8 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap in
let alts := alts.hmap $ λ alt, match alt with
| Alt.ctor c b :=
let (b, altLiveVars) := visitFnBody b (updateRefUsingCtorInfo ctx x c) in
let ctx := updateRefUsingCtorInfo ctx x c in
let (b, altLiveVars) := visitFnBody b ctx in
let b := addDecForAlt ctx caseLiveVars altLiveVars b in
Alt.ctor c b
| Alt.default b :=