More precision in partial evaluation

[cdisselkoen]

Category

Lean formalization

Describe the feature you'd like to request

Although there are many ways in which partial evaluation could be more precise, this issue is specifically about evaluateHasAttr and evaluateGetAttr. Currently, when evaluating x has attr or x.attr, if x is a Partial.Value.residual, these functions make no attempt to simplify. But, in some cases, even if x is a residual we may know concretely whether it contains the particular attr we care about (hasAttr case) or we may have a concrete value for the particular attr we care about (getAttr case). These functions could check for these conditions and be more aggressive.

Describe alternatives you've considered

Status quo is still sound.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change