/WritingSystem.lean at e03a846a47cc16ccf1011fd40c3395d2bb1e0f1f

import Std.Data.HashMap

-- https://en.wikipedia.org/wiki/Standard_Chinese_phonology#Consonants
inductive ConsonantManner where
  | n
  | t : Bool → ConsonantManner
  | c : Bool → ConsonantManner
  | s
  | l

inductive ConsonantPlace where
  | la | da | rf | ap | ve

structure Consonant where
  manner : ConsonantManner
  place : ConsonantPlace

def parseConsonant : Char → Option Consonant
  | 'ㄅ' => some ⟨.t false, .la⟩
  | 'ㄆ' => some ⟨.t true, .la⟩
  | 'ㄇ' => some ⟨.n, .la⟩
  | 'ㄈ' => some ⟨.s, .la⟩
  | 'ㄉ' => some ⟨.t false, .da⟩
  | 'ㄊ' => some ⟨.t true, .da⟩
  | 'ㄋ' => some ⟨.n, .da⟩
  | 'ㄌ' => some ⟨.l, .da⟩
  | 'ㄍ' => some ⟨.t false, .ve⟩
  | 'ㄎ' => some ⟨.t true, .ve⟩
  | 'ㄏ' => some ⟨.s, .ve⟩
  | 'ㄐ' => some ⟨.c false, .ap⟩
  | 'ㄑ' => some ⟨.c true, .ap⟩
  | 'ㄒ' => some ⟨.s, .ap⟩
  | 'ㄓ' => some ⟨.c false, .rf⟩
  | 'ㄔ' => some ⟨.c true, .rf⟩
  | 'ㄕ' => some ⟨.s, .rf⟩
  | 'ㄖ' => some ⟨.l, .rf⟩
  | 'ㄗ' => some ⟨.c false, .da⟩
  | 'ㄘ' => some ⟨.c true, .da⟩
  | 'ㄙ' => some ⟨.s, .da⟩
  | _ => none

instance : ToString Consonant where
  toString c :=
    let f : Bool → String := (if · then "" else Char.ofNat 0x323 |>.toString)
    (match c.manner with
      | .n => "n"
      | .t asp => "ꞇ" ++ f asp
      | .c asp => "c" ++ f asp
      | .s => "s"
      | .l => "l")
    ++ ((match c.place with
      | .la => some 0x313
      | .da => none
      | .rf => some 0x307
      | .ap => some 0x308
      | .ve => some 0x304)
        |>.map Char.ofNat
        |>.map toString
        |>.getD "")

-- https://en.wikipedia.org/wiki/Standard_Chinese_phonology#Vowels
-- Technically not all of these are medials but idk what to call it
inductive VowelMedial where
  | a | e | i | o | u | yu | r

inductive VowelCoda where
  | i | u | n | ng

inductive Vowel where
  | medial : VowelMedial → Vowel
  | coda : Bool → VowelCoda → Vowel

def parseVowel : Char → Option Vowel
  | 'ㄚ' => some <| .medial .a
  | 'ㄛ' => some <| .medial .e
  | 'ㄜ' => some <| .medial .e
  | 'ㄝ' => some <| .medial .e
  | 'ㄞ' => some <| .coda true .i
  | 'ㄟ' => some <| .coda false .i
  | 'ㄠ' => some <| .coda true .u
  | 'ㄡ' => some <| .coda false .u
  | 'ㄢ' => some <| .coda true .n
  | 'ㄣ' => some <| .coda false .n
  | 'ㄤ' => some <| .coda true .ng
  | 'ㄥ' => some <| .coda false .ng
  | 'ㄦ' => some <| .medial .r
  | 'ㄧ' => some <| .medial .i
  | 'ㄨ' => some <| .medial .u
  | 'ㄩ' => some <| .medial .yu
  | _ => none

instance : ToString Vowel where
  toString v := match v with
    | .medial m => (match m with
      | .a => "a"
      | .e => "e"
      | .i => "ı"
      | .o => "o"
      | .u => "u"
      | .yu => "y"
      | .r => "r")
    | .coda b c => (match c with
      | .i => "ı"
      | .u => "o"
      | .n => "n"
      | .ng => "ŋ") ++ (if b then Char.ofNat 0x30A |>.toString else "")

inductive Tone where
  | er | san | si | wu

def parseTone : Char → Option Tone
  | 'ˊ' => some .er
  | 'ˇ' => some .san
  | 'ˋ' => some .si
  | '˙' => some .wu
  | _ => none

instance : ToString Tone where
  toString t := Char.ofNat (match t with
    | .er => 0x301
    | .san => 0x30C
    | .si => 0x300
    | .wu => 0x307)
      |>.toString

def convert (s : String) :=
  s.toList.map (fun x ↦
    match parseConsonant x with
    | some c => toString c
    | none => match parseVowel x with
      | some v => toString v
      | none => match parseTone x with
        | some t => toString t
        | none => x.toString)
  |> String.intercalate ""

/-
早上好中国，现在我有冰淇淋，我很喜欢冰淇淋，但是，速度与激情9，比冰淇淋，速度与激情，速度与激情9，我最喜欢。所以…现在是音乐时间，准备 1 2 3，
两个礼拜以后，速度与激情9，两个礼拜以后，速度与激情9，两个礼拜以后，速度与激情9。
不要忘记，不要错过，去电影院看速度与激情9，因为非常好电影，动作非常好，差不多一样。冰淇淋，再见。

ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。

C̣o̊̌ṡŋ̊̀ s̄o̊̌ Ċ̣uŋꞇ̣̄uoé, s̈ın̊̀c̣ı̊̀ uě ıǒ ꞇ̣̓ıŋc̈ı́lıń, uě s̄ň s̈ı̌s̄un̊ ꞇ̣̓ıŋc̈ı́lıń, ꞇ̣n̊̀ṡ̀, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ꞇ̣̓ı̌ ꞇ̣̓ıŋc̈ı́lıń, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, uě c̣uı̀ s̈ı̌s̄un̊. Suěı̌... s̈ın̊̀c̣ı̊̀ ṡ̀ ınyè ṡ́c̣̈ın̊, ċ̣uňꞇ̣̓ı̀ 1 2 3,
Lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9.
Ꞇ̣̓ùıo̊̀ uŋ̊̀c̣̈ı̀, ꞇ̣̓ùıo̊̀ cuèꞇ̣̄uè, c̈ỳ ꞇ̣ın̊̀ıŋ̌yn̊̀ ꞇ̄n̊̀ Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ınuı́ s̓ıċŋ̊́ s̄o̊̌ ꞇ̣ın̊̀ıŋ̌, ꞇ̣uŋ̀c̣uè s̓ıċŋ̊́ s̄o̊̌, ċàꞇ̣̓ùꞇ̣ue ııŋ̊̀. Ꞇ̣̓ıŋc̈ı́lıń, c̣ı̊̀c̣̈ın̊̀.
-/

#eval convert "ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。"