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.
48 lines
1.2 KiB
Plaintext
48 lines
1.2 KiB
Plaintext
;; 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!)
|