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

feat: activate all passes

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-07 16:17:31 -08:00
parent 828a815821
commit a5dadfdb7a
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/LCNF/Passes.lean
View file

@ -45,7 +45,6 @@ def builtinPassManager : PassManager := {
init,
pullInstances,
cse,
/-
simp,
floatLetIn,
findJoinPoints,
@ -56,9 +55,7 @@ def builtinPassManager : PassManager := {
specialize,
simp (occurrence := 2),
cse (occurrence := 1),
-/
saveBase, -- End of base phase
/-
toMono,
simp (occurrence := 3) (phase := .mono),
reduceJpArity (phase := .mono),
@ -72,7 +69,6 @@ def builtinPassManager : PassManager := {
extendJoinPointContext (phase := .mono) (occurrence := 1),
simp (occurrence := 5) (phase := .mono),
cse (occurrence := 2) (phase := .mono),
-/
saveMono -- End of mono phase
]
}