diff options
Diffstat (limited to '')
| -rw-r--r-- | sample/245II.in | 19 | ||||
| -rw-r--r-- | sample/245II_abbr.in | 5 | ||||
| -rw-r--r-- | sample/gcd.in | 6 | ||||
| -rw-r--r-- | sample/gcd_another.in | 16 |
4 files changed, 36 insertions, 10 deletions
diff --git a/sample/245II.in b/sample/245II.in index 6962ace..c71d45d 100644 --- a/sample/245II.in +++ b/sample/245II.in @@ -44,16 +44,23 @@ Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps; Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps; -// Execution +// Nets +// lam x.x 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); + +// lam f. lam x. f(fx) +two ~ Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V); + +// lam f. lam x. f(fx) +four ~ Lam(Lam(dz4, dx2, da1), B(da1, C(App(dz4, dz3), C(App(dz3, dz2), C(App(dz2, dz1), App(dz1, dx2)))), V), V); + +// lam f. lam x. f(fx) +five ~ 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); +two ~ App(aux1, four); +aux1 ~ App(aux2, five); aux2 ~ App(aux3, id1); aux3 ~ App(aux4, id2); aux4; diff --git a/sample/245II_abbr.in b/sample/245II_abbr.in index a6797d8..c2084ec 100644 --- a/sample/245II_abbr.in +++ b/sample/245II_abbr.in @@ -49,11 +49,14 @@ 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: +// If the `<<' could be defined as user macro in future, +// then it becomes more readable: // result << App(lam_term, s) =def= lam_term ~ App(result, s) // Nets + +// lam x.x id1 ~ Lam(x,x,V); id2 ~ Lam(x,x,V); diff --git a/sample/gcd.in b/sample/gcd.in index e616e28..5a57d8d 100644 --- a/sample/gcd.in +++ b/sample/gcd.in @@ -5,12 +5,12 @@ // Rule -gcd(ret) >< (int a, int b) +gcd(ret, int a) >< (int b) | b==0 => ret ~ a -| _ => gcd(ret) ~ (b, a%b); +| _ => gcd(ret, b) ~ a%b; // Net -gcd(r) ~ (14,21); +gcd(r, 14) ~ 21; r; // it should be 7 diff --git a/sample/gcd_another.in b/sample/gcd_another.in new file mode 100644 index 0000000..e616e28 --- /dev/null +++ b/sample/gcd_another.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 + + |