Silly writing system experiments

Changes

1 changed files (+149/-0)

• WritingSystem.lean (new)
  • @@ -0,0 +1,149 @@
    + 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 .o + | 'ㄜ' => some <| .medial .o + | 'ㄝ' => 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 => "μ" + | .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̄o̊̌ Ċ̣uŋꞇ̣̄uó, s̈ın̊̀c̣ı̊̀ uǒ ıǒ ꞇ̣̓ıŋc̈ı́lıń, uǒ s̄ň s̈ı̌s̄un̊ ꞇ̣̓ıŋc̈ı́lıń, ꞇ̣n̊̀ṡ̀, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9, ꞇ̣̓ı̌ ꞇ̣̓ıŋc̈ı́lıń, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9, uǒ c̣uı̀ s̈ı̌s̄un̊. Suǒ ı̌... s̈ın̊̀c̣ı̊̀ ṡ̀ ınlò ṡ́c̣̈ın̊, ċ̣uňꞇ̣̓ı̀ 1 2 3, + Lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9, lıŋ̊̌ ꞇ̣̄ò lı̌ꞇ̣̓ı̊̀ ı̌s̄ò, Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9. + Ꞇ̣̓ùıo̊̀ uŋ̊̀c̣̈ı̀, ꞇ̣̓ùıo̊̀ cuòꞇ̣̄uò, c̈μ̀ ꞇ̣ın̊̀ıŋ̌μn̊̀ ꞇ̄n̊̀ Sùꞇ̣ù Μ̌ C̣̈ıc̈ıŋ́ 9, ınuı́ s̓ıċŋ̊́ s̄o̊̌ ꞇ̣ın̊̀ıŋ̌, ꞇ̣uŋ̀c̣uò s̓ıċŋ̊́ s̄o̊̌, ċàꞇ̣̓ùꞇ̣uo ııŋ̊̀. Ꞇ̣̓ıŋc̈ı́lıń, c̣ı̊̀c̣̈ın̊̀. + -/ + + #eval convert "ㄗㄠˇ ㄕㄤˋ ㄏㄠˇ ㄓㄨㄥ ㄍㄨㄛˊ ， ㄒㄧㄢˋ ㄗㄞˋ ㄨㄛˇ ㄧㄡˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄨㄛˇ ㄏㄣˇ ㄒㄧˇ ㄏㄨㄢ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄉㄢˋ ㄕˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄅㄧˇ ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄨㄛˇ ㄗㄨㄟˋ ㄒㄧˇ ㄏㄨㄢ 。 ㄙㄨㄛˇ ㄧˇ … ㄒㄧㄢˋ ㄗㄞˋ ㄕˋ ㄧㄣ ㄌㄜˋ ㄕˊ ㄐㄧㄢ ， ㄓㄨㄣˇ ㄅㄟˋ 1 2 3， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄌㄧㄤˇ ㄍㄜˋ ㄌㄧˇ ㄅㄞˋ ㄧˇ ㄏㄡˋ ， ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9。 ㄅㄨˋ ㄧㄠˋ ㄨㄤˋ ㄐㄧˋ ， ㄅㄨˋ ㄧㄠˋ ㄘㄨㄛˋ ㄍㄨㄛˋ ， ㄑㄩˋ ㄉㄧㄢˋ ㄧㄥˇ ㄩㄢˋ ㄎㄢˋ ㄙㄨˋ ㄉㄨˋ ㄩˇ ㄐㄧ ㄑㄧㄥˊ 9， ㄧㄣ ㄨㄟˊ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ㄉㄧㄢˋ ㄧㄥˇ ， ㄉㄨㄥˋ ㄗㄨㄛˋ ㄈㄟ ㄔㄤˊ ㄏㄠˇ ， ㄔㄚˋ ㄅㄨˋ ㄉㄨㄛ ㄧ ㄧㄤˋ 。 ㄅㄧㄥ ㄑㄧˊ ㄌㄧㄣˊ ， ㄗㄞˋ ㄐㄧㄢˋ 。 "