aboutsummaryrefslogtreecommitdiff
path: root/comparison/Inpla
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--comparison/Inpla/main.sh8
-rw-r--r--comparison/Inpla/src/bsort-20000-reuse.in77
-rw-r--r--comparison/Inpla/src/bsort-20000.in77
-rw-r--r--comparison/Inpla/src/bsort-efficient-20000-reuse.in40
-rw-r--r--comparison/Inpla/src/bsort-efficient-20000.in40
-rw-r--r--comparison/Inpla/src/isort-20000-reuse.in38
-rw-r--r--comparison/Inpla/src/isort-20000.in38
7 files changed, 314 insertions, 4 deletions
diff --git a/comparison/Inpla/main.sh b/comparison/Inpla/main.sh
index 6975046..13502b9 100644
--- a/comparison/Inpla/main.sh
+++ b/comparison/Inpla/main.sh
@@ -6,11 +6,11 @@ bash ./sptestInpla.sh src/fib-38-reuse.in
bash ./sptestInpla.sh src/ack-stream_3-11.in
bash ./sptestInpla.sh src/ack-stream_3-11-reuse.in
-bash ./sptestInpla.sh src/bsort-40000.in
-bash ./sptestInpla.sh src/bsort-40000-reuse.in
+bash ./sptestInpla.sh src/bsort-20000.in
+bash ./sptestInpla.sh src/bsort-20000-reuse.in
-bash ./sptestInpla.sh src/isort-40000.in
-bash ./sptestInpla.sh src/isort-40000-reuse.in
+bash ./sptestInpla.sh src/isort-20000.in
+bash ./sptestInpla.sh src/isort-20000-reuse.in
bash ./sptestInpla.sh src/qsort-260000.in
bash ./sptestInpla.sh src/qsort-260000-reuse.in '-Xms 17 -Xmt 0'
diff --git a/comparison/Inpla/src/bsort-20000-reuse.in b/comparison/Inpla/src/bsort-20000-reuse.in
new file mode 100644
index 0000000..c5080fe
--- /dev/null
+++ b/comparison/Inpla/src/bsort-20000-reuse.in
@@ -0,0 +1,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;
diff --git a/comparison/Inpla/src/bsort-20000.in b/comparison/Inpla/src/bsort-20000.in
new file mode 100644
index 0000000..e012bc6
--- /dev/null
+++ b/comparison/Inpla/src/bsort-20000.in
@@ -0,0 +1,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~[];
+len_stream_(len, list, int ct) >< x:xs =>
+ list~x:cnt,
+ len_stream_(len, cnt, ct+1) ~xs;
+
+
+len_stream(len, list) >< [] => len~0, list~[];
+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
+| _ => bs_Cons(r, n)~xs;
+
+bs_Cons(r, int n)>< x:xs => bs_ConsCons(r, n, x) ~ xs;
+bs_Cons(r, int n)>< [] => r~[];
+
+bs_ConsCons(r, int n, int x) >< (int y):ys
+| x < y => r~x:cnt, bs(cnt, y:ys) ~(n-1)
+| _ => r~y:cnt, bs(cnt, x:ys)~(n-1);
+bs_ConsCons(r, int n, int x) >< [] => r~[x];
+
+go(r,xs) >< (int n)
+| n==0 => r~xs
+| _ => bs(cnt, xs)~n, go(r, cnt)~(n-1);
+
+bsort(r) >< [] => r~[];
+bsort(r) >< x:xs =>
+ len_stream(len, alist) ~ x:xs,
+ go(r, alist)~lengthDec1,
+ Sub(lengthDec1,len)~1;
+
+
+// creates a random list
+make_RandList(ret) >< (int n)
+| n>0 => ret~(rd:cnt), make_RandList(cnt)~(n-1)
+ where rd=rand(10000)
+| _ => ret~[];
+
+
+// validation checks
+valid(ret) >< [] => ret~True;
+valid(ret) >< x:xs => valid_Cons(ret,x)~xs;
+
+valid_Cons(ret, int x) >< [] => ret~True;
+valid_Cons(ret, int x) >< (int y):ys
+| x<=y => 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; \ No newline at end of file
diff --git a/comparison/Inpla/src/bsort-efficient-20000-reuse.in b/comparison/Inpla/src/bsort-efficient-20000-reuse.in
new file mode 100644
index 0000000..e496c3e
--- /dev/null
+++ b/comparison/Inpla/src/bsort-efficient-20000-reuse.in
@@ -0,0 +1,40 @@
+// Bubble sort
+bsort(ret) >< [] => ret~[];
+bsort(ret) >< x:xs => (*L)bsort(ret)~cnt, (*R)B(cnt, x)~xs;
+bsort(ret) >< M(x) => ret~x;
+
+B(ret, int x) >< [] => ret~M([x]);
+B(ret, int x) >< M(w) => ret~M(x:w);
+B(ret, int x) >< (int y):ys
+| x<y => ret~(*R)(x:cnt), (*L)B(cnt, y)~ys
+| _ => ret~(*R)(y:cnt), (*L)B(cnt, x)~ys;
+
+
+// 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;
diff --git a/comparison/Inpla/src/bsort-efficient-20000.in b/comparison/Inpla/src/bsort-efficient-20000.in
new file mode 100644
index 0000000..c9702fe
--- /dev/null
+++ b/comparison/Inpla/src/bsort-efficient-20000.in
@@ -0,0 +1,40 @@
+// Bubble sort
+bsort(ret) >< [] => ret~[];
+bsort(ret) >< x:xs => bsort(ret)~cnt, B(cnt, x)~xs;
+bsort(ret) >< M(x) => ret~x;
+
+B(ret, int x) >< [] => ret~M([x]);
+B(ret, int x) >< M(w) => ret~M(x:w);
+B(ret, int x) >< (int y):ys
+| x<y => ret~(x:cnt), B(cnt, y)~ys
+| _ => ret~(y:cnt), B(cnt, x)~ys;
+
+
+// creates a random list
+make_RandList(ret) >< (int n)
+| n>0 => ret~(rd:cnt), make_RandList(cnt)~(n-1)
+ where rd=rand(10000)
+| _ => ret~[];
+
+
+// validation checks
+valid(ret) >< [] => ret~True;
+valid(ret) >< x:xs => valid_Cons(ret,x)~xs;
+
+valid_Cons(ret, int x) >< [] => ret~True;
+valid_Cons(ret, int x) >< (int y):ys
+| x<=y => 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;
diff --git a/comparison/Inpla/src/isort-20000-reuse.in b/comparison/Inpla/src/isort-20000-reuse.in
new file mode 100644
index 0000000..9d7c7ab
--- /dev/null
+++ b/comparison/Inpla/src/isort-20000-reuse.in
@@ -0,0 +1,38 @@
+// Insertion sort
+isort(ret) >< [] => ret~[];
+isort(ret) >< x:xs => (*L)I(ret, x)~cnt, (*R)isort(cnt)~xs;
+
+I(ret, int x) >< [] => ret~[x];
+I(ret, int x) >< (int y):ys
+| x<=y => ret~(*L)(x:(*R)(y:ys))
+| _ => ret~(*L)(y:cnt), (*R)I(cnt, x)~ys;
+
+
+// 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),
+isort(sorted)~rndlist,
+valid(ret)~sorted;
+
+ret;
diff --git a/comparison/Inpla/src/isort-20000.in b/comparison/Inpla/src/isort-20000.in
new file mode 100644
index 0000000..3ed10aa
--- /dev/null
+++ b/comparison/Inpla/src/isort-20000.in
@@ -0,0 +1,38 @@
+// Insertion sort
+isort(ret) >< [] => ret~[];
+isort(ret) >< x:xs => I(ret, x)~cnt, isort(cnt)~xs;
+
+I(ret, int x) >< [] => ret~[x];
+I(ret, int x) >< (int y):ys
+| x<=y => ret~(x:y:ys)
+| _ => ret~(y:cnt), I(cnt, x)~ys;
+
+
+// creates a random list
+make_RandList(ret) >< (int n)
+| n>0 => ret~(rd:cnt), make_RandList(cnt)~(n-1)
+ where rd=rand(10000)
+| _ => ret~[];
+
+
+// validation checks
+valid(ret) >< [] => ret~True;
+valid(ret) >< x:xs => valid_Cons(ret,x)~xs;
+
+valid_Cons(ret, int x) >< [] => ret~True;
+valid_Cons(ret, int x) >< (int y):ys
+| x<=y => 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),
+isort(sorted)~rndlist,
+valid(ret)~sorted;
+
+ret;
generated by cgit v1.2.3 (git 2.39.1) at 2026-11-10 23:47:26 +0000