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

1 files changed, 46 insertions, 61 deletions

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