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

• ToAdditive.decapitalizeLike r s = if (String.Pos.Raw.get r 0).isUpper = true then s else ToAdditive.String.decapitalizeSeq s

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

• ToAdditive.decapitalizeFirstLike s (x_1 :: r) = ToAdditive.decapitalizeLike s x_1 :: r
• ToAdditive.decapitalizeFirstLike s [] = []

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

Equations

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

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

• ToAdditive.applyNameDict (x_1 :: r) = (match ToAdditive.nameDict.get? x_1.toLower with | some y => ToAdditive.decapitalizeFirstLike x_1 y | none => [x_1]) ++ ToAdditive.applyNameDict r
• ToAdditive.applyNameDict [] = []

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

Equations

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

@[irreducible]

def ToAdditive.fixAbbreviationAux : 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.
• ToAdditive.fixAbbreviationAux [] [] = ""
• ToAdditive.fixAbbreviationAux [] (x_2 :: s) = x_2 ++ ToAdditive.fixAbbreviationAux s []

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

• ToAdditive.fixAbbreviation l = ToAdditive.fixAbbreviationAux l []

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) => ToAdditive.fixAbbreviation (ToAdditive.applyNameDict (ToAdditive.String.splitCase s))