From 8c48a0be63a17bb0550dae931c0c608d04beda65 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:32:33 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20tako=20+=20dropo=20=E2=80=94=20Peano-inde?= =?UTF-8?q?xed=20prefix=20and=20suffix?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (tako n l prefix) — prefix is the first n elements of l. (dropo n l suffix) — suffix is l after dropping the first n. Both use a Peano natural for the count. Round-trip holds: (tako n l) ⊕ (dropo n l) = l (verified by an end-to-end test) 9 new tests, 368/368 cumulative. --- lib/minikanren/relations.sx | 16 ++++++ lib/minikanren/tests/take-drop.sx | 92 +++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 3 + 3 files changed, 111 insertions(+) create mode 100644 lib/minikanren/tests/take-drop.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index 60200c86..b9f382c5 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -172,3 +172,19 @@ (conde ((fresh (x) (conso x (list) l) (== init (list)))) ((fresh (a d d-init) (conso a d l) (conso a d-init init) (init-o d d-init)))))) + +(define + tako + (fn + (n l prefix) + (conde + ((== n :z) (== prefix (list))) + ((fresh (n-1 a d p-rest) (== n (list :s n-1)) (conso a d l) (conso a p-rest prefix) (tako n-1 d p-rest)))))) + +(define + dropo + (fn + (n l suffix) + (conde + ((== n :z) (== suffix l)) + ((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (dropo n-1 d suffix)))))) diff --git a/lib/minikanren/tests/take-drop.sx b/lib/minikanren/tests/take-drop.sx new file mode 100644 index 00000000..c8c2959d --- /dev/null +++ b/lib/minikanren/tests/take-drop.sx @@ -0,0 +1,92 @@ +;; lib/minikanren/tests/take-drop.sx — Peano-indexed prefix/suffix. + +(define + mk-nat + (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1)))))) + +;; --- tako --- + +(mk-test + "tako-zero" + (run* + q + (tako (mk-nat 0) (list 1 2 3) q)) + (list (list))) + +(mk-test + "tako-two" + (run* + q + (tako + (mk-nat 2) + (list 1 2 3 4 5) + q)) + (list (list 1 2))) + +(mk-test + "tako-all" + (run* + q + (tako (mk-nat 3) (list 1 2 3) q)) + (list (list 1 2 3))) + +(mk-test + "tako-too-many" + (run* + q + (tako (mk-nat 5) (list 1 2 3) q)) + (list)) + +;; --- dropo --- + +(mk-test + "dropo-zero" + (run* + q + (dropo (mk-nat 0) (list 1 2 3) q)) + (list (list 1 2 3))) + +(mk-test + "dropo-two" + (run* + q + (dropo + (mk-nat 2) + (list 1 2 3 4 5) + q)) + (list (list 3 4 5))) + +(mk-test + "dropo-all" + (run* + q + (dropo (mk-nat 3) (list 1 2 3) q)) + (list (list))) + +(mk-test + "dropo-too-many" + (run* + q + (dropo (mk-nat 5) (list 1 2 3) q)) + (list)) + +;; --- take + drop round-trip --- + +(mk-test + "tako-dropo-roundtrip" + (run* + q + (fresh + (p s) + (tako + (mk-nat 2) + (list 1 2 3 4 5) + p) + (dropo + (mk-nat 2) + (list 1 2 3 4 5) + s) + (appendo p s q))) + (list (list 1 2 3 4 5))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 9834c5c4..a2640338 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,9 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **tako + dropo (Peano-indexed prefix/suffix)**: takes / drops + the first n elements via a Peano-encoded count. Round-trip + `(tako n l) ⊕ (dropo n l) = l` holds. 9 new tests, 368/368 cumulative. - **2026-05-08** — **eveno / oddo Peano predicates**: classic miniKanren parity relations. eveno: 0 or successor-of-successor of even; oddo: 1 or successor-of-successor of odd. Both run forward (test) and backward