mk: tako + dropo — Peano-indexed prefix and suffix
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s

(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.
This commit is contained in:
2026-05-08 11:32:33 +00:00
parent 54a58c704e
commit 8c48a0be63
3 changed files with 111 additions and 0 deletions

View File

@@ -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))))))

View File

@@ -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!)

View File

@@ -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