mk: partitiono — split list by predicate
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 26s

(partitiono pred l yes no) — yes is the elements of l where pred
succeeds; no is the rest. Conde dispatches on each element via the
predicate goal vs nafc-of-the-predicate, threading the head through
the matching output list.

Composes with intarith / membero / etc. for any predicate-shaped goal:
  (partitiono (fn (x) (lto-i x 5)) (list 1 7 2 8 3) yes no)
    yes -> (1 2 3); no -> (7 8)

5 new tests, 496/496 cumulative.
This commit is contained in:
2026-05-08 12:18:25 +00:00
parent 363ebc8f04
commit 221c7fef35
3 changed files with 85 additions and 1 deletions

View File

@@ -48,6 +48,14 @@
(l1 l2 l3 result)
(fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result))))
(define
partitiono
(fn
(pred l yes no)
(conde
((nullo l) (nullo yes) (nullo no))
((fresh (a d y-rest n-rest) (conso a d l) (conde ((pred a) (conso a y-rest yes) (== no n-rest) (partitiono pred d y-rest n-rest)) ((nafc (pred a)) (== yes y-rest) (conso a n-rest no) (partitiono pred d y-rest n-rest))))))))
(define
membero
(fn
@@ -80,6 +88,7 @@
((nullo l) (nullo r))
((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
(define
rev-acco
(fn
@@ -88,7 +97,6 @@
((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 palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))

View File

@@ -0,0 +1,75 @@
;; lib/minikanren/tests/partitiono.sx — partition list by predicate.
(mk-test
"partitiono-empty"
(run*
q
(fresh
(yes no)
(partitiono (fn (x) (== x 1)) (list) yes no)
(== q (list yes no))))
(list (list (list) (list))))
(mk-test
"partitiono-by-equality"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (== x 2))
(list 1 2 3 2 4)
yes
no)
(== q (list yes no))))
(list
(list
(list 2 2)
(list 1 3 4))))
(mk-test
"partitiono-by-numeric-pred"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i x 5))
(list 1 7 2 8 3)
yes
no)
(== q (list yes no))))
(list
(list
(list 1 2 3)
(list 7 8))))
(mk-test
"partitiono-all-yes"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i x 100))
(list 1 2 3)
yes
no)
(== q (list yes no))))
(list (list (list 1 2 3) (list))))
(mk-test
"partitiono-all-no"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i 100 x))
(list 1 2 3)
yes
no)
(== q (list yes no))))
(list (list (list) (list 1 2 3))))
(mk-tests-run!)