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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
module AufgabeFFP7
where
import Data.Char
import Data.List hiding ((\\), insert, delete)
import Test.QuickCheck
type Buffer = (Int, String)
-- the empty buffer
empty :: Buffer
empty = (0, "")
-- insert character before cursor
insert :: Char -> Buffer -> Buffer
insert c (cur, buf) = (min (length buf + 1) (max (cur + 1) 1), buf1 ++ [c] ++ buf2)
where
(buf1, buf2) = splitAt cur buf
-- delete character before cursor
delete :: Buffer -> Buffer
delete (cur, buf)
| buf2 == "" = (min cur (length buf1), buf1)
| cur < 0 = (0, buf)
| otherwise = (cur, buf1 ++ tail buf2)
where
(buf1, buf2) = splitAt cur buf
-- move cursor left one character
left :: Buffer -> Buffer
left (cur, buf) = (min (length buf) (max (cur - 1) 0), buf)
-- move cursor right one character
right :: Buffer -> Buffer
right (cur, buf) = (max 0 (min (cur + 1) (length buf)), buf)
-- is cursor at left end?
atLeft :: Buffer -> Bool
atLeft (cur, buf) = cur <= 0
-- is cursor at right end?
atRight :: Buffer -> Bool
atRight (cur, buf) = cur >= length buf
--------------------------------------------------------------------------------
type BufferI = (String, String)
-- the empty buffer
emptyI :: BufferI
emptyI = ("", "")
-- insert character before cursor
insertI :: Char -> BufferI -> BufferI
insertI c (beforeC, afterC) = ([c] ++ beforeC, afterC)
-- delete character before cursor
deleteI :: BufferI -> BufferI
deleteI (beforeC, "") = (beforeC, "")
deleteI (beforeC, c:afterC) = (beforeC, afterC)
-- move cursor left one character
leftI :: BufferI -> BufferI
leftI ("", afterC) = ("", afterC)
leftI (c:beforeC, afterC) = (beforeC, [c] ++ afterC)
-- move cursor right one character
rightI :: BufferI -> BufferI
rightI (beforeC, "") = (beforeC, "")
rightI (beforeC, c:afterC) = ([c] ++ beforeC, afterC)
-- is cursor at left end?
atLeftI :: BufferI -> Bool
atLeftI ("", _) = True
atLeftI (_, _) = False
-- is cursor at right end?
atRightI :: BufferI -> Bool
atRightI (_, "") = True
atRightI (_, _) = False
--------------------------------------------------------------------------------
retrieve :: BufferI -> Buffer
retrieve (beforeC, afterC) = (length beforeC, (reverse beforeC) ++ afterC)
--------------------------------------------------------------------------------
-- quickcheck Buffer == BufferI
bufEqual :: BufferI -> Buffer -> Bool
bufEqual bi b = (retrieve bi) == b
(<==>) = bufEqual
-- generator for equal data
genEqualBuf :: Gen(Buffer, BufferI)
genEqualBuf = do
s <- arbitrary
c <- choose (0, length s)
return ((c, s), revFst (splitAt c s))
where
revFst = \(a, b) -> (reverse a, b)
instance Arbitrary Char where
arbitrary = elements $ ['a'..'z'] ++ ['A'..'Z']
prop_empty :: Bool
prop_empty = emptyI <==> empty
-- naive insert test, will exhaust
--prop_insert :: BufferI -> Buffer -> Char -> Property
--prop_insert bi b c = bi <==> b
-- ==> insertI c bi <==> insert c b
prop_insert :: BufferI -> Char -> Bool
prop_insert bi c = insertI c bi <==> insert c (retrieve bi)
-- use equal data generator
prop_insert2 :: Char -> Property
prop_insert2 c = forAll (genEqualBuf) $ \(b, bi) ->
insertI c bi <==> insert c b
prop_delete :: BufferI -> Bool
prop_delete bi = deleteI bi <==> delete (retrieve bi)
prop_left :: BufferI -> Bool
prop_left bi = leftI bi <==> left (retrieve bi)
prop_right :: BufferI -> Bool
prop_right bi = rightI bi <==> right (retrieve bi)
prop_atLeft :: BufferI -> Bool
prop_atLeft bi = atLeftI bi == atLeft (retrieve bi)
prop_atRight :: BufferI -> Bool
prop_atRight bi = atRightI bi == atRight (retrieve bi)
--------------------------------------------------------------------------------
-- from slide 154
divideAndConquer :: (p -> Bool) -> (p -> s) -> (p -> [p]) -> (p -> [s] -> s) -> p -> s
divideAndConquer indiv solve divide combine initPb = dAC initPb
where
dAC pb
| indiv pb = solve pb
| otherwise = combine pb (map dAC (divide pb))
-- from slide 156
quickSort :: Ord a => [a] -> [a]
quickSort lst = divideAndConquer indiv solve divide combine lst
where
indiv ls = length ls <= 1
solve = id
divide (l:ls) = [[ x | x <- ls, x <= l], [ x | x <- ls, x > l] ]
combine (l:_) [l1,l2] = l1 ++ [l] ++ l2
removeDuplicates :: [Int] -> [Int]
removeDuplicates xs = nub xs
-- from slide 245
ssfn :: [Int] -> Int
ssfn xs = sap 0 (removeDuplicates (quickSort xs))
sap :: Int -> [Int] -> Int
sap n [] = n
sap n (x:xs)
| n /= x = n
| otherwise = sap (n + 1) xs
-- from slide 247
(\\) :: Eq a => [a] -> [a] -> [a]
xs \\ ys = filter (\x -> x `notElem` ys) xs
minfree :: [Int] -> Int
minfree xs = head ([0..] \\ xs)
--------------------------------------------------------------------------------
type Nat = [Int]
prop_ssfn_eq_minfree_a :: Nat -> Bool
prop_ssfn_eq_minfree_a xs = minfree pos == ssfn pos
where
pos = filter (>= 0) xs
prop_ssfn_eq_minfree_b :: Nat -> Property
prop_ssfn_eq_minfree_b xs = all (>= 0) xs
==> ssfn xs == minfree xs
|
