Expermintation woth a collections framework for transfer.

transfer/TODO

@@ -20,14 +20,30 @@
 
 * Improve the core language
 
+* Add primitive types operations to core
+
+- add Char type, with primitive operations:
+  - Enum stuff
+
+- add more primitive operations on strings:
+  - make list an isntance of the collection class for strings
+
+* Add more libraries
+
+- Enum class
+
+- Bounded class
+
+- list functions
+
+- a map structure
+
+- collections framework?
+
+- state monad
+
 * Improve compilation
 
-* Add primitive operations to core
-
-- primitive operations on strings:
-
-- add floating-point numbers with primitive oeprations?
-
 * Implement module system in interpreter
 
 * Add type checker for core

transfer/lib/array.tra

@@ -1,9 +0,0 @@
-import nat
-
-data Array : Type -> Nat -> Type where
-   Empty : (A:Type) -> Array A Zero
-   Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n)
-
-mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n
-mapA A B _ f (Empty _) = Empty B
-mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs)

transfer/lib/bintree.tra

@@ -0,0 +1,22 @@
+-- NOTE: this is unfinished and untested
+
+import prelude
+
+data BinTree : Type -> Type where
+	Leaf : (A:Type) -> BinTree A
+	Node : (A:Type) -> BinTree A -> A -> BinTree A -> BinTree A
+
+contains : (A:Type) -> Ord A -> A -> BinTree A -> Bool
+contains _ _ _ (Leaf _) = False
+contains A o x (Node _ l y r) 
+	| x < y = contains A o x l
+	| x > y = contains A o x r
+	| otherwise = True
+
+insert : (A:Type) -> Ord A -> A -> BinTree A -> BinTree A
+insert A o x (Leaf _) = Node A (Leaf A) x (Leaf A)
+insert A o x (Node _ l y r) 
+	| x < y = Node A (insert A o x l) y r
+	| x > y = Node A l y (insert A o x r)
+	| otherwise = Node A l x r
+

transfer/lib/collection.tra

@@ -0,0 +1,77 @@
+-- NOTE: this is unfinished and untested
+
+import prelude
+import bintree
+
+Collection : Type -> Type
+Collection C = 
+  sig 
+	-- types
+	Elem : Type
+	-- Add stuff
+	zero : C
+        plus : C -> C -> C
+	-- Collection-specific stuff
+        size : C -> Integer
+	add : Elem -> C -> C
+	elem : Elem -> C -> Bool
+        map : (Elem -> Elem) -> C -> C
+        filter : (Elem -> Bool) -> C -> C
+        fromList : List Elem -> C
+        toList : C -> List Elem
+
+
+--
+-- Collection String instance
+--
+
+collection_String : Collection String
+collection_String =
+  rec
+	Elem = Char
+	zero = ""
+	plus = prim_add_String
+	size = prim_length_String
+	-- ...
+
+
+--
+-- Collection List instance
+--
+
+collection_List : (A : Type) -> Collection (List A)
+collection_List A = 
+  rec
+	Elem = A
+	zero = Nil A
+	plus = append A
+	size = length A
+	add  = Cons A
+	-- ...
+
+--
+-- Collection Vector instance
+--
+
+collection_Vector : (A : Type) -> (n : Nat) -> Collection (Vector A n)
+collection_Vector A n = 
+  rec
+	Elem = A
+	zero = Empty A
+	plus = appendV A n n -- FIXME: this only works for vectors of the same length!
+	-- ...
+
+
+--
+-- Collection BinTree instance
+--
+
+collection_BinTree : (A : Type) -> Ord A -> Collection (BinTree A)
+collection_BinTree A o = 
+  rec
+	Elem = A
+	zero = Nil A
+	plus = merge A o
+	size = sizeBT A
+	add  = insert A o
+	-- ...

transfer/lib/vector.tra

@@ -0,0 +1,15 @@
+-- NOTE: this is unfinished and untested
+
+import nat
+
+data Vector : Type -> Nat -> Type where
+   Empty : (A:Type) -> Vector A Zero
+   Cell : (A:Type) -> (n:Nat) -> A -> Vector A n -> Vector A (Succ n)
+
+mapV : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Vector A n -> Vector B n
+mapV A B _ f (Empty _) = Empty B
+mapV A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapV A B n f xs)
+
+appendV : (A:Type) -> (n:Nat) -> (m:Nat) -> Vector A n -> Vector A m -> Vector A (plusNat n m)
+appendV A _ _ (Empty _) ys = ys
+appendV A (Succ n) m (Cell _ _ x xs) ys = appendV A n (Succ m) xs (Cell A m x ys)