v0.5.0

6 files changed, 151 insertions, 5 deletions

diff --git a/sample/245II_abbr.in b/sample/245II_abbr.in
new file mode 100644
index 0000000..a6797d8
--- /dev/null
+++ b/sample/245II_abbr.in
@@ -0,0 +1,98 @@
+// 245II in YALE encoding
+
+// Rules
+
+D >< V => ;
+B(a,b,c) >< Z => a~c, b~Z;
+B(a,b,c) >< Lam(x,t,v) => b~Lam(x,t,w), v~DB(a,w,c);
+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) >< AppTo(t,s) =>
+	x~AppTo(a,b), y~AppTo(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 >< AppTo(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;
+
+
+
+Lam(x,t,c) >< AppTo(result,s) => result~t, x~s, c~D;
+// We can write this avtive pair in nets as
+//   result << AppTo(s, lam_term)  for  AppTo(result, s)~ lam_term.
+
+// If the `<<' is defined as user macro, then it becomes more readable:
+//   result << App(lam_term, s)  =def=  lam_term ~ App(result, s)
+
+
+// Nets
+id1 ~ Lam(x,x,V);
+id2 ~ Lam(x,x,V);
+
+
+// lam f. lam x. f(fx)
+two ~ Lam(fb, Lam(x,r2,c),V),
+  fb ~ B(c,f,V),
+  f2,f1 << C(f),   // C(f2,f1) ~ f
+  r2 << AppTo(r1, f2),
+  r1 << AppTo(x, f1);   
+
+
+// lam f. lam x. f(f(f(fx)))
+four ~ Lam(fb, Lam(x, r4, c), V),
+  fb~B(c, f, V),
+  f4, C(f3, C(f2, f1)) << C(f),
+  r4 << AppTo(r3, f4),
+  r3 << AppTo(r2, f3),
+  r2 << AppTo(r1, f2),
+  r1 << AppTo(x, f1);
+
+
+// lam f. lam x. f(f(f(f(fx))))
+five ~ Lam(fb, Lam(x, r5, c), V),
+  fb~B(c, f, V),
+  f5, C(f4, C(f3, C(f2, f1))) << C(f),
+  r5 << AppTo(r4, f5),
+  r4 << AppTo(r3, f4),
+  r3 << AppTo(r2, f3),
+  r2 << AppTo(r1, f2),
+  r1 << AppTo(x, f1);
+
+
+
+// (((24)5)I)I
+aux24 << AppTo(four, two);
+aux245 << AppTo(five, aux24);
+aux245I << AppTo(id1, aux245);
+aux245II << AppTo(id2, aux245I);
+
+aux245II;
+exit;
diff --git a/sample/fib_9.in b/sample/fib_9.in
index f4f17e8..7c4af1f 100644
--- a/sample/fib_9.in
+++ b/sample/fib_9.in
@@ -8,7 +8,7 @@ fib(ret) >< (int n)
 
 
 // Note: Add is implemented as a built-in agent such that:
-//   Add(ret, int m) ~ (int n) --> ret~(n+m);
+//   Add(ret, int m) ~ (int n) --> ret~(m+n);
 
 // Nets
 fib(ret)~9;
diff --git a/sample/fib_9_abbr.in b/sample/fib_9_abbr.in
new file mode 100644
index 0000000..57a8c62
--- /dev/null
+++ b/sample/fib_9_abbr.in
@@ -0,0 +1,16 @@
+// Fibonacci number
+
+// Rules
+fib(ret) >< (int n)
+| n == 0 => ret~0
+| n == 1 => ret~1
+| _ => cnt1 << fib(n-1), cnt2 << fib(n-2), ret << Add(cnt1,cnt2);
+
+
+// Note: Add is implemented as a built-in agent such that:
+//   Add(ret, int m) ~ (int n) --> ret~(m+n);
+
+// Nets
+ret << fib(9);
+ret;
+
diff --git a/sample/linear-systemT.in b/sample/linear-systemT.in
index 648d9e1..f0e3ccb 100644
--- a/sample/linear-systemT.in
+++ b/sample/linear-systemT.in
@@ -36,7 +36,7 @@ Dup(x,y) >< Itc(a,b,c,d) =>
 	a~Dup(u1,u2), b~Dup(w1,w2), c~Dup(z1,z2), d~Dup(k1,k2);
 
 
-/* needed */
+/* required */
 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),
@@ -116,7 +116,7 @@ free res;
 
 
 // Ack 3 10
-// ver 1: the same as the example on the paper
+// 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),
@@ -124,7 +124,7 @@ 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))
+// 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),
@@ -132,7 +132,7 @@ 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.
+// 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),
diff --git a/sample/processnet1.in b/sample/processnet1.in
index d02404e..c648650 100644
--- a/sample/processnet1.in
+++ b/sample/processnet1.in
@@ -9,6 +9,8 @@ inc(r) >< []         => r~[];
 // Nets
 dup(r,w)~r1, inc(r1) ~ (0:w);
 
+// r,w << dup(r1), r1 << inc(0:w)
+
 //       +-----+       +-----+        +---+
 // r ----|     |  r1   |     |        |   |
 //       | dup |--->---| inc |---><---| 0 |----+
diff --git a/sample/processnet_fib.in b/sample/processnet_fib.in
new file mode 100644
index 0000000..ab19eec
--- /dev/null
+++ b/sample/processnet_fib.in
@@ -0,0 +1,30 @@
+// Rules
+dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs;
+dup(a1,a2) >< []         => a1~[], a2~[];
+
+add(r, ys) >< (int i):xs => addn(r, xs, i)~ys;
+addn(r, xs, int i) >< (int j):ys => r~(i+j):w, add(w,ys)~xs;
+
+
+// Nets
+dup(r, r1)~(1:xs), r1~add(sum, w), dup(xs, w)~(1:sum);
+
+// r,r1 << dup(1:xs),
+// xs,w << dup(1:sum),
+// sum << add(r1,w);
+
+//       +-----+        +---+   
+// r ----|     |        |   | xs  +-----+        +---+
+//       | dup |---><---| 1 |-----|     |        |   |
+//   +---|     |        |   |     | dup |---><---| 1 |----+
+//   |   +-----+        +---+  +--|     |        |   |    |
+//   |                         |  +-----+        +---+    | sum
+//   |                         |                          |
+//   |                         |                       +-----+
+//   |                         |                       | add |
+//   |                         |                       +-----+
+//   |                         |        w               |   |
+//   |                         +------------------------+   v
+//   |     r1                                               |
+//   +------------------------------------------------------+
+//