Modops: the strengthening functions can work without any env argument

 The env was used for a particular case of Cbytegen.compile_constant_body,
 but we can actually guess that it will answer a particular BCallias con.

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

6 files changed, 67 insertions, 77 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index bd12528c79..8da06f4355 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -728,6 +728,9 @@ let compile_constant_body env = function
 	    let to_patch = to_memory res in
 	    BCdefined to_patch
 
+(* Shortcut of the previous function used during module strengthening *)
+
+let compile_alias kn = BCallias (constant_of_kn (canonical_con kn))
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 74fb3f7ffe..d0bfd46c00 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -11,6 +11,9 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
 
 val compile_constant_body : env -> constant_def -> body_code
 
+(** Shortcut of the previous function used during module strengthening *)
+
+val compile_alias : constant -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b8162340f7..a384c836ca 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -167,14 +167,14 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      in
 	      let mb_mp1 = (lookup_module mp1 env) in
 	      let mtb_mp1 = 
-		module_type_of_module env' None mb_mp1  in
+		module_type_of_module None mb_mp1  in
 	      let cst =
 		match old.mod_expr with
 		    None ->
 		      begin
 			try union_constraints
 			  (check_subtypes env' mtb_mp1 
-			     (module_type_of_module env' None old))
+			     (module_type_of_module None old))
 			  old.mod_constraints
 			with Failure _ -> error_incorrect_with_constraint (label_of_id id)
 		      end
@@ -183,8 +183,8 @@ and check_with_aux_mod env sign with_decl mp equiv =
 		      old.mod_constraints
 		  | _ ->  error_generative_module_expected l
 	      in
-	      let new_mb = strengthen_and_subst_mb mb_mp1
-		(MPdot(mp,l)) env false in
+	      let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
+	      in
 	      let new_spec = SFBmodule {new_mb with 
 					  mod_mp = MPdot(mp,l);
 					  mod_expr = Some (SEBident mp1);
@@ -279,7 +279,7 @@ and translate_apply env inl ftrans mexpr mkalg =
     try path_of_mexpr mexpr
     with Not_path -> error_application_to_not_path mexpr
   in
-  let mtb = module_type_of_module env None (lookup_module mp1 env) in
+  let mtb = module_type_of_module None (lookup_module mp1 env) in
   let cst2 = check_subtypes env mtb farg_b in
   let mp_delta = discr_resolver env mtb in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
@@ -303,7 +303,7 @@ and translate_functor env inl arg_id arg_e trans mkalg =
 and translate_struct_module_entry env mp inl = function
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp env false in
+      let mb' = strengthen_and_subst_mb mb mp false in
       mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
   | MSEfunctor (arg_id, arg_e, body_expr) ->
       let trans env' = translate_struct_module_entry env' mp inl body_expr in
@@ -345,13 +345,13 @@ and translate_module_type env mp inl mte =
      typ_expr = sign;
      typ_expr_alg = None;
      typ_constraints = cst;
-     typ_delta = resolve} mp env
+     typ_delta = resolve} mp
   in {mtb with typ_expr_alg = alg}
 
 let rec translate_struct_include_module_entry env mp inl = function
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp env true in
+      let mb' = strengthen_and_subst_mb mb mp true in
       let mb_typ = clean_bounded_mod_expr mb'.mod_type in
       mb_typ,None,mb'.mod_delta,Univ.empty_constraint
   | MSEapply (fexpr,mexpr) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index df9b7e81f6..84d8ca67ab 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -289,96 +289,83 @@ and add_module mb env =
       | SEBfunctor _ -> env
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let strengthen_const env mp_from l cb resolver = 
+let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
       let con = make_con mp_from empty_dirpath l in
-      let con =  constant_of_delta resolver con in
-      let const = mkConst con in 
-      let def = Def (Declarations.from_val const) in
+      let con = constant_of_delta resolver con in
       { cb with
-	const_body = def;
-	const_body_code = Cemitcodes.from_val (compile_constant_body env def)
+	const_body = Def (Declarations.from_val (mkConst con));
+	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
       }
 
-let rec strengthen_mod env mp_from mp_to mb = 
+let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then
-    mb 
+    mb
   else
     match mb.mod_type with
-     | SEBstruct (sign) -> 
-	 let resolve_out,sign_out = 
-	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+     | SEBstruct (sign) ->
+	 let resolve_out,sign_out =
+	   strengthen_sig mp_from sign mp_to mb.mod_delta in
 	   { mb with
 	       mod_expr = Some (SEBident mp_to);
 	       mod_type = SEBstruct(sign_out);
 	       mod_type_alg = mb.mod_type_alg;
 	       mod_constraints = mb.mod_constraints;
-	       mod_delta = add_mp_delta_resolver mp_from mp_to 
+	       mod_delta = add_mp_delta_resolver mp_from mp_to
 	       (add_delta_resolver mb.mod_delta resolve_out);
 	       mod_retroknowledge = mb.mod_retroknowledge}
      | SEBfunctor _ -> mb
      | _ -> anomaly "Modops:the evaluation of the structure failed "
-	 
-and strengthen_sig env mp_from sign mp_to resolver =
+
+and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = 
-	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
-	let resolve_out,rest' =
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item'::rest'
+	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = 
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in 
-	let mb_out = 
-	  strengthen_mod env mp_from' mp_to' mb in
+	let mp_to' = MPdot(mp_to,l) in
+	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  add_delta_resolver resolve_out mb.mod_delta,
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
-	let env' = add_modtype 
-	  (MPdot(mp_from,l)) mty env
-	in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
-    
-let strengthen env mtb mp = 
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	add_delta_resolver resolve_out mb.mod_delta, item':: rest'
+    | (l,SFBmodtype mty as item) :: rest ->
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
+
+let strengthen mtb mp =
   if mp_in_delta mtb.typ_mp mtb.typ_delta then
     (* in this case mtb has already been strengthened*)
-    mtb 
+    mtb
   else
     match mtb.typ_expr with
-      | SEBstruct (sign) -> 
+      | SEBstruct (sign) ->
 	  let resolve_out,sign_out =
-	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
+	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
 	    {mtb with
 	       typ_expr = SEBstruct(sign_out);
 	       typ_delta = add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
-	  
-let module_type_of_module env mp mb =
+
+let module_type_of_module mp mb =
   match mp with
       Some mp ->
-	strengthen env {
+	strengthen {
 	  typ_mp = mp;
 	  typ_expr = mb.mod_type;
 	  typ_expr_alg = None;
 	  typ_constraints = mb.mod_constraints;
 	  typ_delta = mb.mod_delta} mp
-	  
+
     | None ->
 	{typ_mp = mb.mod_mp;
 	 typ_expr = mb.mod_type;
@@ -409,7 +396,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
   make_inline delta constants
 
 let rec strengthen_and_subst_mod
-    mb subst env mp_from mp_to env resolver =
+    mb subst mp_from mp_to resolver =
      match mb.mod_type with
 	 SEBstruct(str) ->
 	   let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
@@ -418,7 +405,7 @@ let rec strengthen_and_subst_mod
 	       (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb 
 	   else
 	     let resolver,new_sig = 
-	       strengthen_and_subst_struct str subst env
+	       strengthen_and_subst_struct str subst
 		 mp_from mp_from mp_to false false mb.mod_delta 
 	     in
 	       {mb with 
@@ -434,7 +421,7 @@ let rec strengthen_and_subst_mod
        | _ -> anomaly "Modops:the evaluation of the structure failed "
 	   
 and strengthen_and_subst_struct 
-    str subst env mp_alias mp_from mp_to alias incl resolver =
+    str subst mp_alias mp_from mp_to alias incl resolver =
   match str with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
@@ -442,12 +429,12 @@ and strengthen_and_subst_struct
 	  (* case alias no strengthening needed*)
 	  l,SFBconst (subst_const_body subst cb) 
 	else 
-	  l,SFBconst (strengthen_const env mp_from l 
+	  l,SFBconst (strengthen_const mp_from l
 			(subst_const_body subst cb) resolver)
 	in
 	let con = make_con mp_from empty_dirpath l in
 	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst env 
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	  if incl then
 	    (* If we are performing an inclusion we need to add
@@ -468,7 +455,7 @@ and strengthen_and_subst_struct
 	let item' = l,SFBmind (subst_mind subst mib) in
 	let mind = make_mind mp_from empty_dirpath l in
 	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst env 
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	  if incl then
 	    let old_name =  mind_of_delta resolver mind in 
@@ -485,12 +472,11 @@ and strengthen_and_subst_struct
 	  (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb 
 	else
 	  strengthen_and_subst_mod
-	    mb subst env mp_from' mp_to' env resolver
+	    mb subst mp_from' mp_to' resolver
 	in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_and_subst_struct rest subst env' 
+	let resolve_out,rest' =
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	  (* if mb is a functor we should not derive new equivalences
 	     on names, hence we add the fact that the functor can only
@@ -508,8 +494,7 @@ and strengthen_and_subst_struct
 	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
 	let mty = subst_modtype subst' 
 	  (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
-	let env' = add_modtype mp_from' mty env	in
-	let resolve_out,rest' = strengthen_and_subst_struct rest subst env' 
+	let resolve_out,rest' = strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	  (add_mp_delta_resolver 
 	     mp_to' mp_to' resolve_out),(l,SFBmodtype mty)::rest'
@@ -518,7 +503,7 @@ and strengthen_and_subst_struct
 (* Let P be a module path when we write "Module M:=P." or "Module M. Include P. End M."
    we need to perform two operations to compute the body of M. The first one is applying
    the substitution {P <- M} on the type of P and the second one is strenghtening. *)
-let strengthen_and_subst_mb mb mp env include_b =
+let strengthen_and_subst_mb mb mp include_b =
     match mb.mod_type with
 	SEBstruct str ->
 	  let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
@@ -531,7 +516,7 @@ let strengthen_and_subst_mb mb mp env include_b =
 	      (subst_dom_delta_resolver subst_resolver mb.mod_delta) in
 	  let subst = map_mp mb.mod_mp mp new_resolver in 
 	  let resolver_out,new_sig = 
-	    strengthen_and_subst_struct str subst env
+	    strengthen_and_subst_struct str subst
 	     mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta 
 	  in
 	    {mb with 
@@ -547,7 +532,7 @@ let strengthen_and_subst_mb mb mp env include_b =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let subst_modtype_and_resolver mtb mp env =
+let subst_modtype_and_resolver mtb mp =
   let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
   let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in 
   let full_subst = (map_mp mtb.typ_mp mp new_delta) in
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 35be04665b..b9c36d5af4 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -19,7 +19,7 @@ open Mod_subst
 
 val module_body_of_type : module_path -> module_type_body  -> module_body 
 
-val module_type_of_module : env -> module_path option -> module_body -> 
+val module_type_of_module : module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
@@ -37,16 +37,15 @@ val add_module : module_body -> env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> module_path -> module_type_body
 
 val inline_delta_resolver :
   env -> inline -> module_path -> mod_bound_id -> module_type_body ->
   delta_resolver -> delta_resolver
 
-val strengthen_and_subst_mb : module_body -> module_path -> env -> bool 
-  -> module_body
+val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
 
-val subst_modtype_and_resolver : module_type_body -> module_path -> env ->
+val subst_modtype_and_resolver : module_type_body -> module_path ->
   module_type_body
 
 val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2430dc6f0f..00af99d980 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -302,8 +302,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
    | _ -> error DefinitionFieldExpected
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
-  let mty1 = module_type_of_module env None msb1 in
-  let mty2 =  module_type_of_module env None msb2 in
+  let mty1 = module_type_of_module None msb1 in
+  let mty2 =  module_type_of_module None msb2 in
   let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
     cst
 
@@ -397,6 +397,6 @@ let check_subtypes env sup super =
   let env = add_module 
 		(module_body_of_type sup.typ_mp sup) env in
   check_modtypes empty_constraint env 
-    (strengthen env sup sup.typ_mp) super empty_subst 
+    (strengthen sup sup.typ_mp) super empty_subst
     (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false