/-
this implementation of the Conway-Wechsler naming scheme by Ian Henderson <ian@ianhenderson.org> on 2026 february 17
based on zillion.py from https://kyodaisuu.github.io/illion/ by Fish https://googology.wikia.org/wiki/User:Kyodaisuu
i did some spot checks but it hasn't been thoroughly tested -- please report any defects to my email above!
-/

def units : Fin 10 → String
  | 0 => ""
  | 1 => "un"
  | 2 => "duo"
  | 3 => "tre"
  | 4 => "quattuor"
  | 5 => "quin"
  | 6 => "se"
  | 7 => "septe"
  | 8 => "octo"
  | 9 => "nove"

def tens : Fin 10 → String
  | 0 => ""
  | 1 => "dec"
  | 2 => "vigint"
  | 3 => "trigint"
  | 4 => "quadragint"
  | 5 => "quinquagint"
  | 6 => "sexagint"
  | 7 => "septuagint"
  | 8 => "octogint"
  | 9 => "nonagint"

def lastTensLetter : Fin 10 → String
  | 0 => ""
  | 1 => "i"
  | 2 => "i"
  | _ => "a"

def huns (l : String) : Fin 10 → String
  | 0 => ""
  | 1 => l ++ "cent"
  | 2 => l ++ "ducent"
  | 3 => l ++ "trecent"
  | 4 => l ++ "quadringent"
  | 5 => l ++ "quingent"
  | 6 => l ++ "sescent"
  | 7 => l ++ "septingent"
  | 8 => l ++ "octingent"
  | 9 => l ++ "nongent"

def precN : Nat → String → String
  | 7, s => s ++ "n"
  | 9, s => s ++ "n"
  | _, s => s
def precM : Nat → String → String
  | 7, s => s ++ "m"
  | 9, s => s ++ "m"
  | _, s => s
def precX : Nat → String → String
  | 3, _ => "tres"
  | 6, _ => "sex"
  | _, s => s
def precS : Nat → String → String
  | 3, s => s ++ "s"
  | 6, s => s ++ "s"
  | _, s => s

def prec (s : String) : Fin 10 → Fin 10 → Fin 10 → String
  | _, 1, u => precN u s
  | _, 2, u => precM u (precS u s)
  | _, 3, u => precN u (precS u s)
  | _, 4, u => precN u (precS u s)
  | _, 5, u => precN u (precS u s)
  | _, 6, u => precN u s
  | _, 7, u => precN u s
  | _, 8, u => precM u (precX u s)
  | _, 9, _ => s
  | 0, 0, _ => s
  | 1, 0, u => precN u (precX u s)
  | 2, 0, u => precN u s
  | 3, 0, u => precN u (precS u s)
  | 4, 0, u => precN u (precS u s)
  | 5, 0, u => precN u (precS u s)
  | 6, 0, u => precN u s
  | 7, 0, u => precN u s
  | 8, 0, u => precM u (precX u s)
  | 9, 0, _ => s

def base : Fin 1000 → String
  | 0 => "nilli"
  | 1 => "milli"
  | 2 => "billi"
  | 3 => "trilli"
  | 4 => "quadrilli"
  | 5 => "quintilli"
  | 6 => "sextilli"
  | 7 => "septilli"
  | 8 => "octilli"
  | 9 => "nonilli"
  | n =>
    let unit : Fin 10 := .ofNat _ n
    let ten : Fin 10 := .ofNat _ (n / 10)
    let hun : Fin 10 := ⟨n / 100, by omega⟩
    prec (units unit) hun ten unit ++ tens ten ++ huns (lastTensLetter ten) hun ++ "illi"

def concat (n : Nat) : String :=
  if h : n < 1000 then
    base ⟨n, h⟩
  else
    concat (n / 1000) ++ base (.ofNat _ n)

def llion (n : Nat) : String := concat n ++ "on"

def onesPlace : Fin 10 → String
  | 0 => "zero"
  | 1 => "one"
  | 2 => "two"
  | 3 => "three"
  | 4 => "four"
  | 5 => "five"
  | 6 => "six"
  | 7 => "seven"
  | 8 => "eight"
  | 9 => "nine"

def tensPlace : Fin 10 → String
  | 0 => ""
  | 1 => ""
  | 2 => "twenty"
  | 3 => "thirty"
  | 4 => "forty"
  | 5 => "fifty"
  | 6 => "sixty"
  | 7 => "seventy"
  | 8 => "eighty"
  | 9 => "ninety"

def smaller : Fin 100 → String
  | 10 => "ten"
  | 11 => "eleven"
  | 12 => "twelve"
  | 13 => "thirteen"
  | 14 => "fourteen"
  | 15 => "fifteen"
  | 16 => "sixteen"
  | 17 => "seventeen"
  | 18 => "eighteen"
  | 19 => "nineteen"
  | n =>
    if h : n < 10 then
      onesPlace ⟨n, h⟩
    else
      tensPlace ⟨n / 10, by omega⟩ ++ (if n % 10 == 0 then "" else onesPlace (.ofNat _ n))

def small (n : Fin 1000) : String :=
  if h : n < 100 then
    smaller ⟨n, h⟩
  else
    onesPlace ⟨n / 100, by omega⟩ ++ "hundred" ++ (if n % 100 == 0 then "" else smaller (.ofNat _ n))

def medium (n : Fin 1000000) : String :=
  if h : n < 1000 then
    small ⟨n, h⟩
  else
    small ⟨n / 1000, by omega⟩ ++ "thousand" ++ (if n % 1000 == 0 then "" else small (.ofNat _ n))

def large (n : Nat) (m : Nat) : String :=
  let k : Fin 1000 := .ofNat _ n
  (if n >= 1000 then large (n / 1000) (m + 1) else "") ++ (if k == 0 then "" else small k ++ llion m)

def sayNumber (n : Nat) :=
  let k : Fin 1000000 := .ofNat _ n
  (if n >= 1000000 then large (n / 1000000) 1 else "") ++ (if k == 0 then "" else medium k)