Add documentation for egg subpackage by Copilot · Pull Request #159 · USTC-KnowledgeComputingLab/ds

Copilot · 2025-12-22T11:09:20Z

The egg subpackage (E-Graph library for DS) was missing documentation. Added comprehensive docs following bnf subpackage structure.

Changes

/egg/README.md: Full package documentation with installation, usage examples, API reference, and core concepts (E-Graph and congruence closure). Includes reference to the egg library as inspiration for this implementation.
/docs/support-packages/egg.md: Documentation site page with usage patterns and streamlined API reference
/README.md: Added egg package link in "Support Packages" section (equality reasoning only)
/mkdocs.yml: Added egg navigation entry under "Support Packages"

Example Usage

import apyds
from apyds_egg import EGraph

eg = EGraph()
ax = eg.add(apyds.Term("(+ a x)"))
bx = eg.add(apyds.Term("(+ b x)"))

# Initially different E-classes
assert eg.find(ax) != eg.find(bx)

# Merge a and b, rebuild for congruence
eg.merge(eg.add(apyds.Term("a")), eg.add(apyds.Term("b")))
eg.rebuild()

# Now congruent terms share E-class
assert eg.find(ax) == eg.find(bx)

Documentation Scope

The documentation focuses on the core E-Graph functionality for equality reasoning. Internal implementation details (Union-Find, E-Nodes) are not exposed in the user-facing API documentation. Test commands use uv run pytest to match the project's build system.

Documentation follows E-class (lowercase) terminology consistent with source code.

Original prompt

This section details on the original issue you should resolve

<issue_title>需要给egg subpackage补充 docs的一个页面, 以及README上的一个link</issue_title>
<issue_description>模仿bnf这个subpackage的格式和颗粒度</issue_description>

Comments on the Issue (you are @copilot in this section)

Fixes 需要给egg subpackage补充 docs的一个页面, 以及README上的一个link #150

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

- Created README.md for egg subpackage with detailed API and usage examples - Added docs/support-packages/egg.md documentation page - Updated main README.md to include link to egg subpackage - Updated mkdocs.yml to include egg documentation in navigation Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

- Simplify GitHub repository link in egg/README.md - Clarify hash-consing terminology in docs/support-packages/egg.md - Expand Items and Variables explanation with examples Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

- Updated all occurrences to use lowercase 'c' for consistency with source code - Fixed variable example formatting in documentation Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

hzhangxyz · 2025-12-22T11:18:48Z

 ## 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 and term rewriting. See [/egg](/egg) for details.


这个只支持equality reasoning, 没有rewriting功能.

Removed "term rewriting" mention in c2c9475.

hzhangxyz · 2025-12-22T11:19:17Z

+
+An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
+
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning and term rewriting.


没有term rewriting功能, 把这个去掉.

Removed "term rewriting" in c2c9475.

hzhangxyz · 2025-12-22T11:22:33Z

+
+An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
+
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning and term rewriting.


加一下 egg 的链接: https://egraphs-good.github.io/ 我们是照着他实现的

Added egg library reference link in c2c9475.

hzhangxyz · 2025-12-22T11:24:10Z

+- **Union-Find**: Data structure for managing E-class equivalence
+- **Congruence**: Two terms are congruent if they have the same operator and their children are in equivalent E-classes
+
+### Union-Find


union find 不需要在core concepts里介绍

Removed Union-Find section from Core Concepts in c2c9475.

hzhangxyz · 2025-12-22T11:24:24Z

+assert uf.find(a) == uf.find(b)
+```
+
+### E-Nodes


e nodes不需要在core concepts里介绍

Removed E-Nodes section from Core Concepts in c2c9475.

hzhangxyz · 2025-12-22T11:25:03Z

+- `find(x: T) -> T`: Find canonical representative with path compression
+- `union(a: T, b: T) -> T`: Union two sets
+
+### ENode


这个也不需要介绍

Removed ENode from API Overview in c2c9475.

hzhangxyz · 2025-12-22T11:26:09Z

+uv build
+
+# Run tests
+pytest


应该是uv run pytest 和 uv run pytest --cov

Updated to use "uv run pytest" and "uv run pytest --cov" in c2c9475.

hzhangxyz · 2025-12-22T11:26:53Z

+pytest --cov
+```
+
+### Running Tests


这个没啥用, running tests删了吧

Removed "Running Tests" section in c2c9475.

hzhangxyz · 2025-12-22T11:27:31Z

+
+## Repository
+
+- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds)


加一下 (in /egg directory) 的说法在这里

Added "(in /egg directory)" to repository link in c2c9475.

hzhangxyz · 2025-12-22T11:28:01Z

@@ -0,0 +1,167 @@
+# E-Graph Support Package


这个文件还没检查, 但是参考我对README的评论先修改一版

Applied similar changes to docs/support-packages/egg.md in c2c9475: removed Union-Find example, removed UnionFind/ENode/EClassId API sections, and added egg library reference.

- Remove "term rewriting" mentions (only supports equality reasoning) - Add egg library reference link (https://egraphs-good.github.io/) - Remove Union-Find and E-Nodes sections from Core Concepts - Remove UnionFind, ENode, and EClassId from API Overview - Update test commands to use "uv run pytest" - Remove "Running Tests" section - Add "(in /egg directory)" to repository link Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

hzhangxyz · 2025-12-22T11:36:03Z

+
+An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
+
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning. Based on the [egg library](https://egraphs-good.github.io/).


不是based on....我们只是参考了这个库

Changed to "Inspired by" in de8116b.

hzhangxyz · 2025-12-22T11:36:19Z

@@ -0,0 +1,123 @@
+# E-Graph Support Package


这个文件依然没有检查, 请对照对readme的评论

Updated docs/support-packages/egg.md with the same "Inspired by" wording in de8116b. The file already had all the simplifications from the README (no Union-Find/E-Nodes sections in Core Concepts, no UnionFind/ENode/EClassId in API Reference).

The implementation references the egg library but is not directly based on it. Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Copilot

Pull request overview

This PR adds comprehensive documentation for the egg subpackage (E-Graph library), following the structure and granularity established by the bnf subpackage. The documentation covers installation, usage examples, core concepts (E-Graph structure, congruence closure, deferred rebuilding), and API reference.

Key changes:

Complete package documentation with examples demonstrating equality reasoning and congruence closure
Documentation site integration under "Support Packages" section
Main repository README updated to reference the new package

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
egg/README.md	New comprehensive README covering features, installation, usage examples, core concepts, API overview, and build instructions for the egg package
docs/support-packages/egg.md	New documentation site page with detailed usage patterns, core concepts explanation, and API reference for the E-Graph support package
README.md	Added egg package entry in the Support Packages section linking to apyds-egg on PyPI
mkdocs.yml	Added E-Graph navigation entry under Support Packages section

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-22T11:52:46Z

+
+Terms are converted to E-Nodes and added to the E-Graph:
+
+- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or backtick-prefixed variables like `x` are represented as E-Nodes with no children


The example for backtick-prefixed variables is missing the backtick prefix. Change "like x" to "like `x" to correctly demonstrate the backtick prefix syntax for variables.

Suggested change

- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or backtick-prefixed variables like `x` are represented as E-Nodes with no children

- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or backtick-prefixed variables like `` `x `` are represented as E-Nodes with no children

Initial plan

3e0c879

Copilot AI assigned Copilot and hzhangxyz Dec 22, 2025

Copilot started work on behalf of hzhangxyz December 22, 2025 11:09 View session

Copilot AI and others added 4 commits December 22, 2025 11:13

Address code review feedback

837a2bf

- Simplify GitHub repository link in egg/README.md - Clarify hash-consing terminology in docs/support-packages/egg.md - Expand Items and Variables explanation with examples Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Fix markdown backtick formatting

2ca7157

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Improve consistency: use E-class instead of E-Class

325eb2f

- Updated all occurrences to use lowercase 'c' for consistency with source code - Fixed variable example formatting in documentation Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Copilot AI changed the title ~~[WIP] Add documentation page for egg subpackage~~ Add documentation for egg subpackage Dec 22, 2025

Copilot AI requested a review from hzhangxyz December 22, 2025 11:20

Copilot finished work on behalf of hzhangxyz December 22, 2025 11:20

hzhangxyz requested changes Dec 22, 2025

View reviewed changes

Copilot started work on behalf of hzhangxyz December 22, 2025 11:28 View session

Copilot AI requested a review from hzhangxyz December 22, 2025 11:33

Copilot finished work on behalf of hzhangxyz December 22, 2025 11:33

hzhangxyz requested changes Dec 22, 2025

View reviewed changes

Copilot started work on behalf of hzhangxyz December 22, 2025 11:37 View session

Change "Based on" to "Inspired by" for egg library reference

de8116b

The implementation references the egg library but is not directly based on it. Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>

Copilot AI requested a review from hzhangxyz December 22, 2025 11:40

Copilot finished work on behalf of hzhangxyz December 22, 2025 11:40

hzhangxyz approved these changes Dec 22, 2025

View reviewed changes

hzhangxyz marked this pull request as ready for review December 22, 2025 11:46

Copilot AI review requested due to automatic review settings December 22, 2025 11:46

hzhangxyz merged commit 67b2286 into main Dec 22, 2025
63 checks passed

Copilot started reviewing on behalf of hzhangxyz December 22, 2025 11:48 View session

Copilot AI reviewed Dec 22, 2025

View reviewed changes


		An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.

		This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning and term rewriting.


		## Repository

		- GitHub: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds)


		Terms are converted to E-Nodes and added to the E-Graph:

		- Items (constants/functors) and Variables: Atomic terms like `a`, `b`, or backtick-prefixed variables like `x` are represented as E-Nodes with no children

Uh oh!

Conversation

Copilot AI commented Dec 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Example Usage

Documentation Scope

Comments on the Issue (you are @copilot in this section)

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Dec 22, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Copilot AI commented Dec 22, 2025 •

edited

Loading