From eddac153a064648bee2aef6fb733ab6820bb96c3 Mon Sep 17 00:00:00 2001 From: Shinya Sato Date: Thu, 28 Apr 2022 21:41:58 +0900 Subject: v0.8.2 --- comparison/Inpla/src/isort-40000-reuse.in | 34 +++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) (limited to 'comparison/Inpla/src/isort-40000-reuse.in') diff --git a/comparison/Inpla/src/isort-40000-reuse.in b/comparison/Inpla/src/isort-40000-reuse.in index 3e7e2d2..1f7153d 100644 --- a/comparison/Inpla/src/isort-40000-reuse.in +++ b/comparison/Inpla/src/isort-40000-reuse.in @@ -1,6 +1,6 @@ // Insertion sort -IS(ret) >< [] => ret~[]; -IS(ret) >< x:xs => (*L)I(ret, x)~cnt, (*R)IS(cnt)~xs; +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 @@ -8,13 +8,31 @@ I(ret, int x) >< (int y):ys | _ => ret~(*L)(y:cnt), (*R)I(cnt, x)~ys; -const LIST_ELEM=40000; - -MkRandList(ret) >< (int n) -| n>0 => ret~(rd:cnt), (*L)MkRandList(cnt)~(n-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~[]; -MkRandList(cnt)~(LIST_ELEM), -IS(ret)~cnt; + +// validation checks +valid(ret) >< [] => ret~False; +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=40000; + +make_RandList(rndlist)~(LIST_ELEM), +isort(sorted)~rndlist, +valid(ret)~sorted; + ret; -- cgit v1.2.3