From fd73f3c51b6701d26394256fadb2aa04ae6fb5e1 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 07:41:51 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20phase=205D=20=E2=80=94=20matche=20pattern?=
 =?UTF-8?q?=20matching,=20phase=205=20complete?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Pattern grammar: _, symbol, atom (number/string/keyword/bool), (), and
(p1 ... pn) list patterns (recursive). Symbols become fresh vars in a
fresh form, atoms become literals to unify against, lists recurse
position-wise. Repeated names produce the same fresh var (so they
unify by ==).

Macro is built with explicit cons/list rather than a quasiquote because
the quasiquote expander does not recurse into nested lambda bodies —
the natural `\`(matche-clause (quote ,target) cl)` spelling left
literal `(unquote target)` forms in the output.

14 tests, 222/222 cumulative. Phase 5 done (project, conda, condu,
onceo, nafc, matche all green).
---
 lib/minikanren/matche.sx       |  74 ++++++++++++++++++
 lib/minikanren/tests/matche.sx | 138 +++++++++++++++++++++++++++++++++
 plans/minikanren-on-sx.md      |  16 +++-
 3 files changed, 226 insertions(+), 2 deletions(-)
 create mode 100644 lib/minikanren/matche.sx
 create mode 100644 lib/minikanren/tests/matche.sx

diff --git a/lib/minikanren/matche.sx b/lib/minikanren/matche.sx
new file mode 100644
index 00000000..9d671c85
--- /dev/null
+++ b/lib/minikanren/matche.sx
@@ -0,0 +1,74 @@
+;; lib/minikanren/matche.sx — Phase 5 piece D: pattern matching over terms.
+;;
+;;   (matche TARGET
+;;     (PATTERN1 g1 g2 ...)
+;;     (PATTERN2 g1 ...)
+;;     ...)
+;;
+;; Each clause unifies TARGET with PATTERN, introducing a fresh variable
+;; for every plain symbol in the pattern, and runs its goal body. The
+;; pattern grammar:
+;;
+;;   _                 wildcard — fresh anonymous var
+;;   x                 plain symbol — fresh var, bind by name
+;;   ATOM              literal (number, string, keyword, boolean) — must equal
+;;   ()                empty list — must equal
+;;   (p1 p2 ... pn)    list pattern — recurse on each element
+;;
+;; The macro expands to a `conde` whose clauses are
+;;   `((fresh (vars...) (== target pat-expr) body...))`.
+;;
+;; Fixed-length list patterns only — no rest patterns. To match "head + rest",
+;; use `(fresh (a d) (conso a d target) body)` directly.
+;;
+;; Note: the macro builds the expansion via `cons` / `list` rather than a
+;; quasiquote — the quasiquote expander does not recurse into lambda
+;; bodies, which broke the natural `\`(matche-clause (quote ,target) cl)`
+;; spelling.
+
+(define matche-symbol-var? (fn (s) (symbol? s)))
+
+(define
+  matche-collect-vars
+  (fn (pat) (matche-collect-vars-acc pat (list))))
+
+(define
+  matche-collect-vars-acc
+  (fn
+    (pat acc)
+    (cond
+      ((matche-symbol-var? pat)
+        (if (some (fn (s) (= s pat)) acc) acc (append acc (list pat))))
+      ((and (list? pat) (not (empty? pat)))
+        (reduce (fn (a p) (matche-collect-vars-acc p a)) acc pat))
+      (:else acc))))
+
+(define
+  matche-pattern->expr
+  (fn
+    (pat)
+    (cond
+      ((matche-symbol-var? pat) pat)
+      ((and (list? pat) (empty? pat)) (list (quote list)))
+      ((list? pat) (cons (quote list) (map matche-pattern->expr pat)))
+      (:else (list (quote quote) pat)))))
+
+(define
+  matche-clause
+  (fn
+    (target cl)
+    (let
+      ((pat (first cl)) (body (rest cl)))
+      (let
+        ((vars (matche-collect-vars pat)))
+        (let
+          ((pat-expr (matche-pattern->expr pat)))
+          (list
+            (cons
+              (quote fresh)
+              (cons vars (cons (list (quote ==) target pat-expr) body)))))))))
+
+(defmacro
+  matche
+  (target &rest clauses)
+  (cons (quote conde) (map (fn (cl) (matche-clause target cl)) clauses)))
diff --git a/lib/minikanren/tests/matche.sx b/lib/minikanren/tests/matche.sx
new file mode 100644
index 00000000..8309cfbf
--- /dev/null
+++ b/lib/minikanren/tests/matche.sx
@@ -0,0 +1,138 @@
+;; lib/minikanren/tests/matche.sx — Phase 5 piece D tests for `matche`.
+
+;; --- literal patterns ---
+
+(mk-test
+  "matche-literal-number"
+  (run* q (matche q (1 (== q 1))))
+  (list 1))
+
+(mk-test
+  "matche-literal-string"
+  (run* q (matche q ("hello" (== q "hello"))))
+  (list "hello"))
+
+(mk-test
+  "matche-literal-no-clause-matches"
+  (run*
+    q
+    (matche 7 (1 (== q :a)) (2 (== q :b))))
+  (list))
+
+;; --- variable patterns ---
+
+(mk-test
+  "matche-symbol-pattern"
+  (run* q (fresh (x) (== x 99) (matche x (a (== q a)))))
+  (list 99))
+
+(mk-test
+  "matche-wildcard"
+  (run* q (fresh (x) (== x 7) (matche x (_ (== q :any)))))
+  (list :any))
+
+;; --- list patterns ---
+
+(mk-test
+  "matche-empty-list"
+  (run* q (matche (list) (() (== q :ok))))
+  (list :ok))
+
+(mk-test
+  "matche-pair-binds"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 2))
+      (matche x ((a b) (== q (list b a))))))
+  (list (list 2 1)))
+
+(mk-test
+  "matche-triple-binds"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 2 3))
+      (matche x ((a b c) (== q (list :sum a b c))))))
+  (list (list :sum 1 2 3)))
+
+(mk-test
+  "matche-mixed-literal-and-var"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 99 3))
+      (matche x ((1 m 3) (== q m)))))
+  (list 99))
+
+;; --- multi-clause dispatch ---
+
+(mk-test
+  "matche-multi-clause-shape"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 5 6))
+      (matche
+        x
+        (() (== q :empty))
+        ((a) (== q (list :one a)))
+        ((a b) (== q (list :two a b))))))
+  (list (list :two 5 6)))
+
+(mk-test
+  "matche-three-shapes-via-fresh"
+  (run*
+    q
+    (fresh
+      (x)
+      (matche
+        x
+        (() (== q :empty))
+        ((a) (== q (list :one a)))
+        ((a b) (== q (list :two a b))))))
+  (list
+    :empty (list :one (make-symbol "_.0"))
+    (list :two (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; --- nested patterns ---
+
+(mk-test
+  "matche-nested"
+  (run*
+    q
+    (fresh
+      (x)
+      (==
+        x
+        (list (list 1 2) (list 3 4)))
+      (matche x (((a b) (c d)) (== q (list a b c d))))))
+  (list (list 1 2 3 4)))
+
+;; --- repeated var names create the same fresh var → must unify ---
+
+(mk-test
+  "matche-repeated-var-implies-equality"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 7 7))
+      (matche x ((a a) (== q a)))))
+  (list 7))
+
+(mk-test
+  "matche-repeated-var-mismatch-fails"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 7 8))
+      (matche x ((a a) (== q a)))))
+  (list))
+
+(mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index 0bddf5a0..e5f70fdb 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -125,8 +125,13 @@ Key semantic mappings:
 - [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
       in the body's lexical scope, then runs `(mk-conj body...)` on the same
       substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
-- [ ] `matche` — pattern matching over logic terms (extension from core.logic)
-      `(matche l ((head . tail) goal) (() goal))`
+- [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` /
+      symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes
+      `(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol
+      names in a pattern produce the same fresh var, so they unify (== check).
+      Built without quasiquote (the expander does not recurse into lambda
+      bodies). Fixed-length list patterns only — head/tail destructuring uses
+      `(fresh (a d) (conso a d target) body)` directly.
 - [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
       flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
 - [x] `condu` — committed choice (Phase 2)
@@ -161,6 +166,13 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-08** — **Phase 5 piece D — matche, Phase 5 done**: pattern matching
+  macro (`lib/minikanren/matche.sx`) — symbols become fresh vars, atoms become
+  literals, lists recurse positionally, repeated names unify. 14 new tests
+  (literals, vars, wildcards, list patterns, multi-clause dispatch, nested
+  patterns, repeated-var-implies-eq). Built via `cons`/`list` rather than
+  quasiquote because SX's quasiquote does not recurse into lambda bodies — a
+  worth-knowing gotcha. 222/222 cumulative.
 - **2026-05-08** — **Phase 4 piece C — permuteo + inserto**: standard recursive
   insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3
   as a set check. 208/208 cumulative.