epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Extract SymbolTransformerComposition to not be local #220

Closed sankalpgambhir closed 3 months ago

sankalpgambhir commented 3 months ago

Move local class def outside the local scope.

The documented reason for the existence of the local class was to provide an equality function on composition of transformers. The type check for this causes a warning

Simply moving the class out of the local scope is not enough, as dotty is not convinced that the type refinements actually work out. The solution is to add a shallow local class with more precise types, but have the equality function be extracted to a non-local class.