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

6 files changed, 109 insertions, 63 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index dd9dbb8e6..2ffa30526 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -384,7 +384,9 @@ GEXTEND Gram
         filename = ne_string -> 
 	  VernacRequireFrom (export, specif, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
-      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ]
+      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) 
+      | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr))
+      | IDENT "Include"; IDENT "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
@@ -415,12 +417,13 @@ GEXTEND Gram
 
   (* Module expressions *)
   module_expr:
-    [ [ qid = qualid -> CMEident qid
-      | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2)
-      | "("; me = module_expr; ")" -> me
-(* ... *)
+    [ [ me = module_expr_atom -> me
+      | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2)
       ] ]
   ;
+  module_expr_atom:
+    [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ]
+  ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
           CWith_Definition (fqid,c)
@@ -431,8 +434,9 @@ GEXTEND Gram
   module_type:
     [ [ qid = qualid -> CMTEident qid
 (* ... *)
-      | mty = module_type; "with"; decl = with_declaration -> 
-	  CMTEwith (mty,decl) ] ]
+      | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) 
+      | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
+      ] ]
   ;
 END
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 96b2a7167..7e7ea7c56 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -222,6 +222,18 @@ let rec pr_module_type pr_c = function
       let m = pr_module_type pr_c mty in
       let p = pr_with_declaration pr_c decl in
       m ++ spc() ++ str"with" ++ spc() ++ p
+  | CMTEapply (fexpr,mexpr)->
+      let f = pr_module_type pr_c fexpr in
+      let m = pr_module_expr mexpr in
+	f ++ spc () ++ m 
+	  
+and  pr_module_expr = function
+  | CMEident qid -> pr_located pr_qualid qid
+  | CMEapply (me1,(CMEident _ as me2)) ->
+      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,me2) ->
+      pr_module_expr me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
 let pr_of_module_type prc (mty,b) =
   str (if b then ":" else "<:") ++
@@ -254,14 +266,6 @@ let pr_module_binders l pr_c =
 
 let pr_module_binders_list l pr_c = pr_module_binders l pr_c
 
-let rec pr_module_expr = function
-  | CMEident qid -> pr_located pr_qualid qid
-  | CMEapply (me1,(CMEident _ as me2)) ->
-      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
-  | CMEapply (me1,me2) ->
-      pr_module_expr me1 ++ spc() ++
-      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
-
 let pr_type_option pr_c = function
   | CHole (loc, k) -> mt()
   | _ as c -> brk(0,2) ++ str":" ++ pr_c c
@@ -721,19 +725,28 @@ let rec pr_vernac = function
   | VernacDefineModule (export,m,bl,ty,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in 
       hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
-             pr_lident m ++ b ++
-             pr_opt (pr_of_module_type pr_lconstr) ty ++
-             pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
+               pr_lident m ++ b ++
+               pr_opt (pr_of_module_type pr_lconstr) ty ++
+               pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
   | VernacDeclareModule (export,id,bl,m1) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
+	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
              pr_lident id ++ b ++
              pr_of_module_type pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Module Type " ++ pr_lident id ++ b ++
-             pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
-
+	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
+		 pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
+  | VernacInclude (in_ast) ->
+      begin
+	match in_ast with
+	  | CIMTE mty ->
+	      hov 2 (str"Include" ++ 
+		       (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty)
+	  | CIME mexpr ->
+	      hov 2 (str"Include" ++ 
+		       (fun me -> str " " ++ pr_module_expr me) mexpr)
+      end
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6fe4d80d4..6712af8b9 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -39,7 +39,7 @@ type object_pr = {
   print_section_variable    : variable -> std_ppcmds;
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
-  print_modtype             : kernel_name -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
   print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
@@ -175,7 +175,7 @@ type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
   | Syntactic of kernel_name
-  | ModuleType of qualid * kernel_name
+  | ModuleType of qualid * module_path
   | Undefined of qualid
 
 let locate_any_name ref =
@@ -421,7 +421,8 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
 	  let (mp,_,l) = repr_kn kn in 
 	    Some (print_module with_values (MPdot (mp,l)))
       | (_,"MODULE TYPE") ->
-	  Some (print_modtype kn)
+	  let (mp,_,l) = repr_kn kn in 
+	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
       (* To deal with forgotten cases... *)
@@ -560,7 +561,9 @@ let print_full_pure_context () =
 	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | "MODULE TYPE" ->
 	  (* TODO: make it reparsable *)
-	  print_modtype kn ++ str "." ++ fnl () ++ fnl ()
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
   | _::rest -> prec rest
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 35e23d923..c6478376d 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -74,7 +74,7 @@ type object_pr = {
   print_section_variable    : variable -> std_ppcmds;
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
-  print_modtype             : kernel_name -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
   print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index aaf4a662b..69c596093 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -42,11 +42,13 @@ let print_kn locals kn =
       pr_qualid qid
   with
       Not_found -> 
-	let (mp,_,l) = repr_kn kn in
-	  print_local_modpath locals mp ++ str"." ++ pr_lab l
+	try
+	  print_local_modpath locals kn
+	with
+	    Not_found -> print_modpath locals kn
 
 let rec flatten_app mexpr l = match mexpr with
-  | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
+  | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
   | mexpr -> mexpr::l
 
 let rec print_module name locals with_body mb =
@@ -57,58 +59,80 @@ let rec print_module name locals with_body mb =
 	spc () ++ str ":= " ++ print_modexpr locals mexpr
     | Some mp, _, _ -> str " == " ++ print_modpath locals mp
   in
-  hv 2 (str "Module " ++ name ++ spc () ++ str": " ++ 
-	print_modtype locals mb.mod_type ++ body)
-
-and print_modtype locals mty = match mty with
-  | MTBident kn -> print_kn locals kn
-  | MTBfunsig (mbid,mtb1,mtb2) ->
-(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
-      in *) 
-      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
-      hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
-        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype locals mtb1 ++ 
-      str ")" ++ spc() ++ print_modtype locals' mtb2)
-  | MTBsig (msid,sign) -> 
+  let modtype = match mb.mod_type with
+      None -> str ""
+    | Some t ->  str": " ++ 
+	print_modtype locals t
+  in
+    hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body)
+
+and print_modtype locals mty = 
+  match mty with
+    | SEBident kn -> print_kn locals kn
+    | SEBfunctor (mbid,mtb1,mtb2) ->
+      (*    let env' = Modops.add_module (MPbid mbid) 
+	    (Modops.body_of_type mtb) env 
+	    in *) 
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))
+	::locals in
+	hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
+		 pr_id (id_of_mbid mbid) ++ str " : " ++ 
+		 print_modtype locals mtb1 ++ 
+		 str ")" ++ spc() ++ print_modtype locals' mtb2)
+  | SEBstruct (msid,sign) -> 
       hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
+  | SEBapply (mexpr,marg,_) -> 
+      let lapp = flatten_app mexpr [marg] in
+      let fapp = List.hd lapp in
+      let mapp = List.tl lapp in
+	hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++ 
+		 prlist_with_sep spc (print_modexpr locals) mapp ++ str")")
+  | SEBwith(seb,With_definition_body(idl,cb))->
+      let s = (String.concat "." (List.map string_of_id idl)) in
+      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
+	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
+  | SEBwith(seb,With_module_body(idl,mp,_))->
+      let s =(String.concat "." (List.map string_of_id idl)) in
+      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
+	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
 
 and print_sig locals msid sign = 
   let print_spec (l,spec) = (match spec with
-    | SPBconst {const_body=Some _; const_opaque=false} -> str "Definition "
-    | SPBconst {const_body=None}
-    | SPBconst {const_opaque=true} -> str "Parameter "
-    | SPBmind _ -> str "Inductive "
-    | SPBmodule _ -> str "Module "
-    | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
+    | SFBconst {const_body=None}
+    | SFBconst {const_opaque=true} -> str "Parameter "
+    | SFBmind _ -> str "Inductive "
+    | SFBmodule _ -> str "Module "
+    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_spec sign
 
 and print_struct locals msid struc = 
   let print_body (l,body) = (match body with
-    | SEBconst {const_body=Some _; const_opaque=false} -> str "Definition "
-    | SEBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
-    | SEBconst {const_body=None} -> str "Parameter "
-    | SEBmind _ -> str "Inductive "
-    | SEBmodule _ -> str "Module "
-    | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
+    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
+    | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
+    | SFBconst {const_body=None} -> str "Parameter "
+    | SFBmind _ -> str "Inductive "
+    | SFBmodule _ -> str "Module "
+    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_body struc
 
 and print_modexpr locals mexpr = match mexpr with 
-  | MEBident mp -> print_modpath locals mp
-  | MEBfunctor (mbid,mty,mexpr) ->
+  | SEBident mp -> print_modpath locals mp
+  | SEBfunctor (mbid,mty,mexpr) ->
 (*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
       in *)
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
       hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ 
 	     str ":" ++ print_modtype locals mty ++ 
       str "]" ++ spc () ++ print_modexpr locals' mexpr)
-  | MEBstruct (msid, struc) -> 
+  | SEBstruct (msid, struc) -> 
       hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
-  | MEBapply (mexpr,marg,_) -> 
+  | SEBapply (mexpr,marg,_) -> 
       let lapp = flatten_app mexpr [marg] in
 	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
-
+  | SEBwith (_,_)-> anomaly "Not avaible yet"
 
 
 let rec printable_body dir =     
@@ -128,6 +152,8 @@ let print_module with_body mp =
     print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
 
 let print_modtype kn = 
+  let mtb = match Global.lookup_modtype kn with
+    | mtb,_ -> mtb in
   let name = print_kn [] kn in
-    str "Module Type " ++ name ++ str " = " ++ 
-      print_modtype [] (Global.lookup_modtype kn) ++ fnl ()
+      str "Module Type " ++ name ++ str " = " ++ 
+	print_modtype [] mtb ++ fnl ()
diff --git a/parsing/printmod.mli b/parsing/printmod.mli
index 2df0581c4..a3a16e8ec 100644
--- a/parsing/printmod.mli
+++ b/parsing/printmod.mli
@@ -14,4 +14,4 @@ val printable_body : dir_path -> bool
 
 val print_module : bool -> module_path -> std_ppcmds
 
-val print_modtype : kernel_name -> std_ppcmds
+val print_modtype : module_path -> std_ppcmds