Merge PR #857: Extraction: various fixes related with bug 4720

6 files changed, 112 insertions, 22 deletions

diff --git a/API/API.mli b/API/API.mli
index 309719539..5160ca3c2 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1222,6 +1222,10 @@ 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 Environ :
@@ -1380,6 +1384,9 @@ 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 f5aa5e6c3..39826d744 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 a896a8d03..1e0c33190 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 ad60b58d5..17a6e8db6 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 000000000..9265b60c1
--- /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 000000000..231d103a5
--- /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.