msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

added transfer module for Numeral to Digits and back

Browse Source
This commit is contained in:
krasimir
2009-09-17 14:35:19 +00:00
parent 45bfba4103
commit d9365c6cf0
3 changed files with 99 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
lib/src/abstract/Grammar.gf
View File

@@ -10,6 +10,7 @@ abstract Grammar =
Adjective,
Adverb,
Numeral,
NumeralTransfer,
Sentence,
Question,
Relative,

14
lib/src/abstract/Numeral.gf
View File

@@ -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 ;
}

91
lib/src/abstract/NumeralTransfer.gf Normal file
View File

@@ -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 ;
}