This PR moves the constructor layout code from C++ to Lean. When writing the new compiler, we just reused the existing C++ code, even though it was a bit inconvenient, because we wanted to ensure that constructor layout always matched the existing compiler. This fixes #2589 by handling struct field types just like any other type being lowered, and thus applying the trivial structure optimization in the process. Originally, I wanted to port the code to Lean without any functional changes, but I found that it took less code to just implement it "correctly" and get this fix as a consequence than to emulate the bugs of the existing C++ implementation. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||