Merge pull request #27 from metadsl/modules

Add proper module system

Author: saulshanabrook

docs/changelog.md

@@ -12,6 +12,8 @@ _This project uses semantic versioning. Before 1.0.0, this means that every brea
   - Added `Vec` sort
   - Added support for variable args for builtin functions, to use in creation of `Vec` and `Set` sorts.
 - Switch generated egg names to use `.` as seperate (i.e. `Math.__add__`) instead of `_` (i.e. `Math___add__`)
+- Adds support for modules to define functions/sorts/rules without executing them, for reuse in other modules
+  - Moved simplifying and running rulesets to the `run` and `simplify` methods on the `EGraph` from those methods on the `Ruleset` since we can now create `Rulset`s for modules which don't have an EGraph attached and can't be run
 
 ## 0.4.0 (2023-05-03)
 

docs/reference/egglog-translation.md

@@ -311,7 +311,7 @@ path_ruleset = egraph.ruleset("path")
 # (rule ((edge x y))
 #       ((path x y)) :ruleset path)
 x, y = vars_("x y", i64)
-path_ruleset.register(rule(edge(x, y)).then(path(x, y)))
+egraph.register(rule(edge(x, y), ruleset=path_ruleset).then(path(x, y)))
 ```
 
 ### Rewrites
@@ -348,8 +348,7 @@ Rulsets can be run as well, by calling the `run` method on them:
 
 ```{code-cell} python
 # egg: (run 10 :ruleset path)
-run_report = path_ruleset.run(10)
-run_report
+egraph.run(10, ruleset=path_ruleset)
 ```
 
 After a run, you get a run report, with some timing information as well as whether things were updated.
@@ -406,19 +405,18 @@ step_egraph.register(left(i64(0)), right(i64(0)))
 x, y = vars_("x y", i64)
 
 step_left = step_egraph.ruleset("step-left")
-step_left.register(
+step_right = step_egraph.ruleset("step-right")
+step_egraph.register(
     rule(
         left(x),
         right(x),
-    ).then(left(x + 1))
-)
-
-step_right = step_egraph.ruleset("step-right")
-step_right.register(
+        ruleset=step_left
+    ).then(left(x + 1)),
     rule(
         left(x),
         right(y),
         eq(x).to(y + 1),
+        ruleset=step_right
     ).then(right(x))
 )
 
@@ -501,3 +499,48 @@ with egraph:
     egraph.check(eq(Math(0)).to(Math(1)))
 egraph.check_fail(eq(Math(0)).to(Math(1)))
 ```
+
+## Include
+
+The `(include <path>)` command is used to add modularity, by allowing you to pull in the source from another egglog file into the current file.
+
+In Python, we support the same use case with the ability to define a `Module` which is then depended on in `EGraph`. All commands registered on a `Module` won't be run immediately on an `EGraph`, but instead stored so that when they are included, they will be run:
+
+```{code-cell} python
+# egg file: path.egg
+# (relation path (i64 i64))
+# (relation edge (i64 i64))
+#
+# (rule ((edge x y))
+#       ((path x y)))
+#
+# (rule ((path x y) (edge y z))
+#       ((path x z)))
+#
+# egg:
+# (include "path.egg")
+# (edge 1 2)
+# (edge 2 3)
+# (edge 3 4)
+# (run 3)
+# (check (path 1 3))
+
+path_mod = Module()
+path = path_mod.relation("path", i64, i64)
+edge = path_mod.relation("edge", i64, i64)
+
+x, y, z = vars_("x y z", i64)
+path_mod.register(
+    rule(edge(x, y)).then(path(x, y)),
+    rule(path(x, y), edge(y, z)).then(path(x, z)),
+)
+
+egraph = EGraph([path_mod])
+egraph.register(
+    edge(1, 2),
+    edge(2, 3),
+    edge(3, 4)
+)
+egraph.run(3)
+egraph.check(path(1, 3))
+```

python/egglog/bindings.pyi

@@ -214,6 +214,7 @@ class ExtractReport:
 ##
 # Schedules
 ##
+
 @final
 class Saturate:
     schedule: _Schedule