search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
395 stars 59 forks source link

remove backtracking in `reduce_full_match` #401

Closed amosr closed 10 months ago

amosr commented 10 months ago

this PR (hopefully) addresses a performance / non-termination problem I was having.

I had a problematic program contains many matches where the scrutinee itself contains nested matches (eg match match match match match match t with ... with ... with ...). in reduce_full_matches, it reduces the scrutinee and the branch, then if it can't apply case-of-constructor it backtracks, which ends up having to reduce the scrutinee and branch again separately. in my case with lots of nested matches, this seemed to be taking exponential time in the number of nested matches.

amosr commented 10 months ago

ah, I think my test case was wrong (it was returning -1). hopefully fixed now.