mk: phase 4C — permuteo (with inserto helper)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s

inserto a l p: p is l with a inserted at some position. Recursive: head
of l first, then push past head and recurse.

permuteo l p: classical recursive permutation. Empty -> empty; otherwise
take a head off l, recursively permute the tail, insert head at any
position in the recursive result.

7 new tests including all-6-perms-of-3 as a set check (independent of
generation order). 208/208 cumulative.
This commit is contained in:
2026-05-08 07:22:41 +00:00
parent a038d41815
commit b8a0c504bc
3 changed files with 86 additions and 1 deletions

View File

@@ -65,3 +65,19 @@
(conde
((nullo l) (== n :z))
((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))
(define
inserto
(fn
(a l p)
(conde
((conso a l p))
((fresh (h t pt) (conso h t l) (conso h pt p) (inserto a t pt))))))
(define
permuteo
(fn
(l p)
(conde
((nullo l) (nullo p))
((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))