coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extracting partial implementations

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Extracting partial implementations
Date: Wed, 31 May 2017 12:21:11 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f48.google.com
Ironport-phdr: 9a23:sai5ABFovopg76zkoXWcXp1GYnF86YWxBRYc798ds5kLTJ78r8WwAkXT6L1XgUPTWs2DsrQf2rSQ7v+oGTRZp83Q7zZaKN0EfiRGoPtVtjRjOvLNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMj4ZvLqc8xgHJr3ZKZu9awX9kKU+Jkxvy4sq9/oRv/zhMt/4k6sVNTbj0c6MkQLNXCzgrL3o76Mr3uxfdUACB/GEcUmIYkhpJBwjK8hT3VYrvvyX5q+RwxjCUMdX5Qr4oVzui6bxrSALzhyccKzE56mDXhddug69dvRmsugZww4/QYIGSKfp+YqbQds4USGZdQspcUTFKD4WhZIUNEuUBJ/5VoIbzp1QMrRWwCwqiCv7xxDBUnXL5x7E23v47HA3awAAtHdQDu2nUotXvM6cSVPi4wq7SwjXfc/NW2Tb955bVchs8vP+MWrNxftTLxkkyCgjIiVCQppb5PzOJzOsNtnOW7+96WuKzl24osQRxriKoxsc2hYnEn4QYwU3K+yV+xYY6P9y4SEhjbN64DpRQsjmaO5FzQsMmRWxjpSU0yqUetJKlYCQHzI4ryh3fZvCdbYSE/xzuWPyeLDp7gn9uZaixiAyo8Ue6z+3xTsm030hOripCitTMs2oC1x3X6sSeVPt9/Vut1S+B1w3c6exIO080la3cK54uxr4/iIAfvljEHi/zgEn2jamWeVs4+uWw9ejrfrHrqoWfOoJ0kA3yLLkil8KlDek3MQUCR22b9v691L3n8035WrJKjvgun6ncqp/aOdgbpq64AwBLz4Yv8Q2/DzCn0dsGh3YHMUlIeB2Cj4fzOlHOJOr0Auu4g1SpiDtr3ezJPqX9ApXRKXjOiKvufbFk60JF1AUzyc1f6IlPB7EaIPPzX1fxu8bCAh84NQy02efnB89n2oMQQ2LcSpOeZajVqBqD4v8lC+iKfo4c/jjneNY/4Pu7qHYlhV8ccLTh5pwFZXmlVqBjKlmFaH/Eh94dDW4P+A0kQ7q52xW5TTdPaiPqDOoH7TYhBdf+AA==

I guess you could use an extraction directive to extract foo to [Obj.magic ()] to avoid this.

On Mon, May 29, 2017 at 4:21 PM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

I’d like to be able to extract an ML program from a Coq file that is missing some definitions. For example, suppose I have a file temp.v containing

Definition foo (x:nat) : bool. Admitted.
Definition bar (x:nat) : bool := true.

and I want to play with bar before finishing foo. If I do

Require Import temp.
Extraction Library temp.

what I get in temp.ml is

open Datatypes

(** val foo : nat -> bool **)

let foo =
failwith "AXIOM TO BE REALIZED"

(** val bar : nat -> bool **)

let bar _ =
Coq_true

which is not helpful (executing this code simply raises an error, whether or not foo is called).

Is there a better way?

Thanks!

- Benjamin

[Coq-Club] Extracting partial implementations, Benjamin C. Pierce, 05/29/2017
- Re: [Coq-Club] Extracting partial implementations, Fabian Kunze, 05/29/2017
- Re: [Coq-Club] Extracting partial implementations, Matthieu Sozeau, 05/31/2017
  - Re: [Coq-Club] Extracting partial implementations, Benjamin C. Pierce, 05/31/2017