Desugar global variables away

egraphs-good / egglog

egraphs + datalog!

https://egraphs-good.github.io/egglog/

MIT License

459 stars 54 forks source link

Desugar global variables away #338

Closed oflatt closed 8 months ago

oflatt commented 9 months ago

This PR adds a brand new, type-preserving pass that gets rid of all global variables by tuning them into functions. This does not yet resolve the issue about declare: #334 Example:

(let x 3)
(Add x x)

becomes

(function x () i64)
(set (x) 3)
(Add (x) (x))

Most of this PR is helpers, such as map_exprs, which allows us to map over all exprs in the whole egglog program.

Here are some questions we need to resolve before this is merged:

[ ] While refactoring map_exprs, I had to add a lot of type constraints throughout the ast. It's a lot of boilerplate- is there a way to get rid of them?
[x] How does this affect visualizations? Right now the function is unextractable, but probably still shows up in the viz which is incorrect
[ ] Can we remove AtomTerm::Global? Seems like the typechecker uses core actions so maybe not? Right now we have several panics in the back end when we see a global.

oflatt commented 9 months ago

Assigning @yihozhang to review, added @saulshanabrook in case they wanted to take a look

saulshanabrook commented 9 months ago

Is there a feature/bug this resolves or is it mainly meant to make the implementation cleaner?

oflatt commented 9 months ago

It just makes it cleaner Also will help with adding proofs

oflatt commented 9 months ago

This PR is ready to merge The two other remaining TODOs are optional

oflatt commented 9 months ago

Just had another pass. This is great and the code is easy to follow. Besides questions in the comments, I have a higher-level question:

Have you thought about removing global variables during the desugaring phase before the type checking? This way ResolvedVar does not need to carry an is_global_ref field around. Currently, this field makes sense only for the typechecking and the globals removal passes.

If we can do this, then the typechecking and passes after this will only be dealing with local variables, and we can entirely remove AtomTerm::Global.

Instead of having TypeInfo to track the set of global variables, we can have Desugar responsible for managing a set of globals to be desugared.

I've thought of this, and I agree it would be much nicer. The problem is, this pass actually does depend on type information: it needs to know the type of the global being desugared.

oflatt commented 9 months ago

@yihozhang is this ready to merge?

oflatt commented 9 months ago

Thanks for fixing up, I must have lost the commit where I fixed those

oflatt commented 8 months ago

@yihozhang I've refactored this PR to not look up values in actions. It adds to the query instead. I'm going to refactor generating fresh symbols next.