Extraction inside a module

[Lysxia]

Description of the problem

The following snippet, with a definition at the toplevel, then a Recursive Extraction command inside a module, extracts to literally nothing:

Require Extraction.

Definition f := 0.
Module M.
  Recursive Extraction f.
  (* No extracted output at all, not even "f" *)

  Extraction f.
  (* Error: Anomaly "reference not found in extracted structure." *)

Related to #9365 which was redirected to QuickChick, but I've minimized the example to that, which is no longer within QuickChick's jurisdiction.

Coq Version

tested on 8.9 and 8.10+alpha (Aug 18 2019)

[maximedenes]

Wow, thanks for the reduced test case! Maybe @pi8027 could be interested in this.

[pi8027]

The Extraction f command does the same thing as Recursive Extraction f, find f in the result, then print it. So the second problem would be disappeared if Recursive Extraction gets fixed.

[ppedrot]

Not that I want to play Cassandra, but asking to be able to extract definitions in the middle of a module does look like giving a stick to get beaten with...

[Lysxia]

I'm actually not asking for that feature. I think it would be okay to disallow it, and display a clear error instead of the current warning saying that extraction in a module is "experimental".

The point is to clarify what should and what shouldn't be expected to work, as here are people who are unsure about the status of things unless they take the time to dig into it.

[JasonGross]

Not that I want to play Cassandra, but asking to be able to extract definitions in the middle of a module does look like giving a stick to get beaten with...

What? Why? Extraction should absolutely work in the middle of a module (though feel free to disallow it in the middle of Module Types and inside functors, i.e., modules with non-zero numbers of parameters). Forbidding extraction inside modules will break my bug minimizer, which relies on modules to replicate the effect of file and directory structure within a single file.

[maximedenes]

Not that I want to play Cassandra, but asking to be able to extract definitions in the middle of a module does look like giving a stick to get beaten with...

In the context of QuickChick, I can imagine you sometimes want to run a test (which uses extraction) while writing a module.

TBH, I don't see why it would be difficult to support (especially if we forbid it in functors, like @JasonGross says). What risk do you have in mind?

[ppedrot]

My main concern are functors indeed, although you can still get suspicious behaviours when extracting a module that is supposed to be sealed by a signature. What is the expected semantics of this, or more generally extraction inside a module?

[JasonGross]

when extracting a module that is supposed to be sealed by a signature. What is the expected semantics of this, or more generally extraction inside a module?

The semantics are the same as if you extract something at top-level in the middle of a file (which I model as just a module). I would be fine if extraction errored inside a sealed module, though I think the better thing is to probably just ignore the sealing while inside the module.

[pi8027]

I'd like to share the results of my investigation. Monolithic extraction tries to dump all the definitions in the current toplevel here:

coq/plugins/extraction/extract_env.ml

Line 59 in 02d9b43

| [] when Option.is_empty dir_opt -> [Lib.current_mp (), toplevel_env ()]

In @Lysxia's example, toplevel_env () is the contents of Top but Lib.current_mp () is Top.M (which indeed must be Top), then extract_structure uses that incorrect module name to reconstruct fully qualified names by make_cst:

coq/plugins/extraction/extract_env.ml

Lines 305 to 318 in 02d9b43

	let rec extract_structure env mp reso ~all = function
	| [] -> []
	| (l,SFBconst cb) :: struc ->
	(try
	let sg = Evd.from_env env in
	let vl,recd,struc = factor_fix env sg l cb struc in
	let vc = Array.map (make_cst reso mp) vl in
	let ms = extract_structure env mp reso ~all struc in
	let b = Array.exists Visit.needed_cst vc in
	if all || b then
	let d = extract_fixpoint env sg vc recd in
	if (not b) && (logical_decl d) then ms
	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
	else ms

So the reconstructed name of f is Top.M.f which cannot be recognized as Top.f by Visit.needed_cst. We need to fix this line 59.

[pi8027]

This issue may have been introduced in f6d8fc1. We may need to check other uses of Lib.current_mp in extraction...

[pi8027]

Since I checked how the extraction bypasses opaqueness of modules, here, I strongly agree with @ppedrot. But leaving extraction in modules as an experimental function and trying to fix it would also be fine.

[herbelin]

Another example of the anomaly, this time with Recursive Extraction:

Require Extraction.
Definition a:=0.
Module M.
Definition b:=a.
Recursive Extraction b.

@pi8027: I worked from your line 59 above and added a kernel function that "flattens" the environment, i.e. that adds the necessary amount of End to close the current stack of open modules, module type and functors. Together with a few other tunings, this seems now to work, even in functors (see PR #17344). Thanks for the analysis of the issue.