From 1c20b5341956fb77fcf2c2601e64075e51d5f858 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 13 Apr 2024 11:08:50 -0700 Subject: [PATCH] feat: shorten auto-generated instance names (#3089) Implements a new method to generate instance names for anonymous instances that uses a heuristic that tends to produce shorter names. A design goal is to make them relatively unique within projects and definitely unique across projects, while also using accessible names so that they can be referred to as needed, both in Lean code and in discussions. The new method also takes into account binders provided to the instance, and it adds project-based suffixes. Despite this, a median new name is 73% its original auto-generated length. (Compare: [old generated names](https://gist.github.com/kmill/b72bb43f5b01dafef41eb1d2e57a8237) and [new generated names](https://gist.github.com/kmill/393acc82e7a8d67fc7387829f4ed547e).) Some notes: * The naming is sensitive to what is explicitly provided as a binder vs what is provided via a `variable`. It does not make use of `variable`s since, when names are generated, it is not yet known which variables are used in the body of the instance. * If the instance name refers to declarations in the current "project" (given by the root module), then it does not add a suffix. Otherwise, it adds the project name as a suffix to protect against cross-project collisions. * `set_option trace.Elab.instance.mkInstanceName true` can be used to see what name the auto-generator would give, even if the instance already has an explicit name. There were a number of instances that were referred to explicitly in meta code, and these have been given explicit names. Removes the unused `Lean.Elab.mkFreshInstanceName` along with the Command state's `nextInstIdx`. Fixes #2343 --- RELEASES.md | 11 + src/Init/Control/Lawful/Instances.lean | 4 +- src/Init/Data/Int/Basic.lean | 6 +- src/Init/Data/Nat/Div.lean | 4 +- src/Init/Prelude.lean | 30 +-- src/Init/System/IO.lean | 2 +- src/Lean/Elab/Command.lean | 1 - src/Lean/Elab/DeclNameGen.lean | 254 ++++++++++++++++++ src/Lean/Elab/DeclUtil.lean | 8 - src/Lean/Elab/DefView.lean | 45 +--- src/Lean/Elab/PreDefinition/Basic.lean | 1 + src/Lean/Expr.lean | 40 +-- src/Lean/Meta/NatInstTesters.lean | 4 +- src/Lean/Meta/Offset.lean | 4 +- .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 4 +- tests/lean/621.lean | 2 +- tests/lean/621.lean.expected.out | 2 +- tests/lean/755.lean.expected.out | 6 +- tests/lean/951.lean | 9 +- tests/lean/951.lean.expected.out | 4 +- tests/lean/run/lcnf1.lean | 2 +- tests/lean/run/regressions3210.lean | 4 +- tests/lean/run/structWithAlgTCSynth.lean | 2 +- tests/lean/synthorder.lean.expected.out | 2 +- 24 files changed, 341 insertions(+), 110 deletions(-) create mode 100644 src/Lean/Elab/DeclNameGen.lean diff --git a/RELEASES.md b/RELEASES.md index 2e03f7e51e9d..cb62720247e4 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -57,6 +57,15 @@ v4.8.0 (development in progress) ``` is recognized without having to say `termination_by arr.size - i`. +* Shorter instances names. There is a new algorithm for generating names for anonymous instances. + Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%. + With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters. + The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm. + While the new algorithm produces names that are 1.2% less unique, + it avoids cross-project collisions by adding a module-based suffix + when it does not refer to declarations from the same "project" (modules that share the same root). + PR [#3089](https://github.com/leanprover/lean4/pull/3089). + * Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩` rather than `{a := x, b := y, c := z}`. This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`. @@ -121,6 +130,8 @@ fact.def : * The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release. +* The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names. + v4.7.0 --------- diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index 80a0710892c1..f662c4c55f3a 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -235,13 +235,13 @@ end StateT instance : LawfulMonad (EStateM ε σ) := .mk' (id_map := fun x => funext <| fun s => by - dsimp only [EStateM.instMonadEStateM, EStateM.map] + dsimp only [EStateM.instMonad, EStateM.map] match x s with | .ok _ _ => rfl | .error _ _ => rfl) (pure_bind := fun _ _ => rfl) (bind_assoc := fun x _ _ => funext <| fun s => by - dsimp only [EStateM.instMonadEStateM, EStateM.bind] + dsimp only [EStateM.instMonad, EStateM.bind] match x s with | .ok _ _ => rfl | .error _ _ => rfl) diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 390a646594bd..ba8d16de2966 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -100,7 +100,7 @@ protected def neg (n : @& Int) : Int := ``` -/ @[default_instance mid] -instance : Neg Int where +instance instNegInt : Neg Int where neg := Int.neg /-- Subtraction of two natural numbers. -/ @@ -173,13 +173,13 @@ inductive NonNeg : Int → Prop where /-- Definition of `a ≤ b`, encoded as `b - a ≥ 0`. -/ protected def le (a b : Int) : Prop := NonNeg (b - a) -instance : LE Int where +instance instLEInt : LE Int where le := Int.le /-- Definition of `a < b`, encoded as `a + 1 ≤ b`. -/ protected def lt (a b : Int) : Prop := (a + 1) ≤ b -instance : LT Int where +instance instLTInt : LT Int where lt := Int.lt set_option bootstrap.genMatcherCode false in diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index 9407c4284507..8bd98b8d5215 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -28,7 +28,7 @@ protected def div (x y : @& Nat) : Nat := 0 decreasing_by apply div_rec_lemma; assumption -instance : Div Nat := ⟨Nat.div⟩ +instance instDiv : Div Nat := ⟨Nat.div⟩ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by show Nat.div x y = _ @@ -90,7 +90,7 @@ protected def mod : @& Nat → @& Nat → Nat | 0, _ => 0 | x@(_ + 1), y => Nat.modCore x y -instance : Mod Nat := ⟨Nat.mod⟩ +instance instMod : Mod Nat := ⟨Nat.mod⟩ protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by cases x with diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 9dd83028f3f8..8d3354fc0338 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1098,7 +1098,7 @@ class OfNat (α : Type u) (_ : Nat) where ofNat : α @[default_instance 100] /- low prio -/ -instance (n : Nat) : OfNat Nat n where +instance instOfNatNat (n : Nat) : OfNat Nat n where ofNat := n /-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`.-/ @@ -1432,31 +1432,31 @@ class ShiftRight (α : Type u) where shiftRight : α → α → α @[default_instance] -instance [Add α] : HAdd α α α where +instance instHAdd [Add α] : HAdd α α α where hAdd a b := Add.add a b @[default_instance] -instance [Sub α] : HSub α α α where +instance instHSub [Sub α] : HSub α α α where hSub a b := Sub.sub a b @[default_instance] -instance [Mul α] : HMul α α α where +instance instHMul [Mul α] : HMul α α α where hMul a b := Mul.mul a b @[default_instance] -instance [Div α] : HDiv α α α where +instance instHDiv [Div α] : HDiv α α α where hDiv a b := Div.div a b @[default_instance] -instance [Mod α] : HMod α α α where +instance instHMod [Mod α] : HMod α α α where hMod a b := Mod.mod a b @[default_instance] -instance [Pow α β] : HPow α β α where +instance instHPow [Pow α β] : HPow α β α where hPow a b := Pow.pow a b @[default_instance] -instance [NatPow α] : Pow α Nat where +instance instPowNat [NatPow α] : Pow α Nat where pow a n := NatPow.pow a n @[default_instance] @@ -1523,7 +1523,7 @@ protected def Nat.add : (@& Nat) → (@& Nat) → Nat | a, Nat.zero => a | a, Nat.succ b => Nat.succ (Nat.add a b) -instance : Add Nat where +instance instAddNat : Add Nat where add := Nat.add /- We mark the following definitions as pattern to make sure they can be used in recursive equations, @@ -1543,7 +1543,7 @@ protected def Nat.mul : (@& Nat) → (@& Nat) → Nat | _, 0 => 0 | a, Nat.succ b => Nat.add (Nat.mul a b) a -instance : Mul Nat where +instance instMulNat : Mul Nat where mul := Nat.mul set_option bootstrap.genMatcherCode false in @@ -1559,7 +1559,7 @@ protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat | 0 => 1 | succ n => Nat.mul (Nat.pow m n) m -instance : NatPow Nat := ⟨Nat.pow⟩ +instance instNatPowNat : NatPow Nat := ⟨Nat.pow⟩ set_option bootstrap.genMatcherCode false in /-- @@ -1636,14 +1636,14 @@ protected inductive Nat.le (n : Nat) : Nat → Prop /-- If `n ≤ m`, then `n ≤ m + 1`. -/ | step {m} : Nat.le n m → Nat.le n (succ m) -instance : LE Nat where +instance instLENat : LE Nat where le := Nat.le /-- The strict less than relation on natural numbers is defined as `n < m := n + 1 ≤ m`. -/ protected def Nat.lt (n m : Nat) : Prop := Nat.le (succ n) m -instance : LT Nat where +instance instLTNat : LT Nat where lt := Nat.lt theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False @@ -1795,7 +1795,7 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat | a, 0 => a | a, succ b => pred (Nat.sub a b) -instance : Sub Nat where +instance instSubNat : Sub Nat where sub := Nat.sub /-- @@ -3361,7 +3361,7 @@ protected def seqRight (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) : | Result.error e s => Result.error e s @[always_inline] -instance : Monad (EStateM ε σ) where +instance instMonad : Monad (EStateM ε σ) where bind := EStateM.bind pure := EStateM.pure map := EStateM.map diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index bad54a3f4dbd..4a3d0c5bce8b 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -802,7 +802,7 @@ class Eval (α : Type u) where -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`) eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit -instance [ToString α] : Eval α where +instance instEval [ToString α] : Eval α where eval a _ := IO.println (toString (a ())) instance [Repr α] : Eval α where diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index cebd8e4c00a5..d0071714ac0c 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -30,7 +30,6 @@ structure State where scopes : List Scope := [{ header := "" }] nextMacroScope : Nat := firstFrontendMacroScope + 1 maxRecDepth : Nat - nextInstIdx : Nat := 1 -- for generating anonymous instance names ngen : NameGenerator := {} infoState : InfoState := {} traceState : TraceState := {} diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean new file mode 100644 index 000000000000..8d94e6435323 --- /dev/null +++ b/src/Lean/Elab/DeclNameGen.lean @@ -0,0 +1,254 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Lean.Elab.Command + +/-! +# Name generator for declarations + +This module provides functionality to generate a name for a declaration using its binders and its type. +This is used to generate names for anonymous instances. + +It uses heuristics to generate an informative but terse name given its namespace, supplied binders, and type. +It tries to make these relatively unique, +and it uses suffixes derived from the module to ensure cross-project uniqueness +when the instance doesn't refer to anything defined in the current project. + +The name generator can be thought of as a kind of pretty printer, rendering an expression in textual form. +The general structure of this generator is +1. `Lean.Elab.Command.NameGen.winnowExpr` takes an expression and re-uses `Expr` as a data structure + to record the "Syntax"-like structure. +2. `Lean.Elab.Command.NameGen.mkBaseNameCore` formats the result of that as a string. + It actually does a bit more computation than that, since it further removes duplicate expressions, + reporting only the first occurrence of each subexpression. +-/ + +namespace Lean.Elab.Command + +open Meta + +namespace NameGen + +/-- +If `e` is an application of a projection to a parent structure, returns the term being projected. +-/ +private def getParentProjArg (e : Expr) : MetaM (Option Expr) := do + let .const c@(.str _ field) _ := e.getAppFn | return none + let env ← getEnv + let some info := env.getProjectionFnInfo? c | return none + unless e.getAppNumArgs == info.numParams + 1 do return none + let some (.ctorInfo cVal) := env.find? info.ctorName | return none + if isSubobjectField? env cVal.induct (Name.mkSimple field) |>.isNone then return none + return e.appArg! + +/-- +Strips out universes and arguments we decide are unnecessary for naming. +The resulting expression can have loose fvars and be mangled in other ways. +Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned. +-/ +private partial def winnowExpr (e : Expr) : MetaM Expr := do + let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr := checkCache e fun _ => do + match e with + | .app .. => + if let some e' ← getParentProjArg e then + return (← visit e') + e.withApp fun f args => do + -- Visit only the explicit arguments to `f` and also its type (and type family) arguments. + -- The reason we visit type arguments is so that, for example, `Decidable (_ < _)` has + -- a chance to insert type information. Type families are for reporting things such as type constructors and monads. + let mut fty ← inferType f + let mut j := 0 + let mut e' ← visit f + for i in [0:args.size] do + unless fty.isForall do + fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args + j := i + let .forallE _ _ fty' bi := fty | failure + fty := fty' + let arg := args[i]! + if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then + unless (← isProof arg) do + e' := .app e' (← visit arg) + return e' + | .forallE n ty body bi => + withLocalDecl n bi ty fun arg => do + -- In a dependent forall the body implies `ty`, so we won't mention it. + let ty' ← if body.hasLooseBVars then pure (.bvar 0) else visit ty + return .forallE n ty' (← visit (body.instantiate1 arg)) bi + | .lam n ty body bi => + if let some e := Expr.etaExpandedStrict? e then + visit e + else + withLocalDecl n bi ty fun arg => do + -- Don't record the `.lam` since `ty` should be recorded elsewhere in the expression. + visit (body.instantiate1 arg) + | .letE _n _t v b _ => visit (b.instantiate1 v) + | .sort .. => + if e.isProp then return .sort levelZero + else if e.isType then return .sort levelOne + else return .sort (.param `u) + | .const name .. => return .const name [] + | .mdata _ e' => visit e' + | _ => return .bvar 0 + visit e |>.run + +/-- +State for name generation. +-/ +private structure MkNameState where + /-- Keeps track of expressions already visited so that we do not include them again. -/ + seen : ExprSet := {} + /-- Keeps track of constants that appear in the generated name. -/ + consts : NameSet := {} + +/-- +Monad for name generation. +-/ +private abbrev MkNameM := StateRefT MkNameState MetaM + +/-- +Core algorithm for generating a name. The provided expression should be a winnowed expression. + +- `omitTopForall` if true causes "Forall" to not be included if the binding type results in an empty string. +-/ +private def mkBaseNameCore (e : Expr) (omitTopForall : Bool := false) : MkNameM String := + visit e omitTopForall +where + visit (e : Expr) (omitTopForall : Bool := false) : MkNameM String := do + if (← get).seen.contains e then + return "" + else + let s ← visit' e omitTopForall + modify fun st => {st with seen := st.seen.insert e} + return s + visit' (e : Expr) (omitTopForall : Bool) : MkNameM String := do + match e with + | .const name .. => + modify (fun st => {st with consts := st.consts.insert name}) + return match name.eraseMacroScopes with + | .str _ str => str.capitalize + | _ => "" + | .app f x => (· ++ ·) <$> visit f <*> visit x + | .forallE _ ty body _ => + let sty ← visit ty + if omitTopForall && sty == "" then + visit body true + else + ("Forall" ++ sty ++ ·) <$> visit body + | .sort .zero => return "Prop" + | .sort (.succ _) => return "Type" + | .sort _ => return "Sort" + | _ => return "" + +/-- +Generate a name, while naming the top-level foralls using "Of". +The provided expression should be a winnowed expression. +-/ +private partial def mkBaseNameAux (e : Expr) : MkNameM String := do + let (foralls, sb) ← visit e + return sb ++ String.join foralls +where + visit (e : Expr) : MkNameM (List String × String) := do + match e with + | .forallE _ ty body _ => + let (foralls, sb) ← visit body + let st ← mkBaseNameCore ty (omitTopForall := true) + if st == "" then + return (foralls, sb) + else + return (("Of" ++ st) :: foralls, sb) + | _ => return ([], ← mkBaseNameCore e) + +/-- +Adds all prefixes of `ns` as seen constants. +-/ +private def visitNamespace (ns : Name) : MkNameM Unit := do + match ns with + | .anonymous => pure () + | .num ns' _ => visitNamespace ns' + | .str ns' _ => + let env ← getEnv + if env.contains ns then + modify fun st => {st with seen := st.seen.insert (.const ns []), consts := st.consts.insert ns} + visitNamespace ns' + +/-- +Given an expression, generates a "base name" for a declaration. +The top-level foralls in `e` are treated as being binders, so use the `...Of...` naming convention. +The current namespace is used to seed the seen expressions with each prefix of the namespace that's a global constant. + +Collects all constants that contribute to the name in the `MkInstM` state. +This can be used to decide whether to further transform the generated name; +in particular, this enables checking whether the generated name mentions declarations +from the current module or project. +-/ +def mkBaseName (e : Expr) : MkNameM String := do + let e ← instantiateMVars e + visitNamespace (← getCurrNamespace) + mkBaseNameAux (← winnowExpr e) + +/-- +Converts a module name into a suffix. Includes a leading `_`, +so for example `Lean.Elab.DefView` becomes `_lean_elab_defView`. +-/ +private def moduleToSuffix : Name → String + | .anonymous => "" + | .num n _ => moduleToSuffix n + | .str n s => moduleToSuffix n ++ "_" ++ s.decapitalize + +/-- +Uses heuristics to generate an informative but terse base name for a term of the given type, using `mkBaseName`. +Makes use of the current namespace. +It tries to make these names relatively unique ecosystem-wide, +and it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module. +-/ +def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM String := do + let (name, st) ← mkBaseName type |>.run {} + let name := pre ++ name + let project := (← getMainModule).getRoot + -- Collect the modules for each constant that appeared. + let modules ← st.consts.foldM (init := Array.mkEmpty st.consts.size) fun mods name => return mods.push (← findModuleOf? name) + -- We can avoid adding the suffix if the instance refers to module-local names. + let isModuleLocal := modules.any Option.isNone + -- We can also avoid adding the full module suffix if the instance refers to "project"-local names. + let isProjectLocal := isModuleLocal || modules.any fun mod? => mod?.map (·.getRoot) == project + if !isProjectLocal then + return s!"{name}{moduleToSuffix project}" + else + return name + +/-- +Elaborates the binders and type and then uses `mkBaseNameWithSuffix` to generate a name. +Furthermore, uses `mkUnusedBaseName` on the result. +-/ +def mkBaseNameWithSuffix' (pre : String) (binders : Array Syntax) (type : Syntax) : TermElabM Name := do + let name ← + try + Term.withAutoBoundImplicit <| Term.elabBinders binders fun binds => Term.withoutErrToSorry do + let ty ← mkForallFVars binds (← Term.elabType type) + mkBaseNameWithSuffix pre ty + catch _ => + pure pre + liftMacroM <| mkUnusedBaseName <| Name.mkSimple name + +end NameGen + +/-- +Generates an instance name for a declaration that has the given binders and type. +It tries to make these names relatively unique ecosystem-wide. + +Note that this elaborates the binders and the type. +This means that when elaborating an instance declaration, we elaborate these twice. +-/ +def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do + let savedState ← get + try + -- Unfortunately we can't include any of the binders from `runTermElabM` since, without + -- elaborating the body of the instance, we have no idea which of these binders are + -- actually used. + runTermElabM fun _ => NameGen.mkBaseNameWithSuffix' "inst" binders type + finally + set savedState diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index 9b5025ad41e3..e62d3513bcc2 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -54,14 +54,6 @@ def expandDeclSig (stx : Syntax) : Syntax × Syntax := let typeSpec := stx[1] (binders, typeSpec[1]) -def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name := - (env.mainModule ++ `_instance).appendIndexAfter nextIdx - -def isFreshInstanceName (name : Name) : Bool := - match name with - | .str _ s => "_instance".isPrefixOf s - | _ => false - /-- Sort the given list of `usedParams` using the following order: - If it is an explicit level `allUserParams`, then use user given order. diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 1ac40b2bfd3f..091e3a3f3c74 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import Lean.Meta.ForEachExpr import Lean.Elab.Command +import Lean.Elab.DeclNameGen import Lean.Elab.DeclUtil namespace Lean.Elab @@ -66,41 +66,6 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView := { ref := stx, kind := DefKind.theorem, modifiers, declId := stx[1], binders, type? := some type, value := stx[3] } -def mkFreshInstanceName : CommandElabM Name := do - let s ← get - let idx := s.nextInstIdx - modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 } - return Lean.Elab.mkFreshInstanceName s.env idx - -/-- - Generate a name for an instance with the given type. - Note that we elaborate the type twice. Once for producing the name, and another when elaborating the declaration. -/ -def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do - let savedState ← get - try - let result ← runTermElabM fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => Term.withoutErrToSorry do - let type ← instantiateMVars (← Term.elabType type) - let ref ← IO.mkRef "" - Meta.forEachExpr type fun e => do - if e.isForall then ref.modify (· ++ "ForAll") - else if e.isProp then ref.modify (· ++ "Prop") - else if e.isType then ref.modify (· ++ "Type") - else if e.isSort then ref.modify (· ++ "Sort") - else if e.isConst then - match e.constName!.eraseMacroScopes with - | .str _ str => - if str.front.isLower then - ref.modify (· ++ str.capitalize) - else - ref.modify (· ++ str) - | _ => pure () - ref.get - set savedState - liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ result) - catch _ => - set savedState - mkFreshInstanceName - def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal let attrKind ← liftMacroM <| toAttributeKind stx[0] @@ -109,9 +74,14 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De let (binders, type) := expandDeclSig stx[4] let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx } let declId ← match stx[3].getOptional? with - | some declId => pure declId + | some declId => + if ← isTracingEnabledFor `Elab.instance.mkInstanceName then + let id ← mkInstanceName binders.getArgs type + trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id} for {declId}" + pure declId | none => let id ← mkInstanceName binders.getArgs type + trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}" pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] return { ref := stx, kind := DefKind.def, modifiers := modifiers, @@ -166,6 +136,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := throwError "unexpected kind of definition" builtin_initialize registerTraceClass `Elab.definition +builtin_initialize registerTraceClass `Elab.instance.mkInstanceName end Command end Lean.Elab diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 7e86071fa255..0963d017d455 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -7,6 +7,7 @@ prelude import Lean.Compiler.NoncomputableAttr import Lean.Util.CollectLevelParams import Lean.Meta.AbstractNestedProofs +import Lean.Meta.ForEachExpr import Lean.Elab.RecAppSyntax import Lean.Elab.DefView import Lean.Elab.PreDefinition.WF.TerminationHint diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 96e610de3a1a..c2dd647c6d2a 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -2025,43 +2025,43 @@ def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q /-! Constants for Nat typeclasses. -/ namespace Nat -def natType : Expr := mkConst ``Nat +protected def mkType : Expr := mkConst ``Nat -def instAdd : Expr := mkConst ``instAddNat -def instHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) natType instAdd +def mkInstAdd : Expr := mkConst ``instAddNat +def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) Nat.mkType mkInstAdd -def instSub : Expr := mkConst ``instSubNat -def instHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) natType instSub +def mkInstSub : Expr := mkConst ``instSubNat +def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) Nat.mkType mkInstSub -def instMul : Expr := mkConst ``instMulNat -def instHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) natType instMul +def mkInstMul : Expr := mkConst ``instMulNat +def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) Nat.mkType mkInstMul -def instDiv : Expr := mkConst ``Nat.instDivNat -def instHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) natType instDiv +def mkInstDiv : Expr := mkConst ``Nat.instDiv +def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) Nat.mkType mkInstDiv -def instMod : Expr := mkConst ``Nat.instModNat -def instHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) natType instMod +def mkInstMod : Expr := mkConst ``Nat.instMod +def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) Nat.mkType mkInstMod -def instNatPow : Expr := mkConst ``instNatPowNat -def instPow : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) natType instNatPow -def instHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) natType natType instPow +def mkInstNatPow : Expr := mkConst ``instNatPowNat +def mkInstPow : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) Nat.mkType mkInstNatPow +def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) Nat.mkType Nat.mkType mkInstPow -def instLT : Expr := mkConst ``instLTNat -def instLE : Expr := mkConst ``instLENat +def mkInstLT : Expr := mkConst ``instLTNat +def mkInstLE : Expr := mkConst ``instLENat end Nat private def natAddFn : Expr := let nat := mkConst ``Nat - mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.instHAdd + mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.mkInstHAdd private def natSubFn : Expr := let nat := mkConst ``Nat - mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.instHSub + mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.mkInstHSub private def natMulFn : Expr := let nat := mkConst ``Nat - mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.instHMul + mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.mkInstHMul /-- Given `a : Nat`, returns `Nat.succ a` -/ def mkNatSucc (a : Expr) : Expr := @@ -2080,7 +2080,7 @@ def mkNatMul (a b : Expr) : Expr := mkApp2 natMulFn a b private def natLEPred : Expr := - mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.instLE + mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.mkInstLE /-- Given `a b : Nat`, return `a ≤ b` -/ def mkNatLE (a b : Expr) : Expr := diff --git a/src/Lean/Meta/NatInstTesters.lean b/src/Lean/Meta/NatInstTesters.lean index ee4b81d3c459..028894bb3fb2 100644 --- a/src/Lean/Meta/NatInstTesters.lean +++ b/src/Lean/Meta/NatInstTesters.lean @@ -24,10 +24,10 @@ def isInstMulNat (e : Expr) : MetaM Bool := do let_expr instMulNat ← e | return false return true def isInstDivNat (e : Expr) : MetaM Bool := do - let_expr Nat.instDivNat ← e | return false + let_expr Nat.instDiv ← e | return false return true def isInstModNat (e : Expr) : MetaM Bool := do - let_expr Nat.instModNat ← e | return false + let_expr Nat.instMod ← e | return false return true def isInstNatPowNat (e : Expr) : MetaM Bool := do let_expr instNatPowNat ← e | return false diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index 9b125a1a1488..a4940982227f 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -87,8 +87,8 @@ partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do let (s, k) ← getOffset a return (s, k+1) | Nat.add a b => add a b - | Add.add _ i a b => guard (← matchesInstance i Nat.instAdd); add a b - | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.instHAdd); add a b + | Add.add _ i a b => guard (← matchesInstance i Nat.mkInstAdd); add a b + | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.mkInstHAdd); add a b | _ => failure end diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 27cef9d94ef6..f9f2c077768d 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean @@ -76,14 +76,14 @@ private inductive NatOffset where private partial def NatOffset.asOffset (e : Expr) : Meta.SimpM (Option (Expr × Nat)) := do if e.isAppOfArity ``HAdd.hAdd 6 then let inst := e.appFn!.appFn!.appArg! - unless ← matchesInstance inst Nat.instHAdd do return none + unless ← matchesInstance inst Nat.mkInstHAdd do return none let b := e.appFn!.appArg! let o := e.appArg! let some n ← Nat.fromExpr? o | return none pure (some (b, n)) else if e.isAppOfArity ``Add.add 4 then let inst := e.appFn!.appFn!.appArg! - unless ← matchesInstance inst Nat.instAdd do return none + unless ← matchesInstance inst Nat.mkInstAdd do return none let b := e.appFn!.appArg! let some n ← Nat.fromExpr? e.appArg! | return none pure (some (b, n)) diff --git a/tests/lean/621.lean b/tests/lean/621.lean index 40b9a4f411b3..1152cdf048a9 100644 --- a/tests/lean/621.lean +++ b/tests/lean/621.lean @@ -1,4 +1,4 @@ -instance (ϕ : α → Prop) : CoeSort (Subtype ϕ) α where +instance inst621 (ϕ : α → Prop) : CoeSort (Subtype ϕ) α where coe := fun x => x.val example (ϕ : α → Prop) (xs : Subtype ϕ) (x : xs) : True := trivial diff --git a/tests/lean/621.lean.expected.out b/tests/lean/621.lean.expected.out index 9711895ddaff..837ce9d9f1f9 100644 --- a/tests/lean/621.lean.expected.out +++ b/tests/lean/621.lean.expected.out @@ -3,4 +3,4 @@ to a type, after applying `CoeSort.coe`, result is still not a type xs.val this is often due to incorrect `CoeSort` instances, the synthesized instance was - instCoeSortSubtype ϕ + inst621 ϕ diff --git a/tests/lean/755.lean.expected.out b/tests/lean/755.lean.expected.out index 1124e5f70ae8..e36765b8705c 100644 --- a/tests/lean/755.lean.expected.out +++ b/tests/lean/755.lean.expected.out @@ -3,13 +3,13 @@ has type 0 = @OfNat.ofNat Nat 0 (instOfNatNat 0) : Prop but is expected to have type - 0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditive : Prop + 0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditiveOfOfNatNat : Prop 755.lean:24:2-24:5: error: type mismatch rfl has type 2 * 3 = @HMul.hMul Nat Nat Nat instHMul 2 3 : Prop but is expected to have type - 2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFoo 2 3 : Prop + 2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFooOfHAdd 2 3 : Prop 755.lean:27:2-27:5: error: type mismatch rfl has type @@ -21,4 +21,4 @@ but is expected to have type has type 2 - 3 = @HSub.hSub Nat Nat Nat instHSub 2 3 : Prop but is expected to have type - 2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFoo 2 3 : Prop + 2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFooOfHAdd 2 3 : Prop diff --git a/tests/lean/951.lean b/tests/lean/951.lean index b107b0c87db5..37b3cc5a0deb 100644 --- a/tests/lean/951.lean +++ b/tests/lean/951.lean @@ -1,3 +1,7 @@ +/-! +# Names of inferred instances clash (issue 951) +-/ + inductive ThingA where | mkA deriving Ord @@ -5,8 +9,7 @@ instance : LE ThingA where le a b := (compare a b).isLE instance (t₁ t₂ : ThingA) : Decidable (t₁ <= t₂) := inferInstance --- TODO: we may want to suppress the name of nested instances -#check instDecidableLeThingAInstLEThingA +#check instDecidableLeThingA inductive ThingB where | mkB @@ -14,4 +17,4 @@ deriving Ord instance : LE ThingB where le a b := (compare a b).isLE instance (t₁ t₂ : ThingB) : Decidable (t₁ <= t₂) := inferInstance -#check instDecidableLeThingBInstLEThingB +#check instDecidableLeThingB diff --git a/tests/lean/951.lean.expected.out b/tests/lean/951.lean.expected.out index 44c6d7ad2431..79fe685950c7 100644 --- a/tests/lean/951.lean.expected.out +++ b/tests/lean/951.lean.expected.out @@ -1,2 +1,2 @@ -instDecidableLeThingAInstLEThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂) -instDecidableLeThingBInstLEThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂) +instDecidableLeThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂) +instDecidableLeThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂) diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean index e487ca8c4f07..219f13acccb9 100644 --- a/tests/lean/run/lcnf1.lean +++ b/tests/lean/run/lcnf1.lean @@ -104,4 +104,4 @@ def gebner2 (x : UInt64) := x &&& ((1 : UInt64) <<< 5 : UInt64) #eval Compiler.compile #[``Lean.Core.instMonadCoreM] #eval Compiler.compile #[``instMonadEIO] -- set_option pp.explicit true in -#eval Compiler.compile #[``EStateM.instMonadEStateM] +#eval Compiler.compile #[``EStateM.instMonad] diff --git a/tests/lean/run/regressions3210.lean b/tests/lean/run/regressions3210.lean index 4ed0930f3bff..591c88d4f4b9 100644 --- a/tests/lean/run/regressions3210.lean +++ b/tests/lean/run/regressions3210.lean @@ -15,7 +15,7 @@ instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where example : Not (@Eq.{1} Nat - (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat) + (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat (nat_lit 1))))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) := by @@ -23,7 +23,7 @@ example : Not example : Not (@Eq.{1} Nat - (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat) + (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod) (@OfNat.ofNat.{0} Nat 1 (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat 1)))) (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) := by diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean index 128e851f563c..df43eab4b6dd 100644 --- a/tests/lean/run/structWithAlgTCSynth.lean +++ b/tests/lean/run/structWithAlgTCSynth.lean @@ -1311,7 +1311,7 @@ instance : Semiring (Quot_r R M) := RingQuot.instSemiring _ instance {S : Type w} [CommRing S] : CommRing (Quot_r S M) := - RingQuot.instCommRingRingQuotToSemiringToCommSemiring _ + RingQuot.instCommRing _ instance instAlgebra {R A M} [CommSemiring R] [CommRing A] [Algebra R A] : diff --git a/tests/lean/synthorder.lean.expected.out b/tests/lean/synthorder.lean.expected.out index d891c4ec711e..707c333edea2 100644 --- a/tests/lean/synthorder.lean.expected.out +++ b/tests/lean/synthorder.lean.expected.out @@ -18,7 +18,7 @@ all remaining arguments have metavariables: Four α β One β TwoHalf β -[Meta.synthOrder] synthesizing the arguments of @instFour in the order [4, 2, 3]: +[Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]: Three α β One β TwoHalf β