From 7ff72cefb24f3c88d12049776e5606496ad01dc0 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 12:15:53 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20lengtho-i=20=E2=80=94=20integer-indexed?= =?UTF-8?q?=20length?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drop-in fast replacement for Peano lengtho when the count fits in a host integer. Two conde clauses: empty list -> 0; recurse, n = 1 + length(tail). Uses pluso-i so the length walks to a native int. 5 new tests, 486/486 cumulative. --- lib/minikanren/intarith.sx | 8 ++++++++ lib/minikanren/tests/lengtho-i.sx | 28 ++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 3 files changed, 37 insertions(+) create mode 100644 lib/minikanren/tests/lengtho-i.sx diff --git a/lib/minikanren/intarith.sx b/lib/minikanren/intarith.sx index 015bea2d..e9548b4b 100644 --- a/lib/minikanren/intarith.sx +++ b/lib/minikanren/intarith.sx @@ -109,3 +109,11 @@ (conde ((nullo l) (== total 1)) ((fresh (a d rest-prod) (conso a d l) (producto d rest-prod) (*o-i a rest-prod total)))))) + +(define + lengtho-i + (fn + (l n) + (conde + ((nullo l) (== n 0)) + ((fresh (a d n-1) (conso a d l) (lengtho-i d n-1) (pluso-i 1 n-1 n)))))) diff --git a/lib/minikanren/tests/lengtho-i.sx b/lib/minikanren/tests/lengtho-i.sx new file mode 100644 index 00000000..6759e24e --- /dev/null +++ b/lib/minikanren/tests/lengtho-i.sx @@ -0,0 +1,28 @@ +;; lib/minikanren/tests/lengtho-i.sx — integer-indexed length (fast). + +(mk-test "lengtho-i-empty" (run* q (lengtho-i (list) q)) (list 0)) +(mk-test + "lengtho-i-singleton" + (run* q (lengtho-i (list :a) q)) + (list 1)) +(mk-test + "lengtho-i-three" + (run* q (lengtho-i (list 1 2 3) q)) + (list 3)) +(mk-test + "lengtho-i-five" + (run* + q + (lengtho-i + (list 1 2 3 4 5) + q)) + (list 5)) + +(mk-test + "lengtho-i-mixed-types" + (run* + q + (lengtho-i (list 1 "two" :three (list 4 5)) q)) + (list 4)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 5ba00636..c55abc7d 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **lengtho-i**: integer-indexed length (intarith). Empty list -> 0; recurse with pluso-i. Drop-in fast replacement for Peano lengtho when the count fits in a host integer. 5 new tests, 486/486 cumulative. - **2026-05-08** — **sumo + producto (intarith)**: fold a list of ground integers to its sum or product. Empty list -> identity (0 / 1). Recurse via pluso-i / *o-i. 9 new tests, 481/481 cumulative. - **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative. - **2026-05-08** — **sortedo (intarith)**: list is non-decreasing under integer ordering. Three conde clauses: empty / singleton / pair-and-recurse. Uses lteo-i for the adjacent-pair check (ground integers). 7 new tests, 463/463 cumulative.