search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
367 stars 79 forks source link

Implement a general Show typeclass in MetaCoq.Utils #1063

Closed mattam82 closed 5 months ago

mattam82 commented 5 months ago

This allows to conveniently print anything for debugging purposes, or using the FFIs to print messages in the various extractions (the live and extracted ones, malfunction or certicoq)

JasonGross commented 5 months ago

If you want a version that does levels-based parenthesizing, Fiat Crypto has such a class: https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/Strings/Show.v

gmalecha commented 5 months ago

ExtLib has a Show class and instances as well. Is there any interest in unifying things like this? Would people depend on another opam library to get Show with a bunch of instances for standard types, e.g. bool, nat, N, etc?

JasonGross commented 5 months ago

Does ExtLib do level-based printing, so that it can parenthesize as much as needed but not more?

In any case, it seems in https://github.com/MetaCoq/metacoq/pull/952#issuecomment-1521449731 that we're receptive to depending on extlib

gmalecha commented 5 months ago

ExtLib does not do level based printing that I am aware of. The underlying setup is parameterized by a Monoid with an injection from Ascii I think. You could add a wrapper for a level though to get this extra functionality.

My main motivation is to avoid repeated work, if you benefit from this, other might as well and that would make for reducing overall maintenance.