fixed bug with aliases

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

1 files changed, 6 insertions, 166 deletions

diff --git a/checker/modops.ml b/checker/modops.ml
index fc8636a0b..f79e52c2e 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -339,169 +339,9 @@ and strengthen_sig env msid sign mp = match sign with
     
 let strengthen env mtb mp = strengthen_mtb env mp mtb
 
-
-(*
-
-
-let rec scrape_modtype env = function
-  | MTBident kn ->
-      let mtb =
-        try lookup_modtype kn env
-        with Not_found ->
-          anomalylabstrm "scrape_modtype"
-            (str"scrape_modtype: cannot find "(*++pr_kn kn*)) in
-      scrape_modtype env mtb
-  | mtb -> mtb
-
-
-(* the constraints are not important here *)
-let module_spec_of_body mb = 
-  { msb_modtype = mb.mod_type; 
-    msb_equiv = mb.mod_equiv; 
-    msb_constraints = Constraint.empty}
-
-
-
-let destr_functor = function
-  | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
-  | mtb -> error_not_a_functor mtb
-
-let rec check_modpath_equiv env mp1 mp2 = 
-  if mp1=mp2 then () else
-  let mb1 = lookup_module mp1 env in
-    match mb1.mod_equiv with
-      | None ->
-	  let mb2 = lookup_module mp2 env in
-	    (match mb2.mod_equiv with
-	      | None -> error_not_equal mp1 mp2
-	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
-      | Some mp1' -> check_modpath_equiv env mp2 mp1'
-
-
-(* we assume that the substitution of "mp" into "msid" is already done
-(or unnecessary) *)
-let rec add_signature mp sign env = 
-  let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
-    let con = make_con mp empty_dirpath l in
-      match elem with
-	| SPBconst cb -> add_constant con cb env
-	| SPBmind mib -> add_mind kn mib env
-	| SPBmodule mb -> 
-	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
-	    (* adds components as well *)
-	| SPBmodtype mtb -> add_modtype kn mtb env
-  in
-    List.fold_left add_one env sign
-
-
-and add_module mp mb env = 
-  let env = shallow_add_module mp mb env in
-    match scrape_modtype env mb.mod_type with
-      | MTBident _ -> anomaly "scrape_modtype does not work!"
-      | MTBsig (msid,sign) -> 
-	  add_signature mp (subst_signature_msid msid mp sign) env
-      | MTBfunsig _ -> env
-
-
-let rec constants_of_specification env mp sign =
- let aux (env,res) (l,elem) =
-  match elem with
-   | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
-   | SPBmind _ -> env,res
-   | SPBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l)) (module_body_of_spec mb) env in 
-       new_env,(constants_of_modtype env (MPdot (mp,l))
-		  (module_body_of_spec mb).mod_type) @ res
-   | SPBmodtype mtb -> 
-       (* module type dans un module type. 
-	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
-	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
-	  mtb
-	  ex: 
-	  Module Type T1. 
-	  Module Type T2.
-	     ....
-    	    End T2.
-	  .....
-            Declare Module M : T2.
-         End T2 
-	  si on ne rajoute pas T2 dans l'environement de typage 
-	  on va exploser au moment du Declare Module
-       *)
-       let new_env = add_modtype (make_kn mp empty_dirpath l) mtb env in 
-       new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
- in
- snd (List.fold_left aux (env,[]) sign)
-
-and constants_of_modtype env mp modtype =
- match scrape_modtype env modtype with
-    MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBsig (msid,sign) ->
-     constants_of_specification env mp
-      (subst_signature_msid msid mp sign)
-  | MTBfunsig _ -> []
-
-
-let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None -> 
-      let const = Const (make_con mp empty_dirpath l) in 
-      let const_subs = Some (from_val const) in
-	{cb with 
-      	   const_body = const_subs;
-	   const_opaque = false(*;
-           const_body_code = Cemitcodes.from_val
-             (compile_constant_body env const_subs false false)*)
-	}
-
-let strengthen_mind env mp l mib = match mib.mind_equiv with
-  | Some _ -> mib
-  | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
-    
-let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
-  | MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBfunsig _ -> mtb
-  | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-
-and strengthen_mod env mp msb = 
-  { msb_modtype = strengthen_mtb env mp msb.msb_modtype;
-    msb_equiv = begin match msb.msb_equiv with
-      | Some _ -> msb.msb_equiv
-      | None -> Some mp 
-    end ;
-    msb_constraints = msb.msb_constraints; }
-
-and strengthen_sig env msid sign mp = match sign with
-  | [] -> []
-  | (l,SPBconst cb) :: rest ->
-      let item' = l,SPBconst (strengthen_const env mp l cb) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SPBmind mib) :: rest ->
-      let item' = l,SPBmind (strengthen_mind env mp l mib) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SPBmodule mb) :: rest ->
-      let mp' = MPdot (mp,l) in
-      let item' = l,SPBmodule (strengthen_mod env mp' mb) in
-      let env' = add_module 
-		   (MPdot (MPself msid,l)) 
-		   (module_body_of_spec mb) 
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item'::rest'
-  | (l,SPBmodtype mty as item) :: rest -> 
-      let env' = add_modtype 
-		   (make_kn (MPself msid) empty_dirpath l) 
-		   mty
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item::rest'
-
-let strengthen env mtb mp = strengthen_mtb env mp mtb
-*)
+let update_subst env mb mp =
+  match type_of_mb env mb with
+    | SEBstruct(msid,str) -> false, join_alias 
+	(subst_key (map_msid msid mp) mb.mod_alias)
+	(map_msid msid mp)
+    | _ -> true, mb.mod_alias