mk: not-membero — relational "x is not in l"
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Mirrors the structure all-distincto already uses internally: walk the
list, ensure each element is not equal to x via nafc, recurse on tail.
Useful as a constraint-style filter:
(membero x (list 1 2 3 4 5))
(not-membero x (list 2 4))
-> x in {1, 3, 5}
4 new tests, 382/382 cumulative.
This commit is contained in:
@@ -50,6 +50,14 @@
|
|||||||
((fresh (d) (conso x d l)))
|
((fresh (d) (conso x d l)))
|
||||||
((fresh (a d) (conso a d l) (membero x d))))))
|
((fresh (a d) (conso a d l) (membero x d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
not-membero
|
||||||
|
(fn
|
||||||
|
(x l)
|
||||||
|
(conde
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d))))))
|
||||||
|
|
||||||
(define
|
(define
|
||||||
reverseo
|
reverseo
|
||||||
(fn
|
(fn
|
||||||
@@ -82,6 +90,7 @@
|
|||||||
((nullo l) (nullo p))
|
((nullo l) (nullo p))
|
||||||
((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))
|
((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))
|
||||||
|
|
||||||
|
|
||||||
(define
|
(define
|
||||||
flatteno
|
flatteno
|
||||||
(fn
|
(fn
|
||||||
@@ -97,7 +106,6 @@
|
|||||||
(appendo hf tf flat)))
|
(appendo hf tf flat)))
|
||||||
((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
|
((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
|
||||||
|
|
||||||
|
|
||||||
(define
|
(define
|
||||||
rembero
|
rembero
|
||||||
(fn
|
(fn
|
||||||
|
|||||||
29
lib/minikanren/tests/not-membero.sx
Normal file
29
lib/minikanren/tests/not-membero.sx
Normal file
@@ -0,0 +1,29 @@
|
|||||||
|
;; lib/minikanren/tests/not-membero.sx — relational "not in list".
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"not-membero-absent"
|
||||||
|
(run* q (not-membero 99 (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"not-membero-present"
|
||||||
|
(run* q (not-membero 2 (list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
(mk-test
|
||||||
|
"not-membero-empty"
|
||||||
|
(run* q (not-membero 1 (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"not-membero-as-filter"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(membero
|
||||||
|
x
|
||||||
|
(list 1 2 3 4 5))
|
||||||
|
(not-membero x (list 2 4))
|
||||||
|
(== q x)))
|
||||||
|
(list 1 3 5))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
@@ -173,6 +173,10 @@ _(none yet)_
|
|||||||
|
|
||||||
_Newest first._
|
_Newest first._
|
||||||
|
|
||||||
|
- **2026-05-08** — **not-membero**: relational "x is not a member of l".
|
||||||
|
Uses `nafc + ==` per element (the same skeleton all-distincto uses).
|
||||||
|
Useful as a constraint-style filter: `(membero x dom) (not-membero x
|
||||||
|
excluded)`. 4 new tests, 382/382 cumulative.
|
||||||
- **2026-05-08** — **repeato + concato**: repeato builds a list of n copies
|
- **2026-05-08** — **repeato + concato**: repeato builds a list of n copies
|
||||||
(Peano n); concato is fold-appendo over a list of lists. Both run forward
|
(Peano n); concato is fold-appendo over a list of lists. Both run forward
|
||||||
and backward — repeato can recover the count from a uniform list. 10 new
|
and backward — repeato can recover the count from a uniform list. 10 new
|
||||||
|
|||||||
Reference in New Issue
Block a user