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