posts

posts/2022-10-24-fib.md

@@ -0,0 +1,92 @@
+---
+title: fibonacci in maude and ats
+date: 2022-10-24
+tags: [computer, maude, ATS]
+...
+
+i might submit these [here], if i can be bothered to get a new github account.
+
+[here]: https://braxtonhall.ca/fib/
+
+:::aside
+update: i did it
+:::
+
+
+# maude
+
+```maude
+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)
+```
+
+
+# ats
+
+```ats
+#include "share/atspre_define.hats"
+#include "share/atspre_staload.hats"
+
+// is_fib(i, n): n is the i-th fibonacci number
+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
+  // m, n : accs
+  // i : index of m
+  // t : target index
+  fun go {m, n, i, t : 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), t : int(t)) :<>
+        fib(t) =
+    if i = t then
+      (M | m)
+    else
+      go(N, Fplus(M, N) | n, m + n, i + 1, t)
+in
+  go(F0, F1 | 0, 1, 0, t)
+end
+
+fun fib_(i : Nat) : Nat = let val (_ | res) = fib(i) in res end
+
+implement main0() = println!("fib(15) = ", fib_(15))
+```
+
+```sh
+$ make fib
+$ ./fib
+fib(15) = 610
+```
+
+same makefile as [last time].
+
+[last time]: ./2022-09-16-ats.html#install

posts/2022-11-12-idris2-features.md

@@ -0,0 +1,102 @@
+---
+title: undocumented idris2 features
+date: 2022-11-12
+tags: [computer, idris]
+header-includes: |
+  <style>
+    .sidebyside {
+      display: grid;
+      grid-template-columns: 1fr 1fr;
+    }
+    .sidebyside :is(.input, .goal) {
+      box-sizing: border-box;
+      width:  95%;
+      height: 95%;
+    }
+    .sidebyside .input { grid-area: 0 / 1; }
+    .sidebyside .goal { grid-area: 1 / 2; }
+  </style>
+...
+
+if these are already in the documentation somewhere, i didn't find it.
+
+## quantities on case, let, with
+
+occasionally, idris can't infer that these expressions should be non-ω. usually
+when there are still holes in the definition, it seems. so you can specify the
+quantity you want directly after the keyword, for [example][viewLsb]:
+
+```idris
+export
+viewLsb : (n : Nat) -> ViewLsb n
+viewLsb n =
+  --  ↓ here
+  let 0 nz : NonZero 2 = %search in
+  rewrite DivisionTheorem n 2 nz nz in
+  rewrite multCommutative (divNatNZ n 2 nz) 2 in
+  viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
+```
+
+[viewLsb]: https://git.rhiannon.website/rhi/quox/src/branch/ope/lib/Quox/NatExtra.idr#L110-L116
+
+
+## syntactic with-abstraction
+
+using `with` can be costly, since it has to evaluate the expression being
+abstracted, as well as the types of the goal and bound variables, to find
+occurrences of it. maybe you know they are all already syntactically equal.
+in that case, you can say `… with %syntactic (expr)`:
+
+
+:::sidebyside
+``` {.idris .input}
+blah : (n : Nat) -> 2 * n = n + (n + 0)
+blah n with (2 * n)
+  blah n | w = ?blah_rhs
+```
+
+``` {.idris .goal}
+   w : Nat
+   n : Nat
+------------------------------
+blah_rhs : w = w
+```
+
+``` {.idris .input}
+blah2 : (n : Nat) -> 2 * n = n + (n + 0)
+blah2 n with %syntactic (2 * n)
+  blah2 n | w = ?blah2_rhs
+```
+
+``` {.idris .goal}
+   w : Nat
+   n : Nat
+------------------------------
+blah2_rhs : w = plus n (plus n 0)
+```
+:::
+
+in `blah2`, only the exact syntactic occurrence of `2 * n` is replaced, and
+the `n + (n + 0)` is left alone.
+
+
+## equality proof in with
+
+a `with`-abstraction can _also_ have a proof of equality between the pattern
+and the original expression, like the old inspect pattern.
+
+:::sidebyside
+``` {.idris .input}
+blah : (n : Nat) -> 2 * n = n + (n + 0)
+blah n with (2 * n) proof eq
+  blah n | w = ?blah_rhs
+```
+
+``` {.idris .goal}
+   w : Nat
+   n : Nat
+   eq : plus n (plus n 0) = w
+------------------------------
+blah_rhs : w = w
+```
+:::