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

perf: try structure eta after delta

Browse source
This commit is contained in:
Gabriel Ebner 2023-04-05 11:55:20 -07:00 • committed by Leonardo de Moura
parent 9211dd6541
commit 89cb94fcab
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/ExprDefEq.lean
View file

@ -1729,13 +1729,17 @@ private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
whenUndefDo (isDefEqEta t s) do
whenUndefDo (isDefEqEta s t) do
-- TODO: investigate whether this is the place for putting this check
if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then return true
if (← isDefEqProj t s) then return true
whenUndefDo (isDefEqNative t s) do
whenUndefDo (isDefEqNat t s) do
whenUndefDo (isDefEqOffset t s) do
whenUndefDo (isDefEqDelta t s) do
-- We try structure eta *after* lazy delta reduction;
-- otherwise we would end up applying it at every step of a reduction chain
-- as soon as one of the sides is a constructor application,
-- which is very costly because it requires us to unify the fields.
if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
return true
if t.isConst && s.isConst then
if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then