mk: selecto — choose element + rest of list
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s

Classic miniKanren relation. (selecto x rest l) holds when l contains
x at any position with `rest` being everything else. Direct base case
(l = (x . rest)) plus the skip-head recursion that threads the head
through to the result rest.

Run modes: enumerate every (x, rest) split; recover rest given an
element; recover an element given the rest; (and ground/all combinations).

6 new tests, 411/411 cumulative.
This commit is contained in:
2026-05-08 11:47:27 +00:00
parent e202c81a0d
commit 4d861575df
3 changed files with 55 additions and 0 deletions

View File

@@ -82,6 +82,14 @@
(appendo front-and-s back l)
(appendo front s front-and-s))))
(define
selecto
(fn
(x rest l)
(conde
((conso x rest l))
((fresh (a d r) (conso a d l) (conso a r rest) (selecto x r d))))))
(define
lengtho
(fn

View File

@@ -0,0 +1,46 @@
;; lib/minikanren/tests/selecto.sx — choose an element + rest of list.
(mk-test
"selecto-enumerate"
(run*
q
(fresh
(x r)
(selecto x r (list 1 2 3))
(== q (list x r))))
(list
(list 1 (list 2 3))
(list 2 (list 1 3))
(list 3 (list 1 2))))
(mk-test
"selecto-find-rest"
(run* q (selecto 2 q (list 1 2 3)))
(list (list 1 3)))
(mk-test
"selecto-find-element"
(run*
q
(selecto
q
(list 1 3)
(list 1 2 3)))
(list 2))
(mk-test
"selecto-element-not-present-fails"
(run* q (selecto 99 q (list 1 2 3)))
(list))
(mk-test
"selecto-empty-list-fails"
(run* q (selecto q (list) (list)))
(list))
(mk-test
"selecto-singleton"
(run* q (fresh (x r) (selecto x r (list :only)) (== q (list x r))))
(list (list :only (list))))
(mk-tests-run!)

View File

@@ -173,6 +173,7 @@ _(none yet)_
_Newest first._
- **2026-05-08** — **selecto**: classic miniKanren "choose an element + rest". Direct base (l = (x . rest)) plus skip-head recurse. Enumerates all (element, rest) splits in run*; runs forward, backward, mid-pipeline. 6 new tests, 411/411 cumulative.
- **2026-05-08** — **subo (contiguous sublist)**: Two appendos chained — l = front ++ s ++ back. Goal order matters: appendo on the ground l first, so the search is finitary; then constrain front. 7 new tests, 405/405 cumulative.
- **2026-05-08** — **prefixo + suffixo**: classic appendo-derived sublist relations. (prefixo p l) ≡ p ⊕ ? = l; (suffixo s l) ≡ ? ⊕ s = l. Both enumerate all prefixes/suffixes when given a fresh first arg. 9 new tests, 398/398 cumulative.
- **2026-05-08** — **palindromeo**: 2-line definition (reverseo + ==). Succeeds when a list reads the same forwards and backwards. 7 new tests, 389/389 cumulative.