Simplify so it uses fewer combining marks

Changes

1 changed files (+72/-59)

• WritingSystem.lean
  • @@ -1,5 +1,3 @@
    - import Std.Data.HashMap - -- https://en.wikipedia.org/wiki/Standard_Chinese_phonology#Consonants inductive ConsonantManner where | n
  • @@ -9,7 +7,7 @@ inductive ConsonantManner where
    | l inductive ConsonantPlace where - | la | da | rf | ap | ve + | la | da | rf | ve structure Consonant where manner : ConsonantManner
  • @@ -27,9 +25,9 @@ def parseConsonant : Char → Option Consonant
    | 'ㄍ' => 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⟩ -- 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⟩
  • @@ -41,19 +39,25 @@ def parseConsonant : Char → Option Consonant
    instance : ToString Consonant where toString c := - let f : Bool → String := (if · then "" else Char.ofNat 0x323 |>.toString) + let asp := match c.manner with + | .t asp => asp + | .c asp => asp + | _ => true (match c.manner with | .n => "n" - | .t asp => "ꞇ" ++ f asp - | .c asp => "c" ++ f asp + | .t _ => "г" + | .c _ => "c" | .s => "s" | .l => "l") - ++ ((match c.place with - | .la => some 0x313 - | .da => none - | .rf => some 0x307 - | .ap => some 0x308 - | .ve => some 0x304) + ++ ((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 "")
  • @@ -72,67 +76,76 @@ inductive Vowel where
    def parseVowel : Char → Option Vowel | 'ㄚ' => some <| .medial .a - | 'ㄛ' => some <| .medial .e - | 'ㄜ' => some <| .medial .e + | 'ㄛ' => some <| .medial .o + | 'ㄜ' => some <| .medial .o -- Allophone of ㄛ | 'ㄝ' => 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 <| .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 v := match v with - | .medial m => (match m with + toString + | .medial m => match m with | .a => "a" | .e => "e" | .i => "ı" - | .o => "o" + | .o => "e" | .u => "u" | .yu => "y" - | .r => "r") - | .coda b c => (match c with + | .r => "r" + | .coda _ 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 + | .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.map (fun x ↦ + s.toList.foldl (fun (out, nuc) x ↦ match parseConsonant x with - | some c => toString c + | some c => (out ++ toString c, nuc) | none => match parseVowel x with - | some v => toString v - | none => match parseTone x with - | some t => toString t - | none => x.toString) - |> String.intercalate "" + | 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，
  • @@ -141,9 +154,9 @@ def convert (s : String) :=
    ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。 - C̣o̊̌ṡŋ̊̀ s̄o̊̌ Ċ̣uŋꞇ̣̄uoé, s̈ın̊̀c̣ı̊̀ uě ıǒ ꞇ̣̓ıŋc̈ı́lıń, uě s̄ň s̈ı̌s̄un̊ ꞇ̣̓ıŋc̈ı́lıń, ꞇ̣n̊̀ṡ̀, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ꞇ̣̓ı̌ ꞇ̣̓ıŋc̈ı́lıń, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, uě c̣uı̀ s̈ı̌s̄un̊. Suěı̌... s̈ın̊̀c̣ı̊̀ ṡ̀ ınyè ṡ́c̣̈ın̊, ċ̣uňꞇ̣̓ı̀ 1 2 3, - Lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄è lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9. - Ꞇ̣̓ùıo̊̀ uŋ̊̀c̣̈ı̀, ꞇ̣̓ùıo̊̀ cuèꞇ̣̄uè, c̈ỳ ꞇ̣ın̊̀ıŋ̌yn̊̀ ꞇ̄n̊̀ Sùꞇ̣ù Y̌ C̣̈ıc̈ıŋ́ 9, ınuı́ s̓ıċŋ̊́ s̄o̊̌ ꞇ̣ın̊̀ıŋ̌, ꞇ̣uŋ̀c̣uè s̓ıċŋ̊́ s̄o̊̌, ċàꞇ̣̓ùꞇ̣ue ııŋ̊̀. Ꞇ̣̓ıŋc̈ı́lıń, c̣ı̊̀c̣̈ın̊̀. + C̩o̬ṡŋ̖ s̈o̬ C̣uŋ̄г̤ué, ṡın̖c̩ı̖ uě ıǒ г̱ıŋ̄ċı́lıń, uě s̈ň ṡı̌s̈uṉ г̱ıŋ̄ċı́lıń, г̩n̖ṡˋ, Suг̩u Y̌ C̣ı̄ċıŋ́ 9, г̱ı̌ г̱ıŋ̄ċı́lıń, Suг̩u Y̌ C̣ı̄ċıŋ́, Suг̩u Y̌ C̣ı̄ċıŋ́ 9, uě c̩uı ṡı̌s̈uṉ. Suěı̌... ṡın̖c̩ı̖ ṡˋ ın̄ye ṡˊc̣ıṉ, c̣uňг̱ı 1 2 3: + Lıŋ̬ г̤e lı̌г̱ı̖ ı̌s̈o, Suг̩u Y̌ C̣ı̄ċıŋ́ 9, lıŋ̬ г̤e lı̌г̱ı̖ ı̌s̈o, Suг̩u Y̌ C̣ı̄ċıŋ́ 9, lıŋ̬ г̤e lı̌г̱ı̖ ı̌s̈o, Suг̩u Y̌ C̣ı̄ċıŋ́ 9. + Г̱uıo̖ uŋ̖c̣ı, г̱uıo̖ cueг̤ue, ċy г̩ın̖ıŋ̌yn̖ г̈n̖ Suг̩u Y̌ C̣ı̄ċıŋ́ 9, ın̄uı́ s̄ı̄ċŋ̗ s̈o̬ г̩ın̖ıŋ̌, г̩uŋc̩ue s̄ı̄ċŋ̗ s̈o̬, ċaг̱uг̩uē ı̄ıŋ̖. Г̱ıŋ̄ċı́lıń, c̩ı̖c̣ın̖. -/ #eval convert "ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄩㄝˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。"