From 90af822547db26a15d37e89af4621dcb907045ee Mon Sep 17 00:00:00 2001 From: Inari Listenmaa Date: Fri, 3 Apr 2020 19:36:22 +0200 Subject: [PATCH] (Kor) Add Digits --- src/korean/NounKor.gf | 6 +++++- src/korean/NumeralKor.gf | 42 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 46 insertions(+), 2 deletions(-) diff --git a/src/korean/NounKor.gf b/src/korean/NounKor.gf index 272b004c..2765fddf 100644 --- a/src/korean/NounKor.gf +++ b/src/korean/NounKor.gf @@ -96,7 +96,11 @@ concrete NounKor of Noun = CatKor ** open ResKor, Prelude in { NumCard card = card ; -- : Digits -> Card ; - -- NumDigits dig = + NumDigits dig = baseNum ** { + s = \\_,_ => dig.s ! NCard ; + n = dig.n ; + numtype = IsDig + } ; -- : Numeral -> Card ; NumNumeral num = num ; diff --git a/src/korean/NumeralKor.gf b/src/korean/NumeralKor.gf index 31be00cc..ff1a04e6 100644 --- a/src/korean/NumeralKor.gf +++ b/src/korean/NumeralKor.gf @@ -84,7 +84,6 @@ lin -- : Sub1000 -> Sub1000 -> Sub1000000 ; -- m * 1000 + n pot3plus m n = TODO ; - oper LinDigit : Type = ResKor.Numeral ** {isTwo : Bool ; ten : Str} ; @@ -123,4 +122,45 @@ oper } ; TODO : ResKor.Numeral = mkNum2 "TODO" "TODO" ; + + +-- numerals as sequences of digits + +lincat + Dig = TDigit ; + +lin + -- : Dig -> Digits ; -- 8 + IDig d = d ; + + -- : Dig -> Digits -> Digits ; -- 876 + IIDig d i = { + s = \\o => d.s ! NCard ++ BIND ++ i.s ! o ; + n = Pl + } ; + + D_0 = mkDig "0" ; + D_1 = mk3Dig "1" "1번째" ResKor.Sg ; + D_2 = mkDig "2" ; + D_3 = mkDig "3" ; + D_4 = mkDig "4" ; + D_5 = mkDig "5" ; + D_6 = mkDig "6" ; + D_7 = mkDig "7" ; + D_8 = mkDig "8" ; + D_9 = mkDig "9" ; + +oper + mk2Dig : Str -> Str -> TDigit = \c,o -> mk3Dig c o ResKor.Pl ; + mkDig : Str -> TDigit = \c -> mk2Dig c (c + "번째") ; + + mk3Dig : Str -> Str -> ResKor.Number -> TDigit = \c,o,n -> { + s = table {NCard => c ; NOrd => o} ; + n = n + } ; + + TDigit = { + n : ResKor.Number ; + s : CardOrd => Str + } ; }