From f0be5d6e1e22c1878448b15c0f7d945a0a611e96 Mon Sep 17 00:00:00 2001
From: Saul Shanabrook <s.shanabrook@gmail.com>
Date: Fri, 28 Jul 2023 13:55:39 -0400
Subject: [PATCH] Document properties and conversions

---
 docs/reference.md                    |  1 +
 docs/reference/egglog-translation.md | 31 ++++++++++++++++++++++------
 docs/reference/python-integration.md |  9 ++++++++
 3 files changed, 35 insertions(+), 6 deletions(-)
 create mode 100644 docs/reference/python-integration.md

diff --git a/docs/reference.md b/docs/reference.md
index 9d6b930d..3585f6ab 100644
--- a/docs/reference.md
+++ b/docs/reference.md
@@ -4,5 +4,6 @@
 changelog
 reference/high-level
 reference/egglog-translation
+reference/python-integration
 reference/bindings
 ```
diff --git a/docs/reference/egglog-translation.md b/docs/reference/egglog-translation.md
index 1620e854..613265b0 100644
--- a/docs/reference/egglog-translation.md
+++ b/docs/reference/egglog-translation.md
@@ -12,7 +12,6 @@ The currently unsupported features are:
 
 - Proof mode: Not currently tested, but could add support if needed.
 - Naive mode: Not currently exposed, but could add support
-- `(include ...)`: This command includes another `.egg` file, so not sure how this would translate to Python.
 - `(output ...)`: No examples in the tests, so not sure how this works.
 - `(calc ...)`: Could be implemented, but haven't yet.
 
@@ -145,14 +144,14 @@ Note that by default, the egg name for any method is the Python class name combi
 #   (Num i64)
 #   (Var String)
 #   (Add Math Math)
-#   (Mul Math Math))
+#   (Mul Math Math)
+#   (Neg Math))
 
 @egraph.class_
 class Math(Expr):
     @egraph.method(egg_fn="Num")
     def __init__(self, v: i64Like):
         ...
-
     @egraph.method(egg_fn="Var")
     @classmethod
     def var(cls, v: StringLike) -> Math:
@@ -166,8 +165,28 @@ class Math(Expr):
     def __mul__(self, other: Math) -> Math:
         ...
 
-# egg:  (Mul (Num 2) (Add (Var "x") (Num 3))))
-Math(2) * (Math.var("x") + Math(3))
+    @egraph.method(egg_fn="Neg")
+    @property
+    def neg(self) -> Math:
+        ...
+
+# egg: (Neg (Mul (Num 2) (Add (Var "x") (Num 3)))))
+(Math(2) * (Math.var("x") + Math(3))).neg
+```
+
+As shown above, we can also use the `@classmethod` and `@property` decorators to define class methods and properties.
+
+#### Custom Type Promotion
+
+Similar to how an `int` can be automatically upcasted to an `i64`, we also support registering conversion to your custom types. For example:
+
+```{code-cell} python
+converter(int, Math, Math)
+converter(str, Math, Math.var)
+
+Math(2) + 30 + "x"
+# equal to
+Math(2) + Math(i64(30)) + Math.var(String("x"))
 ```
 
 ### Declarations
@@ -328,7 +347,7 @@ Since it uses a fluent API, static type checkers can verify that the type of the
 
 The `(birewrite ...)` command in egglog is syntactic sugar for creating two rewrites, one in each direction. In Python, we can use the `birewrite(expr).to(expr, *when)` function to create two rules that rewrite in each direction.
 
-### Using funcitons to define vars
+### Using functions to define vars
 
 Instead of defining variables with `vars_`, we can also use functions to define variables. This can be more succinct
 and also will make sure the variables won't be used outside of the scope of the function.
diff --git a/docs/reference/python-integration.md b/docs/reference/python-integration.md
new file mode 100644
index 00000000..c3da4b95
--- /dev/null
+++ b/docs/reference/python-integration.md
@@ -0,0 +1,9 @@
+---
+file_format: mystnb
+---
+
+# Python Integration
+
+Alongside [the support for builtin `egglog` functionality](./egglog-translation.md), `egglog` also provides functionality to more easily integrate with the Python ecosystem.
+
+## Methods, Classmethods, and P