Switch from ansi-wl-pprint to the prettyprinter package.

[brianhuffman]

Note: This PR builds on GaloisInc/what4#77, GaloisInc/saw-core#106, #584, and #585; it will stay in draft status until those PRs are accepted and merged.

EDIT: GaloisInc/saw-core#106, #584, and #585 have all been merged, so we're just waiting on GaloisInc/what4#77.

[kquick]

In about a half-dozen places you fixed the annotation to (); with the parameterized ann the rest of the time that seems like a shortest-path conversion but doesn't enhance the context for later handling like colorization. If the "shortest-path" assumption is correct, it might be nice to note that in the description of the PR for future reference (as opposed to having a reason for it explicitly being ()).

There were lots of locations that were effectively pretty . show, and you marked a couple but not many of those. It would be great to shorten those to pretty where possible and mark them where not possible with some kind of consistent comment mark for future updating.

Also not a lot of consistency between leveraging IsString and using pretty; if this was mostly a mechanical sed-style change, it might be worth going through and standardizing on the former where possible.

Mostly an eyeball-glazing mechanical set of changes, thanks for doing all of this! I had a few comments above and throughout but nothing significant enough to prevent merging, so feel free to ignore or change as you'd prefer but I think this is a good step forward to get merged.

[brianhuffman]

About using () as an annotation in some places: I had some doubts about that. None of the code anywhere used any color, ANSI features or other annotations. So I thought the best choice was to make all the pretty printing code polymorphic in the annotation type as much as possible, to make it easy to combine those pretty printers with ones from other packages.

One stumbling block was that there are a few datatypes that stored Doc values inside. What annotation type should I use for that? One possibility is to add an ann parameter to the datatype, which I did in one or two places in GaloisInc/what4#77 (mostly this was for pretty-printing-related datatypes, where it seemed to make sense). Another possibility would be to use rank-2 polymorphism, with a constructor field of type forall ann. Doc ann, but this seemed like overkill. The last possibility is to use a dummy type that basically signals that you're not using any annotations; I considered both () and Void. Actually Doc Void is probably the right choice semantically, as it basically doesn't allow you to use any annotations, but Doc () seemed to convey the intention better. Other places that use Doc () are mostly just the minimum necessary to get things to typecheck. I may have used Doc () in a couple of other places that use Doc only on input parameters, just to avoid ambiguous types (although, now that I think about it, I don't think GHC even has a problem with this kind of ambiguity if there's no class constraint on the variable, so maybe I can get rid of a few of these).

I'm not sure what we should consider the best practice for handling the Doc-inside-a-datatype thing; I couldn't find any relevant advice in the package documentation.

[brianhuffman]

My latest thinking is that we should try to completely avoid pretty (show x), other than to define Pretty instances or custom type-specific pretty printing functions. Every occurrence of pretty (show x) is technical debt, in that we would prefer to get rid of it as soon as possible once other libraries get the required pretty printing support. So we should try to factor out all such occurrences into a small set of top-level functions, to make that later process easier.

[kquick]

I agree that it's unwanted tech-debt, but it's going to be hard to completely eliminate these due to using external libraries (even our own) that don't have prettyprinter Doc formatting.

One suggestion is to use the prettyprinter viaShow function when we can't eliminate this tech-debt: this function makes it clear that the pretty-printing was generated from a Show instance and is a nice footprint for future search/replace tech-debt reduction.

[brianhuffman]

I just came across viaShow and I agree that it would be a good solution to make it easier to find places to fix later. So I think there's really no excuse for using pretty . show at all.

[robdockins]

About using () as an annotation in some places: I had some doubts about that. None of the code anywhere used any color, ANSI features or other annotations. So I thought the best choice was to make all the pretty printing code polymorphic in the annotation type as much as possible, to make it easy to combine those pretty printers with ones from other packages.

One stumbling block was that there are a few datatypes that stored Doc values inside. What annotation type should I use for that? One possibility is to add an ann parameter to the datatype, which I did in one or two places in GaloisInc/what4#77 (mostly this was for pretty-printing-related datatypes, where it seemed to make sense). Another possibility would be to use rank-2 polymorphism, with a constructor field of type forall ann. Doc ann, but this seemed like overkill. The last possibility is to use a dummy type that basically signals that you're not using any annotations; I considered both () and Void. Actually Doc Void is probably the right choice semantically, as it basically doesn't allow you to use any annotations, but Doc () seemed to convey the intention better. Other places that use Doc () are mostly just the minimum necessary to get things to typecheck. I may have used Doc () in a couple of other places that use Doc only on input parameters, just to avoid ambiguous types (although, now that I think about it, I don't think GHC even has a problem with this kind of ambiguity if there's no class constraint on the variable, so maybe I can get rid of a few of these).

I'm not sure what we should consider the best practice for handling the Doc-inside-a-datatype thing; I couldn't find any relevant advice in the package documentation.

I think we should use Void as the annotation type anyplace where we are currently not using annotations. It accurately reflects the intention not to use them, and Void is easily remapped into whatever annotation you like in the places where that becomes necessary.

[kquick]

Re-reviewed with all the updated changes: this looks good to me!