feat: better name guessing for to_additive (leanprover#779)

* `@[to_additive]` will now correctly guess names with `CoeTC`, `CoeT` and `CoeHTCT` in it
* rewrite function `targetName`. 
  - It will now warn the user if it gives a composite name that can be auto-generated (before `to_additive` would never warn if a composite name was given). 
  - the logic when `allowAutoName = true` now corresponds to the docstring
  - Fix a bug where declarations were silently allowed to translate to itself (maybe because the `return` statements returned a value for the whole function?)
  - Add some more tracing
  - The behavior of namespaces when giving a composite name has been changed. It will always generate a name with the same number of components. Example:
```lean
namespace MeasureTheory.MulMeasure
@[to_additive AddMeasure.myOperation] def myOperation := ...
-- before: generates `AddMeasure.myOperation` (and never gives a warning)
-- after: generates `MeasureTheory.AddMeasure.myOperation` (and probably warns that the name can be auto-generated)
end MeasureTheory.MulMeasure
```
* This should fix all problems in leanprover#659 other than leanprover#660

Minor changes:
* When applying `@[to_additive]` to a structure, add a trace message if no translation is inserted for a field.
* Define `Name.fromComponents` and `Name.splitAt`
* Reduce transitive imports of `Tactic/toAdditive`
* Move some auxiliary declarations from `Tactic/Simps` to more appropriate places 
  - swap arguments of `String.isPrefixOf?`
  - improve `Name.getString`

Co-authored-by: Scott Morrison <[email protected]>

Mathlib/Data/String/Defs.lean

@@ -20,4 +20,9 @@ then reassembles the string by intercalating the separator token `c` over the ma
 def mapTokens (c : Char) (f : String → String) : String → String :=
 intercalate (singleton c) ∘ List.map f ∘ (·.split (· = c))
 
+/-- `isPrefixOf? pre s` returns `some post` if `s = pre ++ post`.
+  If `pre` is not a prefix of `s`, it returns `none`. -/
+def isPrefixOf? (pre s : String) : Option String :=
+  if startsWith s pre then some <| s.drop pre.length else none
+
 end String

Mathlib/Lean/Expr/Basic.lean

@@ -6,6 +6,7 @@ Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
 import Lean
 import Mathlib.Util.MapsTo
+import Std.Data.List.Basic
 
 /-!
 # Additional operations on Expr and related types
@@ -43,6 +44,34 @@ def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do
   | str n' s => mkStr (mapPrefix f n') s
   | num n' i => mkNum (mapPrefix f n') i
 
+/-- Build a name from components. For example ``from_components [`foo, `bar]`` becomes
+  ``` `foo.bar```.
+  It is the inverse of `Name.components` on list of names that have single components. -/
+def fromComponents : List Name → Name := go .anonymous where
+  /-- Auxiliary for `Name.fromComponents` -/
+  go : Name → List Name → Name
+  | n, []        => n
+  | n, s :: rest => go (s.updatePrefix n) rest
+
+/-- Update the last component of a name. -/
+def updateLast (f : String → String) : Name → Name
+| .str n s => .str n (f s)
+| n        => n
+
+/-- Get the last field of a name as a string.
+Doesn't raise an error when the last component is a numeric field. -/
+def getString : Name → String
+| .str _ s => s
+| .num _ n => toString n
+| .anonymous => ""
+
+/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`, i.e.
+  `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
+  Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/
+def splitAt (nm : Name) (n : Nat) : Name × Name :=
+  let (nm2, nm1) := (nm.componentsRev.splitAt n)
+  (.fromComponents <| nm1.reverse, .fromComponents <| nm2.reverse)
+
 end Name
 
 

Mathlib/Tactic/Simps/Basic.lean

@@ -63,35 +63,14 @@ There are some small changes in the attribute. None of them should have great ef
 structures, projections, simp, simplifier, generates declarations
 -/
 
--- move
-namespace String
-
-/-- `isPrefixOf? s pre` returns `some post` if `s = pre ++ post`.
-  If `pre` is not a prefix of `s`, it returns `none`. -/
-def isPrefixOf? (s pre : String) : Option String :=
-  if startsWith s pre then some <| s.drop pre.length else none
-
-end String
-
 open Lean Meta Parser Elab Term Command
 
-/-- Update the last component of a name. -/
-def Lean.Name.updateLast (f : String → String) : Name → Name
-| .str n s => .str n (f s)
-| n        => n
-
 /-- `updateName nm s is_prefix` adds `s` to the last component of `nm`,
   either as prefix or as suffix (specified by `isPrefix`), separated by `_`.
   Used by `simps_add_projections`. -/
 def updateName (nm : Name) (s : String) (isPrefix : Bool) : Name :=
   nm.updateLast fun s' ↦ if isPrefix then s ++ "_" ++ s' else s' ++ "_" ++ s
 
-/-- Get the last field of a name as a string.
-Doesn't raise an error when the last component is a numeric field. -/
-def Lean.Name.getString : Name → String
-| .str _ s => s
-| _        => ""
-
 -- move
 namespace Lean.Meta
 open Tactic Simp
@@ -455,7 +434,7 @@ partial def getCompositeOfProjectionsAux (str : Name) (proj : String) (x : Expr)
   let env ← getEnv
   let projs := (getStructureInfo? env str).get!
   let projInfo := projs.fieldNames.toList.mapIdx fun n p ↦
-    return (← proj.isPrefixOf? ("_" ++ p.getString!), n, p)
+    return (← ("_" ++ p.getString!).isPrefixOf? proj, n, p)
   let some (projRest, index, projName) := (projInfo.filterMap id).getLast?
     | throwError "Failed to find constructor {proj.drop 1} in structure {str}."
   let strDecl := (env.find? str).get!
@@ -992,7 +971,7 @@ partial def simpsAddProjections (nm : Name) (type lhs rhs : Expr)
       }be customly defined for `simps`, and differ from the projection names of the structure."
   let nms ← projInfo.concatMapM fun ⟨newRhs, proj, projExpr, projNrs, isDefault, isPrefix⟩ ↦ do
     let newType ← inferType newRhs
-    let newTodo := todo.filterMap fun x ↦ x.isPrefixOf? ("_" ++ proj.getString)
+    let newTodo := todo.filterMap fun x ↦ ("_" ++ proj.getString).isPrefixOf? x
     -- we only continue with this field if it is default or mentioned in todo
     if !(isDefault && todo.isEmpty) && newTodo.isEmpty then return #[]
     let newLhs := projExpr.instantiateLambdasOrApps #[lhsAp]

Mathlib/Tactic/ToAdditive.lean

@@ -5,12 +5,7 @@ Authors: Mario Carneiro, Yury Kudryashov, Floris van Doorn, Jon Eugster
 Ported by: E.W.Ayers
 -/
 import Mathlib.Data.String.Defs
-import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.Expr.ReplaceRec
-import Mathlib.Lean.Expr
-import Lean
-import Lean.Data
-import Lean.Elab.Term
 import Std.Lean.NameMapAttribute
 import Std.Data.Option.Basic
 
@@ -50,9 +45,20 @@ macro "to_additive!?" rest:to_additiveRest : attr => `(attr| to_additive ! ? $re
 /-- The `to_additive` attribute. -/
 macro "to_additive?!" rest:to_additiveRest : attr => `(attr| to_additive ! ? $rest)
 
-/-- A set of strings of names that are written in all-caps. -/
-def allCapitalNames : RBTree String compare :=
-.ofList ["LE", "LT", "WF"]
+/-- A set of strings of names that end in a capital letter.
+* If the string contains a lowercase letter, the string should be split between the first occurrence
+  of a lower-case letter followed by a upper-case letter.
+* If multiple strings have the same prefix, they should be grouped by prefix
+* In this case, the second list should be prefix-free
+  (no element can be a prefix of a later element)
+
+Todo: automate the translation from `String` to an element in this `RBMap`
+  (but this would require having something similar to the `rb_lmap` from Lean 3). -/
+def endCapitalNames : Lean.RBMap String (List String) compare :=
+-- endCapitalNamesOfList ["LE", "LT", "WF", "CoeTC", "CoeT", "CoeHTCT"]
+.ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])]
+
+
 
 /--
 This function takes a String and splits it into separate parts based on the following
@@ -62,21 +68,28 @@ E.g. `#eval  "InvHMulLEConjugate₂Smul_ne_top".splitCase` yields
 `["Inv", "HMul", "LE", "Conjugate₂", "Smul", "_", "ne", "_", "top"]`.
 -/
 partial def String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) : List String :=
+Id.run do
   -- We test if we need to split between `i₀` and `i₁`.
   let i₁ := s.next i₀
   if s.atEnd i₁ then
     -- If `i₀` is the last position, return the list.
     let r := s::r
-    r.reverse
+    return r.reverse
   /- We split the string in three cases
   * We split on both sides of `_` to keep them there when rejoining the string;
-  * We split after a sequence of capital letters in `allCapitalNames`;
-  * We split after a lower-case letter that is followed by an upper-case letter. -/
-  else if s.get i₀ == '_' || s.get i₁ == '_' ||
-    ((s.get i₁).isUpper && (!(s.get i₀).isUpper || allCapitalNames.contains (s.extract 0 i₁))) then
-    splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r
-  else
-    splitCase s i₁ r
+  * We split after a name in `endCapitalNames`;
+  * We split after a lower-case letter that is followed by an upper-case letter
+    (unless it is part of a name in `endCapitalNames`). -/
+  if s.get i₀ == '_' || s.get i₁ == '_' then
+    return splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r
+  if (s.get i₁).isUpper then
+    if let some strs := endCapitalNames.find? (s.extract 0 i₁) then
+      if let some (pref, newS) := strs.findSome?
+        fun x ↦ x.isPrefixOf? (s.extract i₁ s.endPos) |>.map (x, ·) then
+        return splitCase newS 0 <| (s.extract 0 i₁ ++ pref)::r
+    if !(s.get i₀).isUpper then
+      return splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r
+  return splitCase s i₁ r
 
 namespace ToAdditive
 
@@ -271,7 +284,7 @@ def applyReplacementFun : Expr → MetaM Expr :=
     match e with
     | .lit (.natVal 1) => pure <| mkRawNatLit 0
     | .const n₀ ls => do
-      let n₁ := Name.mapPrefix (findTranslation? <|← getEnv) n₀
+      let n₁ := n₀.mapPrefix (findTranslation? <|← getEnv)
       if n₀ != n₁ then
         trace[to_additive_detail] "applyReplacementFun: {n₀} → {n₁}"
       let ls : List Level ← (do -- [todo] just get Lean to figure out the levels?
@@ -675,21 +688,21 @@ def guessName : String → String :=
 
 /-- Return the provided target name or autogenerate one if one was not provided. -/
 def targetName (src tgt : Name) (allowAutoName : Bool) : CoreM Name := do
-  let res ← do
-    if tgt.getPrefix != Name.anonymous || allowAutoName then
-      return tgt
-    let .str pre s := src | throwError "to_additive: can't transport {src}"
-    let tgt_auto := guessName s
-    if tgt.toString == tgt_auto then
-      dbg_trace "{src}: correctly autogenerated target name {tgt_auto
-        }, you may remove the explicit {tgt} argument."
-    let pre := pre.mapPrefix <| findTranslation? (← getEnv)
-    if tgt == Name.anonymous then
-      return Name.mkStr pre tgt_auto
-    else
-      return  Name.mkStr pre tgt.toString
+  let .str pre s := src | throwError "to_additive: can't transport {src}"
+  trace[to_additive_detail] "The name {s} splits as {s.splitCase}"
+  let tgt_auto := guessName s
+  let depth := tgt.getNumParts
+  let pre := pre.mapPrefix <| findTranslation? (← getEnv)
+  let (pre1, pre2) := pre.splitAt (depth - 1)
+  if tgt == pre2.str tgt_auto && !allowAutoName then
+    dbg_trace "to_additive correctly autogenerated target name for {src}. {"\n"
+      }You may remove the explicit argument {tgt}."
+  let res := if tgt == .anonymous then pre.str tgt_auto else pre1 ++ tgt
+  -- we allow translating to itself if `tgt == src`, which is occasionally useful for `additiveTest`
   if res == src && tgt != src then
     throwError "to_additive: can't transport {src} to itself."
+  if tgt != .anonymous then
+    trace[to_additive_detail] "The automatically generated name would be {pre.str tgt_auto}"
   return res
 
 private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (Array Name)) : CoreM Unit := do
@@ -700,6 +713,8 @@ private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (Array Name))
   for (srcField, tgtField) in srcFields.zip tgtFields do
     if srcField != tgtField then
       insertTranslation (src ++ srcField) (tgt ++ tgtField)
+    else
+      trace[to_additive] "Translation {src ++ srcField} ↦ {tgt ++ tgtField} is automatic."
 
 /-- Add the structure fields of `src` to the translations dictionary
 so that future uses of `to_additive` will map them to the corresponding `tgt` fields. -/

test/toAdditive.lean

@@ -103,6 +103,9 @@ run_cmd do
   let t ← Elab.Command.liftCoreM <| Lean.Meta.MetaM.run' <| ToAdditive.expand c.type
   let decl := c |>.updateName `Test.barr6 |>.updateType t |>.updateValue e |>.toDeclaration!
   Elab.Command.liftCoreM <| addAndCompile decl
+  -- test that we cannot transport a declaration to itself
+  successIfFail <| Elab.Command.liftCoreM <|
+    ToAdditive.addToAdditiveAttr `bar11_works { ref := ← getRef }
 
 /-! Test the namespace bug (#8733). This code should *not* generate a lemma
   `add_some_def.in_namespace`. -/
@@ -160,7 +163,7 @@ def pi_nat_has_one {I : Type} : One ((x : I) → Nat)  := pi.has_one
 
 example : @pi_nat_has_one = @pi_nat_has_zero := rfl
 
-section noncomputablee
+section test_noncomputable
 
 @[to_additive Bar.bar]
 noncomputable def Foo.foo (h : ∃ _ : α, True) : α := Classical.choose h
@@ -171,9 +174,9 @@ def Foo.foo' : ℕ := 2
 theorem Bar.bar'_works : Bar.bar' = 2 := by decide
 
 run_cmd (do
-  if !isNoncomputable (← getEnv) `Bar.bar then throwError "bar shouldn't be computable"
-  if isNoncomputable (← getEnv) `Bar.bar' then throwError "bar' should be computable")
-end noncomputablee
+  if !isNoncomputable (← getEnv) `Test.Bar.bar then throwError "bar shouldn't be computable"
+  if isNoncomputable (← getEnv) `Test.Bar.bar' then throwError "bar' should be computable")
+end test_noncomputable
 
 section instances
 
@@ -254,6 +257,9 @@ run_cmd
   checkGuessName "LTHMulHPowLEHDiv" "LTHAddHSMulLEHSub"
   checkGuessName "OneLEHMul" "NonnegHAdd"
   checkGuessName "OneLTHPow" "PosHSMul"
+  checkGuessName "instCoeTCOneHom" "instCoeTCZeroHom"
+  checkGuessName "instCoeTOneHom" "instCoeTZeroHom"
+  checkGuessName "instCoeOneHom" "instCoeZeroHom"
 
 end guessName