Extracted Declarations are Temporary Variables

[saulshanabrook]

Currently, declarations are a bit odd since they cannot be extracted. Or they can, but what you end up with is a temporary variable that it's unclear how it relates to the original declaration. For example:

(datatype Hi)
(declare x Hi)
(extract x)
# (v0___)

Why

This is how declare is currently desugared:

https://github.com/egraphs-good/egglog/blob/b78f69ca1f7187c363bb31271c8e8958f477f15d/src/ast/desugar.rs#L392-L409

It makes a fresh function (which is what is extracted) and creates a let binding with that name to the function.

There @yihozhang had a previous PR that changes this behavior to make declare's unextractable (https://github.com/egraphs-good/egglog/pull/141) but it was closed.

Personally, it would be nice if there would be a way to make them extractable. In the Python bindings, I compile the "constant" (aka a "declare") into a nullary function, but I make the function name the name that the user passes in and return it called. Then, on pretty printing, I just show it as a constant, instead of as a function call. However, if I could compile directly to the declare that would be nice!

[oflatt]

Good catch I see two solutions:

1. Get rid of declare all together because it's annoying and currently broken
2. Make declare actually work as you mentioned, by transforming all code after it to refer to a nullary function

I'm currently working on desugaring all globals to use nullary functions again internally We could desugar declare similarly

[oflatt]

I'm actually in favor of getting rid of declare, since it causes confusion.

[yihozhang]

declare is convenient for declaring constants like True and False (similar to declare-const in z3).

IMO it might be more consistent to desugar both declare and let to extractable function with a special flag can_be_used_without_parentheses (I'm sure we can come up with a shorter name). This is also aligned with our goal to remove globals from the backend implementation.

[saulshanabrook]

IMO it might be more consistent to desugar both declare and let to extractable function

That sounds good to me, but with let functions being marked unextractable.

[yihozhang]

Good point! I remember @oflatt also mentioned that we want to mark let-bound E-classes special in the visualization, but not as an E-node, so this means:

• declare: desugars to function, don't need parentheses, extractable, shown in the viz as an E-node in an E-class.
• let: desugars to function, don't need parentheses, not extractable, shown in the viz as a tag over an E-class.

[saulshanabrook]

That sounds good. Previously I had the types of each e-class as a tag visually, so I don't think it should be too hard to get the tag(s) to show up there if we can get them in the serialized format somehow.

[oflatt]

I don't like the idea of can_be_used_without_parenthesis I would prefer must_be_used_without_parenthesis since in the past the ambiguity between parenthesis or none has been a source of bugs and confusion.

But also I'd rather write a compiler pass that adds parenthesis everywhere and this flag won't be necessary (except maybe as an annotation for visualization)

[oflatt]

But besides disallowing parenthesis, I like the visualization ideas Yihong had

[yihozhang]

Closing since declare are gone #418