coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Changing the way that literals are extracted

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Changing the way that literals are extracted
Date: Fri, 26 Feb 2016 17:30:54 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f176.google.com
Ironport-phdr: 9a23:MlSVWRdh15d0HiRKYKgupsgwlGMj4u6mDksu8pMizoh2WeGdxc6yYh7h7PlgxGXEQZ/co6odzbGG7Oa+BSdbsd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcOPKF4YzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1i162MYQ1kRx1BqBAjDpC77U5j1vzqw/r5/3ymcIuXwQK89Qyij9K5tU1njjyJRZBAj92SCwO53jKQTnxOsqBhy0sScNIOSNPxhVqXQYtoAWWtaV8BKESdGB9XvPMM0E+MdMLMA/MHGrFwUoE7mCA==
Organization: New Artisans LLC

I have some code that includes nat and String constants, and I'd like to
extract these into Haskell as Integer and String (Haskell) constants. For
example, I'd like have "foo" be extracted as "foo", and 1234 extracted as
1234, rather than as calls to an introduction function.

In my particular case, an 864-line Gallina term, which does heavy String
manipulation, is extracting to a 23k-line Haskell term, where 90% of the code
appears to be doing elimination on the 8-fields of Ascii (in order to match
against constant strings). I'd like to eliminate Ascii from the extraction
entirely, but this still doesn't stop elimination by way of the extracted
recursor, due to the constants.

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

[Coq-Club] Changing the way that literals are extracted, John Wiegley, 02/27/2016