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