FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Normalize residual comps

Open mtzguido opened this issue 2 years ago • 0 comments

The normalizer is not currently reducing lambdas in the types of residual comps in Tm_abs and Tm_match nodes. This simple patch makes it so, opening the PR just to:

  • Make sure this is in fact desirable?
  • Confirm that performance is acceptable. I ran the diff script and got the images below, with mixed results. I understand the <1 slope means that things are in average slightly better?
  • Point to the last patch, which works around another gensym-related Heisenbug! I don't plan to get that commit to master, just adding it here to get a green. It will hopefully go away once other patches land.

I ran into this while trying to removing Tm_names from checked files, and some remained in unreduced residual comps. They should not be there anyway.. as it's supposed to be closed, but still tracking that down.

Figure_1 Figure_2

mtzguido avatar Mar 07 '23 15:03 mtzguido