Skip to content

Commit 71093ea

Browse files
saulshanabrooksaulshanabrook
committed
Add begining of rust docs
1 parent a0c37d6 commit 71093ea

File tree

2 files changed

+320
-0
lines changed

2 files changed

+320
-0
lines changed

‎docs/explanation.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
# Explanation
22

3+
```{toctree}
4+
explanation/compared_to_rust
5+
```
6+
37
## Status of this project
48

59
This package is in development and is not ready for production use. `egg-smol` itself

‎docs/explanation/compared_to_rust.md‎

Lines changed: 316 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,316 @@
1+
---
2+
file_format: mystnb
3+
kernelspec:
4+
name: python3
5+
---
6+
7+
# Compared to Rust implementation
8+
9+
This package serves two purposes:
10+
11+
1. Exposing the machinery of the Rust implementation to Python.
12+
2. Providing a Pythonic interface to build e-graphs.
13+
14+
Instead of skipping directly to the second step, we first expose the primitives
15+
from the rust library as close as we can to the original API. Then we build a
16+
higher level API on top of that, that is more friendly to use.
17+
18+
We can show show these two APIs starting witht he eqsat_basic example. The
19+
egg text version of this from the tests is:
20+
21+
```lisp
22+
(datatype Math
23+
(Num i64)
24+
(Var String)
25+
(Add Math Math)
26+
(Mul Math Math))
27+
28+
;; expr1 = 2 * (x + 3)
29+
(define expr1 (Mul (Num 2) (Add (Var "x") (Num 3))))
30+
;; expr2 = 6 + 2 * x
31+
(define expr2 (Add (Num 6) (Mul (Num 2) (Var "x"))))
32+
33+
34+
;; (rule ((= __root (Add a b)))
35+
;; ((union __root (Add b a)))
36+
(rewrite (Add a b)
37+
(Add b a))
38+
(rewrite (Mul a (Add b c))
39+
(Add (Mul a b) (Mul a c)))
40+
(rewrite (Add (Num a) (Num b))
41+
(Num (+ a b)))
42+
(rewrite (Mul (Num a) (Num b))
43+
(Num (* a b)))
44+
45+
(run 10)
46+
(check (= expr1 expr2))
47+
```
48+
49+
## Text API
50+
51+
One way to run this in Python is to parse the text and run it similar to how the
52+
egg CLI works:
53+
54+
```{code-cell} python
55+
eqsat_basic = """(datatype Math
56+
(Num i64)
57+
(Var String)
58+
(Add Math Math)
59+
(Mul Math Math))
60+
61+
;; expr1 = 2 * (x + 3)
62+
(define expr1 (Mul (Num 2) (Add (Var "x") (Num 3))))
63+
;; expr2 = 6 + 2 * x
64+
(define expr2 (Add (Num 6) (Mul (Num 2) (Var "x"))))
65+
66+
67+
;; (rule ((= __root (Add a b)))
68+
;; ((union __root (Add b a)))
69+
(rewrite (Add a b)
70+
(Add b a))
71+
(rewrite (Mul a (Add b c))
72+
(Add (Mul a b) (Mul a c)))
73+
(rewrite (Add (Num a) (Num b))
74+
(Num (+ a b)))
75+
(rewrite (Mul (Num a) (Num b))
76+
(Num (* a b)))
77+
78+
(run 10)
79+
(check (= expr1 expr2))"""
80+
81+
from egg_smol.bindings import EGraph
82+
83+
egraph = EGraph()
84+
egraph.parse_and_run_program(eqsat_basic)
85+
```
86+
87+
## Low level bindings API
88+
89+
However, this isn't the most friendly for Python users. Instead, we can use the
90+
low level APIs that mirror the rust APIs to build the same egraph:
91+
92+
```{code-cell} python
93+
from egg_smol.bindings_py import *
94+
95+
egraph = EGraph()
96+
egraph.declare_sort("Math")
97+
egraph.declare_constructor(Variant("Num", ["i64"]), "Math")
98+
egraph.declare_constructor(Variant("Var", ["String"]), "Math")
99+
egraph.declare_constructor(Variant("Add", ["Math", "Math"]), "Math")
100+
egraph.declare_constructor(Variant("Mul", ["Math", "Math"]), "Math")
101+
102+
# (define expr1 (Mul (Num 2) (Add (Var "x") (Num 3))))
103+
egraph.define(
104+
"expr1",
105+
Call(
106+
"Mul",
107+
[
108+
Call(
109+
"Num",
110+
[
111+
Lit(Int(2)),
112+
],
113+
),
114+
Call(
115+
"Add",
116+
[
117+
Call(
118+
"Var",
119+
[
120+
Lit(String("x")),
121+
],
122+
),
123+
Call(
124+
"Num",
125+
[
126+
Lit(Int(3)),
127+
],
128+
),
129+
],
130+
),
131+
],
132+
),
133+
)
134+
# (define expr2 (Add (Num 6) (Mul (Num 2) (Var "x"))))
135+
egraph.define(
136+
"expr2",
137+
Call(
138+
"Add",
139+
[
140+
Call(
141+
"Num",
142+
[
143+
Lit(Int(6)),
144+
],
145+
),
146+
Call(
147+
"Mul",
148+
[
149+
Call(
150+
"Num",
151+
[
152+
Lit(Int(2)),
153+
],
154+
),
155+
Call(
156+
"Var",
157+
[
158+
Lit(String("x")),
159+
],
160+
),
161+
],
162+
),
163+
],
164+
),
165+
)
166+
# (rewrite (Add a b)
167+
# (Add b a))
168+
egraph.add_rewrite(
169+
Rewrite(
170+
Call(
171+
"Add",
172+
[
173+
Var("a"),
174+
Var("b"),
175+
],
176+
),
177+
Call(
178+
"Add",
179+
[
180+
Var("b"),
181+
Var("a"),
182+
],
183+
),
184+
)
185+
)
186+
# (rewrite (Mul a (Add b c))
187+
# (Add (Mul a b) (Mul a c)))
188+
egraph.add_rewrite(
189+
Rewrite(
190+
Call(
191+
"Mul",
192+
[
193+
Var("a"),
194+
Call(
195+
"Add",
196+
[
197+
Var("b"),
198+
Var("c"),
199+
],
200+
),
201+
],
202+
),
203+
Call(
204+
"Add",
205+
[
206+
Call(
207+
"Mul",
208+
[
209+
Var("a"),
210+
Var("b"),
211+
],
212+
),
213+
Call(
214+
"Mul",
215+
[
216+
Var("a"),
217+
Var("c"),
218+
],
219+
),
220+
],
221+
),
222+
)
223+
)
224+
225+
# (rewrite (Add (Num a) (Num b))
226+
# (Num (+ a b)))
227+
lhs = Call(
228+
"Add",
229+
[
230+
Call(
231+
"Num",
232+
[
233+
Var("a"),
234+
],
235+
),
236+
Call(
237+
"Num",
238+
[
239+
Var("b"),
240+
],
241+
),
242+
],
243+
)
244+
rhs = Call(
245+
"Num",
246+
[
247+
Call(
248+
"+",
249+
[
250+
Var("a"),
251+
Var("b"),
252+
],
253+
)
254+
],
255+
)
256+
egraph.add_rewrite(Rewrite(lhs, rhs))
257+
258+
# (rewrite (Mul (Num a) (Num b))
259+
# (Num (* a b)))
260+
lhs = Call(
261+
"Mul",
262+
[
263+
Call(
264+
"Num",
265+
[
266+
Var("a"),
267+
],
268+
),
269+
Call(
270+
"Num",
271+
[
272+
Var("b"),
273+
],
274+
),
275+
],
276+
)
277+
rhs = Call(
278+
"Num",
279+
[
280+
Call(
281+
"*",
282+
[
283+
Var("a"),
284+
Var("b"),
285+
],
286+
)
287+
],
288+
)
289+
egraph.add_rewrite(Rewrite(lhs, rhs))
290+
291+
egraph.run_rules(10)
292+
egraph.check_fact(
293+
Eq(
294+
[
295+
Var("expr1"),
296+
Var("expr2"),
297+
]
298+
)
299+
)
300+
```
301+
302+
This has a couple of advantages over the text version. Users now know what types
303+
of functions are available to them and also it can be statically type checked with MyPy,
304+
to make sure that the types are correct.
305+
306+
However, it is much more verbose than the text version!
307+
308+
## High level API
309+
310+
So would it be possible to make an API that:
311+
312+
1. Statically type checks as much as possible with MyPy
313+
2. Is concise to write
314+
3. Feels "pythonic"
315+
316+
TODO: Finish this section

0 commit comments

Comments
 (0)