From d891831f0813ff0bfd57b2f8bc43b14e6afb0c68 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 12:25:36 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20simplify-step-o=20=E2=80=94=20algebraic-i?=
 =?UTF-8?q?dentity=20simplifier=20(conda=20demo)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Demonstrates conda for first-match-wins dispatch over a set of rewrite
rules: 0+x = x, x+0 = x, 0*y = 0, x*0 = 0, 1*x = x, x*1 = x, default
unchanged.

Six rules + a fall-through default, all wrapped in a single conda. The
first clause whose head succeeds commits to that rewrite. The fall-
through default ensures the relation always succeeds with at least the
unchanged input.

6 new tests, 521/521 cumulative.
---
 lib/minikanren/tests/simplifyo.sx | 47 +++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 lib/minikanren/tests/simplifyo.sx

diff --git a/lib/minikanren/tests/simplifyo.sx b/lib/minikanren/tests/simplifyo.sx
new file mode 100644
index 00000000..02a56e0b
--- /dev/null
+++ b/lib/minikanren/tests/simplifyo.sx
@@ -0,0 +1,47 @@
+;; lib/minikanren/tests/simplifyo.sx — algebraic expression simplifier
+;; demo using conda for first-match-wins dispatch.
+
+(define
+  simplify-step-o
+  (fn
+    (expr result)
+    (conda
+      ((fresh (x) (== expr (list :+ 0 x)) (== result x)))
+      ((fresh (x) (== expr (list :+ x 0)) (== result x)))
+      ((fresh (y) (== expr (list :* 0 y)) (== result 0)))
+      ((fresh (x) (== expr (list :* x 0)) (== result 0)))
+      ((fresh (x) (== expr (list :* 1 x)) (== result x)))
+      ((fresh (x) (== expr (list :* x 1)) (== result x)))
+      ((== result expr)))))                                  ;; default: unchanged
+
+(mk-test
+  "simplify-zero-plus"
+  (run* q (simplify-step-o (list :+ 0 :y) q))
+  (list :y))
+
+(mk-test
+  "simplify-plus-zero"
+  (run* q (simplify-step-o (list :+ :x 0) q))
+  (list :x))
+
+(mk-test
+  "simplify-zero-times"
+  (run* q (simplify-step-o (list :* 0 :y) q))
+  (list 0))
+
+(mk-test
+  "simplify-one-times"
+  (run* q (simplify-step-o (list :* 1 :y) q))
+  (list :y))
+
+(mk-test
+  "simplify-no-rule-applies"
+  (run* q (simplify-step-o (list :+ :x :y) q))
+  (list (list :+ :x :y)))
+
+(mk-test
+  "simplify-non-identity-form"
+  (run* q (simplify-step-o (list :+ 5 7) q))
+  (list (list :+ 5 7)))
+
+(mk-tests-run!)