Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension.

1 files changed, 94 insertions, 0 deletions

diff --git a/transfer/examples/numerals.tra b/transfer/examples/numerals.tra
new file mode 100644
index 000000000..31bac33ac
--- /dev/null
+++ b/transfer/examples/numerals.tra
@@ -0,0 +1,94 @@
+import prelude
+
+data Cat : Type where {
+  Digit : Cat ;
+  Numeral : Cat ;
+  Sub10 : Cat ;
+  Sub100 : Cat ;
+  Sub1000 : Cat ;
+  Sub1000000 : Cat
+} ;
+
+data Tree : (_ : Cat)-> Type where {
+  n2 : Tree Digit ;
+  n3 : Tree Digit ;
+  n4 : Tree Digit ;
+  n5 : Tree Digit ;
+  n6 : Tree Digit ;
+  n7 : Tree Digit ;
+  n8 : Tree Digit ;
+  n9 : Tree Digit ;
+  num : (_ : Tree Sub1000000)-> Tree Numeral ;
+  pot0 : (_ : Tree Digit)-> Tree Sub10 ;
+  pot01 : Tree Sub10 ;
+  pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ;
+  pot1 : (_ : Tree Digit)-> Tree Sub100 ;
+  pot110 : Tree Sub100 ;
+  pot111 : Tree Sub100 ;
+  pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ;
+  pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ;
+  pot1to19 : (_ : Tree Digit)-> Tree Sub100 ;
+  pot2 : (_ : Tree Sub10)-> Tree Sub1000 ;
+  pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
+  pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ;
+  pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
+  pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000
+}
+
+derive Compos Tree
+
+
+data Binary_Cat : Type where {
+  Bin : Binary_Cat
+} ;
+data Binary_Tree : (_ : Binary_Cat)-> Type where {
+  End : Binary_Tree Bin ;
+  One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ;
+  Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin
+}
+
+
+
+monoid_plus_Int : Monoid Integer
+monoid_plus_Int = rec mzero = 0
+		      mplus = (\x -> \y -> x + y)
+
+
+num2int : Tree Numeral -> Integer
+num2int = tree2int ?
+
+tree2int : (C : Cat) -> Tree C -> Integer 
+tree2int _ n = case n of
+		n2 -> 2
+		n3 -> 3
+		n4 -> 4
+		n5 -> 5
+		n6 -> 6
+		n7 -> 7
+		n8 -> 8
+		n9 -> 9
+		pot01 -> 1
+		pot1 x -> 10 * tree2int ? x
+		pot110 -> 10
+		pot111 -> 11
+		pot1plus x y -> 10 * tree2int ? x + tree2int ? y
+		pot1to19 x -> 10 + tree2int ? x
+		pot2 x -> 100 * tree2int ? x
+		pot2as3 x -> 10 * tree2int ? x
+		pot2plus x y -> 100 * tree2int ? x + tree2int ? y
+		pot3 x -> 1000 * tree2int ? x
+		pot3plus x y -> 1000 * tree2int ? x + tree2int ? y
+                _ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n
+
+int2bin : Integer -> Binary_Tree Bin
+int2bin = int2bin_ End
+
+int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin
+int2bin_ b 0 = b
+int2bin_ b n = let d : Integer = if n % 2 == 0 then Zero else One
+		   q : Integer = n / 2
+                in int2bin_ (d b) q
+
+num2bin : Tree Numeral -> Binary_Tree Bin
+num2bin n = int2bin (num2int n)
+