Name generation APIs for to_additive-like attributes

structure Mathlib.Tactic.GuessName.GuessNameData : Type

The data that is required to guess the name of a translation.

• nameDict : Std.HashMap String (List String)

  Dictionary used by guessName to autogenerate names. This only transforms single name components, unlike abbreviationDict.

  Note: guessName capitalizes the output according to the capitalization of the input. In order for this to work, the input should always start with a lower case letter, and the output should always start with an upper case letter.

• abbreviationDict : Std.HashMap String String

  We need to fix a few abbreviations after applying nameDict, i.e. replacing ZeroLE by Nonneg. This dictionary contains these fixes. The input should contain entries that is in lowerCamelCase (e.g. ltzero; the initial sequence of capital letters should be lower-cased) and the output should be in UpperCamelCase (e.g. LTZero). When applying the dictionary, we lower-case the output if the input was also given in lower-case.

def Mathlib.Tactic.GuessName.endCapitalNames : Std.TreeMap String (List String) compare

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 an 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 TreeMap (but this would require having something similar to the rb_lmap from Lean 3).

partial def Mathlib.Tactic.GuessName.String.splitCase (s : String) (i₀ : String.Pos.Raw := 0) (r : List String := []) : List String

This function takes a String and splits it into separate parts based on the following naming conventions.

E.g. #eval "InvHMulLEConjugate₂SMul_ne_top".splitCase yields ["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"].

partial def Mathlib.Tactic.GuessName.String.decapitalizeSeq (s : String) (i : String.Pos.Raw := 0) : String

Replaces characters in s by lower-casing the first characters until a non-upper-case character is found.

def Mathlib.Tactic.GuessName.decapitalizeLike (r s : String) : String

If r starts with an upper-case letter, return s, otherwise return s with the initial sequence of upper-case letters lower-cased.

def Mathlib.Tactic.GuessName.decapitalizeFirstLike (s : String) : List String → List String

Decapitalize the first element of a list if s starts with a lower-case letter. Note that we need to decapitalize multiple characters in some cases, in examples like HMul or HAdd.

def Mathlib.Tactic.GuessName.applyNameDict (g : GuessNameData) : List String → List String

Apply the nameDict and decapitalize the output like the input.

E.g.

#eval applyNameDict ["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]

yields ["Neg", "HAdd", "LE", "Conjugate₂", "VAdd", "_", "ne", "_", "top"].

@[irreducible]

def Mathlib.Tactic.GuessName.fixAbbreviationAux (g : GuessNameData) : List String → List String → String

Helper for fixAbbreviation. Note: this function has a quadratic number of recursive calls, but is not a performance bottleneck.

def Mathlib.Tactic.GuessName.fixAbbreviation (g : GuessNameData) (l : List String) : String

Replace substrings according to abbreviationDict, matching the case of the first letter.

Example:

#eval applyNameDict ["Mul", "Support"]

gives the preliminary translation ["Add", "Support"]. Subsequently

#eval fixAbbreviation ["Add", "Support"]

"fixes" this translation and returns Support.

def Mathlib.Tactic.GuessName.guessName (g : GuessNameData) : String → String

Autogenerate additive name. This runs in several steps:

1. Split according to capitalisation rule and at _.
2. Apply word-by-word translation rules.
3. Fix up abbreviations that are not word-by-word translations, like "addComm" or "Nonneg".