From 82421261a9d13024a86a805d50730c557050be17 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 25 Dec 2025 17:48:02 +0800
Subject: [PATCH 1/4] docs: update documentation and READMEs for atsds-egg
 implementation

Description
This PR updates the project documentation to include details for the newly added atsds-egg package, ensuring both Python (apyds-egg) and TypeScript (atsds-egg) implementations are well-documented.

Key Changes:
  - `/egg/README.md`: Added TypeScript installation steps, a Quick Start example, and build/test instructions.
  - `/docs/support-packages/egg.md`: Integrated TypeScript usage examples and package links into the main documentation site.
  - `README.md` (root): Updated the "Support Packages" section to include atsds-egg.
  - Package Info: Added npm package links and updated repository metadata.

These changes ensure that users of the TypeScript binding have clear guidance on how to install and use the E-Graph support package.
---
 README.md                    |  2 +-
 docs/support-packages/egg.md | 40 +++++++++++++++++++++++++-
 egg/README.md                | 56 +++++++++++++++++++++++++++++++++++-
 3 files changed, 95 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 60d240b..8b82e48 100644
--- a/README.md
+++ b/README.md
@@ -347,7 +347,7 @@ Each example demonstrates logical inference using propositional logic axioms.
 ## Support Packages
 
 - **BNF Conversion Library** ([apyds-bnf](https://pypi.org/project/apyds-bnf/), [atsds-bnf](https://www.npmjs.com/package/atsds-bnf)): Bidirectional conversion between DS syntax formats. See [/bnf](/bnf) for details.
-- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/)): E-Graph implementation for efficient equality reasoning. See [/egg](/egg) for details.
+- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/), [atsds-egg](https://www.npmjs.com/package/atsds-egg)): E-Graph implementation for efficient equality reasoning. See [/egg](/egg) for details.
 
 ## Development
 
diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index be36d7d..e1d0767 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -14,9 +14,15 @@ pip install apyds-egg
 
 Requires Python 3.11-3.14.
 
+### TypeScript/JavaScript
+
+```bash
+npm install atsds-egg
+```
+
 ## Usage
 
-### Basic Example
+### Python Example
 
 ```python
 import apyds
@@ -47,6 +53,37 @@ eg.rebuild()
 assert eg.find(ax) == eg.find(bx)
 ```
 
+### TypeScript Example
+
+```typescript
+import { Term } from "atsds";
+import { EGraph } from "atsds-egg";
+
+// Create an E-Graph
+const eg = new EGraph();
+
+// Add terms to the E-Graph
+const a = eg.add(new Term("a"));
+const b = eg.add(new Term("b"));
+const x = eg.add(new Term("x"));
+
+// Add compound terms
+const ax = eg.add(new Term("(+ a x)"));
+const bx = eg.add(new Term("(+ b x)"));
+
+// Initially, (+ a x) and (+ b x) are in different E-classes
+if (eg.find(ax) === eg.find(bx)) throw new Error("Should be different");
+
+// Merge a and b
+eg.merge(a, b);
+
+// Rebuild to restore congruence
+eg.rebuild();
+
+// Now (+ a x) and (+ b x) are in the same E-class
+if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same");
+```
+
 ### Congruence Closure
 
 The E-Graph automatically maintains congruence closure. When two E-classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-class:
@@ -120,4 +157,5 @@ Main class for E-Graph operations:
 ## Package Information
 
 - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
+- **npm Package**: [atsds-egg](https://www.npmjs.com/package/atsds-egg)
 - **Source Code**: [GitHub - egg directory](https://github.com/USTC-KnowledgeComputingLab/ds/tree/main/egg)
diff --git a/egg/README.md b/egg/README.md
index 5bf1f1d..49d391b 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -23,6 +23,12 @@ pip install apyds-egg
 
 Requires Python 3.11-3.14.
 
+### TypeScript/JavaScript (npm)
+
+```bash
+npm install atsds-egg
+```
+
 ## Quick Start
 
 ### Python Example
@@ -56,6 +62,37 @@ eg.rebuild()
 assert eg.find(ax) == eg.find(bx)
 ```
 
+### TypeScript Example
+
+```typescript
+import { Term } from "atsds";
+import { EGraph } from "atsds-egg";
+
+// Create an E-Graph
+const eg = new EGraph();
+
+// Add terms to the E-Graph
+const a = eg.add(new Term("a"));
+const b = eg.add(new Term("b"));
+const x = eg.add(new Term("x"));
+
+// Add compound terms
+const ax = eg.add(new Term("(+ a x)"));
+const bx = eg.add(new Term("(+ b x)"));
+
+// Initially, (+ a x) and (+ b x) are in different E-classes
+if (eg.find(ax) === eg.find(bx)) throw new Error("Should be different");
+
+// Merge a and b
+eg.merge(a, b);
+
+// Rebuild to restore congruence
+eg.rebuild();
+
+// Now (+ a x) and (+ b x) are in the same E-class
+if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same");
+```
+
 ## Core Concepts
 
 ### E-Graph
@@ -105,7 +142,8 @@ assert eg.find(fa) == eg.find(fb)
 ### Prerequisites
 
 - Python 3.11-3.14
-- apyds package
+- Node.js and npm
+- apyds and atsds packages
 
 ### Python Package
 
@@ -125,6 +163,21 @@ uv run pytest
 uv run pytest --cov
 ```
 
+### TypeScript Package
+
+```bash
+cd egg
+
+# Install dependencies
+npm install
+
+# Build package
+npm run build
+
+# Run tests
+npm test
+```
+
 ## License
 
 This project is licensed under the GNU Affero General Public License v3.0 or later (AGPL-3.0-or-later).
@@ -133,6 +186,7 @@ This project is licensed under the GNU Affero General Public License v3.0 or lat
 
 - **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/egg` directory)
 - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
+- **npm Package**: [atsds-egg](https://www.npmjs.com/package/atsds-egg)
 
 ## Author
 

From 0a947668082164aaf1315921f37b0708c3579814 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 25 Dec 2025 18:11:29 +0800
Subject: [PATCH 2/4] Update /egg/README.md

---
 egg/README.md | 42 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 37 insertions(+), 5 deletions(-)

diff --git a/egg/README.md b/egg/README.md
index 49d391b..b541d92 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -10,8 +10,6 @@ This package implements the egg-style E-Graph data structure with deferred congr
 - **Union-Find**: Path-compressed union-find for disjoint set management
 - **Congruence Closure**: Automatic maintenance of congruence relationships
 - **Deferred Rebuilding**: egg-style deferred rebuilding for performance
-- **Python Integration**: Seamless integration with apyds terms
-- **Type-Safe**: Full type hints for Python 3.11+
 
 ## Installation
 
@@ -106,7 +104,9 @@ An E-Graph is a data structure that efficiently represents and maintains equival
 
 ### Congruence Closure
 
-The E-Graph maintains congruence closure automatically. When two E-classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-class:
+The E-Graph maintains congruence closure automatically. When two E-classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-class.
+
+#### Python Example
 
 ```python
 eg = EGraph()
@@ -127,16 +127,48 @@ eg.rebuild()
 assert eg.find(fa) == eg.find(fb)
 ```
 
+#### TypeScript Example
+
+```typescript
+import { Term } from "atsds";
+import { EGraph } from "atsds-egg";
+
+const eg = new EGraph();
+
+// Add terms
+const fa = eg.add(new Term("(f a)"));
+const fb = eg.add(new Term("(f b)"));
+
+// Merge a and b
+const a = eg.add(new Term("a"));
+const b = eg.add(new Term("b"));
+eg.merge(a, b);
+
+// Rebuild maintains congruence
+eg.rebuild();
+
+// Now (f a) and (f b) are equivalent
+if (eg.find(fa) !== eg.find(fb)) throw new Error("Congruence failed");
+```
+
 ## API Overview
 
-### EGraph
+### Python (apyds-egg)
 
-- `__init__()`: Create a new E-Graph
+- `EGraph()`: Create a new E-Graph
 - `add(term: apyds.Term) -> EClassId`: Add a term to the E-Graph
 - `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-classes
 - `rebuild() -> None`: Restore congruence closure
 - `find(eclass: EClassId) -> EClassId`: Find canonical E-class representative
 
+### TypeScript (atsds-egg)
+
+- `new EGraph()`: Create a new E-Graph
+- `add(term: Term): EClassId`: Add a term to the E-Graph
+- `merge(a: EClassId, b: EClassId): EClassId`: Merge two E-classes
+- `rebuild(): void`: Restore congruence closure
+- `find(eclass: EClassId): EClassId`: Find canonical E-class representative
+
 ## Building from Source
 
 ### Prerequisites

From 1f641ea3be35dfd3e894833f2b88cf60fd88b933 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 25 Dec 2025 18:17:52 +0800
Subject: [PATCH 3/4] Update /egg/README.md

---
 egg/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/egg/README.md b/egg/README.md
index b541d92..d537225 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -164,7 +164,7 @@ if (eg.find(fa) !== eg.find(fb)) throw new Error("Congruence failed");
 ### TypeScript (atsds-egg)
 
 - `new EGraph()`: Create a new E-Graph
-- `add(term: Term): EClassId`: Add a term to the E-Graph
+- `add(term: atsds.Term): EClassId`: Add a term to the E-Graph
 - `merge(a: EClassId, b: EClassId): EClassId`: Merge two E-classes
 - `rebuild(): void`: Restore congruence closure
 - `find(eclass: EClassId): EClassId`: Find canonical E-class representative

From 39930473c1341103ea11e962f2d694574847a985 Mon Sep 17 00:00:00 2001
From: Hao Zhang <hzhangxyz@outlook.com>
Date: Thu, 25 Dec 2025 18:21:05 +0800
Subject: [PATCH 4/4] Update /docs/support-packages/egg.md

---
 docs/support-packages/egg.md | 51 ++++++++++++++++++++++++++++++------
 1 file changed, 43 insertions(+), 8 deletions(-)

diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index e1d0767..d92ea0e 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -86,7 +86,9 @@ if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same");
 
 ### Congruence Closure
 
-The E-Graph automatically maintains congruence closure. When two E-classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-class:
+The E-Graph automatically maintains congruence closure. When two E-classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-class.
+
+#### Python Example
 
 ```python
 eg = EGraph()
@@ -110,6 +112,33 @@ assert eg.find(fa) == eg.find(fb)
 assert eg.find(gfa) == eg.find(gfb)
 ```
 
+#### TypeScript Example
+
+```typescript
+import { Term } from "atsds";
+import { EGraph } from "atsds-egg";
+
+const eg = new EGraph();
+
+// Add terms with nested structure
+const fa = eg.add(new Term("(f a)"));
+const fb = eg.add(new Term("(f b)"));
+const gfa = eg.add(new Term("(g (f a))"));
+const gfb = eg.add(new Term("(g (f b))"));
+
+// Merge a and b
+const a = eg.add(new Term("a"));
+const b = eg.add(new Term("b"));
+eg.merge(a, b);
+
+// Rebuild propagates equivalence
+eg.rebuild();
+
+// Now all derived terms are equivalent
+if (eg.find(fa) !== eg.find(fb)) throw new Error("fa != fb");
+if (eg.find(gfa) !== eg.find(gfb)) throw new Error("gfa != gfb");
+```
+
 ## Core Concepts
 
 ### E-Graph Structure
@@ -144,15 +173,21 @@ The hash-consing mechanism ensures that identical E-Nodes share the same E-class
 
 ## API Reference
 
-### EGraph
-
-Main class for E-Graph operations:
+### Python (apyds-egg)
 
-- `__init__()`: Create a new empty E-Graph
-- `add(term: apyds.Term) -> EClassId`: Add a term and return its E-class ID
+- `EGraph()`: Create a new E-Graph
+- `add(term: apyds.Term) -> EClassId`: Add a term to the E-Graph
 - `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-classes
-- `rebuild() -> None`: Restore congruence closure by processing the worklist
-- `find(eclass: EClassId) -> EClassId`: Find the canonical E-class representative
+- `rebuild() -> None`: Restore congruence closure
+- `find(eclass: EClassId) -> EClassId`: Find canonical E-class representative
+
+### TypeScript (atsds-egg)
+
+- `new EGraph()`: Create a new E-Graph
+- `add(term: atsds.Term): EClassId`: Add a term to the E-Graph
+- `merge(a: EClassId, b: EClassId): EClassId`: Merge two E-classes
+- `rebuild(): void`: Restore congruence closure
+- `find(eclass: EClassId): EClassId`: Find canonical E-class representative
 
 ## Package Information