Internally, the pretty printer and ugly printer are interconnected and sometimes hard to update. Plus, the ugly printer's output is parsed by Vale, so it must adhere to a given shape which makes it hard to update, or to do other changes (e.g. see the need for this patch https://github.com/FStarLang/FStar/pull/3406/commits/be3f7092ca2678ad93cca13da6893ddcd0211b24 in #3406).
This PR separates them and moves to using typeclasses almost everywhere. Next, I will do a Vale printer so we can fully isolate the output needed by Vale. But this is a big change already and I'd like to merge it.
Please report if you find any error messages have changed for the worse.
Internally, the pretty printer and ugly printer are interconnected and sometimes hard to update. Plus, the ugly printer's output is parsed by Vale, so it must adhere to a given shape which makes it hard to update, or to do other changes (e.g. see the need for this patch https://github.com/FStarLang/FStar/pull/3406/commits/be3f7092ca2678ad93cca13da6893ddcd0211b24 in #3406).
This PR separates them and moves to using typeclasses almost everywhere. Next, I will do a Vale printer so we can fully isolate the output needed by Vale. But this is a big change already and I'd like to merge it.
Please report if you find any error messages have changed for the worse.