coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Connecting strings in Coq and extraction target?

From: Ifaz Kabir <ikabir AT uwaterloo.ca>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Connecting strings in Coq and extraction target?
Date: Fri, 5 Oct 2018 16:06:08 +0000
Accept-language: en-GB, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikabir AT uwaterloo.ca; spf=Pass smtp.mailfrom=ikabir AT uwaterloo.ca; spf=None smtp.helo=postmaster AT mailchk-m04.uwaterloo.ca
Dkim-filter: OpenDKIM Filter v2.11.0 mailchk-m04.uwaterloo.ca w95G67Qx015542
Dmarc-filter: OpenDMARC Filter v1.3.2 mailchk-m04.uwaterloo.ca w95G67Qx015542
Ironport-phdr: 9a23:3iSEzRxz0/rn77nXCy+O+j09IxM/srCxBDY+r6Qd1OMSIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfVzBPDI2/YYsADfYOMulDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzI3wIgEMgPsX/Jqdv6LrwdUeGvzKLVyjjDbvBW1i3m54jJaBAsuuyMXLxqfsrN10YvDQfFjlKXqYD/IzyazP0Avm6G5ORjTeKik3Mrpx91rzS1wsohiJPFip8Lxl3H7yl13og4KNygRE51f9GpE4dcuiSfOoZ3X88vR29ltSM4x7AIpZG0Zy0Hx4glyhLCaPGKdpWH7QzgWeueJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFl8PDtnEJ1xPP6siHSeJx/kK91TuAzQzT9+9FLloolaXFMZ4hxrkwlp0JvUvfBCD6gET2jKmIeUU44uWk9vrrb7H8qpKYNYJ4kBzyProtl8ClH+g1PAkDU3Ce+eum1b3j+UP5QK9Njv0ziqTZsZPaKt4Aqa64GQ9YyZsj6hilADe6ztsYh30HLFVCeB6dk4fmIUnCIOrkAvenn1SsjDBryujaMb3mG5XBN2TMkLP8fblm8ENc0woyzdVH551OEL0BIfTzWlXwtNPCFBM5PRa0kK7bD4BW0ZpWcmaSCOfNO6TL9FSM++gHIu+WZYZTtiyreNY/4Pu7rHEwixc+dKOox9NDaXOxFPV8C1iGaGbhmNMGFiEBt1xtH6TRlFSeXGsLND6JVKUm62R+Udr+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFC60JZibUusBciaVJYlqm25dDOTze8oazRir8TTC5f9/NOONpn8Fqpv/2cJx4OqVnhhgrWUpXfTY6HmESiRPpk1NRzIy2/oh80l0y1OI0as9hqQEU8FM7u9ESAM9MtjXxr4iBg==

Hi Jason,

I can't comment on the strings part, but Menhir (an OCaml parser generator) can produce Coq parsers.

-Ifaz

From: Jason -Zhong Sheng- Hu

Sent: Friday, October 5, 9:56 AM

Subject: [Coq-Club] Connecting strings in Coq and extraction target?

To: Coq Club

Hi all,

I am wondering if there is already a good practice on turning strings in Coq into, say, strings in Haskell? The goal is to push informal part as late as possible, so I am thinking implementing the to-string functions in Coq as well. This is especially important when the objects are dependent. However, these strings need to go to console eventually, so I guess it has to become string in Haskell some point. My problem is, if this transition is not well-guarded, it sort of defeats the purpose of pushing informal parts late already. So how do people normally do this?

Secondly, is there any framework that can turn a context free grammar into a certified parser in Coq?

Thanks,

Jason

[Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Ifaz Kabir, 10/05/2018
  - Re: [Coq-Club] Connecting strings in Coq and extraction target?, Xuanrui Qi, 10/05/2018
    - Re: [Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, sunil, 10/05/2018