mk: swap-firsto — swap first two list elements
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 48s

Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a
purely relational constraint. Self-inverse on length-2+ lists; runs
forward (swap given input) and backward (recover original from the
swapped form). Fails on lists shorter than 2.

6 new tests, 437/437 cumulative.
This commit is contained in:
2026-05-08 11:59:41 +00:00
parent c04ddd105b
commit eb69039935
3 changed files with 44 additions and 0 deletions

View File

@@ -198,6 +198,17 @@
((nullo l1) (nullo l2) (nullo pairs))
((fresh (a1 d1 a2 d2 d-pairs) (conso a1 d1 l1) (conso a2 d2 l2) (conso (list a1 a2) d-pairs pairs) (pairlisto d1 d2 d-pairs))))))
(define
swap-firsto
(fn
(l result)
(fresh
(a b rest mid-l mid-r)
(conso a mid-l l)
(conso b rest mid-l)
(conso b mid-r result)
(conso a rest mid-r))))
(define
everyo
(fn

View File

@@ -0,0 +1,32 @@
;; lib/minikanren/tests/swap-firsto.sx — swap first two elements.
(mk-test
"swap-firsto-pair"
(run* q (swap-firsto (list 1 2) q))
(list (list 2 1)))
(mk-test
"swap-firsto-with-tail"
(run* q (swap-firsto (list 1 2 3 4) q))
(list (list 2 1 3 4)))
(mk-test
"swap-firsto-singleton-fails"
(run* q (swap-firsto (list 1) q))
(list))
(mk-test "swap-firsto-empty-fails" (run* q (swap-firsto (list) q)) (list))
(mk-test
"swap-firsto-self-inverse"
(run*
q
(fresh (mid) (swap-firsto (list :a :b :c :d) mid) (swap-firsto mid q)))
(list (list :a :b :c :d)))
(mk-test
"swap-firsto-backward"
(run* q (swap-firsto q (list :y :x :z)))
(list (list :x :y :z)))
(mk-tests-run!)