Pour satisfaire ProofGeneral

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

11 files changed, 132 insertions, 44 deletions

diff --git a/TODO b/TODO
index e71916d19..e53d95f8e 100644
--- a/TODO
+++ b/TODO
@@ -16,8 +16,6 @@ Vernac:
 
 - Print / Print Proof en fait identiques ; Print ne devrait pas afficher
   les constantes opaques (devrait afficher qqchose comme <opaque>)
-- Print Module d'un module a l'interier d'un type de module ne devrait pas
-  afficher son corps (il n'a pas de corps!)
 
 Theories:
 
diff --git a/library/lib.ml b/library/lib.ml
index 5ce7cf595..c686e2ccf 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -346,7 +346,7 @@ let end_compilation dir =
   !path_prefix,after
 
 (* Returns true if we are inside an opened module type *)
-let is_specification () = 
+let is_modtype () = 
   let opened_p = function
     | _, OpenedModtype _ -> true 
     | _ -> false
diff --git a/library/lib.mli b/library/lib.mli
index 7f22250f1..6acb565a8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -88,7 +88,8 @@ val sections_are_opened : unit -> bool
 val sections_depth : unit -> int
 
 (* Are we inside an opened module type *)
-val is_specification : unit -> bool
+val is_modtype : unit -> bool
+
 
 (* Returns the most recent OpenedThing node *)
 val what_is_opened : unit -> object_name * node
diff --git a/library/nametab.mli b/library/nametab.mli
index bd1a8b1bd..f14b1a123 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -160,7 +160,6 @@ val shortest_qualid_of_module : module_path -> qualid
 val shortest_qualid_of_modtype : kernel_name -> qualid
 
 
-
 (*
 type frozen
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b4a7fce5b..e8268e038 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -355,13 +355,19 @@ GEXTEND Gram
   gallina_ext:
     [ [ 
 	  (* Interactive module declaration *)
-	IDENT "Module"; id = base_ident; bl = module_binders_list;
-	mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr ->
-	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
+	IDENT "Module"; id = base_ident; 
+	bl = module_binders_list; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDefineModule (id, bl, mty_o, mexpr_o)
 	  
       | IDENT "Module"; "Type"; id = base_ident; 
 	bl = module_binders_list; mty_o = OPT is_module_type ->
 	  VernacDeclareModuleType (id, bl, mty_o)
+	  
+      | IDENT "Declare"; IDENT "Module"; id = base_ident; 
+	bl = module_binders_list; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
 
 	  (* This end a Section a Module or a Module Type *)
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index fd728111d..5418c84ba 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -301,13 +301,6 @@ let print_syntactic_def sep kn =
   (str" Syntactic Definition " ++ pr_qualid qid ++ str sep ++ 
   Constrextern.without_symbols pr_rawterm c ++ fnl ())
 
-(*let print_module with_values kn = 
-  str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
-
-let print_modtype kn =
-  str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
-*)
-
 let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
   let tag = object_tag lobj in
   match (oname,tag) with
@@ -465,7 +458,12 @@ let print_name r =
     let kn = Nametab.locate_syntactic_definition qid in
     print_syntactic_def " = " kn
   with Not_found ->
-  try print_module true (Nametab.locate_module qid)
+  try 
+    let globdir = Nametab.locate_dir qid in
+      match globdir with
+	  DirModule (dirpath,(mp,_)) ->
+	    print_module (printable_body dirpath) mp
+	| _ -> raise Not_found
   with Not_found -> 
   try print_modtype (Nametab.locate_modtype qid)
   with Not_found ->
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 2b75049b2..292967b1c 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -107,6 +107,17 @@ and print_modexpr locals mexpr = match mexpr with
 
 
 
+let rec printable_body dir =     
+  let dir = dirpath_prefix dir in
+    try 
+      match Nametab.locate_dir (qualid_of_dirpath dir) with
+	  DirOpenModtype _ -> false
+	| DirModule _ | DirOpenModule _ -> printable_body dir
+	| _ -> true
+    with 
+	Not_found -> true
+
+
 let print_module with_body mp = 
   let name = print_modpath [] mp in
     print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
diff --git a/parsing/printmod.mli b/parsing/printmod.mli
index ed23fb501..5ffd931ed 100644
--- a/parsing/printmod.mli
+++ b/parsing/printmod.mli
@@ -9,6 +9,9 @@
 open Pp
 open Names
 
+(* false iff the module is an element of an open module type *)
+val printable_body : dir_path -> bool
+
 val print_module : bool -> module_path -> std_ppcmds
 
 val print_modtype : kernel_name -> std_ppcmds
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b8a61e0ec..69534b82b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -205,7 +205,7 @@ let refining () = [] <> (Edit.dom proof_edits)
 let check_no_pending_proofs () =
   if refining () then 
     errorlabstrm "check_no_pending_proofs"
-      (str"Proof editing in progress" ++ (msg_proofs false) ++
+      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
          str"Use \"Abort All\" first or complete proof(s).")
 
 let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 321ce980b..0645a87f0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -171,17 +171,20 @@ let print_modules () =
   and loaded = Library.loaded_libraries () in
   let loaded_opened = list_intersect loaded opened
   and only_loaded = list_subtract loaded opened in
-  str"Loaded and imported modules: " ++ 
+  str"Loaded and imported library files: " ++ 
   pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
-  str"Loaded and not imported modules: " ++
+  str"Loaded and not imported library files: " ++
   pr_vertical_list pr_dirpath only_loaded
 
 
 let print_module r =
   let (loc,qid) = qualid_of_reference r in
   try
-    let mp = Nametab.locate_module qid in
-      msgnl (Printmod.print_module true mp)
+    let globdir = Nametab.locate_dir qid in
+      match globdir with
+	  DirModule (dirpath,(mp,_)) ->
+	    msgnl (Printmod.print_module (Printmod.printable_body dirpath) mp)
+	| _ -> raise Not_found
   with
       Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid)
 
@@ -318,13 +321,13 @@ let start_proof_and_print idopt k t hook =
 let vernac_definition local id def hook =
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
-      if Lib.is_specification () then
-	let ref = declare_assumption id (local,Definitional) bl t in
-	hook local ref
+      if Lib.is_modtype () then
+	errorlabstrm "Vernacentries.VernacDefinition"
+	  (str "Proof editing mode not supported in module types")
       else
 	let hook _ _ = () in
         let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in
-	start_proof_and_print (Some id) kind (bl,t) hook
+	  start_proof_and_print (Some id) kind (bl,t) hook
   | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
         | None -> None
@@ -339,15 +342,10 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode");
-  match Lib.is_specification (), sopt with
-    | true, Some id ->
-        let t = generalize_rawconstr t bl in
-	let ref = declare_assumption id (Global,Logical) [] t in
-	hook Global ref
-    | _ -> 
-	(* an explicit Goal command starts the refining mode 
-	   even in a specification *)
-	start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
+  if Lib.is_modtype () then
+    errorlabstrm "Vernacentries.StartProof"
+      (str "Proof editing mode not supported in module types");
+  start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
 
 let vernac_end_proof is_opaque idopt =
   if_verbose show_script ();
@@ -385,32 +383,102 @@ let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
-  
-  match Lib.is_specification (), mty_ast_o, mexpr_ast_o with
-    | _, None, None 
-    | false, _, None ->
+
+  if not (Lib.is_modtype ()) then
+    error "Declare Module allowed in module types only";
+
+  let constrain_mty = match mty_ast_o with
+      Some (_,true) -> true
+    | _ -> false
+  in
+
+  match mty_ast_o, constrain_mty, mexpr_ast_o with
+    | _, false, None ->  (* no ident, no/soft type *)
+	Declaremods.start_module Modintern.interp_modtype
+	  id binders_ast mty_ast_o;
+	if_verbose message 
+	  ("Interactive Declaration of Module "^ string_of_id id ^" started")
+	  
+    | Some _, true, None           (* no ident, hard type *)
+    | _, false, Some (CMEident _) ->  (* ident, no/soft type *)
+	Declaremods.declare_module 
+	  Modintern.interp_modtype Modintern.interp_modexpr
+	  id binders_ast mty_ast_o mexpr_ast_o;
+	if_verbose message 
+	  ("Module "^ string_of_id id ^" is declared")
+
+    | _, true, Some (CMEident _) -> (* ident, hard type *)
+	error "You cannot declare an equality and a type in module declaration"
+
+    | _, _, Some _ ->    (* not ident *)
+	error "Only simple modules allowed in module declarations"
+
+    | None,true,None -> assert false  (* 1st None ==> false *)
+
+let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o = 
+  (* We check the state of the system (in section, in module type)
+     and what module information is supplied *)
+  if Lib.sections_are_opened () then
+    error "Modules and Module Types are not allowed inside sections";
+ 
+  if Lib.is_modtype () then
+    error "Module definitions not allowed in module types. Use Declare Module instead";
+
+  match mexpr_ast_o with
+    | None ->
 	Declaremods.start_module Modintern.interp_modtype
 	  id binders_ast mty_ast_o;
 	if_verbose message 
 	  ("Interactive Module "^ string_of_id id ^" started")
 	  
-    | true, Some _, None
-    | true, _, Some (CMEident _)
-    | false, _, Some _ ->
+    | Some _ ->
 	Declaremods.declare_module 
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o;
 	if_verbose message 
 	  ("Module "^ string_of_id id ^" is defined")
 
-    | true, _, _ ->
-	error "Module definition not allowed in a Module Type"
+(* let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =  *)
+(*   (\* We check the state of the system (in section, in module type) *)
+(*      and what module information is supplied *\) *)
+(*   if Lib.sections_are_opened () then *)
+(*     error "Modules and Module Types are not allowed inside sections"; *)
+ 
+(*   let constrain_mty = match mty_ast_o with *)
+(*       Some (_,true) -> true *)
+(*     | _ -> false *)
+(*   in *)
+
+(*   match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *)
+(*     | _, None, _, None  *)
+(*     | true, Some _, false, None *)
+(*     | false, _, _, None -> *)
+(* 	Declaremods.start_module Modintern.interp_modtype *)
+(* 	  id binders_ast mty_ast_o; *)
+(* 	if_verbose message  *)
+(* 	  ("Interactive Module "^ string_of_id id ^" started") *)
+	  
+(*     | true, Some _, true, None *)
+(*     | true, _, false, Some (CMEident _) *)
+(*     | false, _, _, Some _ -> *)
+(* 	Declaremods.declare_module  *)
+(* 	  Modintern.interp_modtype Modintern.interp_modexpr *)
+(* 	  id binders_ast mty_ast_o mexpr_ast_o; *)
+(* 	if_verbose message  *)
+(* 	  ("Module "^ string_of_id id ^" is defined") *)
+
+(*     | true, _, _, _ -> *)
+(* 	error "Module definition not allowed in a Module Type" *)
 
 
 let vernac_end_module id =
   Declaremods.end_module id;
   if_verbose message 
-    ("Module "^ string_of_id id ^" is defined")
+    (if Lib.is_modtype () then 
+       "Module "^ string_of_id id ^" is declared"
+     else
+       "Module "^ string_of_id id ^" is defined")
+
   
 
 
@@ -1077,6 +1145,8 @@ let interp c = match c with
   (* Modules *)
   | VernacDeclareModule (id,bl,mtyo,mexpro) -> 
       vernac_declare_module id bl mtyo mexpro
+  | VernacDefineModule (id,bl,mtyo,mexpro) -> 
+      vernac_define_module id bl mtyo mexpro
   | VernacDeclareModuleType (id,bl,mtyo) -> 
       vernac_declare_module_type id bl mtyo
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 30628bfb2..59e089251 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -197,6 +197,8 @@ type vernac_expr =
   (* Modules and Module Types *)
   | VernacDeclareModule of identifier * 
       module_binder list * (module_type_ast * bool) option * module_ast option
+  | VernacDefineModule of identifier * 
+      module_binder list * (module_type_ast * bool) option * module_ast option
   | VernacDeclareModuleType of identifier * 
       module_binder list * module_type_ast option