Fix ExtractReport generation and extracting in sub-graph

[saulshanabrook]

In the switch to using an extract action over an extract command in #176, the saving of the extracted expressions in a report was lost.

This PR restores that behavior and also refactors the ExtractReport to be an enum. In #176, the extraction logic was also changed, so that if passed in a non-zero number of variants, it would no longer perform a normal cost-based extraction as well. So now the report captures these two cases as distinct.

This PR also fixes printing the extracted expression in the simplify command, which was broken in #195.

[saulshanabrook]

This function was previously used in a number of places before #176 and was now only being used in the un-tested Output command.

[mwillsey]

Do we want the report to be an enum? I feel that the single and multiple extraction case could be handled uniformly, no?

[saulshanabrook]

Do we want the report to be an enum? I feel that the single and multiple extraction case could be handled uniformly, no?

After #176, the logic for the extraction now seems disjoint between the variants and the best. If there are variants, then there is no "best" expression extracted, and vice versa:

egglog/src/typecheck.rs

Lines 879 to 909 in 9e53038

	if variants == 0 {
	let (cost, expr) = self.extract(
	values[0],
	&mut termdag,
	self.proof_state
	.type_info
	.sorts
	.get(&values[0].tag)
	.unwrap(),
	);
	let extracted = termdag.to_string(&expr);
	log::info!("extracted with cost {cost}: {}", extracted);
	self.print_msg(extracted);
	} else {
	if variants < 0 {
	panic!("Cannot extract negative number of variants");
	}
	let extracted =
	self.extract_variants(values[0], variants as usize, &mut termdag);
	log::info!("extracted variants:");
	let mut msg = String::default();
	msg += "(\n";
	assert!(!extracted.is_empty());
	for expr in extracted {
	let str = termdag.to_string(&expr);
	log::info!(" {}", str);
	msg += &format!(" {}\n", str);
	}
	msg += ")";
	self.print_msg(msg);
	}

Whereas previously, if you extracted some variants, a best was also extracted.

So I thought now an enum is appropriate?

[saulshanabrook]

On another note, I noticed that simplify is not working with this new scheme, due to it running the extraction in a sub-egraph.

As a solution, I am considering changing from a saved "report" to a callback on the EGraph which is called during extraction.

Any thoughts on that?

[mwillsey]

What simplify are we talking about? I’m not sure what the callback would do.

…

On Wed, Aug 23, 2023 at 10:42 AM Saul Shanabrook ***@***.***> wrote: On another note, I noticed that simplify is not working with this new scheme, due to it running the extraction in a sub-egraph. As a solution, I am considering changing from a saved "report" to a callback on the EGraph which is called during extraction. Any thoughts on that? — Reply to this email directly, view it on GitHub <#205 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AANTPTDSK7IR6UMXREKY44LXWY6IFANCNFSM6AAAAAA33ZJDC4> . You are receiving this because you commented.Message ID: ***@***.***>

[saulshanabrook]

What simplify are we talking about?

The simplify command, i.e. like for this example:

(datatype Expr
  (Num i64))

(let x (Num 1))
(simplify (run) x)

I’m not sure what the callback would do.

Instead of adding a report, it would call a callback on every extraction, so that from Python, we could still see what was extracted.

I opted not to do this, due to the added complexity, and instead copy reports from children to parents when popping.

[oflatt]

looks like a good change to me!

[oflatt]

This looks like a good change, and fixes a bug in preserving messages across push/pop.
Had a small nit before we merge.