Experimenting with transfer.

This commit is contained in:
aarne
2003-10-09 16:11:22 +00:00
parent 2ee936c7e2
commit ce253baf15
6 changed files with 173 additions and 1 deletions

View File

@@ -0,0 +1,41 @@
concrete Decimal of Numerals = open ResDecimal in {
flags lexer=chars ; unlexer=concat ;
lincat Sub100 = {s : Zeros => Str} ;
lincat Sub1000 = {s : Zeros => Str} ;
lincat Sub1000000 = {s : Zeros => Str} ;
lin num n = {s = n.s ! noz} ;
lin n2 = ss "2" ;
lin n3 = ss "3" ;
lin n4 = ss "4" ;
lin n5 = ss "5" ;
lin n6 = ss "6" ;
lin n7 = ss "7" ;
lin n8 = ss "8" ;
lin n9 = ss "9" ;
lin pot01 = ss "1" ;
lin pot0 d = d ;
lin pot110 = mkz ("1" ++ "0") ;
lin pot111 = mkz ("1" ++ "1") ;
lin pot1to19 d = mkz ("1" ++ d.s) ;
lin pot0as1 n = {s = table {noz => n.s ; zz => "0" ++ n.s}} ;
lin pot1 d = mkz (d.s ++ "0") ;
lin pot1plus d e = mkz (d.s ++ e.s) ;
lin pot1as2 n = {s = table {noz => n.s ! noz ; zz => "0" ++ n.s ! zz}} ;
lin pot2 d = mkz (d.s ++ "0" ++ "0") ;
lin pot2plus d e = mkz (d.s ++ e.s ! zz) ;
lin pot2as3 n = {s = table {noz => n.s ! noz ; zz => "0" ++ n.s ! zz}} ;
lin pot3 n = mkz (n.s ! noz ++ "0" ++ "0" ++ "0") ;
lin pot3plus n m = {s = table {z => n.s ! z ++ m.s ! zz}} ;
}

View File

@@ -0,0 +1,39 @@
include numerals.Abs.gf ;
param DForm = unit | teen | ten ;
lincat Digit = {s : DForm => Str} ;
lincat Sub10 = {s : DForm => Str} ;
oper mkNum : Str -> Str -> Str -> Lin Digit =
\two -> \twelve -> \twenty ->
{s = table {unit => two ; teen => twelve ; ten => twenty}} ;
oper regNum : Str -> Lin Digit =
\six -> mkNum six (six + "teen") (six + "ty") ;
oper ss : Str -> {s : Str} = \s -> {s = s} ;
lin num x = x ;
lin n2 = mkNum "two" "twelve" "twenty" ;
lin n3 = mkNum "three" "thirteen" "thirty" ;
lin n4 = mkNum "four" "fourteen" "forty" ;
lin n5 = mkNum "five" "fifteen" "fifty" ;
lin n6 = regNum "six" ;
lin n7 = regNum "seven" ;
lin n8 = mkNum "eight" "eighteen" "eighty" ;
lin n9 = regNum "nine" ;
lin pot01 = {s = table {f => "one"}} ;
lin pot0 d = {s = table {f => d.s ! f}} ;
lin pot110 = ss "ten" ;
lin pot111 = ss "eleven" ;
lin pot1to19 d = {s = d.s ! teen} ;
lin pot0as1 n = {s = n.s ! unit} ;
lin pot1 d = {s = d.s ! ten} ;
lin pot1plus d e = {s = d.s ! ten ++ "-" ++ e.s ! unit} ;
lin pot1as2 n = n ;
lin pot2 d = {s = d.s ! unit ++ "hundred"} ;
lin pot2plus d e = {s = d.s ! unit ++ "hundred" ++ "and" ++ e.s} ;
lin pot2as3 n = n ;
lin pot3 n = {s = n.s ++ "thousand"} ;
lin pot3plus n m = {s = n.s ++ "thousand" ++ m.s} ;

View File

@@ -1,7 +1,7 @@
-- Unary and binary natural numbers, and conversions between them. AR 8/10/2003
-- To be used as an example of transfer.
abstract Nat = {
abstract Nat = Numerals ** {
cat Nat ;
fun

View File

@@ -0,0 +1,45 @@
transfer Num2Bin : Numerals -> Nat = {
transfer Numeral = num2bin ;
fun num2bin : Numeral -> Bin ;
def num2bin n = num2nat (nat2bin n) ;
fun
num2nat : Numeral -> Nat ;
sub1000000_2nat : Sub1000000 -> Nat ;
sub1000_2nat : Sub1000 -> Nat ;
sub100_2nat : Sub100 -> Nat ;
sub10_2nat : Sub10 -> Nat ;
digit2nat : Digit -> Nat ;
def
num2nat (num n) = sub1000000_2nat n ;
---
sub1000000_2nat (pot2as3 n) = sub1000_2nat n ;
---
sub1000_2nat (pot1as2 n) = sub100_2nat n ;
---
sub100_2nat (pot0as1 n) = sub10_2nat n ;
sub100_2nat (pot1 d) = tenTimes (digit2nat d) ;
---
sub10_2nat (pot0 d) = digit2nat d ;
digit2nat n2 = Succ One ;
digit2nat n3 = Succ (digit2nat n2) ;
digit2nat n4 = Succ (digit2nat n3) ;
digit2nat n5 = Succ (digit2nat n4) ;
digit2nat n6 = Succ (digit2nat n5) ;
digit2nat n7 = Succ (digit2nat n6) ;
digit2nat n8 = Succ (digit2nat n7) ;
digit2nat n9 = Succ (digit2nat n8) ;
fun
tenTimes : Nat -> Nat ;
tenPlus, ninePlus : Nat -> Nat ;
def
tenTimes One = ninePlus One ; -- the price to pay for starting from One
tenTimes (Succ n) = tenPlus (tenTimes n) ;
tenPlus n = Succ (ninePlus n) ;
ninePlus n = Succ (double (double (double One))) ;
}

View File

@@ -0,0 +1,40 @@
-- numerals from 1 to 999999 in decimal notation. AR 1998 -- 2003
abstract Numerals = {
flags startcat=Numeral ;
cat
Numeral ; -- 0..
Digit ; -- 2..9
Sub10 ; -- 1..9
Sub100 ; -- 1..99
Sub1000 ; -- 1..999
Sub1000000 ; -- 1..999999
fun
num : Sub1000000 -> Numeral ;
n2, n3, n4, n5, n6, n7, n8, n9 : Digit ;
pot01 : Sub10 ; -- 1
pot0 : Digit -> Sub10 ; -- d * 1
pot110 : Sub100 ; -- 10
pot111 : Sub100 ; -- 11
pot1to19 : Digit -> Sub100 ; -- 10 + d
pot0as1 : Sub10 -> Sub100 ; -- coercion of 1..9
pot1 : Digit -> Sub100 ; -- d * 10
pot1plus : Digit -> Sub10 -> Sub100 ; -- d * 10 + n
pot1as2 : Sub100 -> Sub1000 ; -- coercion of 1..99
pot2 : Sub10 -> Sub1000 ; -- m * 100
pot2plus : Sub10 -> Sub100 -> Sub1000 ; -- m * 100 + n
pot2as3 : Sub1000 -> Sub1000000 ; -- coercion of 1..999
pot3 : Sub1000 -> Sub1000000 ; -- m * 1000
pot3plus : Sub1000 -> Sub1000 -> Sub1000000 ; -- m * 1000 + n
data
Numeral = num ;
Digit = n2 | n3 | n4 | n5 | n6 | n7 | n8 | n9 ;
Sub10 = pot01 | pot0 ;
Sub100 = pot110 | pot111 | pot1to19 | pot0as1 | pot1 | pot1plus ;
}

View File

@@ -0,0 +1,7 @@
resource ResDecimal = {
param Zeros = noz | zz ;
oper ss : Str -> {s : Str} = \s -> {s = s} ;
oper mkz : Str -> {s : Zeros => Str} = \s -> {s = table {_ => s}} ;
}