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?
Just a thought, but showing the content of MyModule might help people here to identify the problem.
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.
probably because it does
Extract Inductive N => int [ "0" "" ] "(fun f0 fp n -> if n=0 then f0 () else fp n)".
Is there a way to prevent such a transitive module dependency to interfere with my extraction settings?
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
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
currently there's no way to make that happen though AFAIK
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