The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

You may want to take a look at the directory

  plugins/extraction

in the Coq source tree. There are a lot of directives for such mappings 
for extraction to OCaml there.

On 03/06/2014 01:14 PM, Kevin Sullivan wrote:
> Thanks Greg and Cedric,
>
> I'm not necessarily committed to Haskell. What hooks did you, Greg, have
> in mind for doing such mappings/replacements when extracting to OCaml?
>
> Kevin
>
>
> On Wed, Mar 5, 2014 at 11:05 PM, Greg Morrisett 
> <greg AT eecs.harvard.edu
> <mailto:greg AT eecs.harvard.edu>>
>  wrote:
>
>     I don't have experience extracting Haskell, but when I do OCaml,
>     I tend to map certain things (ascii, nat) to native OCaml
>     types (e.g., char, bignum).  I agree it's less than optimal, but
>     that's the price of interoperability with legacy code...
>
>     Anyway, there are good hooks for doing this kind of replacement.
>
>     -Greg
>
>
>     On 3/5/2014 7:49 PM, Kevin Sullivan wrote:
>
>         Dear Colleagues:
>
>         A grad student of mine is looking at integrating Haskell code
>         extracted
>         from a Coq specification into an industrial environment. The
>         environment
>         in this case includes a standard Haskell installation, the yesod web
>         service framework, etc. The Coq spec uses types such as Coq
>         String, Coq
>         Z, etc. When we extract code, we end up with extracted versions
>         of Coq
>         string, Coq Z etc. But the frameworks expect the use of their
>         "built-in" analogs, e.g., Haskell's String type.
>
>         The question is, what's the current best practice for "bridging"
>         from
>         Coq's types to analogs provided and used natively in target
>         languages
>         and related frameworks? Or for swapping out definitions
>         extracted from
>         Coq and allowing references to be bound to the native versions?
>         Clearly
>         doing such a substitution increases the TCB, nor is it
>         necessarily safe,
>         in that the semantics might not always match exactly.
>
>         So, again, what is the best practice in this regard?
>
>         Thanks,
>         Kevin