Add term match to Python and TypeScript bindings (#93)

* Initial plan

* Add term match function to Python and TypeScript bindings

Co-authored-by: hzhangxyz <[email protected]>

* Fix term match function implementation and tests

Co-authored-by: hzhangxyz <[email protected]>

* Update apyds.

* Update atsds.

* Fix by pre-commit.

[skip ci]

* Update tests and docs for hardcoded scopes in term.match()

Co-authored-by: hzhangxyz <[email protected]>

* Update apyds and atsds.

[skip ci]

* Update tests.

* Update docs.

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: hzhangxyz <[email protected]>
Co-authored-by: Hao Zhang <[email protected]>

Author: Copilot

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);

apyds/term_t.py

@@ -77,6 +77,27 @@ def ground(self, other: Term, scope: str | None = None) -> Term | None:
             return None
         return Term(term, capacity)
 
+    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.
+
+        Returns:
+            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  # "((1 2 `a b))"
+        """
+        capacity = buffer_size()
+        term = ds.Term.match(self.value, other.value, "1", "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.
 

atsds/ds.cc

@@ -88,6 +88,16 @@ 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> {
+    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);
+        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 +173,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());

atsds/index.mts

@@ -357,6 +357,31 @@ 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.
+     * @returns A term representing the unification dictionary (list of tuples), 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());  // "((1 2 `a b))"
+     * }
+     * ```
+     */
+    match(other: term_t): term_t | null {
+        const capacity = buffer_size();
+        const term = ds.Term.match(this.value, other.value, "1", "2", capacity);
+        if (term === null) {
+            return null;
+        }
+        return new term_t(term, capacity);
+    }
+
     /**
      * Rename all variables in this term by adding prefix and suffix.
      *

docs/api/python.md

@@ -266,6 +266,30 @@ if result is not None:
     print(result)  # "b"
 ```
 
+#### \_\_matmul\_\_() / match
+
+Match two terms and return the unification result as a dictionary.
+
+```python
+def __matmul__(self, other: Term) -> Term | None
+```
+
+**Parameters:**
+
+- `other`: The term to match with this term
+
+**Returns:** A term representing the unification dictionary (list of tuples), or None if matching fails.
+
+**Example:**
+
+```python
+a = Term("`a")
+b = Term("b")
+result = a @ b
+if result is not None:
+    print(result)  # "((1 2 `a b))"
+```
+
 #### rename()
 
 Rename all variables in this term by adding prefix and suffix.

docs/api/typescript.md

@@ -261,6 +261,31 @@ if (result !== null) {
 }
 ```
 
+#### match()
+
+Match two terms and return the unification result as a dictionary.
+
+```typescript
+match(other: term_t): term_t | null
+```
+
+**Parameters:**
+
+- `other`: The term to match with this term
+
+**Returns:** A term representing the unification dictionary (list of tuples), 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());  // "((1 2 `a b))"
+}
+```
+
 #### rename()
 
 Rename all variables in this term by adding prefix and suffix.

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());  // ((1 2 `a value))
+    }
+
+    // Match complex terms
+    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());  // ((2 1 `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)  # ((1 2 `a value))
+
+    # Match complex terms
+    term1 = apyds.Term("(f b a)")
+    term2 = apyds.Term("(f `x a)")
+    
+    dict_result = term1 @ term2
+    print(dict_result)  # ((2 1 `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(), "1", "2", buffer + 1000);
+
+        std::cout << ds::term_to_text(result, 1000).get() << std::endl;  // ((1 2 `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.

tests/test_term.mjs

@@ -99,3 +99,26 @@ 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("((1 2 `a b))");
+});
+
+test("match_complex", () => {
+    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("((2 1 `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();
+});

tests/test_term.py

@@ -110,3 +110,26 @@ 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 @ b
+    assert result is not None
+    assert str(result) == "((1 2 `a b))"
+
+
+def test_match_complex() -> None:
+    a = apyds.Term("(f b a)")
+    b = apyds.Term("(f `x a)")
+    result = a @ b
+    assert result is not None
+    assert str(result) == "((2 1 `x b))"
+
+
+def test_match_fail() -> None:
+    a = apyds.Term("(f `x)")
+    b = apyds.Term("(g `y)")
+    result = a @ b
+    assert result is None