# Name generation APIs for `to_additive`-like attributes #

source
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.

Instances For

source
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).

Equations

- Mathlib.Tactic.GuessName.endCapitalNames = Std.TreeMap.ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])] compare

Instances For

source
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"]`.

source
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.

source
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.

Equations

- Mathlib.Tactic.GuessName.decapitalizeLike r s = if (String.Pos.Raw.get r 0).isUpper = true then s else Mathlib.Tactic.GuessName.String.decapitalizeSeq s

Instances For

source
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`.

Equations

- Mathlib.Tactic.GuessName.decapitalizeFirstLike s (x_1 :: r) = Mathlib.Tactic.GuessName.decapitalizeLike s x_1 :: r
- Mathlib.Tactic.GuessName.decapitalizeFirstLike s [] = []

Instances For

source
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"]`.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.GuessName.applyNameDict g [] = []

Instances For

source
@[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.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.GuessName.fixAbbreviationAux g [] [] = ""
- Mathlib.Tactic.GuessName.fixAbbreviationAux g [] (x_2 :: s) = x_2 ++ Mathlib.Tactic.GuessName.fixAbbreviationAux g s []

Instances For

source
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`.

Equations

- Mathlib.Tactic.GuessName.fixAbbreviation g l = Mathlib.Tactic.GuessName.fixAbbreviationAux g l []

Instances For

source
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".

Equations

- One or more equations did not get rendered due to their size.

Instances For