From 3c40ea2733bc0a682df59609945a177a6b72fd85 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 25 Aug 2025 10:55:10 +0200 Subject: [PATCH] chore: revert automatically exposing derived instances (#10101) Heed surrounding `@[expose]` instead --- src/Init/Data/Int/Linear.lean | 4 +-- src/Lean/Elab/Deriving/BEq.lean | 8 ++--- src/Lean/Elab/Deriving/DecEq.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 4 +-- src/Lean/Elab/Deriving/Nonempty.lean | 4 +-- src/Lean/Elab/Deriving/Util.lean | 15 ++++---- .../decEqMutualInductives.lean.expected.out | 9 ++--- tests/lean/run/decEq.lean | 35 ++++++++----------- tests/lean/run/derivingBEq.lean | 4 +-- 9 files changed, 38 insertions(+), 47 deletions(-) diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 9fa4005031..38ece53696 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -39,7 +39,7 @@ inductive Expr where | neg (a : Expr) | mulL (k : Int) (a : Expr) | mulR (a : Expr) (k : Int) - deriving Inhabited, BEq + deriving Inhabited, @[expose] BEq @[expose] def Expr.denote (ctx : Context) : Expr → Int @@ -54,7 +54,7 @@ def Expr.denote (ctx : Context) : Expr → Int inductive Poly where | num (k : Int) | add (k : Int) (v : Var) (p : Poly) - deriving BEq + deriving @[expose] BEq @[expose] protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool := diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 1ff2528239..215d281b27 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -108,8 +108,8 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do if ctx.usePartial then `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term) else - let expAttr := ctx.mkExposeAttrFromCtors - `(@[$expAttr] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term) + let expAttr := ctx.mkNoExposeAttrFromCtors + `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term) def mkMutualBlock (ctx : Context) : TermElabM Syntax := do let mut auxDefs := #[] @@ -129,8 +129,8 @@ private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do let auxFunName := ctx.auxFunNames[0]! let vis := ctx.mkVisibilityFromTypes - let expAttr := ctx.mkExposeAttrFromCtors - `(@[$expAttr] $vis:visibility def $(mkIdent auxFunName):ident (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx) + let expAttr := ctx.mkNoExposeAttrFromCtors + `(@[$[$expAttr],*] $vis:visibility def $(mkIdent auxFunName):ident (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx) private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do let ctx ← mkContext "beq" name diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 79b4fbdd5a..3c8d21ec77 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -103,7 +103,7 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T else `(Parser.Termination.suffix|) let type ← `(Decidable ($target₁ = $target₂)) let vis := ctx.mkVisibilityFromTypes - `(@[expose] $vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term + `($vis:visibility def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term $termSuffix:suffix) def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index a85adf0534..245f59376e 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -85,8 +85,8 @@ where ctorArgs := ctorArgs.push (← ``(Inhabited.default)) let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs*⟩) let vis := ctx.mkVisibilityFromTypes - let expAttr := ctx.mkExposeAttrFromCtors - `(@[$expAttr] $vis:visibility instance $binders:bracketedBinder* : $type := $val) + let expAttr := ctx.mkNoExposeAttrFromCtors + `(@[$[$expAttr],*] $vis:visibility instance $binders:bracketedBinder* : $type := $val) mkInstanceCmd? : TermElabM (Option Syntax) := do let ctorVal ← getConstInfoCtor ctorName diff --git a/src/Lean/Elab/Deriving/Nonempty.lean b/src/Lean/Elab/Deriving/Nonempty.lean index 9d41140192..e53958e372 100644 --- a/src/Lean/Elab/Deriving/Nonempty.lean +++ b/src/Lean/Elab/Deriving/Nonempty.lean @@ -30,9 +30,9 @@ private def mkNonemptyInstance (declName : Name) : TermElabM Syntax.Command := d let ctorTacs ← indVal.ctors.toArray.mapM fun ctor => `(tactic| apply @$(mkCIdent ctor) <;> exact Classical.ofNonempty) let vis := ctx.mkVisibilityFromTypes - let expAttr := ctx.mkExposeAttrFromCtors + let expAttr := ctx.mkNoExposeAttrFromCtors `(command| variable $binders* in - @[$expAttr] $vis:visibility instance : Nonempty (@$(mkCIdent declName) $indArgs*) := + @[$[$expAttr],*] $vis:visibility instance : Nonempty (@$(mkCIdent declName) $indArgs*) := by constructor; first $[| $ctorTacs:tactic]*) def mkNonemptyInstanceHandler (declNames : Array Name) : CommandElabM Bool := do diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 3a2520afc5..d277322d35 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -81,12 +81,13 @@ def Context.mkVisibilityFromTypes (ctx : Context) : TSyntax ``visibility := open Parser.Term in /-- -Returns `no_expose` or `expose` depending on whether any types with private constructors are -referenced in the `deriving` clause. +Returns `no_expose` if any types with private constructors are referenced in the `deriving` clause. +`expose` is assumed to be specified explicitly by the user. -/ -def Context.mkExposeAttrFromCtors (ctx : Context) : TSyntax ``attrInstance := - Unhygienic.run <| - if ctx.typeInfos.any (·.ctors.any isPrivateName) then `(attrInstance| no_expose) else `(attrInstance| expose) +def Context.mkNoExposeAttrFromCtors (ctx : Context) : Array (TSyntax ``attrInstance) := + if ctx.typeInfos.any (·.ctors.any isPrivateName) then + #[Unhygienic.run <| `(attrInstance| no_expose)] + else #[] def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do let indVal ← getConstInfoInduct typeName @@ -144,8 +145,8 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) ( if useAnonCtor then val ← `(⟨$val⟩) let vis := ctx.mkVisibilityFromTypes - let expAttr := ctx.mkExposeAttrFromCtors - let instCmd ← `(@[$expAttr] $vis:visibility instance $binders:implicitBinder* : $type := $val) + let expAttr := ctx.mkNoExposeAttrFromCtors + let instCmd ← `(@[$[$expAttr],*] $vis:visibility instance $binders:implicitBinder* : $type := $val) instances := instances.push instCmd return instances diff --git a/tests/lean/decEqMutualInductives.lean.expected.out b/tests/lean/decEqMutualInductives.lean.expected.out index b422a22738..2ab1508b3f 100644 --- a/tests/lean/decEqMutualInductives.lean.expected.out +++ b/tests/lean/decEqMutualInductives.lean.expected.out @@ -1,6 +1,5 @@ [Elab.Deriving.decEq] [mutual - @[expose✝] public def decEqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with | @Tree.node a✝, @Tree.node b✝ => @@ -8,7 +7,6 @@ if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝ else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption) termination_by structural x✝ - @[expose✝] public def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @ListTree.nil, @ListTree.nil => isTrue✝¹ rfl✝¹ @@ -24,12 +22,11 @@ else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption) termination_by structural x✝² end, - @[expose✝] + @[] public instance : DecidableEq✝ (@ListTree✝) := decEqListTree✝] [Elab.Deriving.decEq] [mutual - @[expose✝] public def decEqFoo₁✝ (x✝ : @Foo₁✝) (x✝¹ : @Foo₁✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with | @Foo₁.foo₁₁, @Foo₁.foo₁₁ => isTrue✝ rfl✝ @@ -40,7 +37,6 @@ if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹ else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption) termination_by structural x✝ - @[expose✝] public def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ => @@ -48,7 +44,6 @@ if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝² else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption) termination_by structural x✝² - @[expose✝] public def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := match x✝⁴, x✝⁵ with | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² => @@ -57,6 +52,6 @@ else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption) termination_by structural x✝⁴ end, - @[expose✝] + @[] public instance : DecidableEq✝ (@Foo₁✝) := decEqFoo₁✝] diff --git a/tests/lean/run/decEq.lean b/tests/lean/run/decEq.lean index 1bf78e92e1..754e3e122b 100644 --- a/tests/lean/run/decEq.lean +++ b/tests/lean/run/decEq.lean @@ -17,7 +17,7 @@ def t1 [DecidableEq α] : DecidableEq (Vec α n) := def t2 [DecidableEq α] : DecidableEq (Test α) := inferInstance -/-! Public structures should yield public exposed instances independent of `public section`. -/ +/-! Public structures should yield public instances independent of `public section`. -/ /-- trace: [Elab.Deriving.decEq] ⏎ @@ -37,25 +37,20 @@ public inductive PubEnum where | a | b deriving DecidableEq -/-- -trace: [Elab.Deriving.decEq] ⏎ - [mutual - @[expose✝] - public def decEqPubInd✝ (x✝ : @PubInd✝) (x✝¹ : @PubInd✝) : Decidable✝ (x✝ = x✝¹) := - match x✝, x✝¹ with - | @PubInd.a a✝, @PubInd.a b✝ => - if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝ - else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption) - | PubInd.a .., PubInd.b .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) - | PubInd.b .., PubInd.a .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) - | @PubInd.b, @PubInd.b => isTrue✝¹ rfl✝¹ - end, - @[expose✝] - public instance : DecidableEq✝ (@PubInd✝) := - decEqPubInd✝] --/ -#guard_msgs in -set_option trace.Elab.Deriving.decEq true in public inductive PubInd where | a (n : Nat) | b deriving DecidableEq + +/-- info: Decidable.rec (fun h => false) (fun h => true) (decEqPubInd✝ PubInd.b PubInd.b) -/ +#guard_msgs in +#with_exporting +#reduce decide (PubInd.b = PubInd.b) + +public inductive PubExpInd where + | a (n : Nat) | b +deriving @[expose] DecidableEq + +/-- info: true -/ +#guard_msgs in +#with_exporting +#reduce decide (PubExpInd.b = PubExpInd.b) diff --git a/tests/lean/run/derivingBEq.lean b/tests/lean/run/derivingBEq.lean index b9640a3f9b..0aa70cb671 100644 --- a/tests/lean/run/derivingBEq.lean +++ b/tests/lean/run/derivingBEq.lean @@ -4,7 +4,7 @@ public section inductive Foo | mk1 | mk2 | mk3 - deriving BEq + deriving @[expose] BEq namespace Foo theorem ex1 : (mk1 == mk2) = false := @@ -22,7 +22,7 @@ end Foo inductive Vec (α : Type u) : Nat → Type u | nil : Vec α 0 | cons : α → {n : Nat} → Vec α n → Vec α (n+1) - deriving BEq + deriving @[expose] BEq namespace Vec theorem ex1 : (cons 10 Vec.nil == cons 20 Vec.nil) = false :=