Is there a way to tell Coq to only extract a subset of the definitions in a module? Here’s a minimal example:
Require Coq.extraction.Extraction. Module Type AType. Parameter a : nat. End AType. Module BMod (A : AType). Definition foo : nat := 4 + A.a. Definition bar : bool := false. End BMod. Module AMod <: AType. Definition a := 3. End AMod. Module B := BMod AMod. Recursive Extraction B.bar.
The “Recursive Extraction” here will generate OCaml code that contains B.foo and B.bar, even though I only wanted B.bar. This could be a problem when B.foo is some complicated function that is only used for proof, and never intended to be executed.
In case that’s too abstract, here’s my exact use case: I have a module containing functions for manipulating quantum programs, expressed as a list of gates (SQIR/UnitaryListRepresentation.v at main · inQWIRE/SQIR · GitHub). Within this module, I have a function that computes the semantics of a quantum program. This denotation function is only used for proofs (and has a lot of machinery behind it) so I really don’t want to extract it to OCaml. One possible solution is to manually extract this denotation function to some dummy value (with “Extract Constant”), but that seems hacky. Do I need to move the denotation function & anything that uses it to a different module?