Skip to content

Commit 1592932

Browse files
committed
perf: match compilation to use exfalso early
This PR lets match compilation use exfalso as soon as no alternatives are left. This way, the compiler does not have to look at subsequent case splits.
1 parent 206eb73 commit 1592932

File tree

1 file changed

+16
-0
lines changed

1 file changed

+16
-0
lines changed

src/Lean/Meta/Match/Match.lean

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -746,12 +746,28 @@ private def checkNextPatternTypes (p : Problem) : MetaM Unit := do
746746
unless (← isDefEq xType eType) do
747747
throwError "Type mismatch in pattern: Pattern{indentExpr e}\n{← mkHasTypeButIsExpectedMsg eType xType}"
748748

749+
def isExFalsoTransition (p : Problem) : MetaM Bool := do
750+
if p.alts.isEmpty then
751+
withGoalOf p do
752+
let targetType ← p.mvarId.getType
753+
return !targetType.isFalse
754+
else
755+
return false
756+
757+
def processExFalso (p : Problem) : MetaM Problem := do
758+
let mvarId' ← p.mvarId.exfalso
759+
return { p with mvarId := mvarId' }
760+
749761
private partial def process (p : Problem) : StateRefT State MetaM Unit := do
750762
traceState p
751763
let isInductive ← isCurrVarInductive p
752764
if isDone p then
753765
traceStep ("leaf")
754766
processLeaf p
767+
else if (← isExFalsoTransition p) then
768+
traceStep ("ex falso")
769+
let p ← processExFalso p
770+
process p
755771
else if hasAsPattern p then
756772
traceStep ("as-pattern")
757773
let p ← processAsPattern p

0 commit comments

Comments
 (0)