Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




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

1 files changed, 171 insertions, 180 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 93d01f12a..201835c10 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -22,14 +22,9 @@ open Mod_subst
 exception Not_path
 
 let path_of_mexpr = function
-  | MEident mb -> mb
+  | MSEident mb -> mb
   | _ -> raise Not_path
 
-let rec replace_first p k = function 
-  | [] -> [] 
-  | h::t when p h -> k::t
-  | h::t -> h::(replace_first p k t)
-
 let rec list_split_assoc k rev_before = function
   | [] -> raise Not_found
   | (k',b)::after when k=k' -> rev_before,b,after
@@ -42,25 +37,88 @@ let rec list_fold_map2 f e = function
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
-let type_modpath env mp = 
-  strengthen env (lookup_module mp env).mod_type mp
+let rec check_with env mtb with_decl = 
+  match with_decl with
+    | With_Definition (id,_) -> 
+	let cb = check_with_aux_def env mtb with_decl in
+	  SEBwith(mtb,With_definition_body(id,cb))
+    | With_Module (id,mp) -> 
+	let cst = check_with_aux_mod env mtb with_decl in
+	  SEBwith(mtb,With_module_body(id,mp,cst))
 
-let rec translate_modtype env mte =
-  match mte with
-    | MTEident ln -> MTBident ln
-    | MTEfunsig (arg_id,arg_e,body_e) -> 
-	let arg_b = translate_modtype env arg_e in
-	let env' = 
-	  add_module (MPbound arg_id) (module_body_of_type arg_b) env in
-	let body_b = translate_modtype env' body_e in
-	  MTBfunsig (arg_id,arg_b,body_b)
-    | MTEwith (mte, with_decl) ->
-	let mtb = translate_modtype env mte in
-	  merge_with env mtb with_decl
+and check_with_aux_def env mtb with_decl = 
+  let msid,sig_b = match (eval_struct env mtb) with 
+    | SEBstruct(msid,sig_b) ->
+	msid,sig_b
+    | _ -> error_signature_expected mtb
+  in
+  let id,idl = match with_decl with 
+    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
+    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  in
+  let l = label_of_id id in
+    try
+      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let before = List.rev rev_before in
+      let env' = Modops.add_signature (MPself msid) before env in
+	match with_decl with
+          | With_Definition ([],_) -> assert false
+	  | With_Definition ([id],c) -> 
+	      let cb = match spec with
+		  SFBconst cb -> cb
+		| _ -> error_not_a_constant l
+	      in 
+		begin
+		  match cb.const_body with
+		    | None -> 
+			let (j,cst1) = Typeops.infer env' c in
+			let typ = Typeops.type_of_constant_type env' cb.const_type in
+			let cst2 = Reduction.conv_leq env' j.uj_type typ in
+			let cst = 
+			  Constraint.union 
+			    (Constraint.union cb.const_constraints cst1)
+			    cst2 in
+			let body = Some (Declarations.from_val j.uj_val) in
+			let cb' = {cb with 
+				     const_body = body;
+				     const_body_code = Cemitcodes.from_val
+                            (compile_constant_body env' body false false);
+                                     const_constraints = cst} in
+			  cb'
+		    | Some b -> 
+			let cst1 = Reduction.conv env' c (Declarations.force b) in
+			let cst = Constraint.union cb.const_constraints cst1 in
+			let body = Some (Declarations.from_val c) in
+			let cb' = {cb with 
+				     const_body = body;
+				     const_body_code = Cemitcodes.from_val
+                            (compile_constant_body env' body false false);
+                                     const_constraints = cst} in
+			  cb'
+	      end
+	  | With_Definition (_::_,_) ->
+	      let old = match spec with
+		  SFBmodule msb -> msb
+		| _ -> error_not_a_module (string_of_label l)
+	      in
+		begin
+		  match old.mod_equiv with
+                    | None ->
+			let new_with_decl = match with_decl with
+			    With_Definition (_,c) -> With_Definition (idl,c)
+			  | With_Module (_,c) -> With_Module (idl,c) in 
+			  check_with_aux_def env' (type_of_mb env old) new_with_decl
+                    | Some mp ->
+			error_a_generative_module_expected l
+		end
+	  | _ -> anomaly "Modtyping:incorrect use of with"
+    with
+	Not_found -> error_no_such_label l
+      | Reduction.NotConvertible -> error_with_incorrect l
 
-and merge_with env mtb with_decl = 
-  let msid,sig_b = match (Modops.scrape_modtype env mtb) with 
-    | MTBsig(msid,sig_b) -> let msid'=(refresh_msid msid) in
+and check_with_aux_mod env mtb with_decl = 
+  let msid,sig_b = match (eval_struct env mtb) with 
+    | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in
 	msid',(subst_signature_msid msid (MPself(msid')) sig_b)
     | _ -> error_signature_expected mtb
   in
@@ -73,107 +131,58 @@ and merge_with env mtb with_decl =
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature (MPself msid) before env in
-      let new_spec = match with_decl with
-        | With_Definition ([],_)
-        | With_Module ([],_) -> assert false
-	| With_Definition ([id],c) -> 
-	    let cb = match spec with
-		SPBconst cb -> cb
-	      | _ -> error_not_a_constant l
-	    in 
-	      begin
-		match cb.const_body with
-		  | None -> 
-		      let (j,cst1) = Typeops.infer env' c in
-		      let typ = Typeops.type_of_constant_type env' cb.const_type in
-		      let cst2 = Reduction.conv_leq env' j.uj_type typ in
-		      let cst = 
-			Constraint.union 
-			  (Constraint.union cb.const_constraints cst1)
-			  cst2 in
-                      let body = Some (Declarations.from_val j.uj_val) in
-			SPBconst {cb with 
-				    const_body = body;
-			            const_body_code = Cemitcodes.from_val
-                        (compile_constant_body env' body false false);
-                                    const_constraints = cst}
-		  | Some b -> 
-		      let cst1 = Reduction.conv env' c (Declarations.force b) in
-		      let cst = Constraint.union cb.const_constraints cst1 in
-                      let body = Some (Declarations.from_val c) in
-			SPBconst {cb with 
-				    const_body = body;
-				    const_body_code = Cemitcodes.from_val
-                        (compile_constant_body env' body false false);
-                                    const_constraints = cst}
-	      end	
-(* and what about msid's ????? Don't they clash ? *)
-	| With_Module ([id], mp) ->
-	    let old = match spec with
-		SPBmodule msb -> msb
-	      | _ -> error_not_a_module (string_of_label l)
-	    in
-	    let mtb = type_modpath env' mp in
-	    let cst =
-              try check_subtypes env' mtb old.msb_modtype
+	match with_decl with
+          | With_Module ([],_) -> assert false
+	  | With_Module ([id], mp) ->
+	      let old = match spec with
+		  SFBmodule msb -> msb
+		| _ -> error_not_a_module (string_of_label l)
+	      in
+	      let mtb' = eval_struct env' (SEBident mp) in
+	      let cst =
+		try check_subtypes env' mtb' (type_of_mb env old)
               with Failure _ -> error_with_incorrect (label_of_id id) in
-	    let equiv = 
- 	      match old.msb_equiv with
+	      let _ = 
+ 		match old.mod_equiv with
 		| None -> Some mp
 		| Some mp' -> 
 		    check_modpath_equiv env' mp mp';
 		    Some mp
-	    in
-	    let msb =
-	      {msb_modtype = mtb; 
-	       msb_equiv = equiv; 
-	       msb_constraints = Constraint.union old.msb_constraints cst }
-	    in
-	      SPBmodule msb
-	| With_Definition (_::_,_)
+	      in
+		cst
         | With_Module (_::_,_) -> 
 	    let old = match spec with
-		SPBmodule msb -> msb
+		SFBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	      begin
-		match old.msb_equiv with
-                   None ->
-                    let new_with_decl = match with_decl with
-                       With_Definition (_,c) -> With_Definition (idl,c)
-                     | With_Module (_,c) -> With_Module (idl,c) in
-                    let modtype = 
-                     merge_with env' old.msb_modtype new_with_decl in
-                    let msb =
-	              {msb_modtype = modtype; 
-	               msb_equiv = None; 
-	               msb_constraints = old.msb_constraints }
-	            in
-	             SPBmodule msb
-                 | Some mp ->
-                    error_a_generative_module_expected l
+		match old.mod_equiv with
+                    None ->
+                      let new_with_decl = match with_decl with
+			  With_Definition (_,c) -> With_Definition (idl,c)
+			| With_Module (_,c) -> With_Module (idl,c) in
+			check_with_aux_mod env' (type_of_mb env old) new_with_decl 
+                  | Some mp ->
+                      error_a_generative_module_expected l
               end
-      in
-	MTBsig(msid,  before@(l,new_spec)::after)
+	| _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
-
-
-and translate_module env  me =
+	  
+and translate_module env 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_modtype env mte in
+	let mtb = translate_struct_entry env mte in
 	{ mod_expr = None;
-	  mod_user_type = Some mtb;
-	  mod_type = mtb;
+	  mod_type = Some mtb;
 	  mod_equiv = None;
-	  mod_constraints = Constraint.empty;
-	  mod_retroknowledge = [] } 
+	  mod_constraints = Constraint.empty; 
+	  mod_retroknowledge = []}
     | Some mexpr, _ -> 
-	let meq_o = (* do we have a transparent module ? *)
+	let meq_o = 
 	  try       (* TODO: transparent field in module_entry *)
 	    match me.mod_entry_type with
 	      | None -> Some (path_of_mexpr mexpr)
@@ -181,17 +190,17 @@ and translate_module env  me =
 	  with 
 	    | Not_path -> None
 	in
-	let meb,mtb1 = translate_mexpr env mexpr in
-	let mtb, mod_user_type, cst =
+	let meb = translate_struct_entry env mexpr in
+	let mod_typ, cst =
 	  match me.mod_entry_type with
-	    | None -> mtb1, None, Constraint.empty
+	    | None ->  None, Constraint.empty
 	    | Some mte -> 
-		let mtb2 = translate_modtype env mte in
-                let cst = check_subtypes env mtb1 mtb2 in
-		mtb2, Some mtb2, cst
+		let mtb1 = translate_struct_entry env mte in
+                let cst = check_subtypes env (eval_struct env meb)
+		  mtb1 in
+		  Some mtb1, cst
 	in
-	  { mod_type = mtb;
-	    mod_user_type = mod_user_type;
+	  { mod_type = mod_typ;
 	    mod_expr = Some meb;
 	    mod_equiv = meq_o;
 	    mod_constraints = cst;
@@ -200,96 +209,78 @@ and translate_module env  me =
 					If it does, I don't really know how to
 					fix the bug.*)
 
-(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
-and translate_mexpr env mexpr = match mexpr with
-  | MEident mp -> 
-      MEBident mp,
-      type_modpath env mp
-  | MEfunctor (arg_id, arg_e, body_expr) ->
-      let arg_b = translate_modtype env arg_e in
+
+and translate_struct_entry env mse = match mse with
+  | MSEident mp -> 
+      SEBident mp
+  | MSEfunctor (arg_id, arg_e, body_expr) ->
+      let arg_b = translate_struct_entry env arg_e in
       let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
-      let (body_b,body_tb) = translate_mexpr env' body_expr in
-	MEBfunctor (arg_id, arg_b, body_b), 
-	MTBfunsig (arg_id, arg_b, body_tb)
-  | MEapply (fexpr,mexpr) ->
-      let feb,ftb = translate_mexpr env fexpr in
-      let ftb = scrape_modtype env ftb in
-      let farg_id, farg_b, fbody_b = destr_functor ftb in
-      let meb,mtb = translate_mexpr env mexpr in
-      let cst = check_subtypes env mtb farg_b in
-      let mp = 
+      let body_b = translate_struct_entry env' body_expr in
+	SEBfunctor (arg_id, arg_b, body_b)
+  | MSEapply (fexpr,mexpr) ->
+      let feb = translate_struct_entry env fexpr in
+      let feb'= eval_struct env feb
+      in
+      let farg_id, farg_b, fbody_b = destr_functor env feb' in
+      let _ = 
 	try
 	  path_of_mexpr mexpr 
 	with
 	  | Not_path -> error_application_to_not_path mexpr
-	      (* place for nondep_supertype *)
-      in
-       let resolve = Modops.resolver_of_environment farg_id farg_b mp env in
-	MEBapply(feb,meb,cst),
-        (* This is the place where the functor formal parameter is
-           substituted by the given argument to compute the type of the
-           functor application. *)
-	subst_modtype 
-         (map_mbid farg_id mp (Some resolve)) fbody_b
- 
+	      (* place for nondep_supertype *) in
+      let meb= translate_struct_entry env mexpr in
+      let cst = check_subtypes env (eval_struct env meb) farg_b in
+	SEBapply(feb,meb,cst)
+  | MSEwith(mte, with_decl) ->
+	let mtb = translate_struct_entry env mte in
+	let mtb' = check_with env mtb with_decl in
+	  mtb'
 
-let translate_module env me = translate_module env  me
 
-let rec add_module_expr_constraints env = function
-  | MEBident _ -> env
+let rec add_struct_expr_constraints env = function
+  | SEBident _ -> env
 
-  | MEBfunctor (_,mtb,meb) -> 
-      add_module_expr_constraints (add_modtype_constraints env mtb) meb
+  | SEBfunctor (_,mtb,meb) -> 
+      add_struct_expr_constraints 
+	(add_modtype_constraints env mtb) meb
 
-  | MEBstruct (_,mod_struct_body) ->
+  | SEBstruct (_,structure_body) ->
       List.fold_left 
         (fun env (l,item) -> add_struct_elem_constraints env item)
         env
-        mod_struct_body
+        structure_body
 
-  | MEBapply (meb1,meb2,cst) ->
+  | SEBapply (meb1,meb2,cst) ->
       Environ.add_constraints cst 
-        (add_module_expr_constraints 
-	  (add_module_expr_constraints env meb1) 
+        (add_struct_expr_constraints 
+	  (add_struct_expr_constraints env meb1) 
 	  meb2)
-
+  | SEBwith(meb,With_definition_body(_,cb))->
+      Environ.add_constraints cb.const_constraints
+	(add_struct_expr_constraints env meb)
+  | SEBwith(meb,With_module_body(_,_,cst))->
+      Environ.add_constraints cst
+	(add_struct_expr_constraints env meb)	
+		
 and add_struct_elem_constraints env = function 
-  | SEBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SEBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SEBmodule mb -> add_module_constraints env mb
-  | SEBmodtype mtb -> add_modtype_constraints env mtb
+  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
+  | SFBmodule mb -> add_module_constraints env mb
+  | SFBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
-  (* if there is a body, the mb.mod_type is either inferred from the
-     body and hence uninteresting or equal to the non-empty
-     user_mod_type *)
   let env = match mb.mod_expr with
-    | None -> add_modtype_constraints env mb.mod_type
-    | Some meb -> add_module_expr_constraints env meb
+    | None -> env
+    | Some meb -> add_struct_expr_constraints env meb
   in
-  let env = match mb.mod_user_type with
+  let env = match mb.mod_type with
     | None -> env
-    | Some mtb -> add_modtype_constraints env mtb
+    | Some mtb -> 
+	add_modtype_constraints env mtb
   in
     Environ.add_constraints mb.mod_constraints env
 
-and add_modtype_constraints env = function
-  | MTBident _ -> env
-  | MTBfunsig (_,mtb1,mtb2) ->
-      add_modtype_constraints
-        (add_modtype_constraints env mtb1)
-        mtb2
-  | MTBsig (_,mod_sig_body) ->
-      List.fold_left 
-        (fun env (l,item) -> add_sig_elem_constraints env item)
-        env
-        mod_sig_body
-
-and add_sig_elem_constraints env = function 
-  | SPBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> 
-      add_modtype_constraints (Environ.add_constraints cst env) mtb
-  | SPBmodtype mtb -> add_modtype_constraints env mtb
-
-
+and add_modtype_constraints env mtb = 
+  add_struct_expr_constraints env mtb
+