From 72e96acd7e96636a9bee68d1015b16f03c83109e Mon Sep 17 00:00:00 2001
From: cremet <cremet@epfl.ch>
Date: Tue, 6 Jan 2004 14:13:51 +0000
Subject: - First commit.

---
 sources/examples/pilib/piNat.scala | 89 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 sources/examples/pilib/piNat.scala

(limited to 'sources/examples/pilib')

diff --git a/sources/examples/pilib/piNat.scala b/sources/examples/pilib/piNat.scala
new file mode 100644
index 0000000000..5fd2dde385
--- /dev/null
+++ b/sources/examples/pilib/piNat.scala
@@ -0,0 +1,89 @@
+import scala.concurrent.pilib._;
+//import pilib._;
+
+/** Church encoding of naturals in the Pi-calculus */
+object piNat with Executable {
+
+  /** Locations of Pi-calculus natural */
+  class NatChan extends Chan[Triple[Chan[unit], Chan[NatChan], Chan[NatChan]]];
+
+  /** Zero */
+  def Z(l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => z.write(()) }
+  );
+
+  /** Successor of Double */
+  def SD(n: NatChan, l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => sd.write(n) }
+  );
+
+  /** Double */
+  def D(n: NatChan, l: NatChan): unit = choice (
+    l * { case Triple(z, sd, d) => d.write(n) }
+  );
+
+  /** Make "l" a location representing the natural "n" */
+  def make(n: int, l: NatChan): unit =
+    if (n == 0) Z(l)
+    else if (n % 2 == 0) { val l1 = new NatChan; spawn < D(l1, l) >; make(n/2, l1) }
+    else { val l1 = new NatChan; spawn < SD(l1, l) >; make(n/2, l1) };
+
+  /** Consume the natural "m" and put it successor at location "n" */
+  def Succ(m: NatChan, n: NatChan): unit = {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < m.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => make(1, n) },
+      sd * { m1 => { val n1 = new NatChan; spawn < D(n1, n) >; Succ(m1, n1) } },
+      d  * { m1 => SD(m1, n) }
+    )
+  }
+
+  /** Consume the natural "l" and put two copies at locations "m" and "n" */
+  def Copy(l: NatChan, m: NatChan, n: NatChan): unit = {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < l.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => spawn < Z(m) >; Z(n)  },
+      sd * { l1 => { val m1 = new NatChan; val n1 = new NatChan;
+                    spawn < SD(m1, m) | SD(n1, n) >;
+                    Copy(l1, m1, n1) } },
+      d * { l1 => { val m1 = new NatChan; val n1 = new NatChan;
+                   spawn < D(m1, m) | D(n1, n) >;
+                   Copy(l1, m1, n1) } }
+    )
+  }
+
+  /** Consume the natural at location "n" and return its value */
+  def value(n: NatChan): int =  {
+    val z = new Chan[unit];
+    val sd = new Chan[NatChan];
+    val d = new Chan[NatChan];
+    spawn < n.write(Triple(z, sd, d)) >;
+    choice (
+      z  * { x => 0  },
+      sd * { n1 => 2 * value(n1) + 1 },
+      d * { n1 => 2 * value(n1) }
+    )
+  }
+
+  // Test
+  val i = 42;
+  val l = new NatChan;
+  val l1 = new NatChan;
+  val l2 = new NatChan;
+  val l3 = new NatChan;
+
+  spawn <
+  make(i, l) |
+  Copy(l, l1, l2) |
+  Succ(l2, l3) |
+  System.out.println("" + i + " = " + value(l1)) |
+  System.out.println("succ " + i + " = " + value(l3))
+  >;
+
+}
-- 
cgit v1.2.3