Name generation APIs for to_additive

def ToAdditive.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

• ToAdditive.endCapitalNames = Std.TreeMap.ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])] compare

partial def String.splitCase (s : String) (i₀ : Pos := 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 ToAdditive.capitalizeLikeAux (s : String) (i : String.Pos := 0) (p : String) : String

Helper for capitalizeLike.

def ToAdditive.capitalizeLike (r s : String) : String

Capitalizes s char-by-char like r. If s is longer, it leaves the tail untouched.

Equations

• ToAdditive.capitalizeLike r s = ToAdditive.capitalizeLikeAux r 0 s

def ToAdditive.capitalizeFirstLike (s : String) : List String → List String

Capitalize First element of a list like s. Note that we need to capitalize multiple characters in some cases, in examples like HMul or hAdd.

Equations

• ToAdditive.capitalizeFirstLike s (x_1 :: r) = ToAdditive.capitalizeLike s x_1 :: r
• ToAdditive.capitalizeFirstLike s [] = []

def ToAdditive.nameDict : String → List String

Dictionary used by guessName to autogenerate names.

Note: guessName capitalizes first element of the output according to capitalization of the input. Input and first element should therefore be lower-case, 2nd element should be capitalized properly.

def ToAdditive.applyNameDict : List String → List String

Turn each element to lower-case, apply the nameDict and capitalize the output like the input.

Equations

• ToAdditive.applyNameDict (x_1 :: r) = ToAdditive.capitalizeFirstLike x_1 (ToAdditive.nameDict x_1.toLower) ++ ToAdditive.applyNameDict r
• ToAdditive.applyNameDict [] = []

def ToAdditive.fixAbbreviation : List String → List String

There are a few abbreviations we use. For example "Nonneg" instead of "ZeroLE" or "addComm" instead of "commAdd". Note: The input to this function is case sensitive! Todo: A lot of abbreviations here are manual fixes and there might be room to improve the naming logic to reduce the size of fixAbbreviation.

def ToAdditive.guessName : 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

• ToAdditive.guessName = String.mapTokens '\'' fun (s : String) => String.join (ToAdditive.fixAbbreviation (ToAdditive.applyNameDict s.splitCase))