/WritingSystem.lean at 65d853773813155eba147fc8a8ca6034fa18c261

-- 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 0x329
      | .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 => "y"
      | .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, nuc)
    | 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 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̇ˋ ın̄ye 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ıŋ̬ г̤e 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, ı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， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。"