mk: simplify-step-o — algebraic-identity simplifier (conda demo)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s

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.
This commit is contained in:
2026-05-08 12:25:36 +00:00
parent 091030f13e
commit d891831f08

View File

@@ -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!)