blob: 59b71a5e997248b68eda326ad6cda9ba2b42c624 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
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
-- ...
|
