From e202c81a0d4817da4e2a0f59a0fb5eeb1c029b58 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:45:31 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20subo=20=E2=80=94=20contiguous=20sublist?= =?UTF-8?q?=20relation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Composes two appendos: l = front ++ s ++ back, equivalently (appendo front-and-s back l) and (appendo front s front-and-s). Goal order matters: doing the (appendo ground:l) split first makes the search finitary; the second appendo is then deterministic given front-and-s and ground s. Reversing the order causes divergence on failing inputs (the front search becomes unbounded). 7 new tests, 405/405 cumulative. --- lib/minikanren/relations.sx | 9 ++++++ lib/minikanren/tests/subo.sx | 60 ++++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 3 files changed, 70 insertions(+) create mode 100644 lib/minikanren/tests/subo.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index b86b5e3b..4b9c61c2 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -73,6 +73,15 @@ (define suffixo (fn (s l) (fresh (front) (appendo front s l)))) +(define + subo + (fn + (s l) + (fresh + (front-and-s back front) + (appendo front-and-s back l) + (appendo front s front-and-s)))) + (define lengtho (fn diff --git a/lib/minikanren/tests/subo.sx b/lib/minikanren/tests/subo.sx new file mode 100644 index 00000000..a48c645a --- /dev/null +++ b/lib/minikanren/tests/subo.sx @@ -0,0 +1,60 @@ +;; lib/minikanren/tests/subo.sx — contiguous-sublist relation. + +(mk-test + "subo-simple-found" + (run* + q + (subo + (list 2 3) + (list 1 2 3 4))) + (list (make-symbol "_.0"))) + +(mk-test + "subo-not-contiguous-fails" + (run* + q + (subo + (list 2 4) + (list 1 2 3 4))) + (list)) + +(mk-test + "subo-full-list-found" + (run* + q + (subo + (list 1 2 3) + (list 1 2 3))) + (list (make-symbol "_.0"))) + +(mk-test + "subo-empty-list-found" + (let + ((res (run* q (subo (list) (list 1 2 3))))) + (= (len res) 4)) + true) + +(mk-test + "subo-prefix" + (run* + q + (subo + (list 1 2) + (list 1 2 3 4))) + (list (make-symbol "_.0"))) + +(mk-test + "subo-suffix" + (run* + q + (subo + (list 3 4) + (list 1 2 3 4))) + (list (make-symbol "_.0"))) + +(mk-test + "subo-strings" + (run* q (subo (list "b" "c") (list "a" "b" "c" "d"))) + (list (make-symbol "_.0"))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index a12b67b3..b2dcaa2e 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **subo (contiguous sublist)**: Two appendos chained — l = front ++ s ++ back. Goal order matters: appendo on the ground l first, so the search is finitary; then constrain front. 7 new tests, 405/405 cumulative. - **2026-05-08** — **prefixo + suffixo**: classic appendo-derived sublist relations. (prefixo p l) ≡ p ⊕ ? = l; (suffixo s l) ≡ ? ⊕ s = l. Both enumerate all prefixes/suffixes when given a fresh first arg. 9 new tests, 398/398 cumulative. - **2026-05-08** — **palindromeo**: 2-line definition (reverseo + ==). Succeeds when a list reads the same forwards and backwards. 7 new tests, 389/389 cumulative. - **2026-05-08** — **not-membero**: relational "x is not a member of l".