search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Reduce dummy ranges. #189

Closed gebner closed 2 months ago

gebner commented 2 months ago

Commit b3c446d1793463c8f2f91fba83970109347cb193 improved the ranges of the instantiate implicits error message (thank you @nikswamy) , but there are still cases where the range is the whole declaration.

It turns out that this happens because we often set the range of a term to be the dummy range, which then causes the range to be defaulted to the whole declaration. Properly setting the range of a term requires an explicit call to set_range which is easy to forget.

This PR adds sensible default ranges in the tm_pureapp etc. constructors, to ensure that we do not generate dummy ranges in the first place. Nullary constructors for fvars etc. still produce dummy ranges; we can't guess the range from the arguments there and specifying it everywhere is a lot of churn.

See testcase for an example where this PR improves an error message range.

mtzguido commented 2 months ago

Thanks Gabriel, I tried it out and it did improve an error I had. I merged master and regen'd the snapshot (hopefully correctfully).

Merging.