coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extracting partial implementations

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Extracting partial implementations
Date: Mon, 29 May 2017 10:21:10 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
Ironport-phdr: 9a23:FDH6wBXF395pc52GnoqFDBK48SfV8LGtZVwlr6E/grcLSJyIuqrYbBSCt8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwewt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZIYJEuEPP/tXr5PlqlUOsRSxCgeiCv7sxDFWgXH7xrc13/gkEQzc3AwsA9ADvXLJp9v1LqcSVuW1wbHGwTjecfxW3zX955LNchAgp/GHQKx9fdDMwkc1FgPKkE+QppD7MD+by+8AtHOU4PZ4VeKulWEnsR1+rSa0y8gwi4nJnZgZyk3c9SpnxoY1I8e0R1Bmbt65CZZdsTyROYhuQs46Xm1luCU3xqcbtZO1YCQG0pYqywPFZ/CafYWE/grvWPuRLDp7nn5pZbyyiwqo/UWgxODwTNe43VJMoyFYiNfDrGoN2AbW6sWfSvty4EOh2TGX2gDT7eFEPEY0mrfBJ5463LE/jIETvV7eHi/uhkr2iqmWel869ee19uTrerTmppmCOI9okgzyL6Qjl8+lDeglPAUCQ3KX9Oah2LH54EH0TqlGguUzkqbDsZDaIcobprS+Aw9Qyoss8AqwDy+n0NsGh3kIMExKdQmbgIjoIFHCOu34De+hjFSqljdn3e7JMaD8ApnVNHjMjK/hfaph605b0Ac80ddf54tNBr4dJPLzR1T+ucfDDh45Ngy02/zoBM981oMYQ2KPA7WWPLncsV+StaoTJLyHY5ZQszLgIdAk4eTvhDk3gwwzZ66siNE9ZXa6F/FnJQ2yJzLUg9obGmpA9l40R/TrhUeJXBZYZm30Qrox4Dd9BY67W9SQDruxiaCMiX/oVqZdYXpLXwiB

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