Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)

 Avoid Anomaly (or Assert False) when a module signature contains
 an applied functor followed by a "with Definition" or "with Module"

 Also fix the dependency computation in presence of a "with Definition"

 Concerning 4720, the code extracted out of this bug report was suboptimal
 in Coq 8.4 (it was compilable, but could have probably been tweaked into a
 real issue producing faulty code).
 But the example of 4720 (and some variants of it) was broken since 8.5,
 for the same reasons as 5177 and 5240. And the good news is that after
 these repairs, the example of bug 4720 is now extracted to correct code
 (the "with" is preserved).

7 files changed, 117 insertions, 22 deletions

diff --git a/API/API.ml b/API/API.ml
index 32c664d7b1..08efdfa871 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -201,4 +201,9 @@ module Entries =
                            | DefinitionEntry of 'a definition_entry
                            | ParameterEntry of parameter_entry
                            | ProjectionEntry of projection_entry
+    type module_struct_entry = Declarations.module_alg_expr
+    type module_params_entry =
+      (Names.MBId.t * module_struct_entry) list
+    type module_type_entry = module_params_entry * module_struct_entry
+
   end
diff --git a/API/API.mli b/API/API.mli
index b1a746e028..c52c305853 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1299,12 +1299,19 @@ sig
                          | DefinitionEntry of 'a definition_entry
                          | ParameterEntry of parameter_entry
                          | ProjectionEntry of projection_entry
+  type module_struct_entry = Declarations.module_alg_expr
+  type module_params_entry =
+    (Names.MBId.t * module_struct_entry) list
+  type module_type_entry = module_params_entry * module_struct_entry
 end
 
 module Mod_typing :
 sig
   type 'alg translation =
     Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.ContextSet.t
+  val translate_modtype :
+    Environ.env -> Names.ModPath.t -> Entries.inline ->
+     Entries.module_type_entry -> Declarations.module_type_body
   val translate_mse :
     Environ.env -> Names.ModPath.t option -> Entries.inline -> Declarations.module_alg_expr ->
     Declarations.module_alg_expr translation
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7d69cbff1f..bc70f768b1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -175,26 +175,32 @@ let factor_fix env l cb msb =
     (hack proposed by Elie)
 *)
 
-let expand_mexpr env mp me =
+let expand_mexpr env mpo me =
   let inl = Some (Flags.get_inline_level()) in
-  Mod_typing.translate_mse env (Some mp) inl me
+  Mod_typing.translate_mse env mpo inl me
 
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
-    To check with Elie. *)
-
-let rec mp_of_mexpr = function
-  | MEident mp -> mp
-  | MEwith (seb,_) -> mp_of_mexpr seb
-  | _ -> assert false
+let expand_modtype env mp me =
+  let inl = Some (Flags.get_inline_level()) in
+  Mod_typing.translate_modtype env mp inl ([],me)
 
 let no_delta = Mod_subst.empty_delta_resolver
 
-let env_for_mtb_with_def env mp me idl =
+let flatten_modtype env mp me_alg struc_opt =
+  match struc_opt with
+  | Some me -> me, no_delta
+  | None ->
+     let mtb = expand_modtype env mp me_alg in
+     mtb.mod_type, mtb.mod_delta
+
+(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def].
+*)
+
+let env_for_mtb_with_def env mp me reso idl =
   let struc = Modops.destr_nofunctor me in
   let l = Label.of_id (List.hd idl) in
   let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
   let before = fst (List.split_when spot struc) in
-  Modops.add_structure mp before no_delta env
+  Modops.add_structure mp before reso env
 
 let make_cst resolver mp l =
   Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
@@ -234,20 +240,24 @@ let rec extract_structure_spec env mp reso = function
    [extract_mexpression_spec] should come from a [mod_type_alg] field.
    This way, any encountered [MEident] should be a true module type. *)
 
-and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
   | MEwith(me',WithDef(idl,(c,ctx)))->
-      let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
-      let mt = extract_mexpr_spec env mp1 (me_struct,me') in
+      let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in
+      let env' = env_for_mtb_with_def env mp1 me_struct delta idl in
+      let mt = extract_mexpr_spec env mp1 (None,me') in
       (match extract_with_type env' c with (* cb may contain some kn *)
 	 | None -> mt
-	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+	 | Some (vl,typ) ->
+            type_iter_references Visit.add_ref typ;
+            MTwith(mt,ML_With_type(idl,vl,typ)))
   | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
-      MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+      MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp))
   | MEapply _ ->
      (* No higher-order module type in OCaml : we use the expanded version *)
-     extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+     let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in
+     extract_msignature_spec env mp1 delta me_struct
 
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
@@ -258,8 +268,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
       let mp = MPbound mbid in
       let env' = Modops.add_module_type mp mtb env in
       MTfunsig (mbid, extract_mbody_spec env mp mtb,
-		extract_mexpression_spec env' mp1 (me_struct',me_alg'))
-  | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
+                extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+  | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m)
 
 and extract_msignature_spec env mp1 reso = function
   | NoFunctor struc ->
@@ -335,7 +345,7 @@ and extract_mexpr env mp = function
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
-      let sign,_,delta,_ = expand_mexpr env mp me in
+      let sign,_,delta,_ = expand_mexpr env (Some mp) me in
       extract_msignature env mp delta ~all:true sign
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index a896a8d037..1e0c331901 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -17,10 +17,15 @@ open Mlutil
 
 (*S Functions upon ML modules. *)
 
+(** Note: a syntax like [(F M) with ...] is actually legal, see for instance
+    bug #4720. Hence the code below tries to handle [MTsig], maybe not in
+    a perfect way, but that should be enough for the use of [se_iter] below. *)
+
 let rec msid_of_mt = function
   | MTident mp -> mp
+  | MTsig(mp,_) -> mp
   | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.")
+  | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *)
 
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
@@ -36,7 +41,7 @@ let se_iter do_decl do_spec do_mp =
 	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
 	let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
-	mt_iter mt; do_decl (Dtype(r,l,t))
+        mt_iter mt; do_spec (Stype(r,l,Some t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
         let mp_w =
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index ad60b58d5d..17a6e8db6f 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -17,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
 type do_ref = global_reference -> unit
 
+val type_iter_references : do_ref -> ml_type -> unit
 val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
 val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
 val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v
new file mode 100644
index 0000000000..9265b60c17
--- /dev/null
+++ b/test-suite/bugs/closed/4720.v
@@ -0,0 +1,46 @@
+(** Bug 4720 : extraction and "with" in module type *)
+
+Module Type A.
+ Parameter t : Set.
+End A.
+
+Module A_instance <: A.
+ Definition t := nat.
+End A_instance.
+
+Module A_private : A.
+ Definition t := nat.
+End A_private.
+
+Module Type B.
+End B.
+
+Module Type C (b : B).
+ Declare Module a : A.
+End C.
+
+Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance).
+End WithMod.
+
+Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat).
+End WithDef.
+
+Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private).
+End WithModPriv.
+
+(* The initial bug report was concerning the extraction of WithModPriv
+   in Coq 8.4, which was suboptimal: it was compiling, but could have been
+   turned into some faulty code since A_private and c'.a were not seen as
+   identical by the extraction.
+
+   In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv
+   were all causing Anomaly or Assert Failure. This shoud be fixed now.
+*)
+
+Require Extraction.
+
+Recursive Extraction WithMod.
+
+Recursive Extraction WithDef.
+
+Recursive Extraction WithModPriv.
diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v
new file mode 100644
index 0000000000..231d103a59
--- /dev/null
+++ b/test-suite/bugs/closed/5177.v
@@ -0,0 +1,21 @@
+(* Bug 5177 https://coq.inria.fr/bug/5177 :
+   Extraction and module type containing application and "with" *)
+
+Module Type T.
+  Parameter t: Type.
+End T.
+
+Module Type A (MT: T).
+  Parameter t1: Type.
+  Parameter t2: Type.
+  Parameter bar: MT.t -> t1 -> t2.
+End A.
+
+Module MakeA(MT: T): A MT with Definition t1 := nat.
+  Definition t1 := nat.
+  Definition t2 := nat.
+  Definition bar (m: MT.t) (x:t1) := x.
+End MakeA.
+
+Require Extraction.
+Recursive Extraction MakeA.