diff options
author | James Yoo | 2022-10-24 23:47:51 +0000 |
---|---|---|
committer | James Yoo | 2022-10-24 23:47:51 +0000 |
commit | 03315f012514bdcc5a4f654056f0103abe11eb83 (patch) | |
tree | 2b7c6e9233ecb503e7be0d8354483691f9a1e16c /entries/lizard-business/fib.dats | |
parent | 0921d8222bb883ea86d51c7200a865a5e4dbc469 (diff) | |
parent | 7ed13a92711a35a9c263c1f53e33e308653ae727 (diff) |
Merging local with remote main
Diffstat (limited to 'entries/lizard-business/fib.dats')
-rw-r--r-- | entries/lizard-business/fib.dats | 25 |
1 files changed, 25 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)) |