Various bug fix on recent features of the module system:

 - Include Self and equivalence of names
 - Include type in modules and nametab
 - Bang operator and composition of substitution



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

3 files changed, 116 insertions, 105 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 75a167f6c5..930d9aa7dd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -140,12 +140,16 @@ let rec find_prefix resolve mp =
       sub_mp mp
     with
 	Not_found -> mp
-	  
+
+exception Change_equiv_to_inline of constr
+
 let solve_delta_kn resolve kn =
   try 
       match Deltamap.find (KN kn) resolve with
 	| Equiv kn1 -> kn1
-	| Inline _ -> raise Inline_kn
+	| Inline (Some c) -> 
+	    raise (Change_equiv_to_inline c)
+	| Inline None -> raise Inline_kn
 	| _ -> anomaly 
 	    "mod_subst: bad association in delta_resolver"
   with
@@ -160,39 +164,50 @@ let solve_delta_kn resolve kn =
 
 let constant_of_delta resolve con =
   let kn = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn new_kn
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn new_kn
+    with 
+	_ -> con 
 	
 let constant_of_delta2 resolve con =
   let kn = canonical_con con in
   let kn1 = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn1 new_kn
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn1 new_kn
+    with 
+	_ -> con
 
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn new_kn
-	
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn new_kn
+    with 
+	_ -> mind 
+
 let mind_of_delta2 resolve mind =
   let kn = canonical_mind mind in
   let kn1 = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn1 new_kn
-
-
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn1 new_kn
+    with 
+	_ -> mind
+	  
 
 let inline_of_delta resolver = 
   let extract key hint l =
@@ -567,7 +582,11 @@ let subst_codom_delta_resolver subst resolver =
 	    Deltamap.fold Deltamap.add derived_resolve
 	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
       | (Equiv kn) ->
-	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	  (try
+	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	   with
+	       Change_equiv_to_inline c ->
+		 Deltamap.add key (Inline (Some c)) resolver)
       | Inline None ->
 	  Deltamap.add key hint resolver
       | Inline (Some t) ->
@@ -585,10 +604,14 @@ let subst_dom_codom_delta_resolver subst resolver =
 	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
       | (KN kn1),(Equiv kn) ->
 	  let key = KN (subst_kn subst kn1) in
-	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	    (try
+	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	     with
+		 Change_equiv_to_inline c ->
+		   Deltamap.add key (Inline (Some c)) resolver)
       | (KN kn),Inline None ->
 	  let key = KN (subst_kn subst kn) in
-	  Deltamap.add key hint resolver
+	    Deltamap.add key hint resolver
       | (KN kn),Inline (Some t) ->
 	  let key = KN (subst_kn subst kn) in
 	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
@@ -607,9 +630,13 @@ let update_delta_resolver resolver1 resolver2 =
 		Prefix_equiv (find_prefix resolver2 mp)
 	      in Deltamap.add key new_hint res
 	  | Equiv kn ->
-	      let new_hint =
-		Equiv (solve_delta_kn resolver2 kn)
-	      in Deltamap.add key new_hint res
+	      (try 
+		 let new_hint =
+		   Equiv (solve_delta_kn resolver2 kn)
+		 in Deltamap.add key new_hint res
+	       with
+		   Change_equiv_to_inline c ->
+		     Deltamap.add key (Inline (Some c)) res)
 	  | _ -> Deltamap.add key hint res
       with not_found -> 
 	Deltamap.add key hint res
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4c6ec35e1..d9c7c9de04 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -438,23 +438,24 @@ let end_module l restype senv =
    let senv = add_constraints cst senv in
    let mp_sup = senv.modinfo.modpath in
      (* Include Self support  *)
-   let rec compute_sign sign mb senv = 
+   let rec compute_sign sign mb resolver senv = 
      match sign with
      | 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 = if not inl then mb.typ_delta else
-	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta
-	 in
+	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta in
+	 let subst = map_mbid mbid mp_sup mpsup_delta in
+	 let resolver = subst_codom_delta_resolver subst resolver in
 	   (compute_sign 
-	     (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv)
-     | str -> str,senv
+	     (subst_struct_expr subst str) mb resolver senv)
+     | str -> resolver,str,senv
    in
-   let sign,senv = compute_sign sign {typ_mp = mp_sup;
+   let resolver,sign,senv = compute_sign sign {typ_mp = mp_sup;
 				      typ_expr = SEBstruct (List.rev senv.revstruct);
 				      typ_expr_alg = None;
 				      typ_constraints = Constraint.empty;
-				      typ_delta = senv.modinfo.resolver} senv in
+				      typ_delta = senv.modinfo.resolver} resolver senv in
    let str = match sign with
      | SEBstruct(str_l) -> str_l
      | _ -> error ("You cannot Include a high-order structure.")
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0092e29c52..bca52c5560 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -386,7 +386,6 @@ let (in_modtype,_) =
       subst_function = subst_modtype;
       classify_function = classify_modtype }
 
-
 let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
   if mbids<>[] then 
     error "Unexpected functor objects"
@@ -744,6 +743,54 @@ let rec get_module_substobjs env mp_from inl = function
   | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
   | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
+
+let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
+  let mmp = Global.start_module id in
+  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
+  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
+  let env = Global.env() in
+  let mty_entry_o, subs, inl_res = match res with
+    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
+    | Topconstr.Check mtys ->
+	None, build_subtypes interp_modtype mmp arg_entries mtys, true
+  in
+ 
+  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, true
+    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
+  in
+  let entry =
+    {mod_entry_type = mty_entry_o;
+     mod_entry_expr = mexpr_entry_o }
+  in
+
+  let substobjs =
+    match entry with
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
+      | _ -> anomaly "declare_module: No type, no body ..."
+  in
+  let (mbids,mp_from,objs) = substobjs in
+  (* Undo the simulated interactive building of the module *)
+  (* and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+  let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in
+
+  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+
+  
+  check_subtypes mp subs;
+
+  let substobjs = (mbids,mp_env,
+		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  ignore (add_leaf
+	    id
+	    (in_module (Some (entry), substobjs)));
+  mmp
+
 (* Include *)
 
 let rec subst_inc_expr subst me =
@@ -784,10 +831,8 @@ let load_include  i (oname,((me,is_mod),(mbis,mp1,objs))) =
 let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-      if is_mod || i = 1 then
-	open_objects i prefix objs
-      else ()
-    
+    open_objects i prefix objs
+          
 let subst_include (subst,((me,is_mod),substobj)) =
   let (mbids,mp,objs) = substobj in
   let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
@@ -804,68 +849,6 @@ let (in_include,out_include) =
     subst_function = subst_include;
     classify_function = classify_include }
 
-let rec update_include (mbids,mp,objs) =
-  let rec replace_include = function
-    | [] -> []
-    | (id,obj)::tail ->
-	if object_tag obj = "INCLUDE" then
-	  let ((me,is_mod),substobjs) = out_include obj in
-	  let substobjs' = update_include substobjs in
-            (id, in_include ((me,true),substobjs'))::
-	      (replace_include tail)
-	else
-	  (id,obj)::(replace_include tail)
-  in
-    (mbids,mp,replace_include objs)
-
-let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
-  let mmp = Global.start_module id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
-  let env = Global.env() in
-  let mty_entry_o, subs, inl_res = match res with
-    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
-    | Topconstr.Check mtys ->
-	None, build_subtypes interp_modtype mmp arg_entries mtys, true
-  in
- 
-  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
-  let mexpr_entry_o, inl_expr = match mexpr_o with
-    | None -> None, true
-    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
-  in
-  let entry =
-    {mod_entry_type = mty_entry_o;
-     mod_entry_expr = mexpr_entry_o }
-  in
-
-  let substobjs =
-    match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
-      | _ -> anomaly "declare_module: No type, no body ..."
-  in
-  let (mbids,mp_from,objs) = update_include substobjs in
-  (* Undo the simulated interactive building of the module *)
-  (* and declare the module as a whole *)
-  Summary.unfreeze_summaries fs;
-  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-  let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in
-
-  if mp_env <> mp then anomaly "Kernel and Library names do not match";
-
-  
-  check_subtypes mp subs;
-
-  let substobjs = (mbids,mp_env,
-		   subst_objects(map_mp mp_from mp_env resolver) objs) in
-  ignore (add_leaf
-	    id
-	    (in_module (Some (entry), substobjs)));
-  mmp
-
-
 let rec include_subst env mb mbids sign inline =
   match mbids with
     | [] -> empty_subst