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
|
// Bubble sort with the same algorithm as others
/*
// length
length_(r,n) >< [] => r~n;
length_(r,int n) >< (int x):xs => length_(r,n+1)~xs;
length(r) >< [] => r~0;
length(r) >< x:xs => length_(r,0) ~ x:xs;
*/
// stream length
len_stream_(len, list, int ct) >< [] => len~ct, list~(*R)[];
len_stream_(len, list, int ct) >< x:xs =>
list~(*R)(x:cnt),
len_stream_(len, cnt, ct+1) ~ xs;
len_stream(len, list) >< [] => len~0, list~(*R)[];
len_stream(len, list) >< x:xs =>
list~(x:cnt),
len_stream_(len, cnt, 1)~xs;
// bubble sort
bs(r, xs) >< (int n)
| n == 0 => r~xs
| _ => (*L)bs_Cons(r, n)~xs;
bs_Cons(r, int n)>< x:xs => (*L)bs_ConsCons(r, n, x) ~ xs;
bs_Cons(r, int n)>< [] => r~(*R)[];
bs_ConsCons(r, int n, int x) >< (int y):ys
| x < y => r~x:cnt, (*L)bs(cnt, y:ys) ~(n-1)
| _ => r~y:cnt, (*L)bs(cnt, x:ys)~(n-1);
bs_ConsCons(r, int n, int x) >< [] => r~(*R)[x];
go(r,xs) >< (int n)
| n==0 => r~xs
| _ => bs(cnt, xs)~n, (*L)go(r, cnt)~(n-1);
bsort(r) >< [] => r~[];
bsort(r) >< x:xs =>
(*L)len_stream(len, alist) ~ (*R)(x:xs),
go(r, alist)~lengthDec1,
Sub(lengthDec1,len)~1;
// Creates a random list
make_RandList(ret) >< (int n)
| n>0 => ret~(rd:cnt), (*L)make_RandList(cnt)~(n-1)
where rd=rand(10000)
| _ => ret~[];
// validation checks
valid(ret) >< [] => ret~True;
valid(ret) >< x:xs => (*L)valid_Cons(ret,x)~xs;
valid_Cons(ret, int x) >< [] => ret~True;
valid_Cons(ret, int x) >< (int y):ys
| x<=y => (*L)valid_Cons(ret,y)~ys
| _ => ret~False, Eraser~ys;
// The `Eraser' is a built-in agent defined for any agents as follows:
//Eraser >< Alpha(a1, ..., a5) => Eraser~a1, ..., Eraser~a5;
// Main
const LIST_ELEM=20000;
make_RandList(rndlist)~(LIST_ELEM),
bsort(sorted)~rndlist,
valid(ret)~sorted;
ret;
|
