|
25
|
1 module SetPairList(Set, empty, insert, isin, size, union, delete) where |
|
23
|
2 |
|
|
3 -- Abstraction function |
|
|
4 {- |
|
25
|
5 alpha :: Set a -> {a} |
|
|
6 alpha (S []) = {} |
|
|
7 alpha (S ((a, b):xs)) = {a..b} union (alpha xs) |
|
23
|
8 |
|
|
9 To show: (10 things) |
|
25
|
10 alpha empty = {} |
|
|
11 invar s ==> alpha (insert x s) = {x} union alpha s |
|
|
12 invar s ==> alpha (delete x s) = alpha s \ {x} |
|
|
13 invar s ==> isin x s = x \in alpha s |
|
|
14 invar s ==> size s = |alpha s| |
|
|
15 invar s1, invar s2 ==> alpha (union s1 s2) = (alpha s1) union (alpha s2) |
|
|
16 |
|
|
17 invar empty |
|
|
18 invar s ==> invar (insert x s) |
|
|
19 invar s ==> invar(delete x s) |
|
|
20 invar s1, invar s2 ==> invar (union s1 s2) |
|
23
|
21 -} |
|
|
22 |
|
|
23 -- Interface |
|
25
|
24 newtype Set a = S (PairList a) |
|
23
|
25 |
|
|
26 invar :: Integral a => Set a -> Bool |
|
25
|
27 invar (S s) = invarPL s |
|
23
|
28 |
|
|
29 empty :: Set a |
|
25
|
30 empty = S emptyPL |
|
23
|
31 |
|
|
32 insert :: Integral a => a -> Set a -> Set a |
|
25
|
33 insert n (S s) = S (insertPL n s) |
|
23
|
34 |
|
|
35 isin :: Integral a => a -> Set a -> Bool |
|
25
|
36 isin n (S s) = isinPL n s |
|
23
|
37 |
|
|
38 size :: Integral a => Set a -> Integer |
|
25
|
39 size (S s) = sizePL s |
|
23
|
40 |
|
|
41 union :: Integral a => Set a -> Set a -> Set a |
|
25
|
42 union (S s1) (S s2) = S (unionPL s1 s2) |
|
23
|
43 |
|
|
44 delete :: Integral a => a -> Set a -> Set a |
|
25
|
45 delete n (S s) = S (deletePL n s) |
|
23
|
46 |
|
|
47 -- Implementation |
|
|
48 type PairList a = [(a, a)] |
|
|
49 |
|
|
50 invarPL :: Integral a => PairList a -> Bool |
|
|
51 invarPL [] = True |
|
|
52 invarPL [(m,n)] = m <= n |
|
|
53 invarPL ((m1,n1):(m2,n2):ms) = |
|
|
54 m1 <= n1 && n1 + 1 < m2 && invarPL ((m2,n2):ms) |
|
|
55 |
|
|
56 emptyPL :: PairList a |
|
|
57 emptyPL = [] |
|
|
58 |
|
|
59 insertPL :: Integral a => a -> PairList a -> PairList a |
|
|
60 insertPL n [] = [(n,n)] |
|
|
61 insertPL n ((k1,l1) : (k2,l2) : ks) |
|
|
62 | l1 + 1 == n && n + 1 == k2 = (k1,l2) : ks |
|
|
63 insertPL n ((k,l) : ks) |
|
|
64 | n + 1 == k = (n,l) : ks |
|
|
65 | n < k = (n,n) : (k,l) : ks |
|
|
66 | k <= n && n <= l = (k,l) : ks |
|
|
67 | l + 1 == n = (k,n) : ks |
|
|
68 | otherwise = (k,l) : insertPL n ks |
|
|
69 |
|
|
70 isinPL :: Ord a => a -> PairList a -> Bool |
|
|
71 isinPL n = any (\(k,l) -> k <= n && n <= l) |
|
|
72 |
|
|
73 sizePL :: Integral a => PairList a -> Integer |
|
|
74 sizePL [] = 0 |
|
|
75 sizePL ((k,l) : s) = toInteger (l - k + 1) + sizePL s |
|
|
76 |
|
|
77 unionPL :: Integral a => PairList a -> PairList a -> PairList a |
|
|
78 unionPL [] ls = ls |
|
|
79 unionPL ks [] = ks |
|
|
80 unionPL ((k1,l1):ks) ((k2,l2):ls) = |
|
|
81 if k1 <= k2 |
|
|
82 then if l1 + 1 < k2 then (k1,l1) : unionPL ks ((k2, l2):ls) |
|
|
83 else if l1 <= l2 then unionPL ks ((k1,l2):ls) |
|
|
84 else {- l1 > l2 -} unionPL ((k1,l1):ks) ls |
|
|
85 else if k1 <= l2 + 1 |
|
|
86 then if l1 <= l2 then unionPL ks ((k2,l2):ls) |
|
|
87 else {- l1 > l2 -} unionPL ((k2,l1):ks) ls |
|
|
88 else (k2,l2) : unionPL ((k1,l1):ks) ls |
|
|
89 |
|
|
90 deletePL :: Integral a => a -> PairList a -> PairList a |
|
|
91 deletePL n [] = [] |
|
|
92 deletePL n ((k,l) : ks) |
|
|
93 | n < k = (k,l) : ks |
|
|
94 | n == k = if k < l then (k+1,l) : ks else ks |
|
|
95 | k < n && n < l = (k,n-1) : (n+1,l) : ks |
|
|
96 | n == l = if k < l then (k,l-1) : ks else ks |
|
|
97 | otherwise = (k,l) : deletePL n ks |
|
|
98 |
