Stream: Coq users

Topic: Extraction to mixed haskell/ocaml

spaceloop (Feb 27 2023 at 09:18):

The following example extracts sensible code for ascii_of_nat:

From Coq Require Import Strings.Ascii Extraction.
Extraction Language Haskell.
Recursive Extraction ascii_of_nat.

However, If I add a Require to my local development like so:

From MyProject Require MyModule.
From Coq Require Import Strings.Ascii Extraction.
Extraction Language Haskell.
Recursive Extraction ascii_of_nat.

It starts extracting incorrect code instead, which looks like a Haskell/OCaml mix. For example

of_succ_nat :: int -> int
of_succ_nat n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (\_ -> 1)
    (\x -> succ (of_succ_nat x))
    n

I have no clue where to start debugging this, as it also doesn't seem to matter which module I require from my project. Any suggestions?

Julin S (Feb 27 2023 at 09:36):

Just a thought, but showing the content of MyModule might help people here to identify the problem.

spaceloop (Feb 27 2023 at 11:05):

Okay, I have narrowed it down to some transitive import in another project I'm using:

Require Import ExtrOcamlZInt.

This is a Coq library, but I haven't investigated further.

So the minimal example is now:

Require Import ExtrOcamlZInt.
From Coq Require Import Strings.Ascii Extraction.
Extraction Language Haskell.
Recursive Extraction ascii_of_nat.

Gaëtan Gilbert (Feb 27 2023 at 11:05):

probably because it does

Extract Inductive N => int [ "0" "" ]
"(fun f0 fp n -> if n=0 then f0 () else fp n)".

spaceloop (Feb 27 2023 at 11:50):

Is there a way to prevent such a transitive module dependency to interfere with my extraction settings?

Paolo Giarrusso (Feb 27 2023 at 13:54):

naive question: could such extraction commands be _extended_ to accept a language when debugging? #[for(OCaml)] Extract Inductive ... wouldn't suffer this problem?

No idea if there's a simpler way today

Gaëtan Gilbert (Feb 27 2023 at 14:07):

I agree they should probably be associated with a language instead of being for all languages
it can be an attribute or they could just pick up the language set when they're declared

Gaëtan Gilbert (Feb 27 2023 at 14:07):

currently there's no way to make that happen though AFAIK

spaceloop (Feb 27 2023 at 14:54):

Thanks, is there a way to reset those Extract Inductives in my environment? I did find Reset Extraction Inline, but nothing about these.

Last updated: Oct 04 2023 at 20:01 UTC