add maude & ATS

2 files changed, 52 insertions, 0 deletions

diff --git a/entries/lizard-business/fib.dats b/entries/lizard-business/fib.dats
new file mode 100644
index 0000000..f6bd5a1
--- /dev/null
+++ b/entries/lizard-business/fib.dats
@@ -0,0 +1,25 @@
+#include "share/atspre_define.hats"
+#include "share/atspre_staload.hats"
+
+dataprop is_fib(int, int) =
+| F0(0, 0) | F1(1, 1)
+| {i, m, n : nat} Fplus(i + 2, m + n) of (is_fib(i, m), is_fib(i + 1, n))
+
+typedef fib(i : int) = [n : nat] (is_fib(i, n) | int(n))
+
+
+fun fib {t : nat} .<>. (t : int(t)) :<> fib(t) =
+let
+  fun go {m, n, i : nat | i <= t} .<t - i>.
+         (M : is_fib(i, m), N : is_fib(i + 1, n) |
+          m : int(m), n : int(n), i : int(i)) :<>
+        fib(t) =
+    if i = t then (M | m)
+    else go(N, Fplus(M, N) | n, m + n, i + 1)
+in
+  go(F0, F1 | 0, 1, 0)
+end
+
+fun fib_(i : Nat) : Nat = let val (_ | res) = fib(i) in res end
+
+implement main0 () = println!("fib(15) = ", fib_(15))
diff --git a/entries/lizard-business/fib.maude b/entries/lizard-business/fib.maude
new file mode 100644
index 0000000..20bc428
--- /dev/null
+++ b/entries/lizard-business/fib.maude
@@ -0,0 +1,27 @@
+smod FIB is
+  pr LIST{Nat} .
+
+  vars M N : Nat .
+  var  Ns  : List{Nat} .
+
+  rl [start]: nil => 0 1 .
+  rl [next]:  Ns M N => Ns M N (M + N) .
+  rl [drop] : Ns N => N .
+
+  strats fib fibgo : Nat @ List{Nat} .
+  sd fib(N)      := start ; fibgo(N) .
+  sd fibgo(0)    := top(drop) .
+  sd fibgo(s(N)) := top(next) ; fibgo(N) .
+endsm
+
+***(
+  Maude> srew nil using fib(10) .
+  srewrite in FIB : nil using fib(10) .
+
+  Solution 1
+  rewrites: 8330 in 12ms cpu (12ms real) (694166 rewrites/second)
+  result NzNat: 89
+
+  No more solutions.
+  rewrites: 8469 in 12ms cpu (13ms real) (705750 rewrites/second)
+)