/WritingSystem.lean at 7fe0361f2ce175b59dc8ef9cb951387defe22172

-- 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 | 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, .rf⟩ -- Technically this is alveolo-palatal
  | 'ㄑ' => some ⟨.c true, .rf⟩ -- Same as above
  | 'ㄒ' => some ⟨.s, .rf⟩ -- Same as above
  | 'ㄓ' => 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 asp := match c.manner with
      | .t asp => asp
      | .c asp => asp
      | _ => true
    (match c.manner with
      | .n => "n"
      | .t _ => "г"
      | .c _ => "c"
      | .s => "s"
      | .l => "l")
    ++ ((match c.place, asp with
      | .la, true => some 0x304
      | .da, true => none
      | .rf, true => some 0x307
      | .ve, true => some 0x308
      | .la, false => some 0x331
      | .da, false => some 0x32F
      | .rf, false => some 0x323
      | .ve, false => some 0x324)
        |>.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 .o
  | 'ㄜ' => some <| .medial .o -- Allophone of ㄛ
  | 'ㄝ' => some <| .medial .e
  | 'ㄞ' => some <| .coda false .i
  | 'ㄟ' => some <| .coda true .i
  | 'ㄠ' => some <| .coda false .u
  | 'ㄡ' => some <| .coda true .u
  | 'ㄢ' => some <| .coda false .n
  | 'ㄣ' => some <| .coda true .n
  | 'ㄤ' => some <| .coda false .ng
  | 'ㄥ' => some <| .coda true .ng
  | 'ㄦ' => some <| .medial .r
  | 'ㄧ' => some <| .medial .i
  | 'ㄨ' => some <| .medial .u
  | 'ㄩ' => some <| .medial .yu
  | _ => none

def Vowel.nucleus : Vowel → Bool
  | .medial _ => true
  | .coda b _ => b

instance : ToString Vowel where
  toString
    | .medial m => match m with
      | .a => "a"
      | .e => "e"
      | .i => "ı"
      | .o => "e"
      | .u => "u"
      | .yu => "v"
      | .r => "r"
    | .coda _ c => match c with
      | .i => "ȷ"
      | .u => "o"
      | .n => "n"
      | .ng => "ŋ"

def parseTone : Char → Fin 5
  | 'ˊ' => 1
  | 'ˇ' => 2
  | 'ˋ' => 3
  | '˙' => 4
  | _ => 0

instance : ToString (Fin 5 × Bool) where
  toString t := (match t with
    | ⟨0, true⟩ => some 0x304
    | ⟨1, true⟩ => some 0x301
    | ⟨2, true⟩ => some 0x30C
    | ⟨3, true⟩ => none -- Falling tone is most common
    | ⟨4, true⟩ => some 0x30A
    | ⟨0, false⟩ => some 0x331
    | ⟨1, false⟩ => some 0x317
    | ⟨2, false⟩ => some 0x32C
    | ⟨3, false⟩ => some 0x316
    | ⟨4, false⟩ => some 0x325)
      |>.map Char.ofNat
      |>.map toString
      |>.getD ""

def convert (s : String) :=
  s.toList.foldl (fun (out, nuc) x ↦
    match parseConsonant x with
    | some c => (out ++ toString c, some true)
    | none => match parseVowel x with
      | some v => (out ++ toString v, some v.nucleus)
      | none => match nuc with
        | some nuc => (out ++ toString (parseTone x, nuc), none)
        | none => (out ++ x.toString, none))
    ("", none) |>.1

/-
早上好中国，现在我有冰淇淋，我很喜欢冰淇淋，但是，速度与激情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ŋ̄г̤ué, ṡın̖c̯ȷ̖ uě ıǒ г̱ıŋ̄ċı́lıń, uě s̈ň ṡı̌s̈uṉ г̱ıŋ̄ċı́lıń, г̯n̖ṡ, Suг̯u V̌ C̣ı̄ċıŋ́ 9, г̱ı̌ г̱ıŋ̄ċı́lıń, Suг̯u V̌ C̣ı̄ċıŋ́, Suг̯u V̌ C̣ı̄ċıŋ́ 9, uě c̯uȷ ṡı̌s̈uṉ. Suěı̌... ṡın̖c̯ı̖ ṡ ın̄ve ṡ́c̣ıṉ, c̣uňг̱ȷ̖ 1 2 3:
Lıŋ̬ г̤e lı̌гȷ̖ ı̌s̈o, Suг̯u V̌ C̣ı̄ċıŋ́ 9, lıŋ̬ г̤e lı̌г̱ȷ̖ ı̌s̈o, Suг̯u V̌ C̣ı̄ċıŋ́ 9, lıŋ̬ г̤e lı̌г̱ȷ̖ ı̌s̈o, Suг̯u V̌ C̣ı̄ċıŋ́ 9.
Г̱uıo̖ uŋ̖c̣ı, г̱uıo̖ cueг̤ue, ċv г̯ın̖ıŋ̌vn̖ г̈n̖ Suг̯u V̌ C̣ı̄ċıŋ́ 9, ın̄uȷ́ 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， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。"