From 1e7d564377cc16a4a8e68e06723b9fa3095849b1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 5 Mar 2023 01:01:56 +0100
Subject: [PATCH] Fixes #10739: anomaly with Extraction within a module.

---
 kernel/safe_typing.ml             | 10 ++++++++++
 kernel/safe_typing.mli            |  2 ++
 plugins/extraction/extract_env.ml |  7 ++++---
 plugins/extraction/table.ml       | 21 +++------------------
 plugins/extraction/table.mli      |  1 -
 test-suite/bugs/bug_10739.v       | 21 +++++++++++++++++++++
 6 files changed, 40 insertions(+), 22 deletions(-)
 create mode 100644 test-suite/bugs/bug_10739.v

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2a0e5600c3048..ee8aca3246bf1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1399,6 +1399,16 @@ let close_section senv =
   in
   List.fold_right fold entries senv
 
+let flatten_env senv =
+  let label = function MPdot (_,l) -> l | _ -> assert false in
+  let rec close senv =
+    match senv.modvariant with
+    | STRUCT _ -> close (snd (end_module (label senv.modpath) None senv))
+    | SIG _ -> close (snd (end_modtype (label senv.modpath) senv))
+    | LIBRARY | NONE -> senv in
+  let senv = close senv in
+  (senv.modpath, senv.revstruct)
+
 (** {6 Safe typing } *)
 
 type judgment = {
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b0cdc90f58e9a..dddd72c364ba7 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val sections_of_safe_env : safe_environment -> section_data Section.t option
 
 val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
 
+val flatten_env : safe_environment -> ModPath.t * Declarations.structure_body
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 34f3a892afafd..7e0d9906a8e61 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -27,11 +27,12 @@ open Common
 (***************************************)
 
 let toplevel_env () =
-  List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ()))
+  let mp, struc = Safe_typing.flatten_env (Global.safe_env ()) in
+  mp, List.rev struc
 
 let environment_until dir_opt =
   let rec parse = function
-    | [] when Option.is_empty dir_opt -> [Lib.current_mp (), toplevel_env ()]
+    | [] when Option.is_empty dir_opt -> [toplevel_env ()]
     | [] -> []
     | d :: l ->
       let meb =
@@ -565,7 +566,7 @@ let reset () =
   Visit.reset (); reset_tables (); reset_renaming_tables Everything
 
 let init ?(compute=false) ?(inner=false) modular library =
-  if not inner then (check_inside_section (); check_inside_module ());
+  if not inner then check_inside_section ();
   set_keywords (descr ()).keywords;
   set_modular modular;
   set_library library;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c0639a264ccc6..b1311e9125ad2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -87,15 +87,13 @@ let common_prefix_from_list mp0 mpl =
     | mp :: l -> if MPset.mem mp prefixes then Some mp else f l
   in f mpl
 
-let rec parse_labels2 ll mp1 = function
-  | mp when ModPath.equal mp1 mp -> mp,ll
-  | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
+let rec parse_labels2 ll = function
+  | MPdot (mp,l) -> parse_labels2 (l::ll) mp
   | mp -> mp,ll
 
 let labels_of_ref r =
-  let mp_top = Lib.current_mp () in
   let mp,l = repr_of_r r in
-  parse_labels2 [l] mp_top mp
+  parse_labels2 [l] mp
 
 
 (*S The main tables: constants, inductives, records, ... *)
@@ -365,19 +363,6 @@ let error_axiom_scheme ?loc r i =
        safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
-let warn_extraction_inside_module =
-  CWarnings.create ~name:"extraction-inside-module" ~category:"extraction"
-      (fun () -> strbrk "Extraction inside an opened module is experimental." ++ spc () ++
-       strbrk "In case of problem, close it first.")
-
-
-let check_inside_module () =
-  if Lib.is_modtype () then
-    err (str "You can't do that within a Module Type." ++ fnl () ++
-         str "Close it and try again.")
-  else if Lib.is_module () then
-    warn_extraction_inside_module ()
-
 let check_inside_section () =
   if Global.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index d95a19cfdef43..30063dbb62938 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -35,7 +35,6 @@ val error_unknown_module : ?loc:Loc.t -> qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : GlobRef.t -> 'a
 val error_MPfile_as_mod : ModPath.t -> bool -> 'a
-val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : ModPath.t -> unit
 val msg_of_implicit : kill_reason -> string
diff --git a/test-suite/bugs/bug_10739.v b/test-suite/bugs/bug_10739.v
new file mode 100644
index 0000000000000..f56988e030c9a
--- /dev/null
+++ b/test-suite/bugs/bug_10739.v
@@ -0,0 +1,21 @@
+Require Extraction.
+
+Definition f := 0.
+Module M.
+  Recursive Extraction f.
+  Extraction f.
+
+  Definition g := f.
+  Recursive Extraction g.
+  Extraction g.
+
+  Module Type S. End S.
+  Module N : S.
+    Definition h := g.
+    Recursive Extraction h.
+    Extraction h.
+  End N.
+
+  Recursive Extraction nat.
+  Extraction nat.
+End M.