fresh! macro #34
fresh! macro #34
Conversation
There was a problem hiding this comment.
Pull request overview
This PR introduces the unstable-fresh! macro for egglog-experimental, which enables the generation of fresh values in rewrite rules. The macro desugars into a generated constructor function that captures query context and produces unique values based on the rule's matched expressions and an incremental counter.
Key changes:
- Implements
FreshMacrocommand macro with proper type-checking integration - Adds comprehensive test coverage through both Rust tests and
.eggtest files - Changes dependencies from git URLs to local paths for development purposes
Reviewed changes
Copilot reviewed 7 out of 8 changed files in this pull request and generated 10 comments.
Show a summary per file
| File | Description |
|---|---|
| src/fresh_macro.rs | Core implementation of the unstable-fresh! macro with typechecking support |
| src/fresh_macro_typed.rs | Unused alternative implementation that should be removed |
| src/lib.rs | Registers the fresh macro and reorganizes parser setup, but accidentally removes run-schedule command registration |
| Cargo.toml | Changes dependencies to local paths (should be reverted before merge) |
| Cargo.lock | Updates lock file to reflect local dependencies |
| tests/test_fresh.rs | Comprehensive Rust integration tests for fresh macro functionality |
| tests/test_fresh.egg | Test case verifying fresh value uniqueness |
| tests/test_simple_fresh.egg | Basic fresh macro test case |
| tests/test_working_fresh.egg | Test case with multiple check statements |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
yihozhang
left a comment
yihozhang
left a comment
There was a problem hiding this comment.
Left some comments mostly about things that could be drastically simplified using visit_exprs and subst. Also followed up on Slack about a Skolemization-related question.
Are the failing tests only those related to resugaring? Could you describe what caused the failure again? I think I am fine with disabling resugaring tests, since they are nice to have but don't exhibit a real use case right now.
| } | ||
| } | ||
|
|
||
| fn collect_fresh_sorts(actions: &[Action]) -> Vec<Symbol> { |
There was a problem hiding this comment.
We don't need contains_fresh_* if we already have collect_fresh_*
There was a problem hiding this comment.
This should be implementable with Actions::visit_exprs
| fn collect_fresh_from_expr(expr: &Expr, sorts: &mut Vec<Symbol>) { | ||
| match expr { | ||
| Expr::Call(_span, head, args) if head.as_str() == "unstable-fresh!" => { | ||
| if args.len() == 1 { |
There was a problem hiding this comment.
What if args.len() != 1, or the argument is not a variable? Will an error be thrown somewhere?
| ) -> Result<Vec<Command>, Error> { | ||
| // Collect unstable-fresh! sorts from actions | ||
| let fresh_sorts = collect_fresh_sorts(&rule.head.0); | ||
| if fresh_sorts.is_empty() { |
There was a problem hiding this comment.
This seems redundant since the assumption was this rule contains fresh!
| let rule_span = rule.span.clone(); | ||
|
|
||
| // Typecheck the query to get resolved facts with type information | ||
| let resolved_facts = type_info.typecheck_facts(symbol_gen, &rule.body)?; |
There was a problem hiding this comment.
Nit: In some corner cases, queries in rules don't have unique types. It needs to be inferred together with the actions. For example:
(rule (
(= x (new-vec))
) (
(R x)
))
| } | ||
|
|
||
| // Convert ResolvedExpr to surface Expr | ||
| fn resolved_to_surface(expr: &ResolvedExpr) -> Expr { |
There was a problem hiding this comment.
This can be implemented using Expr::subst, similar to Fact::make_unresolved in egglog main.
| } | ||
|
|
||
| // Collect all unique subexpressions from resolved facts with their types | ||
| fn collect_query_columns(resolved_facts: &[ResolvedFact]) -> IndexSet<(Expr, Symbol)> { |
There was a problem hiding this comment.
can be simplified with visit_exprs?
| output: output_sort, | ||
| }, | ||
| cost: None, | ||
| unextractable: true, |
There was a problem hiding this comment.
Hmm, not sure about unextractability.. This doesn't matter for eggcc, but for chase-like applications the skolem term might be the sole e-node in its e-class, and we want to print tuples with skolem terms. On the other hand the term would look ugly
| } | ||
| } | ||
|
|
||
| fn rewrite_fresh_action( |
|
Yeah I also agree that disabling sugaring tests could be OK for now here |
Depends on https://github.com/egraphs-good/egglog/pull/741/files