diff --git a/doc/examples/widgets.lean b/doc/examples/widgets.lean index 56b98f43bc..886f7914b6 100644 --- a/doc/examples/widgets.lean +++ b/doc/examples/widgets.lean @@ -111,8 +111,8 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) := withWaitFindSnapAtPos params.pos fun snap => do runTermElabM snap do let name ← resolveGlobalConstNoOverloadCore params.name - let some c ← Meta.getConst? name - | throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩ + let c ← try getConstInfo name + catch _ => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩ Widget.ppExprTagged c.type /-! diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index c7737f4937..2ed7c55f2d 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -833,9 +833,9 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) : else return none -/-- Remark: we later define `getConst?` at `GetConst.lean` after we define `Instances.lean`. +/-- 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 `getConst?`, but it returns none when `TransparencyMode.instances` and + 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 diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index daf7bce260..0a86085076 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1148,7 +1148,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do match t.getAppFn with | Expr.const c _ => - match (← getConst? c) with + match (← getUnfoldableConst? c) with | r@(some info) => if info.hasValue then return r else return none | _ => return none | _ => pure none diff --git a/src/Lean/Meta/GetConst.lean b/src/Lean/Meta/GetUnfoldableConst.lean similarity index 71% rename from src/Lean/Meta/GetConst.lean rename to src/Lean/Meta/GetUnfoldableConst.lean index e16e5161f0..77c7bee075 100644 --- a/src/Lean/Meta/GetConst.lean +++ b/src/Lean/Meta/GetUnfoldableConst.lean @@ -26,14 +26,25 @@ def canUnfold (info : ConstantInfo) : MetaM Bool := do else canUnfoldDefault ctx.config info -def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do +/-- +Look up a constant name, returning the `ConstantInfo` +if it should be unfolded at the current reducibility settings, +or `none` otherwise. + +This is part of the implementation of `whnf`. +External users wanting to look up names should be using `Lean.getConstInfo`. +-/ +def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do match (← getEnv).find? constName with | some (info@(.thmInfo _)) => getTheoremInfo info | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none | some info => return some info | none => throwUnknownConstant constName -def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do +/-- +As with `getUnfoldableConst?` but return `none` instead of failing if the constant is not found. +-/ +def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do match (← getEnv).find? constName with | some (info@(.thmInfo _)) => getTheoremInfo info | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index e876165c84..d4cfa085d9 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Structure import Lean.Util.Recognizers -import Lean.Meta.GetConst +import Lean.Meta.GetUnfoldableConst import Lean.Meta.FunInfo import Lean.Meta.Match.MatcherInfo import Lean.Meta.Match.MatchPatternAttr @@ -62,7 +62,7 @@ def isAuxDef (constName : Name) : MetaM Bool := do @[inline] private def matchConstAux {α} (e : Expr) (failK : Unit → MetaM α) (k : ConstantInfo → List Level → MetaM α) : MetaM α := match e with | Expr.const name lvls => do - let (some cinfo) ← getConst? name | failK () + let (some cinfo) ← getUnfoldableConst? name | failK () k cinfo lvls | _ => failK () @@ -71,7 +71,7 @@ def isAuxDef (constName : Name) : MetaM Bool := do -- =========================== private def getFirstCtor (d : Name) : MetaM (Option Name) := do - let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getConstNoEx? d | pure none + let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getUnfoldableConstNoEx? d | pure none return some ctor private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) := do @@ -209,7 +209,7 @@ private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : let major ← whnf major match major with | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do - let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getConstNoEx? majorFn | failK () + let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getUnfoldableConstNoEx? majorFn | failK () let f := recArgs[argPos]! let r := mkApp f majorArg let recArity := majorPos + 1 @@ -272,7 +272,7 @@ mutual | .mvar mvarId => return some mvarId | _ => getStuckMVar? e | .const fName _ => - match (← getConstNoEx? fName) with + match (← getUnfoldableConstNoEx? fName) with | some <| .recInfo recVal => isRecStuck? recVal e.getAppArgs | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs | _ => @@ -720,7 +720,7 @@ mutual if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then return none else - let some cinfo ← getConstNoEx? declName | pure none + let some cinfo ← getUnfoldableConstNoEx? declName | pure none unless cinfo.hasValue do return none deltaDefinition cinfo lvls (fun _ => pure none)