From 8ec03b09ec3f2b78a57a55fd49d1dbf05bccd6e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Oct 2019 14:55:48 -0700 Subject: [PATCH] fix: make sure `maxIndex` takes into account dead variables too --- library/Init/Lean/Compiler/IR/FreeVars.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/Init/Lean/Compiler/IR/FreeVars.lean b/library/Init/Lean/Compiler/IR/FreeVars.lean index 861331020c..98c8894058 100644 --- a/library/Init/Lean/Compiler/IR/FreeVars.lean +++ b/library/Init/Lean/Compiler/IR/FreeVars.lean @@ -58,8 +58,8 @@ private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collecto collectArray alts $ fun alt => f alt.body partial def collectFnBody : FnBody → Collector -| FnBody.vdecl x _ v b => collectExpr v >> collectFnBody b -| FnBody.jdecl j ys v b => collectFnBody v >> collectParams ys >> collectFnBody b +| FnBody.vdecl x _ v b => collectVar x >> collectExpr v >> collectFnBody b +| FnBody.jdecl j ys v b => collectJP j >> collectFnBody v >> collectParams ys >> collectFnBody b | FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b | FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b | FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b