From 4c717196fd630c5c207e114ffa9ca9c301eb1198 Mon Sep 17 00:00:00 2001 From: Jonathan Chan Date: Sun, 23 Oct 2022 23:07:43 -0400 Subject: Fortran :) (also moved my Agda file up a dir) --- README.md | 3 ++- entries/ionathanch/Fib.agda | 19 +++++++++++++++++++ entries/ionathanch/agda/Fib.agda | 19 ------------------- entries/ionathanch/fib.f90 | 21 +++++++++++++++++++++ 4 files changed, 42 insertions(+), 20 deletions(-) create mode 100644 entries/ionathanch/Fib.agda delete mode 100644 entries/ionathanch/agda/Fib.agda create mode 100644 entries/ionathanch/fib.f90 diff --git a/README.md b/README.md index 51ade8f..0fcbc53 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,8 @@ For a submission to the upcoming "Reclaim your space" exhibition at [Hatch Art G ### [`ionathanch`](https://github.com/ionathanch) -- [`agda`](./entries/ionathanch/agda/Fib.agda) +- [`agda`](./entries/ionathanch/Fib.agda) +- [`fortran`](./entries/ionathanch/fib.f90) ### [`funemy`](https://github.com/funemy) - [`agda`](./entries/funemy/agda/fib1.agda) diff --git a/entries/ionathanch/Fib.agda b/entries/ionathanch/Fib.agda new file mode 100644 index 0000000..a12b0a5 --- /dev/null +++ b/entries/ionathanch/Fib.agda @@ -0,0 +1,19 @@ + +open import Agda.Builtin.Nat +open import Agda.Builtin.List +open import Agda.Builtin.Reflection + +data Fib : Nat → Nat → Set where + instance F0 : Fib 0 0 + instance F1 : Fib 1 1 + instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m) + +fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat +fib' k {n} ⦃ fib ⦄ = n + +macro + fib : Term → Term → TC _ + fib t hole = unify hole (def (quote fib') (arg i t ∷ [])) + where i = arg-info visible (modality relevant quantity-ω) + +{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -} diff --git a/entries/ionathanch/agda/Fib.agda b/entries/ionathanch/agda/Fib.agda deleted file mode 100644 index a12b0a5..0000000 --- a/entries/ionathanch/agda/Fib.agda +++ /dev/null @@ -1,19 +0,0 @@ - -open import Agda.Builtin.Nat -open import Agda.Builtin.List -open import Agda.Builtin.Reflection - -data Fib : Nat → Nat → Set where - instance F0 : Fib 0 0 - instance F1 : Fib 1 1 - instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m) - -fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat -fib' k {n} ⦃ fib ⦄ = n - -macro - fib : Term → Term → TC _ - fib t hole = unify hole (def (quote fib') (arg i t ∷ [])) - where i = arg-info visible (modality relevant quantity-ω) - -{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -} diff --git a/entries/ionathanch/fib.f90 b/entries/ionathanch/fib.f90 new file mode 100644 index 0000000..3cf1850 --- /dev/null +++ b/entries/ionathanch/fib.f90 @@ -0,0 +1,21 @@ +PROGRAM main + ! The 93rd Fibonacci number is the largest that fits in 64 bits anyway + CHARACTER(3) :: kth + INTEGER :: k + CALL get_command_argument(1, kth) + READ(kth, *) k + WRITE(*, *) fib(k) +CONTAINS + +PURE RECURSIVE INTEGER*8 FUNCTION fib(k) RESULT(n) + INTEGER, INTENT (IN) :: k + IF (k == 0) THEN + n = 0 + ELSE IF (k == 1) THEN + n = 1 + ELSE + n = fib(k - 1) + fib(k - 2) + END IF +END FUNCTION fib + +END PROGRAM -- cgit v1.2.3-70-g09d2