Fixes #10739: anomaly with Extraction within a module

doc/changelog/13-misc/17344-master+fixes10739-extraction-inside-a-module.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  Anomaly when extracting within a module or module type
+  (`#17344 <https://github.com/coq/coq/pull/17344>`_,
+  fixes `#10739 <https://github.com/coq/coq/issues/10739>`_,
+  by Hugo Herbelin).

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 (params,env) -> close (snd (end_module (label senv.modpath) None {senv with modvariant = STRUCT (params,env)}))
+    | LIBRARY | NONE -> senv in
+  let senv = close senv in
+  (senv.modpath, senv.revstruct)
+
 (** {6 Safe typing } *)
 
 type judgment = {

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

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;

plugins/extraction/modutil.ml

@@ -233,9 +233,12 @@ let get_decl_in_structure r struc =
             | SEdecl d -> d
             | SEmodtype m -> assert false
             | SEmodule m ->
-                match m.ml_mod_expr with
+                let rec aux = function
                   | MEstruct (_,sel) -> go ll sel
-                  | _ -> error_not_visible r
+                  | MEfunctor (_,_,sel) -> aux sel
+                  | MEident _ | MEapply _ -> error_not_visible r
+                in aux m.ml_mod_expr
+
     in go ll sel
   with Not_found ->
     anomaly (Pp.str "reference not found in extracted structure.")

plugins/extraction/table.ml

@@ -61,13 +61,15 @@ let raw_string_of_modfile = function
   | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
-let is_toplevel mp = ModPath.equal mp (Lib.current_mp ())
+let extraction_current_mp () = fst (Safe_typing.flatten_env (Global.safe_env ()))
+
+let is_toplevel mp = ModPath.equal mp (extraction_current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let mp_length mp =
-  let mp0 = Lib.current_mp () in
+  let mp0 = extraction_current_mp () in
   let rec len = function
     | mp when ModPath.equal mp mp0 -> 1
     | MPdot (mp,_) -> 1 + len mp
@@ -89,15 +91,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 = KerName.repr (repr_of_r r) in
-  parse_labels2 [l] mp_top mp
+  parse_labels2 [l] mp
 
 
 (*S The main tables: constants, inductives, records, ... *)
@@ -367,19 +367,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:CWarnings.CoreCategories.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 Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
@@ -482,7 +469,7 @@ let warning_remaining_implicit k =
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
-        match base_mp (Lib.current_mp ()) with
+        match base_mp (extraction_current_mp ()) with
           | MPfile dp' when not (DirPath.equal dp dp') ->
             err (str "Please load library " ++ DirPath.print dp ++ str " first.")
           | _ -> ()

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

test-suite/bugs/bug_10796.v

@@ -4,6 +4,6 @@ Module Example.
 
   Definition a : nat := 0.
 
-  Fail Separate Extraction a.
+  Separate Extraction a.
 
 End Example.

test-suite/output/bug_10739.out

@@ -0,0 +1,121 @@
+
+type nat =
+| O
+| S of nat
+
+(** val f : nat **)
+
+let f =
+  O
+
+(** val f : nat **)
+
+let f =
+  O
+
+type nat =
+| O
+| S of nat
+
+(** val f : nat **)
+
+let f =
+  O
+
+module M =
+ struct
+  (** val g : nat **)
+
+  let g =
+    f
+ end
+
+(** val g : nat **)
+
+let g =
+  f
+
+type nat =
+| O
+| S of nat
+
+(** val f : nat **)
+
+let f =
+  O
+
+module M =
+ struct
+  (** val g : nat **)
+
+  let g =
+    f
+
+  module N =
+   struct
+    (** val h : nat **)
+
+    let h =
+      g
+   end
+ end
+
+(** val h : nat **)
+
+let h =
+  M.g
+
+type nat =
+| O
+| S of nat
+
+(** val add : nat -> nat -> nat **)
+
+let rec add n m =
+  match n with
+  | O -> m
+  | S p -> S (add p m)
+
+(** val f : nat **)
+
+let f =
+  O
+
+module M =
+ struct
+  (** val g : nat **)
+
+  let g =
+    f
+
+  module type S =
+   sig
+    val b : nat
+   end
+
+  module F =
+   functor (X:S) ->
+   struct
+    (** val h : nat **)
+
+    let h =
+      add g X.b
+   end
+ end
+
+(** val h : nat **)
+
+let h =
+  add M.g X.b
+
+type nat =
+| O
+| S of nat
+
+type nat =
+| O
+| S of nat
+(** val foo : nat **)
+
+let foo =
+  O

test-suite/output/bug_10739.v

@@ -0,0 +1,38 @@
+Require Extraction.
+
+Definition f := 0.
+Module M.
+  Recursive Extraction f.
+  Extraction f.
+
+  Definition g := f.
+  Recursive Extraction g.
+  Extraction g.
+
+  Module Type S. Definition b := 0. End S.
+
+  (* Test with sealed module *)
+  Module N : S.
+    Definition b := 0.
+    Definition h := g.
+    Recursive Extraction h.
+    Extraction h.
+  End N.
+
+  (* Test with a functor *)
+  Module F (X:S).
+    Definition h := g + X.b.
+    Recursive Extraction h.
+    Extraction h.
+  End F.
+
+  (* Test elsewhere *)
+  Recursive Extraction nat.
+  Extraction nat.
+
+  Module Type T.
+    Definition foo := 0.
+    Extraction foo.
+  End T.
+
+End M.