giles
863e9d93a4
Pure-functional pattern-match + unification, shipped for miniKanren
(minikraken) / Datalog and any other logic-flavoured guest that wants
immutable unification without writing it from scratch.
Canonical wire format (config callbacks let other shapes plug in):
var (:var NAME)
constructor (:ctor HEAD ARGS)
literal number / string / boolean / nil
Public API:
empty-subst walk walk* extend occurs?
unify (symmetric, with occurs check)
unify-with (cfg-driven for non-canonical term shapes)
match-pat (asymmetric pattern→value, vars only in pattern)
match-pat-with (cfg-driven)
lib/guest/tests/match.sx — 25 tests covering walk chains, occurs,
unify (literal/var/ctor, head + arity mismatch, transitive vars),
match-pat. All passing.
The brief flagged this as the highest-risk step ("revert and redesign
on any regression"). The two existing engines — haskell/match.sx
(pure asymmetric, lazy, returns env-or-nil) and prolog runtime.sx
pl-unify! (mutating symmetric, trail-based, returns bool) — are
structurally divergent and forcing a shared core under either of their
contracts would risk the 746 tests they currently pass. Both are
untouched; they remain at baseline (haskell 156/156, prolog 590/590)
because none of their source files were modified.
PARTIAL — kit shipped, prolog/haskell ports deferred until a guest
chooses to migrate or until a third consumer (minikraken / datalog)
provides a less risky migration path.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
109 lines
3.8 KiB
Plaintext
109 lines
3.8 KiB
Plaintext
;; lib/guest/tests/match.sx — exercises lib/guest/match.sx.
|
|
|
|
(define gmatch-test-pass 0)
|
|
(define gmatch-test-fail 0)
|
|
(define gmatch-test-fails (list))
|
|
|
|
(define
|
|
gmatch-test
|
|
(fn (name actual expected)
|
|
(if (= actual expected)
|
|
(set! gmatch-test-pass (+ gmatch-test-pass 1))
|
|
(begin
|
|
(set! gmatch-test-fail (+ gmatch-test-fail 1))
|
|
(append! gmatch-test-fails {:name name :expected expected :actual actual})))))
|
|
|
|
;; ── walk / extend / occurs ────────────────────────────────────────
|
|
(gmatch-test "walk-direct"
|
|
(walk (mk-var "x") (extend "x" 5 (empty-subst))) 5)
|
|
|
|
(gmatch-test "walk-chain"
|
|
(walk (mk-var "a") (extend "a" (mk-var "b") (extend "b" 7 (empty-subst)))) 7)
|
|
|
|
(gmatch-test "walk-no-binding"
|
|
(let ((v (mk-var "u"))) (= (walk v (empty-subst)) v)) true)
|
|
|
|
(gmatch-test "walk*-recursive"
|
|
(walk* (mk-ctor "Just" (list (mk-var "x"))) (extend "x" 9 (empty-subst)))
|
|
(mk-ctor "Just" (list 9)))
|
|
|
|
(gmatch-test "occurs-direct"
|
|
(occurs? "x" (mk-var "x") (empty-subst)) true)
|
|
|
|
(gmatch-test "occurs-nested"
|
|
(occurs? "x" (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) true)
|
|
|
|
(gmatch-test "occurs-not"
|
|
(occurs? "x" (mk-var "y") (empty-subst)) false)
|
|
|
|
;; ── unify (symmetric) ─────────────────────────────────────────────
|
|
(gmatch-test "unify-equal-literals"
|
|
(len (unify 5 5 (empty-subst))) 0)
|
|
|
|
(gmatch-test "unify-different-literals"
|
|
(unify 5 6 (empty-subst)) nil)
|
|
|
|
(gmatch-test "unify-var-literal"
|
|
(get (unify (mk-var "x") 5 (empty-subst)) "x") 5)
|
|
|
|
(gmatch-test "unify-literal-var"
|
|
(get (unify 5 (mk-var "x") (empty-subst)) "x") 5)
|
|
|
|
(gmatch-test "unify-same-var"
|
|
(len (unify (mk-var "x") (mk-var "x") (empty-subst))) 0)
|
|
|
|
(gmatch-test "unify-two-vars"
|
|
(let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
|
|
(or (= (get s "x") (mk-var "y")) (= (get s "y") (mk-var "x")))) true)
|
|
|
|
(gmatch-test "unify-ctor-equal"
|
|
(len (unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1 2)) (empty-subst))) 0)
|
|
|
|
(gmatch-test "unify-ctor-with-var"
|
|
(get (unify (mk-ctor "Just" (list (mk-var "x"))) (mk-ctor "Just" (list 7)) (empty-subst)) "x") 7)
|
|
|
|
(gmatch-test "unify-ctor-head-mismatch"
|
|
(unify (mk-ctor "Just" (list 1)) (mk-ctor "Nothing" (list)) (empty-subst)) nil)
|
|
|
|
(gmatch-test "unify-ctor-arity-mismatch"
|
|
(unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1)) (empty-subst)) nil)
|
|
|
|
(gmatch-test "unify-occurs-check"
|
|
(unify (mk-var "x") (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) nil)
|
|
|
|
(gmatch-test "unify-transitive-vars"
|
|
(let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
|
|
(let ((s2 (unify (mk-var "y") 42 s)))
|
|
(walk (mk-var "x") s2))) 42)
|
|
|
|
;; ── match-pat (asymmetric) ────────────────────────────────────────
|
|
(gmatch-test "match-var-binds"
|
|
(get (match-pat (mk-var "x") 99 (empty-subst)) "x") 99)
|
|
|
|
(gmatch-test "match-literal-equal"
|
|
(len (match-pat 5 5 (empty-subst))) 0)
|
|
|
|
(gmatch-test "match-literal-mismatch"
|
|
(match-pat 5 6 (empty-subst)) nil)
|
|
|
|
(gmatch-test "match-ctor-binds"
|
|
(get (match-pat (mk-ctor "Just" (list (mk-var "y")))
|
|
(mk-ctor "Just" (list 11))
|
|
(empty-subst)) "y") 11)
|
|
|
|
(gmatch-test "match-ctor-head-mismatch"
|
|
(match-pat (mk-ctor "Just" (list (mk-var "y")))
|
|
(mk-ctor "Nothing" (list))
|
|
(empty-subst)) nil)
|
|
|
|
(gmatch-test "match-ctor-arity-mismatch"
|
|
(match-pat (mk-ctor "f" (list (mk-var "x") (mk-var "y")))
|
|
(mk-ctor "f" (list 1))
|
|
(empty-subst)) nil)
|
|
|
|
(define gmatch-tests-run!
|
|
(fn ()
|
|
{:passed gmatch-test-pass
|
|
:failed gmatch-test-fail
|
|
:total (+ gmatch-test-pass gmatch-test-fail)}))
|