coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to access "typeclass arguments" in an extraction plugin?

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to access "typeclass arguments" in an extraction plugin?
Date: Mon, 01 Jan 2018 12:57:21 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=johnw AT newartisans.com; spf=Pass smtp.mailfrom=johnw AT newartisans.com; spf=None smtp.helo=postmaster AT out2-smtp.messagingengine.com
Ironport-phdr: 9a23:yiDHYR/QHPdQzv9uRHKM819IXTAuvvDOBiVQ1KB42+4cTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaOTA592LZhcJ/g61Hux+huwBzzpTIbI2JLvdyYqXQds4aS2pbWcZRUjRMDo24YYsID+oBO/tToIn8p1QQohu+ARejBePhxjRVgXL236o60+QnEQDIxwEgGcwBsXrOo9XvKKcSUPu1w7POzTXYdf9ZxTD96I3Rfx0nvPqCU7Vwcc/LxkkuEQPIllOQppLrPjyPzOQNr2mb7/F6WuKpkG4rsR1+oj+qxsoql4LHhZoVx0jF+Ch42oo5OMC0RFNhbdOrCpdcqSCXO5N0T84jWW1kpig3x7IctZO6eCUG0okryhHbZvGBboOG+AjsVPyLLjd9nH9leKywhxK18UW4ze38S9W03EhToipel9nMqmgN2wbW6seZUft95V2u2TmO1wDV5eFLP0Y0laXaK54n3LE8jIYcsUPGHiPumUX2irGZdlk89+Wp6unreKjqqoKBO4NuhQzyKLoil82nDeQ9KAcOXmyb+eqm1L3k+E30WLdKjvo2kqnfvpHXPsIbqbC3AgBPyIYj9xe/Dyy839QehnkLNk5KeBWCj4TxIVHBPOj4Deujg1SriDpk2/fGPqT4DprRKnjDjazucK1m609czQoz1cpQ64hVCrEHOvLzW1X+uMbWDh8jYESIxLPsD8w43YcDU0qOBLWYOeXcqwym/OUqdqOuY48T8An8Jvch6u+kxSs7nl8bYoGv0IQecmy5Bf1gOAOSZn+60YRJKnsDogdrFL+is1aFSzMGP3s=
Organization: New Artisans LLC

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

[Coq-Club] How to access "typeclass arguments" in an extraction plugin?, John Wiegley, 01/01/2018
- Re: [Coq-Club] How to access "typeclass arguments" in an extraction plugin?, Jason Gross, 01/02/2018