The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

As I understand it (and someone please correct me if I'm wrong), this kind of information is not stored in the ast.  There is literally no difference between records and records that are typeclasses (and typeclasses can also be definitions, axioms, etc).  My current understanding (which may again be wrong) is that there is a separate table somewhere which stores a list of which identifiers are classes.

On Mon, Jan 1, 2018, 3:57 PM John Wiegley <johnw AT newartisans.com> wrote:

Hello,

I'm trying to extend MiniML to remember details about type classes, such as
which arguments used in a call are intended to be type class dictionaries.

Although I realize that Coq and Haskell type classes can yield different
results, this is for a situation where we convert from Haskell to Coq, prove
things about the resulting Coq code, and then extract back to Haskell. So, in
a sense I "know" correct behavior will result from replicating the Haskell
style in the extracted code.

To do this I need to distinguish type classes from records, type class
instances from record values, and type class arguments from plain arguments
(so that they can be elided).

Are there any examples to look at for determining this sort of information
from the Coq AST in OCaml?

Thanks,
--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2