Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

perf: optimize isClassQuickConst? #4319

Closed
wants to merge 5 commits into from
Closed

perf: optimize isClassQuickConst? #4319

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
85d45c4
perf: optimize `isClassQuickConst`
JovanGerb May 31, 2024
fd831ac
revert, to see perf diff
JovanGerb May 31, 2024
8f26b78
Revert "revert, to see perf diff"
JovanGerb Jun 1, 2024
afa80d3
fix throwing error
JovanGerb Jun 1, 2024
b5c7848
use explicit `else`
JovanGerb Jun 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 15 additions & 31 deletions src/Lean/Meta/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -986,34 +986,18 @@ def getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
else
return none

private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
match (← getTransparency) with
| TransparencyMode.all => return some info
| TransparencyMode.default => return some info
| _ =>
if (← isReducible info.name) then
return some info
else
return none

/-- Remark: we later define `getUnfoldableConst?` at `GetConst.lean` after we define `Instances.lean`.
This method is only used to implement `isClassQuickConst?`.
It is very similar to `getUnfoldableConst?`, but it returns none when `TransparencyMode.instances` and
`constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/
private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
match (← getEnv).find? constName with
| some (info@(ConstantInfo.thmInfo _)) => getTheoremInfo info
| some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
| some info => pure (some info)
| none => throwUnknownConstant constName

private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
if isClass (← getEnv) constName then
return .some constName
else
match (← getConstTemp? constName) with
| some (.defnInfo ..) => return .undef -- We may be able to unfold the definition
| _ => return .none
match (← getEnv).find? constName with
| some (.defnInfo val) =>
if ← isReducible val.name then
return .undef -- We may be able to unfold the definition
else
return .none
| some _ => return .none
| none => throwUnknownConstant constName

private partial def isClassQuick? : Expr → MetaM (LOption Name)
| .bvar .. => return .none
Expand Down Expand Up @@ -1173,14 +1157,14 @@ mutual
withReducible do -- when testing whether a type is a type class, we only unfold reducible constants.
forallTelescopeReducingAux type none (cleanupAnnotations := false) fun _ type => isClassApp? type

private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
match (← isClassQuick? type) with
| .none => return none
| .some c => return (some c)
| .undef => isClassExpensive? type

end

private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
match (← isClassQuick? type) with
| .none => return none
| .some c => return (some c)
| .undef => isClassExpensive? type

/--
`isClass? type` return `some ClsName` if `type` is an instance of the class `ClsName`.
Example:
Expand Down Expand Up @@ -1318,7 +1302,7 @@ where
match type with
| .forallE n d b bi =>
let d := d.instantiateRevRange j mvars.size mvars
let k := if bi.isInstImplicit then MetavarKind.synthetic else kind
let k := if bi.isInstImplicit then MetavarKind.synthetic else kind
let mvar ← mkFreshExprMVar d k n
let mvars := mvars.push mvar
let bis := bis.push bi
Expand Down
Loading