v0.4.1

14 files changed, 435 insertions, 0 deletions

diff --git a/sample/245II.in b/sample/245II.in
new file mode 100644
index 0000000..6962ace
--- /dev/null
+++ b/sample/245II.in
@@ -0,0 +1,60 @@
+// 245II in YALE encoding
+
+// Rules
+Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D;
+D >< V => ;
+B(a,b,c) >< Z => a~c, b~Z;
+B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e);
+DB(a,b,c) >< V => a~c, b~V;
+C(x,y) >< Z => x~Z, y~Z;
+C(x,y) >< Lam(s,t,u) =>
+	 x~Lam(a,b,c), y~Lam(d,e,f),
+	 s~Delta(a,d), t~Delta(b,e), u~C(c,f);
+C(x,y) >< V => x~V, y~V;
+Delta(x,y) >< Delta(a,b) => x~a, y~b;
+B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d));
+Delta(a,b) >< CB(x,y,z) =>
+	x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f));
+Delta(x,y) >< S(z) =>
+	x~S(a), y~S(b), z~Delta(a,b);
+Delta(x,y) >< Z => x~Z, y~Z;
+Delta(x,y) >< V => x~V, y~V;
+Delta(x,y) >< C(t,s) =>
+	x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c);
+Delta(x,y) >< App(t,s) =>
+	x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d);
+Delta(x,y) >< Lam(t,s,u)=>
+	x~Lam(a,b,c), y~Lam(d,e,f),
+	t~Delta(a,d), s~Delta(b,e), u~Delta(c,f);
+DB(x,y,z) >< CB(t,s,u) =>
+	x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z);
+C(x,y) >< CB(t,s,u) =>
+	x~CB(a,b,c), y~CB(d,e,f), 
+	t~Delta(a,d), s~C(b,e), u~C(c,f);
+D >< CB(a,b,c) => a~c, b~D;
+
+Eps >< Eps => ;
+Eps >< S(x) => x~Eps;
+Eps >< V => ;
+Eps >< D =>;
+Eps >< Delta(t,s) => t~Eps,s~Eps;
+Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps;
+Eps >< App(t,s) => t~Eps,s~Eps;
+Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps;
+Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps;
+
+
+// Execution
+id1 ~ Lam(i,i,V);
+id2 ~ Lam(i2,i2,V);
+two1 ~ Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V);
+four1 ~ Lam(Lam(dz4, dx2, da1), B(da1, C(App(dz4, dz3), C(App(dz3, dz2), C(App(dz2, dz1), App(dz1, dx2)))), V), V);
+five3 ~ Lam(Lam(z53, x23, a13), B(a13, C(App(z53, z43), C(App(z43, z33), C(App(z33,z23), C(App(z23, z13), App(z13, x23))))), V), V);
+
+// 245II
+two1 ~ App(aux1, four1);
+aux1 ~ App(aux2, five3);
+aux2 ~ App(aux3, id1);
+aux3 ~ App(aux4, id2);
+aux4;
+exit;
diff --git a/sample/AckSZ-3_5.in b/sample/AckSZ-3_5.in
new file mode 100644
index 0000000..0d0ebe4
--- /dev/null
+++ b/sample/AckSZ-3_5.in
@@ -0,0 +1,18 @@
+// Ackermann function on unary natural numbers
+// fun ack(0,y) = y+1
+//   | ack(x,0) = ack(x-1,1)        
+//   | ack(x,y) = ack(x-1,ack(x,y-1));
+//
+ack(r,y)>< Z => r~S(y);
+ack(r,y)>< S(x) => ack_Sx(r, x)~y;
+ack_Sx(r,x)>< Z => ack(r, S(Z))~x;
+ack_Sx(r,x)>< S(y) => dup(x1,x2)~x, ack(r,cnt)~x1, ack_Sx(cnt,x2)~y;
+
+
+dup(a1,a2)>< Z => a1~Z, a2~Z;
+dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), dup(w1,w2)~x;
+
+// Ack 3 5
+ack(r, S(S(S(S(S(Z))))))~S(S(S(Z)));
+prnat r;
+exit;
diff --git a/sample/FibSZ_9.in b/sample/FibSZ_9.in
new file mode 100644
index 0000000..288a8bc
--- /dev/null
+++ b/sample/FibSZ_9.in
@@ -0,0 +1,29 @@
+// Fibonacci number on unary natural numbers
+fib(r)><Z => r~Z;
+fib(r)><S(x) => fibS(r)~x;
+fibS(r)><Z => r~S(Z);
+fibS(r)><S(x) => dup(x1,x2)~x, add(r,r2)~r1, fib(r2)~x2, fibS(r1)~x1;
+
+
+
+// ------ DUP ------
+dup(x1,x2)><Z => x1~Z, x2~Z;
+dup(x1,x2)><S(x) => x1~S(w1), x2~S(w2), dup(w1,w2)~x;
+
+
+//------ ADD ------
+//Add para
+add(r,x)><Z => r~x;
+add(r,x)><S(y) => r~S(w), add(w,x)~y;
+
+//Add_Seq
+//add(r,y)><Z => y~r;
+//add(r,y)><S(x) => add(r, S(y))~x;
+
+
+// Execution
+// Fib 9
+fib(r)~S(S(S(S(S(S(S(S(S(Z)))))))));
+prnat r;
+free r;
+
diff --git a/sample/ack_3_5.in b/sample/ack_3_5.in
new file mode 100644
index 0000000..87057a2
--- /dev/null
+++ b/sample/ack_3_5.in
@@ -0,0 +1,32 @@
+// Ackermann Function
+//
+// fun ack(0,n) = n+1
+//   | ack(m,0) = ack(m-1,1)        
+//   | ack(m,n) = ack(m-1,ack(m,n-1));
+
+// The below rule is wrong because there is no gurantee that
+// the 'cnt' is an integer agent when ack(r)~(m-1,cnt) is evaluated.
+//
+// ack(r) >< (int m, int n)
+// | m==0 => r~(n+1)
+// | n==0 => ack(r) ~ (m-1,1)
+// | _ => ack(cnt)~(m,n-1), ack(r)~(m-1,cnt);
+
+
+ack(ret, n) >< (int m)
+| m==0 => inc(ret)~n
+| _ => ackn(ret, m)~n;
+
+ackn(ret, int m) >< (int n)
+| n==0 => ack(ret,1) ~ (m-1)
+| _ => ack(cnt,n-1)~m, ack(ret,cnt)~(m-1);
+
+inc(ret)><(int n) => ret~(n+1);
+
+
+ackMain(ret)><(int m, int n) => ack(ret,n)~m;
+
+ackMain(ret)~(3,5);
+ret;
+free ret;
+
diff --git a/sample/bsort.in b/sample/bsort.in
new file mode 100644
index 0000000..7b2e2d6
--- /dev/null
+++ b/sample/bsort.in
@@ -0,0 +1,18 @@
+// Bubble sort
+
+// Rules
+bsort(ret) >< [] => ret~[];
+bsort(ret) >< x:xs => bsort(ret)~cnt, bubble(cnt, x)~xs;
+bsort(ret) >< M(x) => ret~x;
+
+bubble(ret, int x) >< [] => ret~M([x]);
+bubble(ret, int x) >< M(w) => ret~M(x:w);
+bubble(ret, int x) >< (int y):ys
+| x<y => ret~(x:cnt), bubble(cnt, y)~ys
+| _   => ret~(y:cnt), bubble(cnt, x)~ys;
+
+
+// Nets
+bsort(r)~[3,6,1,9,2];
+r;
+
diff --git a/sample/fib-tail-38.in b/sample/fib-tail-38.in
new file mode 100644
index 0000000..5996337
--- /dev/null
+++ b/sample/fib-tail-38.in
@@ -0,0 +1,10 @@
+// Fibonacci number
+fibt(r, int a, int b) >< (int n)
+| n == 0 => r~1
+| n == 1 => r~a
+| _ => fibt(r, a+b, a) ~ (n-1);
+
+fibMain(r) >< (int n) => fibt(r, 1, 1) ~ n;
+
+fibMain(r)~9;
+r;
diff --git a/sample/fib-tail_9.in b/sample/fib-tail_9.in
new file mode 100644
index 0000000..58f4cc5
--- /dev/null
+++ b/sample/fib-tail_9.in
@@ -0,0 +1,10 @@
+// Fibonacci number
+fibt(r, int a, int b) >< (int n)
+| n == 0 => r~0
+| n == 1 => r~a
+| _ => fibt(r, a+b, a) ~ (n-1);
+
+fibMain(r) >< (int n) => fibt(r, 1, 0) ~ n;
+
+fibMain(r)~9;
+r;
diff --git a/sample/fib_9.in b/sample/fib_9.in
new file mode 100644
index 0000000..f4f17e8
--- /dev/null
+++ b/sample/fib_9.in
@@ -0,0 +1,16 @@
+// Fibonacci number
+
+// Rules
+fib(ret) >< (int n)
+| n == 0 => ret~0
+| n == 1 => ret~1
+| _ => fib(cnt1)~(n-1), fib(cnt2)~(n-2), Add(ret, cnt2)~cnt1;
+
+
+// Note: Add is implemented as a built-in agent such that:
+//   Add(ret, int m) ~ (int n) --> ret~(n+m);
+
+// Nets
+fib(ret)~9;
+ret;
+
diff --git a/sample/gcd.in b/sample/gcd.in
new file mode 100644
index 0000000..e616e28
--- /dev/null
+++ b/sample/gcd.in
@@ -0,0 +1,16 @@
+// Greatest common divisor
+//
+//def gcd(a: Int, b: Int): Int =
+//  if (b==0) a else gcd(b, a%b)
+
+
+// Rule
+gcd(ret) >< (int a, int b)
+| b==0 => ret ~ a
+| _ => gcd(ret) ~ (b, a%b);
+
+// Net
+gcd(r) ~ (14,21);
+r; // it should be 7
+
+
diff --git a/sample/isort.in b/sample/isort.in
new file mode 100644
index 0000000..e637055
--- /dev/null
+++ b/sample/isort.in
@@ -0,0 +1,15 @@
+// Insertion sort
+
+// Rules
+isort(ret) >< [] => ret~[];
+isort(ret) >< x:xs => insert(ret, x)~cnt, isort(cnt)~xs;
+
+insert(ret, int x) >< [] => ret~[x];
+insert(ret, int x) >< (int y):ys
+| x<=y => ret~(x:y:ys)
+| _    => ret~(y:cnt), insert(cnt, x)~ys;
+
+
+// Nets
+isort(r)~[3,6,1,9,2];
+r;
diff --git a/sample/linear-systemT.in b/sample/linear-systemT.in
new file mode 100644
index 0000000..648d9e1
--- /dev/null
+++ b/sample/linear-systemT.in
@@ -0,0 +1,142 @@
+// sample programs of linear-systemT (see POPL2016 paper)
+
+// Basic Rules ----------------------------------------
+Lamc(x,y) >< App(a,b) => a~x, b~y;
+Times(a,b) >< Par(x,y) => a~x, b~y;
+B(a,b,c) >< Lamc(x,y) => a~c, b~Lamc(x,y);
+V >< Lam(x,y,z) => z~Lamc(x,y);
+B(a,b,c)><S(x) => b~S(w), x~B(a,w,c);	// original
+//B(a,b,c) >< S(x) => a~c, b~S(x);	// alternative
+B(a,b,c) >< Z => a~c, b~Z;
+
+
+// Iterator ----------------------------------------
+Iter(r,n,u) >< Lamc(x,t) => n~Itc(u,x,t,r);
+Itc(u,x,t,r) >< Z => u~r,x~Eps,t~Eps;
+Itc(u,x,t,r) >< S(y) => y~Itc(t2,w,t1,r), x~Dup(w,u),t~Dup(t1,t2);
+
+// Dup ----------------------------------------
+Dup(x,y) >< Dup(a,b) => x~a, y~b;
+Dup(x,y) >< Lamc(a,b) => x~Lamc(w1,w2), y~Lamc(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< App(a,b) => x~App(w1,w2), y~App(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< Times(a,b) => x~Times(w1,w2), y~Times(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< Par(a,b) => x~Par(w1,w2), y~Par(z1,z2), a~Dup(w1,z1), b~Dup(w2,z2);
+Dup(x,y) >< V => x~V, y~V;
+
+Dup(a1,a2)>< Z => a1~Z, a2~Z;
+Dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), x~Dup(w1,w2);
+
+
+Dup(x,y) >< Iter(a,b,c) =>
+	x~Iter(u1,w1,z1), y~Iter(u2,w2,z2),
+	a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2);
+
+Dup(x,y) >< Itc(a,b,c,d) =>
+	x~Itc(u1,w1,z1,k1), y~Itc(u2,w2,z2,k2), 
+	a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2);
+
+
+/* needed */
+Dup(x,y) >< B(a,b,c) => x~B(u1,z1,w1), y~B(u2,z2,w2),
+	a~Dup(u1,u2), b~Dup(z1,z2), c~Dup(w1,w2);
+Dup(x,y) >< Lam(a,b,c) => x~Lam(w1,u1,z1), y~Lam(w2,u2,z2),
+	a~Dup(w1,w2), b~Dup(u1,u2), c~Dup(z1,z2);
+
+
+// Eps ----------------------------------------
+Eps >< Eps => ;
+Eps >< Dup(x,y) => Eps~x,Eps~y;
+Eps >< Lamc(x,y) => Eps~x,Eps~y;
+Eps >< App(x,y) => Eps~x, Eps~y;
+Eps >< Par(x,y) => Eps~x, Eps~y;
+Eps >< Times(x,y) => Eps~x, Eps~y;
+
+Eps >< S(x) => x~Eps;
+Eps >< Z => ;
+
+Eps >< Iter(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< Itc(a,b,c,d) => a~Eps, b~Eps, c~Eps,d~Eps;
+
+/* required */
+Eps >< B(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< Lam(a,b,c) => a~Eps, b~Eps, c~Eps;
+Eps >< V => ;
+
+
+// sample ----------------------------------------
+// Cp: nat -o nat Times nat
+n~S(S(Z)),
+cp~Lamc(x,r), Iter(r,x,Times(Z,Z))~Lamc(Par(a,b),Times(S(a),S(b)));
+cp~App(n,res);
+res;
+free res;
+
+// fst: nat Times nat -o nat
+pair~Times(S(S(S(Z))),S(Z)),
+fst~Lamc(Par(n,m), r), Iter(r,m,n)~Lamc(x,x);
+fst~App(pair,res);
+res;
+free res;
+
+// snd: nat Times nat -o nat
+pair~Times(S(S(S(Z))),S(Z)),
+snd~Lamc(Par(n,m), r), Iter(r,n,m)~Lamc(x,x);
+snd~App(pair,res);
+res;
+free res;
+
+
+// ((Add a) b)
+a~S(S(Z)), b~S(S(S(Z))),
+add~Lamc(B(V,u,Lam(n,r,r1)),r1), Iter(r,n,u)~Lamc(x,S(x));
+add~App(a,App(b,res));
+prnat res;
+free res;
+
+
+// ((Mult a) b)
+a~S(S(Z)), b~S(S(S(Z)));
+add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)),
+App(n,Iter(r,m,Z))~add,
+mult~Lamc(B(V,n,Lam(m,r,r1)),r1);
+mult~App(a,App(b,res));
+prnat res;
+free res;
+
+// ((Exp a) b)
+a~S(S(Z)), b~S(S(S(Z)));
+add~Lamc(B(V,au,Lam(an,ar,ar1)),ar1),Iter(ar,an,au)~Lamc(ax,S(ax)),
+App(mn,Iter(mr,mm,Z))~add,
+mult~Lamc(B(V,mn,Lam(mm,mr,mr1)),mr1),
+App(n,Iter(r,m,S(Z)))~mult,
+exp~Lamc(B(V,n,Lam(m,r,r1)),r1);
+exp~App(a,App(b,res));
+prnat res;
+free res;
+
+
+// Ack 3 10
+// ver 1: the same as the example on the paper
+a~S(S(S(Z))),
+b~S(S(S(S(S(S(S(S(S(S(Z))))))))));
+Iter(t,x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1),
+Lamc(x,t)~App(a,App(b, r));
+prnat r;
+free r;
+
+// ver 2: \m.(\n.(iter m (\x.(S x)) (\x.(\y.(iter (S y) (S 0) x))) n))
+a~S(S(S(Z))),
+b~S(S(S(S(S(S(S(S(S(S(Z))))))))));
+Iter(App(n,apr),x,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1),
+Lamc(B(V,x,Lam(n,apr,nr)),nr)~App(a,App(b, r));
+prnat r;
+free r;
+
+// ver 3: another encoding of ver 2.
+a~S(S(S(Z))),
+b~S(S(S(S(S(S(S(S(S(S(Z))))))))));
+Iter(t,m,Lamc(x1,S(x1)))~Lamc(B(V,Iter(r2,S(y),S(Z)),Lam(y,r2,r1)),r1),
+Lamc(m,t)~App(n,apr),
+Lamc(n,apr)~App(a,App(b, r));
+prnat r;
+free r;
diff --git a/sample/msort.in b/sample/msort.in
new file mode 100644
index 0000000..599990b
--- /dev/null
+++ b/sample/msort.in
@@ -0,0 +1,28 @@
+// Merge sort
+
+// Rules
+msort(ret) >< [] => ret~[];
+msort(ret) >< x:xs => ms_tail(ret, x)~xs;
+
+ms_tail(ret, n) >< [] => ret~[n];
+ms_tail(ret, n) >< x:xs => 
+	split(left,right) ~ (n:x:xs),
+	msort(a)~left, msort(b)~right, merge(ret,b)~a;
+
+merge(ret, snd) >< [] => ret~snd;
+merge(ret, snd) >< x:xs => mergeCC(ret, x, xs)~snd;
+
+mergeCC(ret, int y, ys) >< [] => ret~(y:ys);
+mergeCC(ret, int y, ys) >< (int x):xs
+| x <= y => ret~(x:cnt), mergeCC(cnt, y, ys) ~ xs
+| _      => ret~(y:cnt), mergeCC(cnt, x, xs) ~ ys;
+
+
+split(right,left) >< [] => right~[], left~[];
+split(right,left) >< x:xs =>
+	right~(x:cntl), left~cntr, split(cntr,cntl)~xs;
+
+
+// Nets
+msort(ret)~[3,6,1,9,2];
+ret;
\ No newline at end of file
diff --git a/sample/processnet1.in b/sample/processnet1.in
new file mode 100644
index 0000000..d02404e
--- /dev/null
+++ b/sample/processnet1.in
@@ -0,0 +1,20 @@
+// Rules
+dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs;
+dup(a1,a2) >< []         => a1~[], a2~[];
+
+inc(r) >< (int i):xs => r~(i+1):w, inc(w)~xs;
+inc(r) >< []         => r~[];
+
+
+// Nets
+dup(r,w)~r1, inc(r1) ~ (0:w);
+
+//       +-----+       +-----+        +---+
+// r ----|     |  r1   |     |        |   |
+//       | dup |--->---| inc |---><---| 0 |----+
+//   +---|     |       |     |        |   |    |
+//   |   +-----+       +-----+        +---+    |
+//   |                                         |
+//   +-----------------------------------------+
+//             w
+	     
\ No newline at end of file
diff --git a/sample/qsort.in b/sample/qsort.in
new file mode 100644
index 0000000..35de8e4
--- /dev/null
+++ b/sample/qsort.in
@@ -0,0 +1,21 @@
+// Quick sort
+
+// Rules
+qsort(ret) >< [] => ret~[];
+qsort(ret) >< (int x):xs =>
+	part(x, left, right)~xs,
+	qsort(cntl)~left, qsort(cntr)~right,
+	Append(ret, x:cntl)~cntr;
+
+// Note: `Append' is implemented as built-in.
+// Append(ret, a)~b  -->  ret ~ b@a
+
+part(int x, a, b) >< [] => a~[], b~[];
+part(int x, a, b) >< (int y):ys
+| y<x => b~(y:cnt), part(x, a, cnt)~ys
+| _   => a~(y:cnt), part(x, cnt, b)~ys;
+
+
+// Nets
+qsort(ret)~[3,6,1,9,2];
+ret;
\ No newline at end of file