chore: re-enable pullInstances and cse passes

This commit is contained in:
Leonardo de Moura 2022-10-31 07:57:27 -07:00
parent 691afbfdc8
commit c8eab4478d
2 changed files with 4 additions and 8 deletions

View file

@ -42,10 +42,10 @@ def saveMono : Pass :=
def builtinPassManager : PassManager := {
passes := #[
init
/-
init,
pullInstances,
cse,
cse
/-
simp,
floatLetIn,
findJoinPoints,

View file

@ -8,10 +8,6 @@ import Lean.Compiler.LCNF.DependsOn
import Lean.Compiler.LCNF.Types
import Lean.Compiler.LCNF.PassManager
set_option warningAsError false
#exit
namespace Lean.Compiler.LCNF
namespace PullLetDecls
@ -107,7 +103,7 @@ def Decl.pullInstances (decl : Decl) : CompilerM Decl :=
decl.pullLetDecls fun letDecl candidates => do
if (← isClass? letDecl.type).isSome then
return true
else if let .proj _ _ (.fvar fvarId) := letDecl.value then
else if let .proj _ _ fvarId := letDecl.value then
return candidates.contains fvarId
else
return false