modules et coqc

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

3 files changed, 90 insertions, 66 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4fb5380f54..c28cfde122 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -341,6 +341,10 @@ GEXTEND Gram
       | IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
       | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
       | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
+      | IDENT "Write"; IDENT "Module"; id = identarg; "." -> 
+	  <:ast< (WriteModule $id) >>
+      | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg; "." -> 
+	  <:ast< (WriteModule $id $s) >>
       | IDENT "Begin"; IDENT "Silent"; "." -> <:ast< (BeginSilent) >>
       | IDENT "End"; IDENT "Silent"; "." -> <:ast< (EndSilent) >>
       | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index e0277761d0..8147fd2b86 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -58,7 +58,7 @@ let fprint_recipe = function
   | None -> [< 'sTR"<uncookable>" >]
 
 let print_typed_recipe (val_0,typ) =
-  [< print_recipe val_0 ; 'fNL ; 'sTR "     : "; prtype typ ; 'fNL >]
+  [< print_recipe val_0; 'fNL; 'sTR "     : "; prtype typ; 'fNL >]
 
 let print_impl_args = function
   | []  -> [<>]
@@ -215,66 +215,74 @@ let print_extracted_mutual sp =
 	print_mutual fwsp (Global.lookup_mind fwsp)
     | Some a -> fprterm a
 
-let print_leaf_entry with_values sep (spopt,lobj) =
+let print_variable sp =
+  let (name,typ,_,_) = out_variable sp in
+  let l = implicits_of_var (kind_of_path sp) name in
+  [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
+
+let print_constant with_values sep sp =
+  let cb = Global.lookup_constant sp in
+  if kind_of_path sp = CCI then
+    let val_0 = cb.const_body in
+    let typ = cb.const_type in
+    let l = constant_implicits sp in
+    hOV 0 [< (match val_0 with 
+		| None -> 
+		    [< 'sTR"*** [ "; 
+		       'sTR (print_basename (ccisp_of sp));  
+		       'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
+		| _ -> 
+		    [< 'sTR(print_basename (ccisp_of sp)) ; 
+		       'sTR sep; 'cUT ;
+		       if with_values then 
+			 print_typed_recipe (val_0,typ) 
+		       else 
+			 [< prtype typ ; 'fNL >] >]); 
+	     print_impl_args (list_of_implicits l); 'fNL >]
+  else
+    hOV 0 [< 'sTR"Fw constant " ; 
+	     'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
+
+let print_inductive sp =
+  let mib = Global.lookup_mind sp in
+  if kind_of_path sp = CCI then
+    [< print_mutual sp mib; 'fNL >]
+  else
+    hOV 0 [< 'sTR"Fw inductive definition "; 
+	     'sTR (print_basename (fwsp_of sp)); 'fNL >]
+
+let print_leaf_entry with_values sep (sp,lobj) =
   let tag = object_tag lobj in
-  match (spopt,tag) with
+  match (sp,tag) with
     | (_,"VARIABLE") ->
-	let (name,typ,_,_) = out_variable spopt in
-	let l = implicits_of_var (kind_of_path spopt) name in
-	[< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
- 
-    | (sp,("CONSTANT"|"PARAMETER")) ->
-	let cb = Global.lookup_constant sp in
-	if kind_of_path sp = CCI then
-	  let val_0 = cb.const_body in
-	  let typ = cb.const_type in
-	  let l = constant_implicits sp in
-	  hOV 0 [< (match val_0 with 
-		      | None -> 
-			  [< 'sTR"*** [ "; 
-			     'sTR (print_basename (ccisp_of sp));  
-			     'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
-		      | _ -> 
-			  [< 'sTR(print_basename (ccisp_of sp)) ; 
-			     'sTR sep; 'cUT ;
-			     if with_values then 
-			       print_typed_recipe (val_0,typ) 
-			     else 
-			       [< prtype typ ; 'fNL >] >]); 
-		   print_impl_args (list_of_implicits l); 'fNL >]
-	else
-	  hOV 0 [< 'sTR"Fw constant " ; 
-		   'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
-
-    | (sp,"INDUCTIVE") ->
-	let mib = Global.lookup_mind sp in
-	if kind_of_path sp = CCI then
-	  [< print_mutual sp mib; 'fNL >]
-	else
-	  hOV 0 [< 'sTR"Fw inductive definition " ; 
-		   'sTR (print_basename (fwsp_of sp)) ; 'fNL >]
-
-    | (_,"AUTOHINT") -> [< 'sTR" Add Auto Marker" ; 'fNL >]
-
-    | (_,"GRAMMAR") -> [< 'sTR" Grammar Marker" ; 'fNL >]
-
-    | (sp,"SYNTAXCONSTANT") -> 
+	print_variable sp
+    | (_,("CONSTANT"|"PARAMETER")) ->
+	print_constant with_values sep sp
+    | (_,"INDUCTIVE") ->
+	print_inductive sp
+    | (_,"AUTOHINT") -> 
+	[< 'sTR" Add Auto Marker"; 'fNL >]
+    | (_,"GRAMMAR") -> 
+	[< 'sTR" Grammar Marker"; 'fNL >]
+    | (_,"SYNTAXCONSTANT") -> 
 	let id = basename sp in
-        [< 'sTR" Syntax Macro " ; 
+        [< 'sTR" Syntax Macro "; 
       	   print_id id ; 'sTR sep;  
            if with_values then 
              let c = Syntax_def.search_syntactic_definition id in 
 	     [< prrawterm c >]
            else [<>]; 'fNL >]
-	
-    | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >]
-
-    | (_,"TOKEN") -> [< 'sTR" Token Marker" ; 'fNL >]
-
-    | (_,"CLASS") -> [< 'sTR" Class Marker" ; 'fNL >]
-    | (_,"COERCION") -> [< 'sTR" Coercion Marker" ; 'fNL >]
-    | (sp,s) -> [< 'sTR(string_of_path sp) ; 'sTR" : " ;
-                   'sTR"Unrecognized object " ; 'sTR s ; 'fNL >]
+    | (_,"PPSYNTAX") -> 
+	[< 'sTR" Syntax Marker"; 'fNL >]
+    | (_,"TOKEN") -> 
+	[< 'sTR" Token Marker"; 'fNL >]
+    | (_,"CLASS") -> 
+	[< 'sTR" Class Marker"; 'fNL >]
+    | (_,"COERCION") -> 
+	[< 'sTR" Coercion Marker"; 'fNL >]
+    | (_,s) -> 
+	[< 'sTR(string_of_path sp); 'sTR" : ";
+           'sTR"Unrecognized object "; 'sTR s; 'fNL >]
 
 let rec print_library_entry with_values ent = 
   let sep = if with_values then " = " else " : " in 
@@ -282,7 +290,9 @@ let rec print_library_entry with_values ent =
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
     | (_,Lib.OpenedSection (str,_)) -> 
-        [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >]
+        [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
+    | (_,Lib.Module str) ->
+	[< 'sTR(" >>>>>>> Module " ^ str); 'fNL >]
     | (_,Lib.FrozenState _) ->
 	[< >]
 	
@@ -374,7 +384,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
                crible_rec rest
 	   | _ -> crible_rec rest)
 
-    | (_, (Lib.OpenedSection _ | Lib.FrozenState _))::rest -> 
+    | (_, (Lib.OpenedSection _ | Lib.FrozenState _ | Lib.Module _))::rest -> 
 	crible_rec rest
     | []      -> ()
   in 
@@ -429,10 +439,19 @@ let print_name name =
   with 
     | Not_found -> 
 	(try 
-	   let (_,typ) = Global.lookup_var name in 
-	   [< print_var str typ;
-              try print_impl_args (implicits_of_var CCI name)
-              with _ -> [<>] >]
+	   (match Declare.global_reference CCI name with
+	      | VAR _ ->
+		  let (_,typ) = Global.lookup_var name in 
+		  [< print_var str typ;
+		     try print_impl_args (implicits_of_var CCI name)
+		     with _ -> [<>] >]
+	      | DOPN(Const sp,_) ->
+		  print_constant true " = " sp
+	      | DOPN(MutInd (sp,_),_) ->
+		  print_inductive sp
+	      | DOPN (MutConstruct((sp,_),_),_) ->
+		  print_inductive sp
+	      | _ -> assert false)
 	 with Not_found | Invalid_argument _ -> 
 	   error (str ^ " not a defined object"))
     | Invalid_argument _ -> error (str ^ " not a defined object")
diff --git a/parsing/printer.ml b/parsing/printer.ml
index df0daa1301..fcda9fb93e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -33,9 +33,10 @@ let with_implicits f x =
     Termast.print_implicits := oimpl; raise e
 
 let pr_qualified sp id = 
-  if Nametab.sp_of_id (kind_of_path sp) id = sp
-  then [< 'sTR(string_of_id id) >]
-  else [< 'sTR(string_of_path sp) >]
+  if Nametab.sp_of_id (kind_of_path sp) id = sp then 
+    [< 'sTR(string_of_id id) >]
+  else 
+    [< 'sTR(string_of_path sp) >]
 
 let pr_constant sp = pr_qualified sp (basename sp)
 
@@ -205,7 +206,7 @@ let dbenv_it_with f env e =
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_sign sign =
   hV 0 [< (sign_it_with (fun id t sign pps ->
-                           [<  pps ; 'wS 2 ; print_decl CCI sign (id,t) >])
+                           [< pps; 'wS 2; print_decl CCI sign (id,t) >])
              sign) [< >] >]
 
 (* Prints an env (variables and de Bruijn). Separator: newline *)
@@ -213,13 +214,13 @@ let pr_env k env =
   let sign_env =
     sign_it_with
       (fun id t sign pps ->
-         let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
+         let pidt =  print_decl k sign (id,t) in [< pps; 'fNL; pidt >])
       (get_globals env) [< >] 
   in
   let db_env =
     dbenv_it_with 
       (fun na t env pps ->
-         let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
+         let pnat = print_binding k env (na,t) in [< pps; 'fNL; pnat >])
       env [< >]
   in 
   [< sign_env; db_env >]
@@ -251,7 +252,7 @@ let pr_env_limit n env =
       dbenv_it_with
         (fun na t env pps ->
            let pnat = print_binding CCI env (na,t) in
-	   [< pps ; 'fNL ;
+	   [< pps; 'fNL;
 	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
 	      pnat >])
         env [< >]