mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-13 06:49:31 -06:00
92 lines
3.6 KiB
Plaintext
92 lines
3.6 KiB
Plaintext
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 d) = nd10 d ;
|
|
nd100 pot110 = IIDig D_1 (IDig D_0) ;
|
|
nd100 pot111 = IIDig D_1 (IDig D_1) ;
|
|
nd100 (pot1to19 d) = IIDig D_1 (IDig (nd d)) ;
|
|
nd100 (pot1 d) = IIDig (nd d) (IDig D_0) ;
|
|
nd100 (pot1plus d x) = IIDig (nd d) (nd10 x) ;
|
|
|
|
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 d) ys = IIDig d ys ;
|
|
dconcat (IIDig d xs) ys = IIDig d (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 ;
|
|
|
|
} |