From 4606c35c40a8260a3384b161e7fd07f620c2107c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 31 Jan 2026 19:03:16 -0800 Subject: [PATCH] feat: `@[instance_reducible]` (#12247) This PR adds the new transparency setting `@[instance_reducible]`. We used to check whether a declaration had `instance` reducibility by using the `isInstance` predicate. However, this was not a robust solution because: - We have scoped instances, and `isInstance` returns `true` only if the scope is active. - We have auxiliary declarations used to construct instances manually, such as: ```lean def lt_wfRel : WellFoundedRelation Nat ``` `isInstance` also returns `false` for this kind of declaration. In both cases, the declaration may be (or may have been) used to construct an instance, but `isInstance` returns `false`. Thus, we claim it is a mistake to check the reducibility status using `isInstance`. `isInstance` indicates whether a declaration is available for the type class resolution mechanism, not its transparency status. **We are decoupling whether a declaration is available for type class resolution from its transparency status.** **Remak**: We need a update stage0 to complete this feature. --------- Co-authored-by: Sebastian Ullrich --- src/Init/Syntax.lean | 3 - src/Lean/Compiler/LCNF/Basic.lean | 2 +- src/Lean/Compiler/LCNF/LambdaLifting.lean | 2 +- .../Compiler/LCNF/Simp/InlineCandidate.lean | 2 +- src/Lean/Compiler/LCNF/Simp/Main.lean | 2 +- src/Lean/Compiler/LCNF/Specialize.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 4 + src/Lean/Elab/DefView.lean | 12 ++- src/Lean/Elab/Deriving/Basic.lean | 2 +- src/Lean/Elab/MutualDef.lean | 3 - src/Lean/Elab/Print.lean | 10 +- src/Lean/Elab/Structure.lean | 2 +- src/Lean/Elab/Tactic/Grind/Main.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Elab/Term/TermElabM.lean | 4 +- src/Lean/LibrarySuggestions/Basic.lean | 4 +- src/Lean/Meta/GetUnfoldableConst.lean | 9 +- src/Lean/Meta/Instances.lean | 47 +++++++++- src/Lean/Meta/SizeOf.lean | 2 +- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/Tactic/Grind/MBTC.lean | 2 +- src/Lean/ReducibilityAttrs.lean | 93 ++++++++++++------- stage0/src/stdlib_flags.h | 1 + tests/lean/defInst.lean.expected.out | 2 +- tests/lean/diamond4.lean.expected.out | 4 +- tests/lean/diamond6.lean.expected.out | 4 +- tests/lean/diamond7.lean.expected.out | 9 +- tests/lean/run/derivingBEq.lean | 4 +- tests/lean/run/derivingBEqLinear.lean | 4 +- tests/lean/run/derivingDelta.lean | 18 ++-- tests/lean/run/derivingInhabited.lean | 2 +- tests/lean/run/derivingRepr.lean | 2 +- tests/lean/run/diagnostics.lean | 18 +--- tests/lean/run/issue10678.lean | 12 +-- tests/lean/run/reduceBEqSimproc.lean | 6 +- tests/lean/run/structInst.lean | 8 +- tests/pkg/module/Module/Basic.lean | 2 +- 37 files changed, 185 insertions(+), 124 deletions(-) diff --git a/src/Init/Syntax.lean b/src/Init/Syntax.lean index 4e2b14f531..1b92164af8 100644 --- a/src/Init/Syntax.lean +++ b/src/Init/Syntax.lean @@ -3,12 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ - module - prelude public import Init.Data.Array.Set - public section /-! diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index 1db18432a1..5d8f6399a9 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -746,7 +746,7 @@ def Decl.isTemplateLike (decl : Decl pu) : CoreM Bool := do let env ← getEnv if ← hasLocalInst decl.type then return true -- `decl` applications will be specialized - else if Meta.isInstanceCore env decl.name then + else if (← isInstanceReducible decl.name) then return true -- `decl` is "fuel" for code specialization else if decl.inlineable || hasSpecializeAttribute env decl.name then return true -- `decl` is going to be inlined or specialized diff --git a/src/Lean/Compiler/LCNF/LambdaLifting.lean b/src/Lean/Compiler/LCNF/LambdaLifting.lean index d930ecb500..2882b8abe1 100644 --- a/src/Lean/Compiler/LCNF/LambdaLifting.lean +++ b/src/Lean/Compiler/LCNF/LambdaLifting.lean @@ -214,7 +214,7 @@ def eagerLambdaLifting : Pass where name := `eagerLambdaLifting run := fun decls => do decls.foldlM (init := #[]) fun decls decl => do - if decl.inlineable || (← Meta.isInstance decl.name) then + if decl.inlineable || (← isInstanceReducible decl.name) then return decls.push decl else return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (allowEtaContraction := false) (suffix := `_elam)) diff --git a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean index d84ce49f4c..f9f53045af 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean @@ -56,7 +56,7 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) : We assume that at the base phase these annotations are for the instance methods that have been lambda lifted. -/ if (← inBasePhase) then - if (← Meta.isInstance decl.name) then + if (← isInstanceReducible decl.name) then unless decl.name == ``instDecidableEqBool do /- TODO: remove this hack after we refactor `Decidable` as suggested by Gabriel. diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index abd12f151d..a9d9a6169f 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -76,7 +76,7 @@ def etaPolyApp? (letDecl : LetDecl .pure) : OptionT SimpM (FunDecl .pure) := do let .const declName us args := letDecl.value | failure let some info := (← getEnv).find? declName | failure guard <| (← hasLocalInst info.type) - guard <| !(← Meta.isInstance declName) + guard <| !(← isInstanceReducible declName) let some ⟨.pure, decl⟩ ← getDecl? declName | failure guard <| decl.getArity > args.size let params ← mkNewParams letDecl.type diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 9c4cce17ab..c304da5cb3 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -399,7 +399,7 @@ mutual partial def specializeApp? (e : LetValue .pure) : SpecializeM (Option (LetValue .pure)) := do let .const declName us args := e | return none if args.isEmpty then return none - if (← Meta.isInstance declName) then return none + if (← isInstanceReducible declName) then return none let some specEntry ← getSpecEntry? declName | return none unless (← shouldSpecialize specEntry args) do return none let some ⟨.pure, decl⟩ ← getDecl? declName | return none diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index e248fd5ff7..fcf18b4867 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -125,6 +125,10 @@ def Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifier def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers := { modifiers with attrs := modifiers.attrs.filter p } +/-- Returns `true` if `modifiers` contains an attribute satisfying `p`. -/ +def Modifiers.anyAttr (modifiers : Modifiers) (p : Attribute → Bool) : Bool := + modifiers.attrs.any p + instance : ToFormat Modifiers := ⟨fun m => let components : List Format := (match m.docString? with diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 6cbbdeaa53..9a2ef00d81 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ module - prelude public import Lean.Elab.DeclNameGen public import Lean.Elab.DeclUtil - public section - namespace Lean.Elab inductive DefKind where @@ -165,11 +162,18 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView := def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal + /- + **Note**: add `instance_reducible` attribute if declaration is not already marked with `@[reducible]` + -/ + let modifiers := if modifiers.anyAttr fun attr => attr.name == `reducible then + modifiers + else + modifiers.addAttr { name := `instance_reducible } let attrKind ← liftMacroM <| toAttributeKind stx[0] let prio ← liftMacroM <| expandOptNamedPrio stx[2] let attrStx ← `(attr| instance $(quote prio):num) - let (binders, type) := expandDeclSig stx[4] let modifiers := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx } + let (binders, type) := expandDeclSig stx[4] let declId ← match stx[3].getOptional? with | some declId => if ← isTracingEnabledFor `Elab.instance.mkInstanceName then diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 674678ed97..dc2570abe4 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -205,7 +205,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints addAndCompile (logCompileErrors := !(← read).isNoncomputableSection) <| Declaration.defnDecl decl trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`" - addInstance instName AttributeKind.global (eval_prio default) + registerInstance instName AttributeKind.global (eval_prio default) addDeclarationRangesFromSyntax instName (← getRef) end Term diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 8e12b0ae9c..ed3302e03f 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Elab.Deriving.Basic public import Lean.Elab.PreDefinition.Main import all Lean.Elab.ErrorUtils - public section - namespace Lean.Elab open Lean.Parser.Term diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 59441a0bce..f4ad4cc5d0 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Meta.Eqns public import Lean.Elab.Command import Lean.PrettyPrinter.Delaborator.Builtins - public section - namespace Lean.Elab.Command private def throwUnknownId (id : Name) : CommandElabM Unit := @@ -29,9 +26,10 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData := private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do let mut attrs := #[] match (← getReducibilityStatus id) with - | ReducibilityStatus.irreducible => attrs := attrs.push m!"irreducible" - | ReducibilityStatus.reducible => attrs := attrs.push m!"reducible" - | ReducibilityStatus.semireducible => pure () + | .irreducible => attrs := attrs.push m!"irreducible" + | .reducible => attrs := attrs.push m!"reducible" + | .instanceReducible => attrs := attrs.push m!"instance_reducible" + | .semireducible => pure () let env ← getEnv if env.header.isModule && (env.setExporting true |>.find? id |>.any (·.isDefinition)) then diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 907f6962e0..fe2650c0e9 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1498,7 +1498,7 @@ private def addParentInstances (parents : Array StructureParentInfo) : MetaM Uni let instParents := instParents.filter fun parent => !resOrders.any (fun resOrder => resOrder[1...*].any (· == parent.structName)) for instParent in instParents do - addInstance instParent.projFn AttributeKind.global (eval_prio default) + registerInstance instParent.projFn AttributeKind.global (eval_prio default) @[builtin_inductive_elab Lean.Parser.Command.«structure»] def elabStructureCommand : InductiveElabDescr where diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index 3a4cc1347a..39f5bcdb65 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/src/Lean/Elab/Tactic/Grind/Main.lean @@ -212,7 +212,7 @@ def elabGrindLocals (params : Grind.Params) : MetaM Grind.Params := do -- Filter similar to LibrarySuggestions.isDeniedPremise (but inlined to avoid dependency) -- Skip internal details, but allow private names (which are accessible from current module) if name.isInternalDetail && !isPrivateName name then continue - if (← Meta.isInstance name) then continue + if (← isInstanceReducible name) then continue match ci with | .defnInfo _ => try diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index d07c490fd5..89923ae104 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -427,7 +427,7 @@ def elabSimpLocals (thms : SimpTheorems) (kind : SimpKind) : MetaM SimpTheorems for (name, ci) in env.constants.map₂.toList do -- Skip internal details, but allow private names (which are accessible from current module) if name.isInternalDetail && !isPrivateName name then continue - if (← Meta.isInstance name) then continue + if (← isInstanceReducible name) then continue match ci with | .defnInfo _ => -- Definitions are added to unfold diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index b0dbe4326c..2bdd3a0423 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -1024,8 +1024,8 @@ private def applyAttributesCore withRef attr.stx do withLogging do let env ← getEnv match getAttributeImpl env attr.name with - | Except.error errMsg => throwError errMsg - | Except.ok attrImpl => + | .error errMsg => throwError errMsg + | .ok attrImpl => let runAttr := attrImpl.add declName attr.stx attr.kind let runAttr := do -- not truly an elaborator, but a sensible target for go-to-definition diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean index 4bcc3b82d2..74bef70263 100644 --- a/src/Lean/LibrarySuggestions/Basic.lean +++ b/src/Lean/LibrarySuggestions/Basic.lean @@ -76,7 +76,7 @@ unsafe def fold {α : Type} (f : Name → α → MetaM α) (e : Expr) (acc : α) return acc else modify fun s => { s with visitedConsts := s.visitedConsts.insert c } - if ← isInstance c then + if ← isInstanceReducible c then return acc else f c acc @@ -320,7 +320,7 @@ def isDeniedPremise (env : Environment) (name : Name) (allowPrivate : Bool := fa if name == ``sorryAx then return true -- Allow private names through if allowPrivate is set (e.g., for currentFile selector) if name.isInternalDetail && !(allowPrivate && isPrivateName name) then return true - if Lean.Meta.isInstanceCore env name then return true + if isInstanceReducibleCore env name then return true if Lean.Linter.isDeprecated env name then return true if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true if let some moduleIdx := env.getModuleIdxFor? name then diff --git a/src/Lean/Meta/GetUnfoldableConst.lean b/src/Lean/Meta/GetUnfoldableConst.lean index f9fb962dd1..0a7d366a74 100644 --- a/src/Lean/Meta/GetUnfoldableConst.lean +++ b/src/Lean/Meta/GetUnfoldableConst.lean @@ -5,7 +5,8 @@ Authors: Leonardo de Moura -/ module prelude -public import Lean.Meta.GlobalInstances +public import Lean.Meta.GlobalInstances -- **TODO**: Delete after update stage0 +import Lean.ReducibilityAttrs public section namespace Lean.Meta @@ -15,9 +16,11 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool : | .all => return true | .default => return !(← isIrreducible info.name) | m => - if (← isReducible info.name) then + let status ← getReducibilityStatus info.name + if status == .reducible then return true - else if m == .instances && isGlobalInstance (← getEnv) info.name then + -- **TODO**: Delete `isGlobalInstance` after update stage0 + else if m == .instances && (isGlobalInstance (← getEnv) info.name || status == .instanceReducible) then return true else return false diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 03b5cff592..ea299e5e5b 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -8,6 +8,7 @@ prelude public import Init.Data.Range.Polymorphic.Stream public import Lean.Meta.DiscrTree.Main public import Lean.Meta.CollectMVars +import Lean.ReducibilityAttrs import Lean.Meta.WHNF public section namespace Lean.Meta @@ -230,11 +231,44 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do let c ← mkConstWithLevelParams declName let keys ← mkInstanceKey c + let status ← getReducibilityStatus declName + unless status matches .reducible | .instanceReducible do + let info ← getConstInfo declName + if info.isDefinition then + -- **TODO**: uncomment after update stage0 + -- logWarning m!"instance `{declName}` must be marked with @[reducible] or @[instance_reducible]" + pure () addGlobalInstance declName attrKind let projInfo? ← getProjectionFnInfo? declName let synthOrder ← computeSynthOrder c projInfo? instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind +/- +Adds instance **and** marks it with reducibility status `@[instance_reducible]`. We use this function +to elaborate `instance` command. + +**Note**: We used to check whether `declName` had `instance` reducibility by using `isInstance declName`. +However, this was not a robust solution because: + +- We have scoped instances, and `isInstance declName` returns true only if the scope is active. + +- We have auxiliary declarations used to construct instances manually, such as: + ``` + def lt_wfRel : WellFoundedRelation Nat + ``` + `isInstance` also returns `false` for this kind of declaration. + +In both cases, the declaration may be (or may have been) used to construct an instance, but `isInstance` +returns `false`. We claim it is a mistake to check the reducibility status using `isInstance`. +`isInstance` indicates whether a declaration is available for the type class resolution mechanism, +not its transparency status. + +Thus, we added a new transparency setting and set it here. +-/ +def registerInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do + setReducibilityStatus declName .instanceReducible + addInstance declName attrKind prio + /-- Registers type class instances. @@ -334,4 +368,15 @@ def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet := def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) := return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD [] -end Lean.Meta +end Meta + +-- **TODO**: Move to `ReducibilityAttrs.lean` after update stage0 +def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool := + getReducibilityStatusCore env declName matches .instanceReducible + || Meta.isInstanceCore env declName -- **TODO**: Delete after update stage0 + +/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/ +def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := + return isInstanceReducibleCore (← getEnv) declName + +end Lean diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index e5058362d9..3981cd7388 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -519,7 +519,7 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do safety := .safe hints := .abbrev } - addInstance instDeclName AttributeKind.global (eval_prio default) + registerInstance instDeclName AttributeKind.global (eval_prio default) enableRealizationsForConst instDeclName if genSizeOfSpec.get (← getOptions) then mkSizeOfSpecTheorems indInfo.all.toArray fns recMap diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 809341ae14..eea50e3174 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -445,7 +445,7 @@ Returns `true` if we should use `funCC` for applications of the given constant s private def useFunCongrAtDecl (declName : Name) : GrindM Bool := do if (← hasFunCCModifier declName) then return true - if (← isInstance declName) then + if (← isInstanceReducible declName) then /- **Note**: Instances are support elements. No `funCC` -/ return false if let some projInfo ← getProjectionFnInfo? declName then diff --git a/src/Lean/Meta/Tactic/Grind/MBTC.lean b/src/Lean/Meta/Tactic/Grind/MBTC.lean index bf91d3b180..56b5b1cdca 100644 --- a/src/Lean/Meta/Tactic/Grind/MBTC.lean +++ b/src/Lean/Meta/Tactic/Grind/MBTC.lean @@ -85,7 +85,7 @@ private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do /-- Returns `true` if `f` is a type class instance -/ private def isFnInstance (f : Expr) : CoreM Bool := do let .const declName _ := f | return false - isInstance declName + isInstanceReducible declName /-- Model-based theory combination. -/ def mbtc (ctx : MBTC.Context) : GoalM Bool := do diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index e93eb55721..f6c2911703 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -16,13 +16,14 @@ namespace Lean Reducibility status for a definition. -/ inductive ReducibilityStatus where - | reducible | semireducible | irreducible + | reducible | semireducible | irreducible | instanceReducible deriving Inhabited, Repr, BEq def ReducibilityStatus.toAttrString : ReducibilityStatus → String | .reducible => "[reducible]" | .irreducible => "[irreducible]" | .semireducible => "[semireducible]" + | .instanceReducible => "[instance_reducible]" builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ← registerPersistentEnvExtension { @@ -111,37 +112,52 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : -- downstream non-`module`s. withoutExporting do unless allowUnsafeReducibility.get (← getOptions) do - match (← getConstInfo declName) with - | .defnInfo _ => - let statusOld := getReducibilityStatusCore (← getEnv) declName - match attrKind with - | .scoped => - throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}" - | .global => - if (← getEnv).getModuleIdxFor? declName matches some _ then - throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}" - match status with - | .reducible => - unless statusOld matches .semireducible do - throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" - | .irreducible => - unless statusOld matches .semireducible do - throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" - | .semireducible => - throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}" - | .local => - match status with - | .reducible => - throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}" - | .irreducible => - unless statusOld matches .semireducible do - throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}" - | .semireducible => - unless statusOld matches .irreducible do - throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}" - | _ => throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}" + unless (← getConstInfo declName).isDefinition do + throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}" + let statusOld := getReducibilityStatusCore (← getEnv) declName + match attrKind with + | .scoped => + throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}" + | .global => + if (← getEnv).getModuleIdxFor? declName matches some _ then + throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}" + match status with + | .reducible => + unless statusOld matches .semireducible do + throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" + | .irreducible => + unless statusOld matches .semireducible do + throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" + | .instanceReducible => + unless statusOld matches .semireducible do + throwError "failed to set `[instance_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" + | .semireducible => + throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}" + | .local => + match status with + | .reducible => + throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}" + | .irreducible => + unless statusOld matches .semireducible do + throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}" + | .instanceReducible => + unless statusOld matches .semireducible do + throwError "failed to set `[local instance_reducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}" + | .semireducible => + unless statusOld matches .irreducible do + throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}" + +/- +**Note**: Some instances are not definitions, but theorems. Thus, they don't need the `[instance_reducible]` attribute, +but the current frontend adds the attribute `[instance_reducible]` when pre-processing the command `instance` before +we know whether its type is a proposition or not. Thus, we just skip these annotations for now. +-/ +private def ignoreAttr (status : ReducibilityStatus) (declName : Name) : CoreM Bool := do + let .instanceReducible := status | return false + return !(← getConstInfo declName).isDefinition private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do + if (← ignoreAttr status declName) then return () Attribute.Builtin.ensureNoArgs stx validate declName status attrKind let ns ← getCurrNamespace @@ -174,6 +190,15 @@ builtin_initialize applicationTime := .afterTypeChecking } +builtin_initialize + registerBuiltinAttribute { + ref := by exact decl_name% + name := `instance_reducible + descr := "semireducible declaration" + add := addAttr .instanceReducible + applicationTime := .afterTypeChecking + } + /-- Return the reducibility attribute for the given declaration. -/ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do return getReducibilityStatusCore (← getEnv) declName @@ -188,15 +213,11 @@ def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit := /-- Return `true` if the given declaration has been marked as `[reducible]`. -/ def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do - match (← getReducibilityStatus declName) with - | .reducible => return true - | _ => return false + return (← getReducibilityStatus declName) matches .reducible /-- Return `true` if the given declaration has been marked as `[irreducible]` -/ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do - match (← getReducibilityStatus declName) with - | .irreducible => return true - | _ => return false + return (← getReducibilityStatus declName) matches .irreducible /-- Set the given declaration as `[irreducible]` -/ def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit := diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ad491b0de1 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean { diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out index 4a75b9a413..e560d73f8e 100644 --- a/tests/lean/defInst.lean.expected.out +++ b/tests/lean/defInst.lean.expected.out @@ -10,5 +10,5 @@ fun x y => x == y : Foo → Foo → Bool false true true -def instMonadM : Monad M := +@[instance_reducible] def instMonadM : Monad M := ReaderT.instMonad diff --git a/tests/lean/diamond4.lean.expected.out b/tests/lean/diamond4.lean.expected.out index 7bbc3bd738..fe3a7b1588 100644 --- a/tests/lean/diamond4.lean.expected.out +++ b/tests/lean/diamond4.lean.expected.out @@ -1,4 +1,4 @@ -def D.toB : {α : Type} → [self : D α] → B α := +@[instance_reducible] def D.toB : {α : Type} → [self : D α] → B α := fun (α : Type) [self : D α] => self.1 -def D.toC : {α : Type} → [self : D α] → C α := +@[instance_reducible] def D.toC : {α : Type} → [self : D α] → C α := fun (α : Type) (self : D α) => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self) diff --git a/tests/lean/diamond6.lean.expected.out b/tests/lean/diamond6.lean.expected.out index 43b66d2836..6d13d982d3 100644 --- a/tests/lean/diamond6.lean.expected.out +++ b/tests/lean/diamond6.lean.expected.out @@ -16,7 +16,7 @@ FooAC.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α] @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) : FooAC α -def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α := +@[instance_reducible] def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α := fun (α : Type) (self : FooAC α) => @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self) (@FooAC.mul_assoc α self) @@ -39,7 +39,7 @@ FooAC'.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α] @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) : FooAC' α -def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α := +@[instance_reducible] def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α := fun (α : Type) (self : FooAC' α) => @FooAssoc'.mk α (@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self) diff --git a/tests/lean/diamond7.lean.expected.out b/tests/lean/diamond7.lean.expected.out index 1621b5efbb..5736e5cc3d 100644 --- a/tests/lean/diamond7.lean.expected.out +++ b/tests/lean/diamond7.lean.expected.out @@ -6,7 +6,8 @@ CommMonoid.mk.{u} {α : Type u} [toMonoid : Monoid.{u} α] (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α toMonoid))) b a)) : CommMonoid.{u} α -def CommMonoid.toCommSemigroup.{u} : {α : Type u} → [self : CommMonoid.{u} α] → CommSemigroup.{u} α := +@[instance_reducible] def CommMonoid.toCommSemigroup.{u} : {α : Type u} → + [self : CommMonoid.{u} α] → CommSemigroup.{u} α := fun (α : Type u) (self : CommMonoid.{u} α) => @CommSemigroup.mk.{u} α (@Monoid.toSemigroup.{u} α (@CommMonoid.toMonoid.{u} α self)) (@CommMonoid.mul_comm.{u} α self) @@ -19,12 +20,12 @@ CommGroup.mk.{u} {α : Type u} [toGroup : Group.{u} α] (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α (@Group.toMonoid.{u} α toGroup)))) b a)) : CommGroup.{u} α -def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α := +@[instance_reducible] def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α := fun (α : Type u) (self : CommGroup.{u} α) => @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self) Field.mk.{u} {α : Type u} [toDivisionRing : DivisionRing α] (mul_comm : ∀ (a b : α), a * b = b * a) : Field α -def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α := +@[instance_reducible] def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α := fun (α : Type u) [self : Field.{u} α] => self.1 -def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α := +@[instance_reducible] def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α := fun (α : Type u) (self : Field.{u} α) => @CommRing.mk.{u} α (@DivisionRing.toRing.{u} α (@Field.toDivisionRing.{u} α self)) (@Field.mul_comm.{u} α self) diff --git a/tests/lean/run/derivingBEq.lean b/tests/lean/run/derivingBEq.lean index 52a1a79d70..56285469fc 100644 --- a/tests/lean/run/derivingBEq.lean +++ b/tests/lean/run/derivingBEq.lean @@ -54,7 +54,7 @@ inductive L' (α : Type u) : Type u end InNamespace /-- -info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) +info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) -/ #guard_msgs in #print sig InNamespace.instBEqL' /-- @@ -163,7 +163,7 @@ private structure PrivStruct where deriving BEq -- Instance and spec should be private -/-- info: private def instBEqPrivStruct : BEq PrivStruct -/ +/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/ #guard_msgs in #print sig instBEqPrivStruct diff --git a/tests/lean/run/derivingBEqLinear.lean b/tests/lean/run/derivingBEqLinear.lean index 11257bf6b3..ca0a8c3dda 100644 --- a/tests/lean/run/derivingBEqLinear.lean +++ b/tests/lean/run/derivingBEqLinear.lean @@ -58,7 +58,7 @@ inductive L' (α : Type u) : Type u end InNamespace /-- -info: @[expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) +info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α) -/ #guard_msgs in #print sig InNamespace.instBEqL' /-- @@ -150,7 +150,7 @@ private structure PrivStruct where deriving BEq -- Instance and spec should be private -/-- info: private def instBEqPrivStruct : BEq PrivStruct -/ +/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/ #guard_msgs in #print sig instBEqPrivStruct diff --git a/tests/lean/run/derivingDelta.lean b/tests/lean/run/derivingDelta.lean index bfab606984..6da7a5354f 100644 --- a/tests/lean/run/derivingDelta.lean +++ b/tests/lean/run/derivingDelta.lean @@ -62,7 +62,7 @@ def MyNat := Nat deriving OfNat /-- -info: def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 := +info: @[instance_reducible] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 := fun _x_1 => instOfNatNat _x_1 -/ #guard_msgs in #print instOfNatMyNat @@ -72,7 +72,7 @@ Explicit parameterization -/ deriving instance (n : Nat) → OfNat _ n for MyNat /-- -info: def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n := +info: @[instance_reducible] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n := fun n => instOfNatNat n -/ #guard_msgs in #print instOfNatMyNat_1 @@ -85,7 +85,7 @@ variable (m : Nat) deriving instance OfNat _ m for MyNat end /-- -info: def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m := +info: @[instance_reducible] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m := fun m => instOfNatNat m -/ #guard_msgs in #print instOfNatMyNat_2 @@ -132,7 +132,7 @@ def MyFin'' := Fin deriving C1 /-- -info: def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' := +info: @[instance_reducible] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' := instC1NatFin -/ #guard_msgs in set_option pp.explicit true in #print instC1NatMyFin'' @@ -164,12 +164,12 @@ instance (n : Nat) : OfNat' n Int := {} def MyInt := Int deriving OfNat', OfNat /-- -info: def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt := +info: @[instance_reducible] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt := fun _x_1 => instOfNat'Int _x_1 -/ #guard_msgs in #print instOfNat'MyInt /-- -info: def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 := +info: @[instance_reducible] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 := fun _x_1 => instOfNat -/ #guard_msgs in #print instOfNatMyInt @@ -201,7 +201,7 @@ def NewRing (R : Type _) [Semiring R] := R deriving Module R /-- -info: def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) := +info: @[instance_reducible] def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) := fun R [Semiring R] => instModule R -/ #guard_msgs in #print instModuleNewRing @@ -221,7 +221,7 @@ def NewRing' (R : Type _) := R deriving instance Module R for NewRing' R /-- -info: def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) := +info: @[instance_reducible] def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) := fun R [Semiring R] => instModule R -/ #guard_msgs in #print instModuleNewRing' @@ -236,7 +236,7 @@ instance : C2 Type Prop := {} def Prop' := Prop deriving C2 /-- -info: def instC2TypeProp' : C2 Type Prop' := +info: @[instance_reducible] def instC2TypeProp' : C2 Type Prop' := instC2TypeProp -/ #guard_msgs in #print instC2TypeProp' diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean index 32dbfdf477..75bbe2224e 100644 --- a/tests/lean/run/derivingInhabited.lean +++ b/tests/lean/run/derivingInhabited.lean @@ -54,7 +54,7 @@ structure A where deriving Inhabited /-- -info: private def instInhabitedA : Inhabited A := +info: @[instance_reducible] private def instInhabitedA : Inhabited A := { default := instInhabitedA.default } -/ #guard_msgs in diff --git a/tests/lean/run/derivingRepr.lean b/tests/lean/run/derivingRepr.lean index 93848eb577..b55daa0d99 100644 --- a/tests/lean/run/derivingRepr.lean +++ b/tests/lean/run/derivingRepr.lean @@ -146,7 +146,7 @@ public structure Public where deriving Repr /-- -info: @[expose] def instReprPublic : Repr Public := +info: @[instance_reducible, expose] def instReprPublic : Repr Public := { reprPrec := instReprPublic.repr } -/ #guard_msgs in diff --git a/tests/lean/run/diagnostics.lean b/tests/lean/run/diagnostics.lean index 4f88e00a3b..82cf0e98a0 100644 --- a/tests/lean/run/diagnostics.lean +++ b/tests/lean/run/diagnostics.lean @@ -6,46 +6,36 @@ def f (x : Nat) : Nat := theorem f_eq : f (x + 1) = q (f x) := rfl -set_option trace.Meta.debug true - /-- trace: [diag] Diagnostics - [reduction] unfolded declarations (max: 15, num: 6): + [reduction] unfolded declarations (max: 15, num: 4): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 [reduction] HAdd.hAdd ↦ 10 [reduction] Nat.add ↦ 10 - [reduction] f ↦ 5 - [reduction] OfNat.ofNat ↦ 5 - [reduction] unfolded instances (max: 5, num: 1): - [reduction] instOfNatNat ↦ 5 [reduction] unfolded reducible declarations (max: 15, num: 1): [reduction] Nat.casesOn ↦ 15 use `set_option diagnostics.threshold ` to control threshold for reporting counters -/ #guard_msgs in example : f (x + 5) = q (q (q (q (q (f x))))) := - set_option diagnostics.threshold 4 in + set_option diagnostics.threshold 5 in set_option diagnostics true in rfl /-- trace: [diag] Diagnostics - [reduction] unfolded declarations (max: 15, num: 6): + [reduction] unfolded declarations (max: 15, num: 4): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 [reduction] HAdd.hAdd ↦ 10 [reduction] Nat.add ↦ 10 - [reduction] f ↦ 5 - [reduction] OfNat.ofNat ↦ 5 - [reduction] unfolded instances (max: 5, num: 1): - [reduction] instOfNatNat ↦ 5 [reduction] unfolded reducible declarations (max: 15, num: 1): [reduction] Nat.casesOn ↦ 15 use `set_option diagnostics.threshold ` to control threshold for reporting counters -/ #guard_msgs in example : f (x + 5) = q (q (q (q (q (f x))))) := by - set_option diagnostics.threshold 4 in + set_option diagnostics.threshold 5 in set_option diagnostics true in rfl diff --git a/tests/lean/run/issue10678.lean b/tests/lean/run/issue10678.lean index 6d77e3bd64..db66ad3188 100644 --- a/tests/lean/run/issue10678.lean +++ b/tests/lean/run/issue10678.lean @@ -9,7 +9,7 @@ deriving Lean.ToExpr, Inhabited -- same namespace for instance and aux decls /-- -info: def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) := +info: @[instance_reducible] def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) := fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] => { toExpr := instToExprA.toExpr inst_1, toTypeExpr := (Lean.Expr.const `A.A [Lean.toLevel]).app (Lean.toTypeExpr α) } -/ @@ -17,7 +17,7 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] => /-- -info: def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) := +info: @[instance_reducible] def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) := fun {a} [Inhabited a] => { default := instInhabitedA.default } -/ #guard_msgs in #print A.instInhabitedA @@ -35,14 +35,14 @@ deriving Lean.ToExpr, Inhabited end /-- -info: def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) := +info: @[instance_reducible] def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) := fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] => { toExpr := instToExprB.toExpr_1 inst_1, toTypeExpr := (Lean.Expr.const `B [Lean.toLevel]).app (Lean.toTypeExpr α) } -/ #guard_msgs in #print instToExprB /-- -info: def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) := +info: @[instance_reducible] def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) := fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] => { toExpr := instToExprB.toExpr_2 inst_1, toTypeExpr := (Lean.Expr.const `C [Lean.toLevel]).app (Lean.toTypeExpr α) } -/ @@ -51,14 +51,14 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] => /-- -info: def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) := +info: @[instance_reducible] def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) := fun {a} => { default := instInhabitedB.default_1 } -/ #guard_msgs in #print instInhabitedB /-- -info: def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) := +info: @[instance_reducible] def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) := fun {a} => { default := instInhabitedC.default_1 } -/ #guard_msgs in diff --git a/tests/lean/run/reduceBEqSimproc.lean b/tests/lean/run/reduceBEqSimproc.lean index fb8f3e3e4d..70d3512b6a 100644 --- a/tests/lean/run/reduceBEqSimproc.lean +++ b/tests/lean/run/reduceBEqSimproc.lean @@ -54,7 +54,7 @@ end Linear namespace A inductive L where | nil : L | cons : Nat → L → L deriving BEq -- NB: Instance, op and theorem are private -/-- info: private def A.instBEqL : BEq L -/ +/-- info: @[instance_reducible] private def A.instBEqL : BEq L -/ #guard_msgs in #print sig instBEqL /-- info: private def A.instBEqL.beq : L → L → Bool -/ #guard_msgs in #print sig instBEqL.beq @@ -66,7 +66,7 @@ end A namespace B public inductive L where | nil : L | cons : Nat → L → L deriving BEq -- NB: Instance is public and exposed, op and theorem are private -/-- info: @[expose] def B.instBEqL : BEq L -/ +/-- info: @[instance_reducible, expose] def B.instBEqL : BEq L -/ #guard_msgs in #print sig instBEqL /-- info: def B.instBEqL.beq : L → L → Bool -/ #guard_msgs in #print sig instBEqL.beq @@ -79,7 +79,7 @@ end B namespace C public inductive L where | nil : L | cons : Nat → L → L deriving @[expose] BEq -- NB: Public exposed instances, implementation and public theorem -/-- info: @[expose] def C.instBEqL : BEq L -/ +/-- info: @[instance_reducible, expose] def C.instBEqL : BEq L -/ #guard_msgs in #print sig instBEqL /-- info: @[expose] def C.instBEqL.beq : L → L → Bool -/ #guard_msgs in #print sig instBEqL.beq diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean index 5a560cd8a3..b2796e49fd 100644 --- a/tests/lean/run/structInst.lean +++ b/tests/lean/run/structInst.lean @@ -274,7 +274,7 @@ instance : B where instance : C where /-- -info: def Issue6046.instC : C := +info: @[instance_reducible] def Issue6046.instC : C := { b := B.b } -/ #guard_msgs in #print Issue6046.instC @@ -342,7 +342,7 @@ class Bar extends Foo where instance instBar : Bar where /-- -info: def Ex6769_1.instBar : Bar := +info: @[instance_reducible] def Ex6769_1.instBar : Bar := { x := 0 } -/ #guard_msgs in #print instBar @@ -361,7 +361,7 @@ instance instBar : Bar where x := 0 /-- -info: def Ex6769_2.instBar : Bar := +info: @[instance_reducible] def Ex6769_2.instBar : Bar := { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 } -/ #guard_msgs in #print instBar @@ -380,7 +380,7 @@ instance instBar : Bar where x := 0 /-- -info: def Ex6769_3.instBar : Bar := +info: @[instance_reducible] def Ex6769_3.instBar : Bar := { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 } -/ #guard_msgs in #print instBar diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 75738d0557..6c80be11cf 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -423,7 +423,7 @@ meta structure Foo where deriving TypeName /-- -info: private meta def instTypeNameFoo : TypeName Foo := +info: @[instance_reducible] private meta def instTypeNameFoo : TypeName Foo := inst✝ -/ #guard_msgs in