diff --git a/transfer/TODO b/transfer/TODO index f53ffab18..d3a78d49d 100644 --- a/transfer/TODO +++ b/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 diff --git a/transfer/lib/array.tra b/transfer/lib/array.tra deleted file mode 100644 index e91fe35e7..000000000 --- a/transfer/lib/array.tra +++ /dev/null @@ -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) diff --git a/transfer/lib/bintree.tra b/transfer/lib/bintree.tra new file mode 100644 index 000000000..0dd21f184 --- /dev/null +++ b/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 + diff --git a/transfer/lib/collection.tra b/transfer/lib/collection.tra new file mode 100644 index 000000000..59b71a5e9 --- /dev/null +++ b/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 + -- ... diff --git a/transfer/lib/vector.tra b/transfer/lib/vector.tra new file mode 100644 index 000000000..2eda35167 --- /dev/null +++ b/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)