diff --git a/lib/src/abstract/Grammar.gf b/lib/src/abstract/Grammar.gf index a1edd59df..2e1528444 100644 --- a/lib/src/abstract/Grammar.gf +++ b/lib/src/abstract/Grammar.gf @@ -10,6 +10,7 @@ abstract Grammar = Adjective, Adverb, Numeral, + NumeralTransfer, Sentence, Question, Relative, diff --git a/lib/src/abstract/Numeral.gf b/lib/src/abstract/Numeral.gf index 43c6f8111..aaeb7a378 100644 --- a/lib/src/abstract/Numeral.gf +++ b/lib/src/abstract/Numeral.gf @@ -26,7 +26,7 @@ cat Sub1000 ; -- 1..999 Sub1000000 ; -- 1..999999 -fun +data num : Sub1000000 -> Numeral ; n2, n3, n4, n5, n6, n7, n8, n9 : Digit ; @@ -48,13 +48,13 @@ fun -- Numerals as sequences of digits have a separate, simpler grammar - cat - Dig ; -- single digit 0..9 +cat + Dig ; -- single digit 0..9 - fun - IDig : Dig -> Digits ; -- 8 - IIDig : Dig -> Digits -> Digits ; -- 876 +data + IDig : Dig -> Digits ; -- 8 + IIDig : Dig -> Digits -> Digits ; -- 876 - D_0, D_1, D_2, D_3, D_4, D_5, D_6, D_7, D_8, D_9 : Dig ; + D_0, D_1, D_2, D_3, D_4, D_5, D_6, D_7, D_8, D_9 : Dig ; } diff --git a/lib/src/abstract/NumeralTransfer.gf b/lib/src/abstract/NumeralTransfer.gf new file mode 100644 index 000000000..1818e0707 --- /dev/null +++ b/lib/src/abstract/NumeralTransfer.gf @@ -0,0 +1,91 @@ +abstract NumeralTransfer = Numeral ** { + +fun digits2num : Digits -> Numeral ; +def digits2num (IDig d1) = num (pot2as3 (pot1as2 (pot0as1 (dn10 d1)))) ; + digits2num (IIDig d2 (IDig d1)) = num (pot2as3 (pot1as2 (dn100 d2 d1))) ; + digits2num (IIDig d3 (IIDig d2 (IDig d1))) = num (pot2as3 (dn1000 d3 d2 d1)) ; + digits2num (IIDig d4 (IIDig d3 (IIDig d2 (IDig d1)))) = num (dn1000000a d4 d3 d2 d1) ; + digits2num (IIDig d5 (IIDig d4 (IIDig d3 (IIDig d2 (IDig d1))))) = num (dn1000000b d5 d4 d3 d2 d1) ; + digits2num (IIDig d6 ((IIDig d5 (IIDig d4 (IIDig d3 (IIDig d2 (IDig d1))))))) = num (dn1000000c d6 d5 d4 d3 d2 d1) ; + +fun num2digits : Numeral -> Digits ; +def num2digits (num x) = nd1000000 x ; + +fun dn10 : Dig -> Sub10 ; +def dn10 D_1 = pot01 ; + dn10 d1 = pot0 (dn d1) ; + +fun dn100 : Dig -> Dig -> Sub100 ; +def dn100 D_0 d1 = pot0as1 (dn10 d1) ; + dn100 D_1 D_0 = pot110 ; + dn100 D_1 D_1 = pot111 ; + dn100 D_1 d1 = pot1to19 (dn d1) ; + dn100 d2 D_0 = pot1 (dn d2) ; + dn100 d2 d1 = pot1plus (dn d2) (dn10 d1) ; + +fun dn1000 : Dig -> Dig -> Dig -> Sub1000 ; +def dn1000 D_0 d2 d1 = pot1as2 (dn100 d2 d1) ; + dn1000 d3 D_0 D_0 = pot2 (dn10 d3) ; + dn1000 d3 d2 d1 = pot2plus (dn10 d3) (dn100 d2 d1) ; + +fun dn1000000a : Dig -> Dig -> Dig -> Dig -> Sub1000000 ; +def dn1000000a D_0 d3 d2 d1 = pot2as3 (dn1000 d3 d2 d1) ; + dn1000000a d4 D_0 D_0 D_0 = pot3 (pot1as2 (pot0as1 (dn10 d4))) ; + dn1000000a d4 d3 d2 d1 = pot3plus (pot1as2 (pot0as1 (dn10 d4))) (dn1000 d3 d2 d1) ; + +fun dn1000000b : Dig -> Dig -> Dig -> Dig -> Dig -> Sub1000000 ; +def dn1000000b D_0 d4 d3 d2 d1 = dn1000000a d4 d3 d2 d1 ; + dn1000000b d5 d4 D_0 D_0 D_0 = pot3 (pot1as2 (dn100 d5 d4)) ; + dn1000000b d5 d4 d3 d2 d1 = pot3plus (pot1as2 (dn100 d5 d4)) (dn1000 d3 d2 d1) ; + +fun dn1000000c : Dig -> Dig -> Dig -> Dig -> Dig -> Dig -> Sub1000000 ; +def dn1000000c D_0 d5 d4 d3 d2 d1 = dn1000000b d5 d4 d3 d2 d1 ; + dn1000000c d6 d5 d4 D_0 D_0 D_0 = pot3 (dn1000 d6 d5 d4) ; + dn1000000c d6 d5 d4 d3 d2 d1 = pot3plus (dn1000 d6 d5 d4) (dn1000 d3 d2 d1) ; + +fun dn : Dig -> Digit ; +def dn D_2 = n2 ; + dn D_3 = n3 ; + dn D_4 = n4 ; + dn D_5 = n5 ; + dn D_6 = n6 ; + dn D_7 = n7 ; + dn D_8 = n8 ; + dn D_9 = n9 ; + +fun nd10 : Sub10 -> Digits ; +def nd10 pot01 = IDig D_1 ; + nd10 (pot0 d1) = IDig (nd d1) ; + +fun nd100 : Sub100 -> Digits ; +def nd100 (pot0as1 dn10) = nd10 dn10 ; + nd100 pot110 = IIDig D_1 (IDig D_0) ; + nd100 pot111 = IIDig D_1 (IDig D_1) ; + nd100 (pot1to19 dn10) = IIDig D_1 (IDig (nd dn10)) ; + nd100 (pot1 dn10) = IIDig (nd dn10) (IDig D_0) ; + +fun nd1000 : Sub1000 -> Digits ; +def nd1000 (pot1as2 x) = nd100 x ; + nd1000 (pot2 x) = dconcat (nd10 x) (IIDig D_0 (IDig D_0)) ; + nd1000 (pot2plus x y) = dconcat (nd10 x) (nd100 y) ; + +fun nd1000000 : Sub1000000 -> Digits ; +def nd1000000 (pot2as3 x) = nd1000 x ; + nd1000000 (pot3 x) = dconcat (nd1000 x) (IIDig D_0 (IIDig D_0 (IDig D_0))) ; + nd1000000 (pot3plus x y) = dconcat (nd1000 x) (nd1000 y) ; + +fun dconcat : Digits -> Digits -> Digits ; +def dconcat (IDig dn10) ys = IIDig dn10 ys ; + dconcat (IIDig dn10 xs) ys = IIDig dn10 (dconcat xs ys) ; + +fun nd : Digit -> Dig ; +def nd n2 = D_2 ; + nd n3 = D_3 ; + nd n4 = D_4 ; + nd n5 = D_5 ; + nd n6 = D_6 ; + nd n7 = D_7 ; + nd n8 = D_8 ; + nd n9 = D_9 ; + +} \ No newline at end of file