From eacb437f437bc79650708af472b7796c7fd041e5 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 20 Mar 2006 14:46:47 +0000 Subject: Expermintation woth a collections framework for transfer. --- transfer/lib/collection.tra | 77 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 transfer/lib/collection.tra (limited to 'transfer/lib/collection.tra') 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 + -- ... -- cgit v1.2.3