3 files changed, 113 insertions, 0 deletions
diff --git a/grammars/numerals/Nat.gf b/grammars/numerals/Nat.gf
new file mode 100644
index 000000000..6209eb216
--- /dev/null
+++ b/grammars/numerals/Nat.gf
@@ -0,0 +1,55 @@
+-- Unary and binary natural numbers, and conversions between them. AR 8/10/2003
+-- To be used as an example of transfer.
+
+abstract Nat = {
+
+  cat Nat ;
+  fun 
+    One : Nat ;              -- 1
+    Succ : Nat -> Nat ;      -- n'
+  data Nat = One | Succ ;
+
+  cat Bin ; 
+  fun 
+    BOne   : Bin ;           -- 1
+    BX     : Bin -> Bin ;    -- b 0
+    BXPlus : Bin -> Bin ;    -- b 1
+  data Bin = BOne | BX | BXPlus ;
+
+  fun succ : Bin -> Bin ;
+  def
+    succ BOne = BX BOne ;
+    succ (BX b) = BXPlus b ;
+    succ (BXPlus BOne) = BX (BX BOne) ;
+    succ b = succAux b (lastZero b) ;
+
+  fun lastZero : Bin -> Nat ;
+  def
+    lastZero (BX _) = One ;
+    lastZero (BXPlus b) = Succ (lastZero b) ;
+
+  fun succAux : Bin -> Nat -> Bin ;
+  def
+    succAux (BXPlus b) One = BX (succ b) ;
+    succAux (BXPlus b) (Succ n) = BX (succAux b n) ;
+    succAux b _ = succ b ;
+
+  -- this is the transfer function
+  fun nat2bin : Nat -> Bin ;
+  def
+    nat2bin One = BOne ;
+    nat2bin (Succ n) = succ (nat2bin n) ;
+
+  -- and the other way round
+  fun bin2nat : Bin -> Nat ;
+  def 
+    bin2nat BOne = One ;
+    bin2nat (BX b) = double (bin2nat b) ;
+    bin2nat (BXPlus b) = Succ (double (bin2nat b)) ;
+
+  fun double : Nat -> Nat ;
+  def  
+    double One = Succ One ;
+    double (Succ n) = Succ (Succ (double n)) ;
+
+}
diff --git a/grammars/numerals/Nat.hs b/grammars/numerals/Nat.hs
new file mode 100644
index 000000000..73bc406ba
--- /dev/null
+++ b/grammars/numerals/Nat.hs
@@ -0,0 +1,46 @@
+module Nat where
+
+-- testing transfer from unary to binary, for Nat.gf. AR 8/10/2003
+
+data Nat = One | Succ Nat deriving Show
+
+data Bin = BOne | BX Bin | BXPlus Bin deriving Show
+
+succBin:: Bin -> Bin
+succBin BOne = BX BOne
+succBin (BX b) = BXPlus b
+succBin (BXPlus BOne) = BX (BX BOne) 
+succBin b = succAux b (lastZero b)
+
+lastZero :: Bin -> Nat
+lastZero (BX _) = One
+lastZero (BXPlus b) = Succ (lastZero b)
+
+succAux :: Bin -> Nat -> Bin
+succAux (BXPlus b) One = BX (succBin b)
+succAux (BXPlus b) (Succ n) = BX (succAux b n)
+succAux b _ = succBin b
+
+int2bin :: Int -> Bin
+int2bin 1 = BOne
+int2bin n = succBin (int2bin (n-1))
+
+bin2nat :: Bin -> Nat
+bin2nat BOne = One
+bin2nat (BX b) = double (bin2nat b) 
+bin2nat (BXPlus b) = Succ (double (bin2nat b))
+
+double :: Nat -> Nat
+double One = Succ One
+double (Succ n) = Succ (Succ (double n))
+
+
+-- to test
+
+prBin :: Bin -> String
+prBin BOne = "1"
+prBin (BX b) = prBin b ++ "0"
+prBin (BXPlus b) = prBin b ++ "1"
+
+test  = map (prBin . int2bin) [1..16]
+test2 = map (bin2nat . int2bin) [1..16]
diff --git a/grammars/numerals/Symb.gf b/grammars/numerals/Symb.gf
new file mode 100644
index 000000000..0648b778f
--- /dev/null
+++ b/grammars/numerals/Symb.gf
@@ -0,0 +1,12 @@
+concrete Symb of Nat = open Prelude in {
+  lincat Nat, Bin = SS ;
+
+  lin 
+    One = ss "1" ;
+    Succ = postfixSS "'" ;
+
+    BOne = ss "1" ;
+    BX = postfixSS "0" ;
+    BXPlus = postfixSS "1" ;
+}
+