equal
deleted
inserted
replaced
5 |
5 |
6 Quicksort |
6 Quicksort |
7 *) |
7 *) |
8 |
8 |
9 Qsort = Sorting + |
9 Qsort = Sorting + |
|
10 |
|
11 (*Version one: higher-order*) |
10 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
12 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
11 |
13 |
12 recdef qsort "measure (size o snd)" |
14 recdef qsort "measure (size o snd)" |
13 simpset "simpset() addsimps [length_filter RS le_less_trans]" |
15 simpset "simpset() addsimps [length_filter RS le_less_trans]" |
14 |
16 |
15 "qsort(le, []) = []" |
17 "qsort(le, []) = []" |
16 |
18 |
17 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
19 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
18 @ (x # qsort(le, [y:xs . le x y]))" |
20 @ (x # qsort(le, [y:xs . le x y]))" |
19 |
21 |
|
22 |
|
23 (*Version two: type classes*) |
|
24 consts quickSort :: "('a::linorder) list => 'a list" |
|
25 |
|
26 recdef quickSort "measure size" |
|
27 simpset "simpset() addsimps [length_filter RS le_less_trans]" |
|
28 |
|
29 "quickSort [] = []" |
|
30 |
|
31 "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])" |
|
32 |
20 end |
33 end |