From 85d45c4062a42812e7cf48ece854198e4e2d7c5d Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Fri, 31 May 2024 23:08:12 +0100 Subject: [PATCH 1/5] perf: optimize `isClassQuickConst` --- src/Lean/Meta/Basic.lean | 40 ++++++++++------------------------------ 1 file changed, 10 insertions(+), 30 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index ad6b0f36c027..3db3a3f7d2b4 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -986,34 +986,14 @@ 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 + if let some (.defnInfo val) := (← getEnv).find? constName then + if ← isReducible val.name then + return .undef -- We may be able to unfold the definition + return .none private partial def isClassQuick? : Expr → MetaM (LOption Name) | .bvar .. => return .none @@ -1173,14 +1153,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: From fd831ac1b3bff4fcf07f7b53d39ddade13a2142d Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 1 Jun 2024 00:13:57 +0100 Subject: [PATCH 2/5] revert, to see perf diff --- src/Lean/Meta/Basic.lean | 40 ++++++++++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 10 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 3db3a3f7d2b4..ad6b0f36c027 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -986,14 +986,34 @@ 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 - if let some (.defnInfo val) := (← getEnv).find? constName then - if ← isReducible val.name then - return .undef -- We may be able to unfold the definition - return .none + match (← getConstTemp? constName) with + | some (.defnInfo ..) => return .undef -- We may be able to unfold the definition + | _ => return .none private partial def isClassQuick? : Expr → MetaM (LOption Name) | .bvar .. => return .none @@ -1153,13 +1173,13 @@ 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 -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 -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 /-- `isClass? type` return `some ClsName` if `type` is an instance of the class `ClsName`. From 8f26b78297f2aaa3556f296c2e8586fba0ce889a Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 1 Jun 2024 01:27:09 +0100 Subject: [PATCH 3/5] Revert "revert, to see perf diff" This reverts commit fd831ac1b3bff4fcf07f7b53d39ddade13a2142d. --- src/Lean/Meta/Basic.lean | 40 ++++++++++------------------------------ 1 file changed, 10 insertions(+), 30 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index ad6b0f36c027..3db3a3f7d2b4 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -986,34 +986,14 @@ 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 + if let some (.defnInfo val) := (← getEnv).find? constName then + if ← isReducible val.name then + return .undef -- We may be able to unfold the definition + return .none private partial def isClassQuick? : Expr → MetaM (LOption Name) | .bvar .. => return .none @@ -1173,14 +1153,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: From afa80d30384b46b9323c53fa27b246910f098b2b Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 1 Jun 2024 13:08:43 +0100 Subject: [PATCH 4/5] fix throwing error --- src/Lean/Meta/Basic.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 3db3a3f7d2b4..912792b6b51f 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -990,10 +990,13 @@ private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do if isClass (← getEnv) constName then return .some constName else - if let some (.defnInfo val) := (← getEnv).find? constName then - if ← isReducible val.name then - return .undef -- We may be able to unfold the definition - return .none + match (← getEnv).find? constName with + | some info => + if let .defnInfo val := info then + if ← isReducible val.name then + return .undef -- We may be able to unfold the definition + return .none + | none => throwUnknownConstant constName private partial def isClassQuick? : Expr → MetaM (LOption Name) | .bvar .. => return .none From b5c7848f1a8ad06fab01595767c9b1275ea994e8 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 1 Jun 2024 16:10:17 +0100 Subject: [PATCH 5/5] use explicit `else` --- src/Lean/Meta/Basic.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 912792b6b51f..1decec858071 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -991,11 +991,12 @@ private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do return .some constName else match (← getEnv).find? constName with - | some info => - if let .defnInfo val := info then - if ← isReducible val.name then - return .undef -- We may be able to unfold the definition - return .none + | 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) @@ -1301,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