From 363ebc8f045054b5b5607a5058d63c1aeab5e0c7 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 12:16:40 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20appendo3=20=E2=80=94=203-list=20append?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Composes two appendos: (appendo a b mid) ∧ (appendo mid c r). Runs forward (concatenate three known lists) and backward (recover any of the three from the other two and the result). 5 new tests, 491/491 cumulative. --- lib/minikanren/relations.sx | 8 +++++- lib/minikanren/tests/appendo3.sx | 49 ++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 3 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 lib/minikanren/tests/appendo3.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index 8f18d87b..c3e5c53f 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -42,6 +42,12 @@ ;; --- membero --- ;; (membero x l) — x appears (at least once) in l. +(define + appendo3 + (fn + (l1 l2 l3 result) + (fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result)))) + (define membero (fn @@ -82,8 +88,8 @@ ((nullo l) (== result acc)) ((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result)))))) -(define rev-2o (fn (l result) (rev-acco l (list) result))) +(define rev-2o (fn (l result) (rev-acco l (list) result))) (define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev)))) diff --git a/lib/minikanren/tests/appendo3.sx b/lib/minikanren/tests/appendo3.sx new file mode 100644 index 00000000..36f58269 --- /dev/null +++ b/lib/minikanren/tests/appendo3.sx @@ -0,0 +1,49 @@ +;; lib/minikanren/tests/appendo3.sx — 3-list append. + +(mk-test + "appendo3-forward" + (run* + q + (appendo3 + (list 1 2) + (list 3 4) + (list 5 6) + q)) + (list + (list 1 2 3 4 5 6))) + +(mk-test + "appendo3-empty-everything" + (run* q (appendo3 (list) (list) (list) q)) + (list (list))) + +(mk-test + "appendo3-recover-middle" + (run* + q + (appendo3 + (list 1 2) + q + (list 5 6) + (list 1 2 3 4 5 6))) + (list (list 3 4))) + +(mk-test + "appendo3-empty-middle" + (run* + q + (appendo3 + (list 1 2) + (list) + (list 3 4) + q)) + (list (list 1 2 3 4))) + +(mk-test + "appendo3-empty-first-and-last" + (run* + q + (appendo3 (list) (list 1 2 3) (list) q)) + (list (list 1 2 3))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index c55abc7d..a3a3e49f 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **appendo3**: 3-list append via two appendos. (appendo3 a b c r) is (appendo a b mid) ∧ (appendo mid c r). Recovers any of the three lists given the other two and the result. 5 new tests, 491/491 cumulative. - **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.