From 316ff35afd1bbbc2b383879f9bed0ba33ca62836 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 6 Sep 2025 20:12:20 +0200 Subject: [PATCH] feat: deriving instances: use accessible names (#10271) This PR changes the naming of the internal functions in deriving instances like BEq to use accessible names. This is necessary to reasonably easily prove things about these functions. For example after `deriving BEq` for a type `T`, the implementation of `instBEqT` is in `instBEqT.beq`. --- src/Lean/CoreM.lean | 2 +- src/Lean/Elab/Deriving/BEq.lean | 4 +- src/Lean/Elab/Deriving/DecEq.lean | 2 +- src/Lean/Elab/Deriving/FromToJson.lean | 4 +- src/Lean/Elab/Deriving/Hashable.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 4 +- src/Lean/Elab/Deriving/Ord.lean | 2 +- src/Lean/Elab/Deriving/Repr.lean | 2 +- src/Lean/Elab/Deriving/ToExpr.lean | 2 +- src/Lean/Elab/Deriving/Util.lean | 25 +++++--- .../decEqMutualInductives.lean.expected.out | 60 +++++++++---------- tests/lean/prvNameWithMacroScopes.lean | 2 - .../prvNameWithMacroScopes.lean.expected.out | 2 - tests/lean/run/2161.lean | 4 +- tests/lean/run/decEq.lean | 4 +- tests/lean/run/derivingBEq.lean | 4 +- tests/lean/run/derivingInhabited.lean | 4 +- tests/lean/run/derivingRepr.lean | 6 +- tests/lean/run/prvNameWithMacroScopes.lean | 13 ++++ 19 files changed, 85 insertions(+), 63 deletions(-) delete mode 100644 tests/lean/prvNameWithMacroScopes.lean delete mode 100644 tests/lean/prvNameWithMacroScopes.lean.expected.out create mode 100644 tests/lean/run/prvNameWithMacroScopes.lean diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index a1de10d2b6..f5d603fcde 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -353,7 +353,7 @@ def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Exp if us == us' then return r unless c.hasValue do - throwError "Not a definition or theorem: {c.name}" + throwError "Not a definition or theorem: {.ofConstName c.name}" let r := c.instantiateValueLevelParams! us modifyInstLevelValueCache fun s => s.insert c.name (us, r) return r diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index e172b9ac18..f0badc021c 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -119,7 +119,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "beq" declName + let ctx ← mkContext ``BEq "beq" declName let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName]) trace[Elab.Deriving.beq] "\n{cmds}" return cmds @@ -129,7 +129,7 @@ private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do `(def $(mkIdent auxFunName):ident (x y : $(mkCIdent name)) : Bool := x.ctorIdx == y.ctorIdx) private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do - let ctx ← mkContext "beq" name + let ctx ← mkContext ``BEq "beq" name let cmds := #[← mkBEqEnumFun ctx name] ++ (← mkInstanceCmds ctx `BEq #[name]) trace[Elab.Deriving.beq] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 5b4a443d78..dfb2f5fc0f 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -194,7 +194,7 @@ def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do `(command| mutual $[$res:command]* end) def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do - let ctx ← mkContext "decEq" indVal.name + let ctx ← mkContext ``DecidableEq "decEq" indVal.name let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false)) trace[Elab.Deriving.decEq] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 0c8e51e71e..9160e25e08 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -215,13 +215,13 @@ def mkFromJsonMutualBlock (ctx : Context) : TermElabM Command := do end) private def mkToJsonInstance (declName : Name) : TermElabM (Array Command) := do - let ctx ← mkContext "toJson" declName + let ctx ← mkContext ``ToJson "toJson" declName let cmds := #[← mkToJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``ToJson #[declName]) trace[Elab.Deriving.toJson] "\n{cmds}" return cmds private def mkFromJsonInstance (declName : Name) : TermElabM (Array Command) := do - let ctx ← mkContext "fromJson" declName + let ctx ← mkContext ``FromJson "fromJson" declName let cmds := #[← mkFromJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``FromJson #[declName]) trace[Elab.Deriving.fromJson] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index 9ddc3eca29..77932d73a9 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -81,7 +81,7 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do `(mutual $auxDefs:command* end) private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "hash" declName + let ctx ← mkContext ``Hashable "hash" declName let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName]) trace[Elab.Deriving.hashable] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index b34c46ecaf..a8244b9a68 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -61,7 +61,7 @@ where /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters at position `i` and `i ∈ assumingParamIdxs`. -/ mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do - let ctx ← Deriving.mkContext "inhabited" inductiveTypeName + let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName let indVal ← getConstInfoInduct inductiveTypeName let ctorVal ← getConstInfoCtor ctorName let mut indArgs := #[] @@ -81,7 +81,7 @@ where for _ in *...ctorVal.numFields do ctorArgs := ctorArgs.push (← ``(Inhabited.default)) let val ← `(@$(mkIdent ctorName):ident $ctorArgs*) - let ctx ← mkContext "default" inductiveTypeName + let ctx ← mkContext ``Inhabited "default" inductiveTypeName let auxFunName := ctx.auxFunNames[0]! `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val instance $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩) diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean index c3d73545d9..a72eeeba0c 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -90,7 +90,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkOrdInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "ord" declName + let ctx ← mkContext ``Ord "ord" declName let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord #[declName]) trace[Elab.Deriving.ord] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 977382bf6d..92065c3c4b 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -114,7 +114,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do end) private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "repr" declName + let ctx ← mkContext ``Repr "repr" declName let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName]) trace[Elab.Deriving.repr] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean index c9e9e9a173..0a7aff9f7b 100644 --- a/src/Lean/Elab/Deriving/ToExpr.lean +++ b/src/Lean/Elab/Deriving/ToExpr.lean @@ -216,7 +216,7 @@ def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) : Returns all the commands necessary to construct the `ToExpr` instances. -/ def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "toExpr" declNames[0]! + let ctx ← mkContext ``ToExpr "toExpr" declNames[0]! let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx declNames) trace[Elab.Deriving.toExpr] "\n{cmds}" return cmds diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 07bf869628..55832e2593 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -9,6 +9,7 @@ prelude public import Lean.Elab.Term public import Lean.Elab.Command meta import Lean.Parser.Command +import Lean.Elab.DeclNameGen public section @@ -84,23 +85,33 @@ def withoutExposeFromCtors (typeName : Name) (cont : CommandElabM α) : CommandE else cont structure Context where + instName : Name typeInfos : Array InductiveVal auxFunNames : Array Name usePartial : Bool -def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do + +def mkContext (className : Name) (fnPrefix : String) (typeName : Name) : TermElabM Context := do let indVal ← getConstInfoInduct typeName let mut typeInfos := #[] for typeName in indVal.all do typeInfos := typeInfos.push (← getConstInfoInduct typeName) + let instName ← do -- anticipate the instance name + let argNames ← mkInductArgNames indVal + let binders ← mkImplicitBinders argNames + let indType ← mkInductiveApp indVal argNames + let type ← `($(mkCIdent className) $indType) + NameGen.mkBaseNameWithSuffix' "inst" (binders.map (·.raw)) type let mut auxFunNames := #[] - for typeName in indVal.all do - match typeName.eraseMacroScopes with - | .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t) - | _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn) - trace[Elab.Deriving.beq] "{auxFunNames}" + if indVal.all.length = 1 then + auxFunNames := auxFunNames.push (instName ++ .mkSimple fnPrefix) + else + for i in [:indVal.all.length] do + auxFunNames := auxFunNames.push (instName ++ .mkSimple s!"{fnPrefix}_{i+1}") + trace[Elab.Deriving] "instName: {instName} auxFunNames: {auxFunNames}" let usePartial := indVal.isNested || typeInfos.size > 1 return { + instName := instName typeInfos := typeInfos auxFunNames := auxFunNames usePartial := usePartial @@ -143,7 +154,7 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) ( let mut val := mkIdent auxFunName if useAnonCtor then val ← `(⟨$val⟩) - let instCmd ← `(instance $binders:implicitBinder* : $type := $val) + let instCmd ← `(instance $(mkIdent ctx.instName):ident $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 d8d0ec512e..0d92e3d9fe 100644 --- a/tests/lean/decEqMutualInductives.lean.expected.out +++ b/tests/lean/decEqMutualInductives.lean.expected.out @@ -1,108 +1,108 @@ [Elab.Deriving.decEq] [mutual - def decEqTree✝ (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) := + def instDecidableEqListTree.decEq_1 (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with | @A.Tree.node a✝, @A.Tree.node b✝ => - let inst✝ := decEqListTree✝ @a✝ @b✝; + let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝; 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✝ - def decEqListTree✝ (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) := + def instDecidableEqListTree.decEq_2 (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @A.ListTree.nil, @A.ListTree.nil => isTrue✝¹ rfl✝¹ | A.ListTree.nil .., A.ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) | A.ListTree.cons .., A.ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹) | @A.ListTree.cons a✝¹ a✝², @A.ListTree.cons b✝¹ b✝² => - let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹; + let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹; if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact - let inst✝² := decEqListTree✝ @a✝² @b✝²; + let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²; if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝² else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption) else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption) termination_by structural x✝² end, - instance : DecidableEq✝ (@A.ListTree✝) := - decEqListTree✝] + instance instDecidableEqListTree : DecidableEq✝ (@A.ListTree✝) := + instDecidableEqListTree.decEq_2] [Elab.Deriving.decEq] [mutual - def decEqFoo₁✝ (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := + def instDecidableEqFoo₁.decEq_1 (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := match x✝, x✝¹ with | @A.Foo₁.foo₁₁, @A.Foo₁.foo₁₁ => isTrue✝ rfl✝ | A.Foo₁.foo₁₁ .., A.Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝) | A.Foo₁.foo₁₂ .., A.Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝) | @A.Foo₁.foo₁₂ a✝, @A.Foo₁.foo₁₂ b✝ => - let inst✝ := decEqFoo₂✝ @a✝ @b✝; + let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝; 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✝ - def decEqFoo₂✝ (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) := + def instDecidableEqFoo₁.decEq_2 (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @A.Foo₂.foo₂ a✝¹, @A.Foo₂.foo₂ b✝¹ => - let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹; + let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹; 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✝² - def decEqFoo₃✝ (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := + def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := match x✝⁴, x✝⁵ with | @A.Foo₃.foo₃ a✝², @A.Foo₃.foo₃ b✝² => - let inst✝² := decEqFoo₁✝ @a✝² @b✝²; + let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²; 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✝⁴ end, - instance : DecidableEq✝ (@A.Foo₁✝) := - decEqFoo₁✝] + instance instDecidableEqFoo₁ : DecidableEq✝ (@A.Foo₁✝) := + instDecidableEqFoo₁.decEq_1] [Elab.Deriving.decEq] [mutual - def decEqTree✝ (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) := + def instDecidableEqListTree.decEq_1 (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) := B.Tree.match_on_same_ctor✝ x✝ x✝¹ rfl✝ @fun a✝ b✝ => - let inst✝ := decEqListTree✝ @a✝ @b✝; + let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝; 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✝ - def decEqListTree✝ (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) := + def instDecidableEqListTree.decEq_2 (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) := if h✝¹ : B.ListTree.ctorIdx✝ x✝² = B.ListTree.ctorIdx✝ x✝³ then B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun => isTrue✝¹ rfl✝) @fun a✝¹ a✝² b✝¹ b✝² => - let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹; + let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹; if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact - let inst✝² := decEqListTree✝ @a✝² @b✝²; + let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²; if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝² else isFalse✝¹ (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption) else isFalse✝² (by intro n✝²; injection n✝²; apply h✝² _; assumption) else isFalse✝³ (fun h'✝ => h✝¹ (congrArg✝ B.ListTree.ctorIdx✝ h'✝)) termination_by structural x✝² end, - instance : DecidableEq✝ (@B.ListTree✝) := - decEqListTree✝] + instance instDecidableEqListTree : DecidableEq✝ (@B.ListTree✝) := + instDecidableEqListTree.decEq_2] [Elab.Deriving.decEq] [mutual - def decEqFoo₁✝ (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := + def instDecidableEqFoo₁.decEq_1 (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) := if h✝ : B.Foo₁.ctorIdx✝ x✝ = B.Foo₁.ctorIdx✝ x✝¹ then B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun => isTrue✝ rfl✝) @fun a✝ b✝ => - let inst✝ := decEqFoo₂✝ @a✝ @b✝; + let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝; if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹ else isFalse✝ (by intro n✝; injection n✝; apply h✝¹ _; assumption) else isFalse✝¹ (fun h'✝ => h✝ (congrArg✝ B.Foo₁.ctorIdx✝ h'✝)) termination_by structural x✝ - def decEqFoo₂✝ (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) := + def instDecidableEqFoo₁.decEq_2 (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) := B.Foo₂.match_on_same_ctor✝ x✝² x✝³ rfl✝ @fun a✝¹ b✝¹ => - let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹; + let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹; 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✝² - def decEqFoo₃✝ (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := + def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := B.Foo₃.match_on_same_ctor✝ x✝⁴ x✝⁵ rfl✝ @fun a✝² b✝² => - let inst✝² := decEqFoo₁✝ @a✝² @b✝²; + let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²; 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✝⁴ end, - instance : DecidableEq✝ (@B.Foo₁✝) := - decEqFoo₁✝] + instance instDecidableEqFoo₁ : DecidableEq✝ (@B.Foo₁✝) := + instDecidableEqFoo₁.decEq_1] diff --git a/tests/lean/prvNameWithMacroScopes.lean b/tests/lean/prvNameWithMacroScopes.lean deleted file mode 100644 index cd97591112..0000000000 --- a/tests/lean/prvNameWithMacroScopes.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Lean -#print Lean.instBEqFVarId diff --git a/tests/lean/prvNameWithMacroScopes.lean.expected.out b/tests/lean/prvNameWithMacroScopes.lean.expected.out deleted file mode 100644 index b19042cbc9..0000000000 --- a/tests/lean/prvNameWithMacroScopes.lean.expected.out +++ /dev/null @@ -1,2 +0,0 @@ -def Lean.instBEqFVarId : BEq Lean.FVarId := -{ beq := Lean.beqFVarId✝ } diff --git a/tests/lean/run/2161.lean b/tests/lean/run/2161.lean index afa0b3f39d..4d2ebe6398 100644 --- a/tests/lean/run/2161.lean +++ b/tests/lean/run/2161.lean @@ -19,7 +19,7 @@ because its `Decidable` instance instDecidableEqFoo (((mul 4 1).mul 1).mul 1) 4 did not reduce to `isTrue` or `isFalse`. -After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance +After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance match h : (((mul 4 1).mul 1).mul 1).num.beq 4 with | true => isTrue ⋯ | false => isFalse ⋯ @@ -39,7 +39,7 @@ because its `Decidable` instance instDecidableEqFoo (((add 4 1).add 1).add 1) 4 did not reduce to `isTrue` or `isFalse`. -After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance +After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance match h : (((add 4 1).add 1).add 1).num.beq 4 with | true => isTrue ⋯ | false => isFalse ⋯ diff --git a/tests/lean/run/decEq.lean b/tests/lean/run/decEq.lean index f7a97bd928..05f91add92 100644 --- a/tests/lean/run/decEq.lean +++ b/tests/lean/run/decEq.lean @@ -32,7 +32,9 @@ public inductive PubInd where | a (n : Nat) | b deriving DecidableEq -/-- info: Decidable.rec (fun h => false) (fun h => true) (decEqPubInd✝ PubInd.b PubInd.b) -/ +/-- +info: Decidable.rec (fun h => false) (fun h => true) (instDecidableEqPubInd.decEq PubInd.b PubInd.b) +-/ #guard_msgs in #with_exporting #reduce decide (PubInd.b = PubInd.b) diff --git a/tests/lean/run/derivingBEq.lean b/tests/lean/run/derivingBEq.lean index bd9c8408c3..9db179cb06 100644 --- a/tests/lean/run/derivingBEq.lean +++ b/tests/lean/run/derivingBEq.lean @@ -75,7 +75,7 @@ structure PrivField where private a : Nat deriving BEq -/-- info: fun a => beqPrivField✝ a a -/ +/-- info: fun a => instBEqPrivField.beq a a -/ #guard_msgs in #with_exporting #reduce fun (a : PrivField) => a == a @@ -88,7 +88,7 @@ public structure PrivField2 where private a : Nat deriving BEq -/-- info: fun a => beqPrivField2✝ a a -/ +/-- info: fun a => instBEqPrivField2.beq a a -/ #guard_msgs in #with_exporting #reduce fun (a : PrivField2) => a == a diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean index 156eb68f80..32dbfdf477 100644 --- a/tests/lean/run/derivingInhabited.lean +++ b/tests/lean/run/derivingInhabited.lean @@ -55,7 +55,7 @@ deriving Inhabited /-- info: private def instInhabitedA : Inhabited A := -{ default := defaultA✝ } +{ default := instInhabitedA.default } -/ #guard_msgs in #print instInhabitedA @@ -66,7 +66,7 @@ public structure PrivField where private a : Nat deriving Inhabited -/-- info: defaultPrivField✝ -/ +/-- info: instInhabitedPrivField.default -/ #guard_msgs in #with_exporting #reduce (default : PrivField) diff --git a/tests/lean/run/derivingRepr.lean b/tests/lean/run/derivingRepr.lean index 726c602d4d..93848eb577 100644 --- a/tests/lean/run/derivingRepr.lean +++ b/tests/lean/run/derivingRepr.lean @@ -122,7 +122,7 @@ structure PrivField where private a : Nat deriving Repr -/-- info: fun a => reprPrivField✝ a 0 -/ +/-- info: fun a => instReprPrivField.repr a 0 -/ #guard_msgs in #with_exporting #reduce fun (a : PrivField) => repr a @@ -135,7 +135,7 @@ public structure PrivField2 where private a : Nat deriving Repr -/-- info: fun a => reprPrivField2✝ a 0 -/ +/-- info: fun a => instReprPrivField2.repr a 0 -/ #guard_msgs in #with_exporting #reduce fun (a : PrivField2) => repr a @@ -147,7 +147,7 @@ deriving Repr /-- info: @[expose] def instReprPublic : Repr Public := -{ reprPrec := reprPublic✝ } +{ reprPrec := instReprPublic.repr } -/ #guard_msgs in #with_exporting diff --git a/tests/lean/run/prvNameWithMacroScopes.lean b/tests/lean/run/prvNameWithMacroScopes.lean new file mode 100644 index 0000000000..99fbf895ef --- /dev/null +++ b/tests/lean/run/prvNameWithMacroScopes.lean @@ -0,0 +1,13 @@ +macro "test%" n:ident : command => + `(def foo := 42 + def $n := foo + ) + +test% bar + +/-- +info: def bar : Nat := +foo✝ +-/ +#guard_msgs in +#print bar