From 0a0735d8458004cbcc188975cbba9ac966504fae Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 10 Dec 2025 15:40:43 +0000
Subject: [PATCH 01/10] Initial plan


From 3b7565a09f8d330bf41534d94cd4b51e02b5c925 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 10 Dec 2025 15:49:35 +0000
Subject: [PATCH 02/10] Add term match function to Python and TypeScript
 bindings

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 apyds/ds.cc            | 10 ++++++++++
 apyds/term_t.py        | 25 +++++++++++++++++++++++++
 atsds/ds.cc            | 12 ++++++++++++
 atsds/index.mts        | 27 +++++++++++++++++++++++++++
 docs/api/python.md     | 26 ++++++++++++++++++++++++++
 docs/api/typescript.md | 27 +++++++++++++++++++++++++++
 tests/test_term.mjs    | 37 +++++++++++++++++++++++++++++++++++++
 tests/test_term.py     | 34 ++++++++++++++++++++++++++++++++++
 8 files changed, 198 insertions(+)

diff --git a/apyds/ds.cc b/apyds/ds.cc
index 17b3490..6339811 100644
--- a/apyds/ds.cc
+++ b/apyds/ds.cc
@@ -81,6 +81,15 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const char* scope, in
     return std::unique_ptr<ds::rule_t>(result);
 }
 
+auto term_match(ds::term_t* term_1, ds::term_t* term_2, const char* scope_1, const char* scope_2, int length) -> std::unique_ptr<ds::term_t> {
+    auto result = reinterpret_cast<ds::term_t*>(operator new(length));
+    if (result->match(term_1, term_2, scope_1, scope_2, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
+        operator delete(result);
+        return std::unique_ptr<ds::term_t>(nullptr);
+    }
+    return std::unique_ptr<ds::term_t>(result);
+}
+
 auto rule_match(ds::rule_t* rule_1, ds::rule_t* rule_2, int length) -> std::unique_ptr<ds::rule_t> {
     auto result = reinterpret_cast<ds::rule_t*>(operator new(length));
     if (result->match(rule_1, rule_2, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
@@ -147,6 +156,7 @@ PYBIND11_MODULE(_ds, m, py::mod_gil_not_used()) {
 
     term_t.def_static("ground", term_ground);
     rule_t.def_static("ground", rule_ground);
+    term_t.def_static("match", term_match);
     rule_t.def_static("match", rule_match);
     term_t.def_static("rename", term_rename);
     rule_t.def_static("rename", rule_rename);
diff --git a/apyds/term_t.py b/apyds/term_t.py
index d23e43e..6ba4560 100644
--- a/apyds/term_t.py
+++ b/apyds/term_t.py
@@ -77,6 +77,31 @@ def ground(self, other: Term, scope: str | None = None) -> Term | None:
             return None
         return Term(term, capacity)
 
+    def match(
+        self, other: Term, scope_1: str | None = None, scope_2: str | None = None
+    ) -> Term | None:
+        """Match two terms and return the unification result as a dictionary.
+
+        Args:
+            other: The term to match with this term.
+            scope_1: Optional scope string for variables in this term.
+            scope_2: Optional scope string for variables in the other term.
+
+        Returns:
+            A term representing the unification dictionary (list of pairs), or None if matching fails.
+
+        Example:
+            >>> a = Term("`a")
+            >>> b = Term("b")
+            >>> result = a.match(b)
+            >>> str(result) if result else None  # "((`a b))"
+        """
+        capacity = buffer_size()
+        term = ds.Term.match(self.value, other.value, scope_1, scope_2, capacity)
+        if term is None:
+            return None
+        return Term(term, capacity)
+
     def rename(self, prefix_and_suffix: Term) -> Term | None:
         """Rename all variables in this term by adding prefix and suffix.
 
diff --git a/atsds/ds.cc b/atsds/ds.cc
index 27d40c4..abe1f46 100644
--- a/atsds/ds.cc
+++ b/atsds/ds.cc
@@ -88,6 +88,17 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const std::string& sc
     return std::unique_ptr<ds::rule_t>(result);
 }
 
+auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length) -> std::unique_ptr<ds::term_t> {
+    const char* scope_1_ptr = scope_1.size() != 0 ? scope_1.data() : nullptr;
+    const char* scope_2_ptr = scope_2.size() != 0 ? scope_2.data() : nullptr;
+    auto result = reinterpret_cast<ds::term_t*>(operator new(length));
+    if (result->match(term_1, term_2, scope_1_ptr, scope_2_ptr, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
+        operator delete(result);
+        return std::unique_ptr<ds::term_t>(nullptr);
+    }
+    return std::unique_ptr<ds::term_t>(result);
+}
+
 auto rule_match(ds::rule_t* rule_1, ds::rule_t* rule_2, int length) -> std::unique_ptr<ds::rule_t> {
     auto result = reinterpret_cast<ds::rule_t*>(operator new(length));
     if (result->match(rule_1, rule_2, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
@@ -163,6 +174,7 @@ EMSCRIPTEN_BINDINGS(ds) {
 
     term_t.class_function("ground", term_ground, em::return_value_policy::take_ownership());
     rule_t.class_function("ground", rule_ground, em::return_value_policy::take_ownership());
+    term_t.class_function("match", term_match, em::return_value_policy::take_ownership());
     rule_t.class_function("match", rule_match, em::return_value_policy::take_ownership());
     term_t.class_function("rename", term_rename, em::return_value_policy::take_ownership());
     rule_t.class_function("rename", rule_rename, em::return_value_policy::take_ownership());
diff --git a/atsds/index.mts b/atsds/index.mts
index 4409ba4..b98f1b5 100644
--- a/atsds/index.mts
+++ b/atsds/index.mts
@@ -357,6 +357,33 @@ export class term_t extends _common_t<dst.Term> {
         return new term_t(term, capacity);
     }
 
+    /**
+     * Match two terms and return the unification result as a dictionary.
+     *
+     * @param other - The term to match with this term.
+     * @param scope_1 - Optional scope string for variables in this term.
+     * @param scope_2 - Optional scope string for variables in the other term.
+     * @returns A term representing the unification dictionary (list of pairs), or null if matching fails.
+     *
+     * @example
+     * ```typescript
+     * const a = new term_t("`a");
+     * const b = new term_t("b");
+     * const result = a.match(b);
+     * if (result !== null) {
+     *     console.log(result.toString());  // "((`a b))"
+     * }
+     * ```
+     */
+    match(other: term_t, scope_1: string = "", scope_2: string = ""): term_t | null {
+        const capacity = buffer_size();
+        const term = ds.Term.match(this.value, other.value, scope_1, scope_2, capacity);
+        if (term === null) {
+            return null;
+        }
+        return new term_t(term, capacity);
+    }
+
     /**
      * Rename all variables in this term by adding prefix and suffix.
      *
diff --git a/docs/api/python.md b/docs/api/python.md
index fb37a3a..86c9db8 100644
--- a/docs/api/python.md
+++ b/docs/api/python.md
@@ -266,6 +266,32 @@ if result is not None:
     print(result)  # "b"
 ```
 
+#### match()
+
+Match two terms and return the unification result as a dictionary.
+
+```python
+def match(self, other: Term, scope_1: str | None = None, scope_2: str | None = None) -> Term | None
+```
+
+**Parameters:**
+
+- `other`: The term to match with this term
+- `scope_1` (optional): Scope string for variables in this term
+- `scope_2` (optional): Scope string for variables in the other term
+
+**Returns:** A term representing the unification dictionary (list of pairs), or None if matching fails.
+
+**Example:**
+
+```python
+a = Term("`a")
+b = Term("b")
+result = a.match(b)
+if result is not None:
+    print(result)  # "((`a b))"
+```
+
 #### rename()
 
 Rename all variables in this term by adding prefix and suffix.
diff --git a/docs/api/typescript.md b/docs/api/typescript.md
index cbf6b49..ff3cee5 100644
--- a/docs/api/typescript.md
+++ b/docs/api/typescript.md
@@ -261,6 +261,33 @@ if (result !== null) {
 }
 ```
 
+#### match()
+
+Match two terms and return the unification result as a dictionary.
+
+```typescript
+match(other: term_t, scope_1?: string, scope_2?: string): term_t | null
+```
+
+**Parameters:**
+
+- `other`: The term to match with this term
+- `scope_1` (optional): Scope string for variables in this term
+- `scope_2` (optional): Scope string for variables in the other term
+
+**Returns:** A term representing the unification dictionary (list of pairs), or null if matching fails.
+
+**Example:**
+
+```typescript
+const a = new term_t("`a");
+const b = new term_t("b");
+const result = a.match(b);
+if (result !== null) {
+    console.log(result.toString());  // "((`a b))"
+}
+```
+
 #### rename()
 
 Rename all variables in this term by adding prefix and suffix.
diff --git a/tests/test_term.mjs b/tests/test_term.mjs
index 5f9ff2d..3420fd0 100644
--- a/tests/test_term.mjs
+++ b/tests/test_term.mjs
@@ -99,3 +99,40 @@ test("rename_invalid", () => {
     const b = new term_t("item");
     expect(a.rename(b)).toBeNull();
 });
+
+test("match_simple", () => {
+    const a = new term_t("`a");
+    const b = new term_t("b");
+    const result = a.match(b);
+    expect(result).not.toBeNull();
+    expect(result.toString()).toBe("((`a b))");
+});
+
+test("match_complex", () => {
+    const a = new term_t("(f `x a)");
+    const b = new term_t("(f b a)");
+    const result = a.match(b);
+    expect(result).not.toBeNull();
+    expect(result.toString()).toBe("((`x b))");
+});
+
+test("match_fail", () => {
+    const a = new term_t("(f `x)");
+    const b = new term_t("(g `y)");
+    const result = a.match(b);
+    expect(result).toBeNull();
+});
+
+test("match_with_scopes", () => {
+    const a = new term_t("`a");
+    const b = new term_t("`b");
+    const result = a.match(b, "scope1", "scope2");
+    expect(result).not.toBeNull();
+    // The result should be a dictionary with scoped variables
+    const resultStr = result.toString();
+    expect(resultStr).toContain("scope1");
+    expect(resultStr).toContain("scope2");
+    expect(resultStr).toContain("`a");
+    expect(resultStr).toContain("`b");
+});
+
diff --git a/tests/test_term.py b/tests/test_term.py
index 6a0d507..9174b71 100644
--- a/tests/test_term.py
+++ b/tests/test_term.py
@@ -110,3 +110,37 @@ def test_rename_invalid() -> None:
     a = apyds.Term("`x")
     b = apyds.Term("item")
     assert a.rename(b) is None
+
+
+def test_match_simple() -> None:
+    a = apyds.Term("`a")
+    b = apyds.Term("b")
+    result = a.match(b)
+    assert result is not None
+    assert str(result) == "((`a b))"
+
+
+def test_match_complex() -> None:
+    a = apyds.Term("(f `x a)")
+    b = apyds.Term("(f b a)")
+    result = a.match(b)
+    assert result is not None
+    assert str(result) == "((`x b))"
+
+
+def test_match_fail() -> None:
+    a = apyds.Term("(f `x)")
+    b = apyds.Term("(g `y)")
+    result = a.match(b)
+    assert result is None
+
+
+def test_match_with_scopes() -> None:
+    a = apyds.Term("`a")
+    b = apyds.Term("`b")
+    result = a.match(b, "scope1", "scope2")
+    assert result is not None
+    # The result should be a dictionary with scoped variables
+    result_str = str(result)
+    assert "scope1" in result_str and "scope2" in result_str and "`a" in result_str and "`b" in result_str
+

From 0f03a8e296a13a1c889c0bc196e6e981d1e0d417 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 10 Dec 2025 16:03:01 +0000
Subject: [PATCH 03/10] Fix term match function implementation and tests

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 apyds/ds.cc            |  7 +++++--
 apyds/term_t.py        |  5 ++++-
 atsds/ds.cc            |  6 +++---
 docs/api/python.md     |  2 +-
 docs/api/typescript.md |  2 +-
 tests/test_term.mjs    | 14 ++++++--------
 tests/test_term.py     |  9 +++++----
 7 files changed, 25 insertions(+), 20 deletions(-)

diff --git a/apyds/ds.cc b/apyds/ds.cc
index 6339811..f7b07d0 100644
--- a/apyds/ds.cc
+++ b/apyds/ds.cc
@@ -2,6 +2,7 @@
 #include <ds/search.hh>
 #include <pybind11/functional.h>
 #include <pybind11/pybind11.h>
+#include <string>
 
 namespace py = pybind11;
 
@@ -81,9 +82,11 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const char* scope, in
     return std::unique_ptr<ds::rule_t>(result);
 }
 
-auto term_match(ds::term_t* term_1, ds::term_t* term_2, const char* scope_1, const char* scope_2, int length) -> std::unique_ptr<ds::term_t> {
+auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length) -> std::unique_ptr<ds::term_t> {
+    // Pass scopes as-is, don't convert empty strings to nullptr
+    // The C++ match implementation expects valid C strings, not nullptr
     auto result = reinterpret_cast<ds::term_t*>(operator new(length));
-    if (result->match(term_1, term_2, scope_1, scope_2, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
+    if (result->match(term_1, term_2, scope_1.data(), scope_2.data(), reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
         operator delete(result);
         return std::unique_ptr<ds::term_t>(nullptr);
     }
diff --git a/apyds/term_t.py b/apyds/term_t.py
index 6ba4560..619cbc0 100644
--- a/apyds/term_t.py
+++ b/apyds/term_t.py
@@ -97,7 +97,10 @@ def match(
             >>> str(result) if result else None  # "((`a b))"
         """
         capacity = buffer_size()
-        term = ds.Term.match(self.value, other.value, scope_1, scope_2, capacity)
+        # Convert None to empty string for C++ binding
+        scope_1_str = scope_1 if scope_1 is not None else ""
+        scope_2_str = scope_2 if scope_2 is not None else ""
+        term = ds.Term.match(self.value, other.value, scope_1_str, scope_2_str, capacity)
         if term is None:
             return None
         return Term(term, capacity)
diff --git a/atsds/ds.cc b/atsds/ds.cc
index abe1f46..a8ee283 100644
--- a/atsds/ds.cc
+++ b/atsds/ds.cc
@@ -89,10 +89,10 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const std::string& sc
 }
 
 auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length) -> std::unique_ptr<ds::term_t> {
-    const char* scope_1_ptr = scope_1.size() != 0 ? scope_1.data() : nullptr;
-    const char* scope_2_ptr = scope_2.size() != 0 ? scope_2.data() : nullptr;
+    // Pass scopes as-is, don't convert empty strings to nullptr
+    // The C++ match implementation expects valid C strings, not nullptr
     auto result = reinterpret_cast<ds::term_t*>(operator new(length));
-    if (result->match(term_1, term_2, scope_1_ptr, scope_2_ptr, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
+    if (result->match(term_1, term_2, scope_1.data(), scope_2.data(), reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
         operator delete(result);
         return std::unique_ptr<ds::term_t>(nullptr);
     }
diff --git a/docs/api/python.md b/docs/api/python.md
index 86c9db8..048a05b 100644
--- a/docs/api/python.md
+++ b/docs/api/python.md
@@ -289,7 +289,7 @@ a = Term("`a")
 b = Term("b")
 result = a.match(b)
 if result is not None:
-    print(result)  # "((`a b))"
+    print(result)  # "((  `a b))"
 ```
 
 #### rename()
diff --git a/docs/api/typescript.md b/docs/api/typescript.md
index ff3cee5..5de4e5b 100644
--- a/docs/api/typescript.md
+++ b/docs/api/typescript.md
@@ -284,7 +284,7 @@ const a = new term_t("`a");
 const b = new term_t("b");
 const result = a.match(b);
 if (result !== null) {
-    console.log(result.toString());  // "((`a b))"
+    console.log(result.toString());  // "((  `a b))"
 }
 ```
 
diff --git a/tests/test_term.mjs b/tests/test_term.mjs
index 3420fd0..b6d8d66 100644
--- a/tests/test_term.mjs
+++ b/tests/test_term.mjs
@@ -105,7 +105,8 @@ test("match_simple", () => {
     const b = new term_t("b");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    expect(result.toString()).toBe("((`a b))");
+    // Result format is ((scope_1 scope_2 key value)) where scopes are empty strings
+    expect(result.toString()).toBe("((  `a b))");
 });
 
 test("match_complex", () => {
@@ -113,7 +114,7 @@ test("match_complex", () => {
     const b = new term_t("(f b a)");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    expect(result.toString()).toBe("((`x b))");
+    expect(result.toString()).toBe("((  `x b))");
 });
 
 test("match_fail", () => {
@@ -128,11 +129,8 @@ test("match_with_scopes", () => {
     const b = new term_t("`b");
     const result = a.match(b, "scope1", "scope2");
     expect(result).not.toBeNull();
-    // The result should be a dictionary with scoped variables
-    const resultStr = result.toString();
-    expect(resultStr).toContain("scope1");
-    expect(resultStr).toContain("scope2");
-    expect(resultStr).toContain("`a");
-    expect(resultStr).toContain("`b");
+    // Format: ((scope1 scope2 `a `b))
+    expect(result.toString()).toBe("((scope1 scope2 `a `b))");
 });
 
+
diff --git a/tests/test_term.py b/tests/test_term.py
index 9174b71..d0239f8 100644
--- a/tests/test_term.py
+++ b/tests/test_term.py
@@ -117,7 +117,8 @@ def test_match_simple() -> None:
     b = apyds.Term("b")
     result = a.match(b)
     assert result is not None
-    assert str(result) == "((`a b))"
+    # Result format is ((scope_1 scope_2 key value)) where scopes are empty strings
+    assert str(result) == "((  `a b))"
 
 
 def test_match_complex() -> None:
@@ -125,7 +126,7 @@ def test_match_complex() -> None:
     b = apyds.Term("(f b a)")
     result = a.match(b)
     assert result is not None
-    assert str(result) == "((`x b))"
+    assert str(result) == "((  `x b))"
 
 
 def test_match_fail() -> None:
@@ -141,6 +142,6 @@ def test_match_with_scopes() -> None:
     result = a.match(b, "scope1", "scope2")
     assert result is not None
     # The result should be a dictionary with scoped variables
-    result_str = str(result)
-    assert "scope1" in result_str and "scope2" in result_str and "`a" in result_str and "`b" in result_str
+    # Format: ((scope1 scope2 `a `b))
+    assert str(result) == "((scope1 scope2 `a `b))"
 

From 7278fcfbf49e09373ef25a2fd5009e2432db9db6 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 00:20:35 +0800
Subject: [PATCH 04/10] Update apyds.

---
 apyds/ds.cc     |  7 ++-----
 apyds/term_t.py | 15 ++++-----------
 2 files changed, 6 insertions(+), 16 deletions(-)

diff --git a/apyds/ds.cc b/apyds/ds.cc
index f7b07d0..6339811 100644
--- a/apyds/ds.cc
+++ b/apyds/ds.cc
@@ -2,7 +2,6 @@
 #include <ds/search.hh>
 #include <pybind11/functional.h>
 #include <pybind11/pybind11.h>
-#include <string>
 
 namespace py = pybind11;
 
@@ -82,11 +81,9 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const char* scope, in
     return std::unique_ptr<ds::rule_t>(result);
 }
 
-auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length) -> std::unique_ptr<ds::term_t> {
-    // Pass scopes as-is, don't convert empty strings to nullptr
-    // The C++ match implementation expects valid C strings, not nullptr
+auto term_match(ds::term_t* term_1, ds::term_t* term_2, const char* scope_1, const char* scope_2, int length) -> std::unique_ptr<ds::term_t> {
     auto result = reinterpret_cast<ds::term_t*>(operator new(length));
-    if (result->match(term_1, term_2, scope_1.data(), scope_2.data(), reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
+    if (result->match(term_1, term_2, scope_1, scope_2, reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
         operator delete(result);
         return std::unique_ptr<ds::term_t>(nullptr);
     }
diff --git a/apyds/term_t.py b/apyds/term_t.py
index 619cbc0..b24b11c 100644
--- a/apyds/term_t.py
+++ b/apyds/term_t.py
@@ -77,15 +77,11 @@ def ground(self, other: Term, scope: str | None = None) -> Term | None:
             return None
         return Term(term, capacity)
 
-    def match(
-        self, other: Term, scope_1: str | None = None, scope_2: str | None = None
-    ) -> Term | None:
+    def __matmul__(self, other: Term) -> Term | None:
         """Match two terms and return the unification result as a dictionary.
 
         Args:
             other: The term to match with this term.
-            scope_1: Optional scope string for variables in this term.
-            scope_2: Optional scope string for variables in the other term.
 
         Returns:
             A term representing the unification dictionary (list of pairs), or None if matching fails.
@@ -93,14 +89,11 @@ def match(
         Example:
             >>> a = Term("`a")
             >>> b = Term("b")
-            >>> result = a.match(b)
-            >>> str(result) if result else None  # "((`a b))"
+            >>> result = a @ b
+            >>> str(result) if result else None  # "((r f `a b))"
         """
         capacity = buffer_size()
-        # Convert None to empty string for C++ binding
-        scope_1_str = scope_1 if scope_1 is not None else ""
-        scope_2_str = scope_2 if scope_2 is not None else ""
-        term = ds.Term.match(self.value, other.value, scope_1_str, scope_2_str, capacity)
+        term = ds.Term.match(self.value, other.value, "r", "f", capacity)
         if term is None:
             return None
         return Term(term, capacity)

From 98642131b30452bc52ee65eada3df5705b0d06a2 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 00:31:52 +0800
Subject: [PATCH 05/10] Update atsds.

---
 atsds/ds.cc     | 5 ++---
 atsds/index.mts | 8 +++-----
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/atsds/ds.cc b/atsds/ds.cc
index a8ee283..1e9b5b1 100644
--- a/atsds/ds.cc
+++ b/atsds/ds.cc
@@ -88,9 +88,8 @@ auto rule_ground(ds::rule_t* rule, ds::rule_t* dictionary, const std::string& sc
     return std::unique_ptr<ds::rule_t>(result);
 }
 
-auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length) -> std::unique_ptr<ds::term_t> {
-    // Pass scopes as-is, don't convert empty strings to nullptr
-    // The C++ match implementation expects valid C strings, not nullptr
+auto term_match(ds::term_t* term_1, ds::term_t* term_2, const std::string& scope_1, const std::string& scope_2, int length)
+    -> std::unique_ptr<ds::term_t> {
     auto result = reinterpret_cast<ds::term_t*>(operator new(length));
     if (result->match(term_1, term_2, scope_1.data(), scope_2.data(), reinterpret_cast<std::byte*>(result) + length) == nullptr) [[unlikely]] {
         operator delete(result);
diff --git a/atsds/index.mts b/atsds/index.mts
index b98f1b5..d92b3fc 100644
--- a/atsds/index.mts
+++ b/atsds/index.mts
@@ -361,8 +361,6 @@ export class term_t extends _common_t<dst.Term> {
      * Match two terms and return the unification result as a dictionary.
      *
      * @param other - The term to match with this term.
-     * @param scope_1 - Optional scope string for variables in this term.
-     * @param scope_2 - Optional scope string for variables in the other term.
      * @returns A term representing the unification dictionary (list of pairs), or null if matching fails.
      *
      * @example
@@ -371,13 +369,13 @@ export class term_t extends _common_t<dst.Term> {
      * const b = new term_t("b");
      * const result = a.match(b);
      * if (result !== null) {
-     *     console.log(result.toString());  // "((`a b))"
+     *     console.log(result.toString());  // "((r f `a b))"
      * }
      * ```
      */
-    match(other: term_t, scope_1: string = "", scope_2: string = ""): term_t | null {
+    match(other: term_t): term_t | null {
         const capacity = buffer_size();
-        const term = ds.Term.match(this.value, other.value, scope_1, scope_2, capacity);
+        const term = ds.Term.match(this.value, other.value, "r", "f", capacity);
         if (term === null) {
             return null;
         }

From 23f7e8ac741c3fc72536b0aa97de36617c8d444d Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 00:33:12 +0800
Subject: [PATCH 06/10] Fix by pre-commit.

[skip ci]
---
 tests/test_term.mjs | 2 --
 tests/test_term.py  | 1 -
 2 files changed, 3 deletions(-)

diff --git a/tests/test_term.mjs b/tests/test_term.mjs
index b6d8d66..1efb3e1 100644
--- a/tests/test_term.mjs
+++ b/tests/test_term.mjs
@@ -132,5 +132,3 @@ test("match_with_scopes", () => {
     // Format: ((scope1 scope2 `a `b))
     expect(result.toString()).toBe("((scope1 scope2 `a `b))");
 });
-
-
diff --git a/tests/test_term.py b/tests/test_term.py
index d0239f8..9646051 100644
--- a/tests/test_term.py
+++ b/tests/test_term.py
@@ -144,4 +144,3 @@ def test_match_with_scopes() -> None:
     # The result should be a dictionary with scoped variables
     # Format: ((scope1 scope2 `a `b))
     assert str(result) == "((scope1 scope2 `a `b))"
-

From f9114aba18a201e8c5060b5a937426f434521d5c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 10 Dec 2025 16:50:03 +0000
Subject: [PATCH 07/10] Update tests and docs for hardcoded scopes in
 term.match()

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 docs/api/python.md     | 10 +++---
 docs/api/typescript.md |  6 ++--
 docs/concepts/terms.md | 71 ++++++++++++++++++++++++++++++++++++++++++
 tests/test_term.mjs    | 14 ++-------
 tests/test_term.py     | 21 +++----------
 5 files changed, 84 insertions(+), 38 deletions(-)

diff --git a/docs/api/python.md b/docs/api/python.md
index 048a05b..39e3c74 100644
--- a/docs/api/python.md
+++ b/docs/api/python.md
@@ -266,19 +266,17 @@ if result is not None:
     print(result)  # "b"
 ```
 
-#### match()
+#### \_\_matmul\_\_() / match
 
 Match two terms and return the unification result as a dictionary.
 
 ```python
-def match(self, other: Term, scope_1: str | None = None, scope_2: str | None = None) -> Term | None
+def __matmul__(self, other: Term) -> Term | None
 ```
 
 **Parameters:**
 
 - `other`: The term to match with this term
-- `scope_1` (optional): Scope string for variables in this term
-- `scope_2` (optional): Scope string for variables in the other term
 
 **Returns:** A term representing the unification dictionary (list of pairs), or None if matching fails.
 
@@ -287,9 +285,9 @@ def match(self, other: Term, scope_1: str | None = None, scope_2: str | None = N
 ```python
 a = Term("`a")
 b = Term("b")
-result = a.match(b)
+result = a @ b
 if result is not None:
-    print(result)  # "((  `a b))"
+    print(result)  # "((r f `a b))"
 ```
 
 #### rename()
diff --git a/docs/api/typescript.md b/docs/api/typescript.md
index 5de4e5b..8f76929 100644
--- a/docs/api/typescript.md
+++ b/docs/api/typescript.md
@@ -266,14 +266,12 @@ if (result !== null) {
 Match two terms and return the unification result as a dictionary.
 
 ```typescript
-match(other: term_t, scope_1?: string, scope_2?: string): term_t | null
+match(other: term_t): term_t | null
 ```
 
 **Parameters:**
 
 - `other`: The term to match with this term
-- `scope_1` (optional): Scope string for variables in this term
-- `scope_2` (optional): Scope string for variables in the other term
 
 **Returns:** A term representing the unification dictionary (list of pairs), or null if matching fails.
 
@@ -284,7 +282,7 @@ const a = new term_t("`a");
 const b = new term_t("b");
 const result = a.match(b);
 if (result !== null) {
-    console.log(result.toString());  // "((  `a b))"
+    console.log(result.toString());  // "((r f `a b))"
 }
 ```
 
diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md
index dace095..64598cc 100644
--- a/docs/concepts/terms.md
+++ b/docs/concepts/terms.md
@@ -202,6 +202,77 @@ Grounding substitutes variables in a term with values from a dictionary. The dic
     }
     ```
 
+### Matching
+
+Matching unifies two terms and returns a dictionary of variable bindings. The dictionary contains the substitutions needed to make the two terms equal.
+
+=== "TypeScript"
+
+    ```typescript
+    import { term_t } from "atsds";
+
+    // Match a variable with a value
+    const a = new term_t("`a");
+    const b = new term_t("value");
+    
+    const result = a.match(b);
+    if (result !== null) {
+        console.log(result.toString());  // ((r f `a value))
+    }
+
+    // Match complex terms
+    const term1 = new term_t("(f `x a)");
+    const term2 = new term_t("(f b a)");
+    
+    const dict = term1.match(term2);
+    if (dict !== null) {
+        console.log(dict.toString());  // ((r f `x b))
+    }
+    ```
+
+=== "Python"
+
+    ```python
+    import apyds
+
+    # Match a variable with a value
+    a = apyds.Term("`a")
+    b = apyds.Term("value")
+    
+    result = a @ b  # Uses @ operator
+    print(result)  # ((r f `a value))
+
+    # Match complex terms
+    term1 = apyds.Term("(f `x a)")
+    term2 = apyds.Term("(f b a)")
+    
+    dict_result = term1 @ term2
+    print(dict_result)  # ((r f `x b))
+    ```
+
+=== "C++"
+
+    ```cpp
+    #include <ds/ds.hh>
+    #include <ds/utility.hh>
+    #include <iostream>
+
+    int main() {
+        // Match a variable with a value
+        auto a = ds::text_to_term("`a", 1000);
+        auto b = ds::text_to_term("value", 1000);
+
+        // Match the terms
+        std::byte buffer[1000];
+        auto result = reinterpret_cast<ds::term_t*>(buffer);
+        result->match(a.get(), b.get(), "r", "f", buffer + 1000);
+
+        std::cout << ds::term_to_text(result, 1000).get() << std::endl;  // ((r f `a value))
+
+        return 0;
+    }
+    ```
+
 ### Renaming
 
 Renaming adds prefixes and/or suffixes to all variables in a term. This is useful for avoiding variable name collisions during unification.
diff --git a/tests/test_term.mjs b/tests/test_term.mjs
index 1efb3e1..6f39376 100644
--- a/tests/test_term.mjs
+++ b/tests/test_term.mjs
@@ -105,8 +105,7 @@ test("match_simple", () => {
     const b = new term_t("b");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    // Result format is ((scope_1 scope_2 key value)) where scopes are empty strings
-    expect(result.toString()).toBe("((  `a b))");
+    expect(result.toString()).toBe("((r f `a b))");
 });
 
 test("match_complex", () => {
@@ -114,7 +113,7 @@ test("match_complex", () => {
     const b = new term_t("(f b a)");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    expect(result.toString()).toBe("((  `x b))");
+    expect(result.toString()).toBe("((r f `x b))");
 });
 
 test("match_fail", () => {
@@ -123,12 +122,3 @@ test("match_fail", () => {
     const result = a.match(b);
     expect(result).toBeNull();
 });
-
-test("match_with_scopes", () => {
-    const a = new term_t("`a");
-    const b = new term_t("`b");
-    const result = a.match(b, "scope1", "scope2");
-    expect(result).not.toBeNull();
-    // Format: ((scope1 scope2 `a `b))
-    expect(result.toString()).toBe("((scope1 scope2 `a `b))");
-});
diff --git a/tests/test_term.py b/tests/test_term.py
index 9646051..d29e337 100644
--- a/tests/test_term.py
+++ b/tests/test_term.py
@@ -115,32 +115,21 @@ def test_rename_invalid() -> None:
 def test_match_simple() -> None:
     a = apyds.Term("`a")
     b = apyds.Term("b")
-    result = a.match(b)
+    result = a @ b
     assert result is not None
-    # Result format is ((scope_1 scope_2 key value)) where scopes are empty strings
-    assert str(result) == "((  `a b))"
+    assert str(result) == "((r f `a b))"
 
 
 def test_match_complex() -> None:
     a = apyds.Term("(f `x a)")
     b = apyds.Term("(f b a)")
-    result = a.match(b)
+    result = a @ b
     assert result is not None
-    assert str(result) == "((  `x b))"
+    assert str(result) == "((r f `x b))"
 
 
 def test_match_fail() -> None:
     a = apyds.Term("(f `x)")
     b = apyds.Term("(g `y)")
-    result = a.match(b)
+    result = a @ b
     assert result is None
-
-
-def test_match_with_scopes() -> None:
-    a = apyds.Term("`a")
-    b = apyds.Term("`b")
-    result = a.match(b, "scope1", "scope2")
-    assert result is not None
-    # The result should be a dictionary with scoped variables
-    # Format: ((scope1 scope2 `a `b))
-    assert str(result) == "((scope1 scope2 `a `b))"

From 46690c803350d922c48cb2f3fcac0256880a3853 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 00:56:45 +0800
Subject: [PATCH 08/10] Update apyds and atsds.

[skip ci]
---
 apyds/term_t.py | 6 +++---
 atsds/index.mts | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/apyds/term_t.py b/apyds/term_t.py
index b24b11c..ad2f579 100644
--- a/apyds/term_t.py
+++ b/apyds/term_t.py
@@ -84,16 +84,16 @@ def __matmul__(self, other: Term) -> Term | None:
             other: The term to match with this term.
 
         Returns:
-            A term representing the unification dictionary (list of pairs), or None if matching fails.
+            A term representing the unification dictionary (list of tuples), or None if matching fails.
 
         Example:
             >>> a = Term("`a")
             >>> b = Term("b")
             >>> result = a @ b
-            >>> str(result) if result else None  # "((r f `a b))"
+            >>> str(result) if result else None  # "((1 2 `a b))"
         """
         capacity = buffer_size()
-        term = ds.Term.match(self.value, other.value, "r", "f", capacity)
+        term = ds.Term.match(self.value, other.value, "1", "2", capacity)
         if term is None:
             return None
         return Term(term, capacity)
diff --git a/atsds/index.mts b/atsds/index.mts
index d92b3fc..69348b2 100644
--- a/atsds/index.mts
+++ b/atsds/index.mts
@@ -361,7 +361,7 @@ export class term_t extends _common_t<dst.Term> {
      * Match two terms and return the unification result as a dictionary.
      *
      * @param other - The term to match with this term.
-     * @returns A term representing the unification dictionary (list of pairs), or null if matching fails.
+     * @returns A term representing the unification dictionary (list of tuples), or null if matching fails.
      *
      * @example
      * ```typescript
@@ -369,13 +369,13 @@ export class term_t extends _common_t<dst.Term> {
      * const b = new term_t("b");
      * const result = a.match(b);
      * if (result !== null) {
-     *     console.log(result.toString());  // "((r f `a b))"
+     *     console.log(result.toString());  // "((1 2 `a b))"
      * }
      * ```
      */
     match(other: term_t): term_t | null {
         const capacity = buffer_size();
-        const term = ds.Term.match(this.value, other.value, "r", "f", capacity);
+        const term = ds.Term.match(this.value, other.value, "1", "2", capacity);
         if (term === null) {
             return null;
         }

From 595726e414f5ff2eb026a2c8de9fe15ef29560dd Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 00:59:49 +0800
Subject: [PATCH 09/10] Update tests.

---
 tests/test_term.mjs | 8 ++++----
 tests/test_term.py  | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/test_term.mjs b/tests/test_term.mjs
index 6f39376..dc9face 100644
--- a/tests/test_term.mjs
+++ b/tests/test_term.mjs
@@ -105,15 +105,15 @@ test("match_simple", () => {
     const b = new term_t("b");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    expect(result.toString()).toBe("((r f `a b))");
+    expect(result.toString()).toBe("((1 2 `a b))");
 });
 
 test("match_complex", () => {
-    const a = new term_t("(f `x a)");
-    const b = new term_t("(f b a)");
+    const a = new term_t("(f b a)");
+    const b = new term_t("(f `x a)");
     const result = a.match(b);
     expect(result).not.toBeNull();
-    expect(result.toString()).toBe("((r f `x b))");
+    expect(result.toString()).toBe("((2 1 `x b))");
 });
 
 test("match_fail", () => {
diff --git a/tests/test_term.py b/tests/test_term.py
index d29e337..00575d6 100644
--- a/tests/test_term.py
+++ b/tests/test_term.py
@@ -117,15 +117,15 @@ def test_match_simple() -> None:
     b = apyds.Term("b")
     result = a @ b
     assert result is not None
-    assert str(result) == "((r f `a b))"
+    assert str(result) == "((1 2 `a b))"
 
 
 def test_match_complex() -> None:
-    a = apyds.Term("(f `x a)")
-    b = apyds.Term("(f b a)")
+    a = apyds.Term("(f b a)")
+    b = apyds.Term("(f `x a)")
     result = a @ b
     assert result is not None
-    assert str(result) == "((r f `x b))"
+    assert str(result) == "((2 1 `x b))"
 
 
 def test_match_fail() -> None:

From 9fc81230054ded890ba502df29592f078346830e Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 11 Dec 2025 01:02:28 +0800
Subject: [PATCH 10/10] Update docs.

---
 docs/api/python.md     |  4 ++--
 docs/api/typescript.md |  4 ++--
 docs/concepts/terms.md | 20 ++++++++++----------
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/docs/api/python.md b/docs/api/python.md
index 39e3c74..c63ed7d 100644
--- a/docs/api/python.md
+++ b/docs/api/python.md
@@ -278,7 +278,7 @@ def __matmul__(self, other: Term) -> Term | None
 
 - `other`: The term to match with this term
 
-**Returns:** A term representing the unification dictionary (list of pairs), or None if matching fails.
+**Returns:** A term representing the unification dictionary (list of tuples), or None if matching fails.
 
 **Example:**
 
@@ -287,7 +287,7 @@ a = Term("`a")
 b = Term("b")
 result = a @ b
 if result is not None:
-    print(result)  # "((r f `a b))"
+    print(result)  # "((1 2 `a b))"
 ```
 
 #### rename()
diff --git a/docs/api/typescript.md b/docs/api/typescript.md
index 8f76929..6e7e364 100644
--- a/docs/api/typescript.md
+++ b/docs/api/typescript.md
@@ -273,7 +273,7 @@ match(other: term_t): term_t | null
 
 - `other`: The term to match with this term
 
-**Returns:** A term representing the unification dictionary (list of pairs), or null if matching fails.
+**Returns:** A term representing the unification dictionary (list of tuples), or null if matching fails.
 
 **Example:**
 
@@ -282,7 +282,7 @@ const a = new term_t("`a");
 const b = new term_t("b");
 const result = a.match(b);
 if (result !== null) {
-    console.log(result.toString());  // "((r f `a b))"
+    console.log(result.toString());  // "((1 2 `a b))"
 }
 ```
 
diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md
index 64598cc..76189f6 100644
--- a/docs/concepts/terms.md
+++ b/docs/concepts/terms.md
@@ -217,16 +217,16 @@ Matching unifies two terms and returns a dictionary of variable bindings. The di
     
     const result = a.match(b);
     if (result !== null) {
-        console.log(result.toString());  // ((r f `a value))
+        console.log(result.toString());  // ((1 2 `a value))
     }
 
     // Match complex terms
-    const term1 = new term_t("(f `x a)");
-    const term2 = new term_t("(f b a)");
+    const term1 = new term_t("(f b a)");
+    const term2 = new term_t("(f `x a)");
     
     const dict = term1.match(term2);
     if (dict !== null) {
-        console.log(dict.toString());  // ((r f `x b))
+        console.log(dict.toString());  // ((2 1 `x b))
     }
     ```
 
@@ -240,14 +240,14 @@ Matching unifies two terms and returns a dictionary of variable bindings. The di
     b = apyds.Term("value")
     
     result = a @ b  # Uses @ operator
-    print(result)  # ((r f `a value))
+    print(result)  # ((1 2 `a value))
 
     # Match complex terms
-    term1 = apyds.Term("(f `x a)")
-    term2 = apyds.Term("(f b a)")
+    term1 = apyds.Term("(f b a)")
+    term2 = apyds.Term("(f `x a)")
     
     dict_result = term1 @ term2
-    print(dict_result)  # ((r f `x b))
+    print(dict_result)  # ((2 1 `x b))
     ```
 
 === "C++"
@@ -265,9 +265,9 @@ Matching unifies two terms and returns a dictionary of variable bindings. The di
         // Match the terms
         std::byte buffer[1000];
         auto result = reinterpret_cast<ds::term_t*>(buffer);
-        result->match(a.get(), b.get(), "r", "f", buffer + 1000);
+        result->match(a.get(), b.get(), "1", "2", buffer + 1000);
 
-        std::cout << ds::term_to_text(result, 1000).get() << std::endl;  // ((r f `a value))
+        std::cout << ds::term_to_text(result, 1000).get() << std::endl;  // ((1 2 `a value))
 
         return 0;
     }