From f05df7c511edebd855e46b9981d0ba500c257a73 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Jun 2019 19:07:07 -0700 Subject: [PATCH] fix(library/init/lean/compiler/ir/simpcase): missing optimization --- library/init/lean/compiler/ir/simpcase.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/library/init/lean/compiler/ir/simpcase.lean b/library/init/lean/compiler/ir/simpcase.lean index 8820540b38..e42a7a061a 100644 --- a/library/init/lean/compiler/ir/simpcase.lean +++ b/library/init/lean/compiler/ir/simpcase.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.lean.compiler.ir.basic +import init.lean.compiler.ir.format namespace Lean namespace IR @@ -17,12 +18,15 @@ else let alts := alts.pop in alts.push (Alt.default last.body) +private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := +let aBody := (alts.get i).body in +alts.iterateFrom 1 (i + 1) $ λ _ a' n, + if a'.body == aBody then n+1 else n + private def maxOccs (alts : Array Alt) : Alt × Nat := -alts.iterateFrom (alts.get 0, 1) 1 $ λ i a p, - let aBody := a.body in - let noccs := alts.iterateFrom 1 (i.val + 1) $ λ _ a' n, - if a'.body == aBody then n+1 else n in - if noccs > p.2 then (a, noccs) else p +alts.iterateFrom (alts.get 0, getOccsOf alts 0) 1 $ λ i a p, + let noccs := getOccsOf alts i.val in + if noccs > p.2 then (alts.fget i, noccs) else p private def addDefault (alts : Array Alt) : Array Alt := if alts.size <= 1 || alts.any Alt.isDefault then alts