From c4b6f1fa0fedf5b8f1c40b4c62006d7bdc742857 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 12:10:52 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20sortedo=20=E2=80=94=20list=20is=20non-dec?=
 =?UTF-8?q?reasing=20(intarith)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three conde clauses: empty list / singleton list / two-or-more (where
the first two satisfy lteo-i and the rest is recursively sorted). Uses
ground-only integer comparison (intarith), so the input list must
walk to ground integers.

7 new tests, 463/463 cumulative.
---
 lib/minikanren/intarith.sx      |  9 ++++++++
 lib/minikanren/tests/sortedo.sx | 40 +++++++++++++++++++++++++++++++++
 plans/minikanren-on-sx.md       |  1 +
 3 files changed, 50 insertions(+)
 create mode 100644 lib/minikanren/tests/sortedo.sx

diff --git a/lib/minikanren/intarith.sx b/lib/minikanren/intarith.sx
index ed3692a9..108caf86 100644
--- a/lib/minikanren/intarith.sx
+++ b/lib/minikanren/intarith.sx
@@ -68,3 +68,12 @@
 (define
   odd-i
   (fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))
+
+(define
+  sortedo
+  (fn
+    (l)
+    (conde
+      ((nullo l))
+      ((fresh (a) (== l (list a))))
+      ((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid))))))
diff --git a/lib/minikanren/tests/sortedo.sx b/lib/minikanren/tests/sortedo.sx
new file mode 100644
index 00000000..6137da0c
--- /dev/null
+++ b/lib/minikanren/tests/sortedo.sx
@@ -0,0 +1,40 @@
+;; lib/minikanren/tests/sortedo.sx — checks list is non-decreasing.
+
+(mk-test
+  "sortedo-empty"
+  (run* q (sortedo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-singleton"
+  (run* q (sortedo (list 42)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-ascending"
+  (run* q (sortedo (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-with-equal-adjacent"
+  (run*
+    q
+    (sortedo (list 1 1 2 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-out-of-order-fails"
+  (run* q (sortedo (list 1 3 2)))
+  (list))
+
+(mk-test
+  "sortedo-descending-fails"
+  (run* q (sortedo (list 3 2 1)))
+  (list))
+
+(mk-test
+  "sortedo-pair-equal"
+  (run* q (sortedo (list 5 5)))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index b34ccb53..3a05e6c6 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -173,6 +173,7 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-08** — **sortedo (intarith)**: list is non-decreasing under integer ordering. Three conde clauses: empty / singleton / pair-and-recurse. Uses lteo-i for the adjacent-pair check (ground integers). 7 new tests, 463/463 cumulative.
 - **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.