idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

[ codegen ] get rid of artifacts introduced when optimizing `IO` #3376

Closed stefan-hoeck closed 2 months ago

stefan-hoeck commented 3 months ago

Description

This fixes #3375 by adding two additional rules to constant folding.

gallais commented 3 months ago

Can we add a test case demonstrating it indeed fixes #3375? In the test runner, you should be able to use something like

awk -v RS= '/\/\* Main.main/' build/exec/main

to extract just the code of the main function from the javascript file.

stefan-hoeck commented 3 months ago

I added a test case using grep instead of awk. It checks the whole .js file for the patterns described in #3375 . None must be found. Funny enough, the new version no longer got rid of all the undefined cases. I therefore simplified the case where the variable term can be replaced.

stefan-hoeck commented 3 months ago

I removed the first line checking for CLocal: It was redundant. In addition, I added example functions for the four different forms of reducable let expressions: Nested and non-nested, the scrutinee being reducable or not.