Variant !F M for functor application that does not honor the Inline declarations

 For F(X:T), the application !F M works as F M, except that if module type T
 contains some "Inline" annotations, they are not taken in account when substituting
 X with M in F. See forthcoming commits for examples of use for this feature.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 60 insertions, 50 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26ad7e383a..cfa256888e 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -224,12 +224,12 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and translate_module env mp me =
+and translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None ->
 	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
     | None, Some mte ->
-	let mtb = translate_module_type env mp mte in
+	let mtb = translate_module_type env mp inl mte in
 	  { mod_mp = mp;
 	    mod_expr = None;
 	    mod_type = mtb.typ_expr;
@@ -239,13 +239,13 @@ and translate_module env mp me =
 	    mod_retroknowledge = []}
    | Some mexpr, _ ->
 	let sign,alg_implem,resolver,cst1 =
-	  translate_struct_module_entry env mp mexpr in
+	  translate_struct_module_entry env mp inl mexpr in
 	let sign,alg1,resolver,cst2 =
 	  match me.mod_entry_type with
 	    | None ->
 		sign,None,resolver,Constraint.empty
 	    | Some mte ->
-		let mtb = translate_module_type env mp mte in
+		let mtb = translate_module_type env mp inl mte in
                 let cst = check_subtypes env
 		  {typ_mp = mp;
 		   typ_expr = sign;
@@ -269,21 +269,23 @@ and translate_module env mp me =
 	       fix the bug.*)
 
 
-and translate_struct_module_entry env mp mse  = match mse with
+and translate_struct_module_entry env mp inl mse  = match mse with
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in 
       let mb' = strengthen_and_subst_mb mb mp env false in
 	mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) arg_e in
+      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) 
 	env in
-      let sign,alg,resolver,cst = translate_struct_module_entry env' 
-	mp body_expr in
-	SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
+      let sign,alg,resolver,cst =
+	translate_struct_module_entry env' mp inl body_expr in
+      SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
       Univ.Constraint.union cst mtb.typ_constraints
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolver,cst1 = translate_struct_module_entry env mp fexpr in
+      let sign,alg,resolver,cst1 =
+	translate_struct_module_entry env mp inl fexpr
+      in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -294,32 +296,35 @@ and translate_struct_module_entry env mp mse  = match mse with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
-      let mp_delta =  discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1 
-	farg_id farg_b mp_delta in
+      let mp_delta = discr_resolver env mtb in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
       (subst_codom_delta_resolver subst resolver),
       Univ.Constraint.union cst1 cst
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp mte in
+      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
       let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
 	sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
 	  
-and translate_struct_type_entry env mse  = match mse with
+and translate_struct_type_entry env inl mse = match mse with
   | MSEident mp1 ->
       let mtb = lookup_modtype mp1 env in 
 	mtb.typ_expr,
       Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) arg_e in
+      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env  in
-      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env' 
-	 body_expr in
+      let sign,alg,resolve,mp_from,cst =
+	translate_struct_type_entry env' inl body_expr in
 	SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
       Univ.Constraint.union cst mtb.typ_constraints
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolve,mp_from,cst1 = translate_struct_type_entry env fexpr in
+      let sign,alg,resolve,mp_from,cst1 =
+	translate_struct_type_entry env inl fexpr
+      in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -331,19 +336,20 @@ and translate_struct_type_entry env mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst2 = check_subtypes env mtb farg_b in
       let mp_delta = discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1
-	farg_id farg_b mp_delta in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),None,
       (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in
+      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
       let sign,alg,resolve,cst1 = 
 	check_with env sign with_decl alg mp_from resolve in
 	sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1    
 
-and translate_module_type env mp mte =
-	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in
+and translate_module_type env mp inl mte =
+	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
 	 subst_modtype_and_resolver 
 	   {typ_mp = mp_from;
 	    typ_expr = sign;
@@ -351,14 +357,14 @@ and translate_module_type env mp mte =
 	    typ_constraints = cst;
 	    typ_delta = resolve} mp env
 	   
-let rec translate_struct_include_module_entry env mp mse  = match mse with
+let rec translate_struct_include_module_entry env mp inl mse  = match mse with
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in 
       let mb' = strengthen_and_subst_mb mb mp env true in
 	mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty
   | MSEapply (fexpr,mexpr) ->
       let sign,resolver,cst1 =
-	translate_struct_include_module_entry env mp fexpr in
+	translate_struct_include_module_entry env mp inl fexpr in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -370,8 +376,9 @@ let rec translate_struct_include_module_entry env mp mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
       let mp_delta =  discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1 
-	farg_id farg_b mp_delta in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),
       (subst_codom_delta_resolver subst resolver),
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 746a80e151..63f7696c48 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -17,20 +17,20 @@ open Names
 (*i*)
 
 
-val translate_module : env -> module_path -> module_entry 
+val translate_module : env -> module_path -> bool -> module_entry
   -> module_body
 
-val translate_module_type : env -> module_path -> module_struct_entry -> 
+val translate_module_type : env -> module_path -> bool -> module_struct_entry ->
   module_type_body
 
-val translate_struct_module_entry : env -> module_path -> module_struct_entry -> 
+val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry ->
   struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
 
-val translate_struct_type_entry : env  -> module_struct_entry -> 
+val translate_struct_type_entry : env -> bool -> module_struct_entry ->
   struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints
 
 val translate_struct_include_module_entry : env -> module_path 
-  -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+  -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
 
 val add_modtype_constraints : env -> module_type_body -> env
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ef2ea800cf..e4c6ec35e1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,10 +262,10 @@ let add_mind dir l mie senv =
 
 (* Insertion of module types *)
 
-let add_modtype l mte senv =
+let add_modtype l mte inl senv =
   check_label l senv.labset;
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let mtb = translate_module_type senv.env mp mte  in
+  let mtb = translate_module_type senv.env mp inl mte  in
   let senv' = add_constraints mtb.typ_constraints senv in
    let env'' = Environ.add_modtype mp mtb senv'.env in
     mp, { old = senv'.old;
@@ -288,10 +288,10 @@ let full_add_module mb senv =
 
 (* Insertion of modules *)
 
-let add_module l me senv =
+let add_module l me inl senv =
   check_label l senv.labset;
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let mb = translate_module senv.env mp me in
+  let mb = translate_module senv.env mp inl me in
   let senv' = full_add_module mb senv  in
   let modinfo = match mb.mod_type with
       SEBstruct _ -> 
@@ -339,7 +339,9 @@ let end_module l restype senv =
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
   let mp = senv.modinfo.modpath in
-  let restype = Option.map (translate_module_type senv.env mp) restype in
+  let restype =
+    Option.map
+      (fun (res,inl) -> translate_module_type senv.env mp inl res) restype in
   let params,is_functor =
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -420,17 +422,17 @@ let end_module l restype senv =
 
 
 (* Include for module and module type*)
- let add_include me is_module senv =
+ let add_include me is_module inl senv =
    let sign,cst,resolver =
      if is_module then
        let sign,resolver,cst =  
 	 translate_struct_include_module_entry senv.env 
-	   senv.modinfo.modpath me in
+	   senv.modinfo.modpath inl me in
 	 sign,cst,resolver
      else
        let mtb = 
 	 translate_module_type senv.env 
-	   senv.modinfo.modpath me in
+	   senv.modinfo.modpath inl me in
        mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
    let senv = add_constraints cst senv in
@@ -441,8 +443,9 @@ let end_module l restype senv =
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
 	 let senv = add_constraints cst_sub senv in
-	 let mpsup_delta = complete_inline_delta_resolver senv.env mp_sup 
-	   mbid mtb mb.typ_delta in
+	 let mpsup_delta = if not inl then mb.typ_delta else
+	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta
+	 in
 	   (compute_sign 
 	     (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv)
      | str -> str,senv
@@ -534,10 +537,10 @@ let end_module l restype senv =
 
 (* Adding parameters to modules or module types *)
 
-let add_module_parameter mbid mte senv =
+let add_module_parameter mbid mte inl senv =
   if  senv.revstruct <> [] or senv.loads <> [] then
     anomaly "Cannot add a module parameter to a non empty module";
-  let mtb = translate_module_type senv.env (MPbound mbid) mte in
+  let mtb = translate_module_type senv.env (MPbound mbid) inl mte in
   let senv = 
     full_add_module (module_body_of_type (MPbound mbid) mtb) senv
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 169fd158d8..c378d8ccc7 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -55,12 +55,12 @@ val add_mind :
 
 (* Adding a module *)
 val add_module :
-  label -> module_entry -> safe_environment
+  label -> module_entry -> bool -> safe_environment
     -> module_path * delta_resolver * safe_environment
 
 (* Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> safe_environment
+  label -> module_struct_entry -> bool -> safe_environment
     -> module_path * safe_environment
 
 (* Adding universe constraints *)
@@ -76,11 +76,11 @@ val start_module :
   label -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> module_struct_entry option 
+  label -> (module_struct_entry * bool) option
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> safe_environment -> delta_resolver * safe_environment
+  mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
@@ -89,7 +89,7 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> bool -> safe_environment ->
+  module_struct_entry -> bool -> bool -> safe_environment ->
    delta_resolver * safe_environment
 
 val pack_module : safe_environment -> module_body