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
|
module AufgabeFFP7
where
import Data.Char
import Data.List hiding ((\\), insert)
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
--TODO deleteI :: BufferI -> BufferI
-- move cursor left one character
leftI :: BufferI -> BufferI
leftI ([], afterC) = ([], afterC)
leftI (last:beforeC, afterC) = (beforeC, [last] ++ afterC)
-- move cursor right one character
--TODO rightI :: BufferI -> BufferI
-- 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
-- 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']
-- naive insert test, will exhaust
prop_insert :: BufferI -> Buffer -> Char -> Property
prop_insert bi b c = bufEqual bi b
==> bufEqual (insertI c bi) (insert c b)
-- use equal data generator
prop_insert2 :: Char -> Property
prop_insert2 c =
forAll (genEqualBuf) $ \(b, bi) -> bufEqual (insertI c bi) (insert c b)
--------------------------------------------------------------------------------
-- 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
|
