diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index 8a2cdcda..8f18d87b 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -58,6 +58,14 @@ ((nullo l)) ((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d)))))) +(define + subseto + (fn + (l1 l2) + (conde + ((nullo l1)) + ((fresh (a d) (conso a d l1) (membero a l2) (subseto d l2)))))) + (define reverseo (fn @@ -76,8 +84,8 @@ (define rev-2o (fn (l result) (rev-acco l (list) result))) -(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev)))) +(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev)))) (define prefixo (fn (p l) (fresh (rest) (appendo p rest l)))) diff --git a/lib/minikanren/tests/subseto.sx b/lib/minikanren/tests/subseto.sx new file mode 100644 index 00000000..68c4cf82 --- /dev/null +++ b/lib/minikanren/tests/subseto.sx @@ -0,0 +1,62 @@ +;; lib/minikanren/tests/subseto.sx — every element of l1 is in l2. + +(mk-test + "subseto-empty" + (run* q (subseto (list) (list 1 2 3))) + (list (make-symbol "_.0"))) + +(mk-test + "subseto-singleton-yes" + (run* + q + (subseto (list 2) (list 1 2 3))) + (list (make-symbol "_.0"))) + +(mk-test + "subseto-singleton-no" + (run* + q + (subseto (list 99) (list 1 2 3))) + (list)) + +(mk-test + "subseto-multi-yes" + (run + 1 + q + (subseto + (list 1 3) + (list 1 2 3 4))) + (list (make-symbol "_.0"))) + +(mk-test + "subseto-multi-no" + (run* + q + (subseto + (list 1 99) + (list 1 2 3))) + (list)) + +(mk-test + "subseto-equal-sets" + (run + 1 + q + (subseto + (list 1 2 3) + (list 1 2 3))) + (list (make-symbol "_.0"))) + +;; allow duplicates in l1 — each just needs membership in l2. +(mk-test + "subseto-duplicates-allowed" + (run + 1 + q + (subseto + (list 1 1 2) + (list 1 2 3))) + (list (make-symbol "_.0"))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 300c3661..b34ccb53 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **subseto**: every element of l1 is a member of l2. Recurses on l1, checking each element via membero. Allows duplicates in l1 (each independently in l2). 7 new tests, 456/456 cumulative. - **2026-05-08** — **cycle-free path search**: mitigation for the cyclic-graph divergence — thread a accumulator through the recursion, gate each step with nafc + membero on visited. Terminates on graphs with cycles; no Phase-7 tabling required for the simple case. 3 new tests, 449/449 cumulative. - **2026-05-08** — **removeo-allo**: removes every occurrence of x (vs rembero, which removes only the first). Three conde clauses: empty -> empty; head matches -> skip and recurse; head differs (nafc) -> keep and recurse. 5 new tests, 446/446 cumulative. - **2026-05-08** — **btree-walko (matche showcase)**: walks a binary tree (:leaf v) | (:node l r) and emits each leaf value via conde. Demonstrates matche dispatch on tagged-list patterns, recursion through both branches via conde, and run* enumerating all 5 leaves of a small tree. 4 new tests, 441/441 cumulative.