Add class KoreDefn

[tothtamas28]

• Encapsulates semantic information about a Definition: sorts, symbols, the sort ordering, rewrite and function rules.
• Method project_to_rewrites removes all sorts, symbols and function rules that are not relevant for rewriting.

[tothtamas28]

Based on an ad-hoc experiment, for imp-semantics, about 40% of sorts, 60% of symbols, and more than 90% of function symbols present in definition.kore are irrelevant for rewriting.

For evm-semantics, the numbers are about 40%, 60% and 75%, respectively.

[jberthold]

Based on an ad-hoc experiment, for imp-semantics, about 40% of sorts, 60% of symbols, and more than 90% of function symbols present in definition.kore are irrelevant for rewriting.

For evm-semantics, the numbers are about 40%, 60% and 75%, respectively.

I agree we are carrying around some (typically auto-generated) payload that we won't usually need (those project_ functions, for one).
However, symbols being "not relevant for rewriting" (i.e. not occurring on rewrite rules) can still not be simply stripped off from the definition. They can be in the input, and need to be known to the rewrite engine to accept them in input.

BTW does the "rewriting" include function equations? Because obviously function symbols don't appear in rewrite rules on the LHS, they can only be on the RHS.

[tothtamas28]

However, symbols being "not relevant for rewriting" (i.e. not occurring on rewrite rules) can still not be simply stripped off from the definition. They can be in the input, and need to be known to the rewrite engine to accept them in input.

That's fair. In this particular case though, we need this transformation for the Lean 4 backend, where only rewrite rules are relevant (or just some of them, which will be a generalization of this transformation).

Edit: #4712 (comment)

BTW does the "rewriting" include function equations?

Yes, for those function symbols that appear in rewrite rules (transitively).

[tothtamas28]

However, symbols being "not relevant for rewriting" (i.e. not occurring on rewrite rules) can still not be simply stripped off from the definition. They can be in the input, and need to be known to the rewrite engine to accept them in input.

I ran into a corner case for this actually: the GeneratedCounterCell constructor is stripped as the cell is abstract in all rewrite rules. Moving the PR back to draft to fix this.

[jberthold]

LGTM