FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Resugaring/printing called during normal checking #3315

Open mtzguido opened 3 weeks ago

mtzguido commented 3 weeks ago

This is not really observable (unless the printing raises an exception) but the typechecker will routinely render terms to put into error message guards, which is probably very wasteful. Giving that resugaring/printing should be pure, we could thunk these computations and be more efficient in the vast majority of cases that do not raise an error.