Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)

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

4 files changed, 88 insertions, 105 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 30fee26a03..d07051b718 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -447,7 +447,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 		  try 
 		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
 		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+		      Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 		([], props) k.cl_props
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 02044b2cf2..83a4703a24 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -108,15 +108,11 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+  let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
     List.iter
       (fun (v,f) ->
 	 States.unfreeze init_state;
-	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
-	 if !Flags.noglob then
-	   Flags.dump := false
-	 else
-	   Flags.dump_into_file (f^".glob");
+	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
 	 if Flags.do_translate () then
 	   with_option translate_file (Vernac.compile v) f
 	 else
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c0ec552280..d3c556147d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,7 +126,7 @@ let rec vernac_com interpfun (loc,com) =
         let cl = !Pp.comments in
         (* end translator state *)
         (* coqdoc state *)
-        let cds = Constrintern.coqdoc_freeze() in
+        let cds = Dumpglob.coqdoc_freeze() in
           if !Flags.translate_file then 
 	    begin
               let _,f = find_file_in_path (Library.get_load_paths ())
@@ -141,13 +141,13 @@ let rec vernac_com interpfun (loc,com) =
               chan_translate := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
-              Constrintern.coqdoc_unfreeze cds
+              Dumpglob.coqdoc_unfreeze cds
 	    with e -> 
 	      if !Flags.translate_file then close_out !chan_translate;
               chan_translate := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
-              Constrintern.coqdoc_unfreeze cds;
+              Dumpglob.coqdoc_unfreeze cds;
 	      raise e
 	  end
 	      
@@ -228,14 +228,15 @@ let compile verbosely f =
   let ldir,long_f_dot_v = Library.start_library f in
   let dumpstate = !Flags.dump in
     if not !Flags.noglob then
-      (Flags.dump_into_file (f ^ ".glob");
-       Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+      (Flags.dump := true; 
+       Dumpglob.open_glob_file f;
+       Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
     if !Flags.xml_export then !xml_start_library ();
     let _ = load_vernac verbosely long_f_dot_v in
      if Pfedit.get_all_proof_names () <> [] then
 	(message "Error: There are pending proofs"; exit 1);
       if !Flags.xml_export then !xml_end_library ();
-      if !Flags.dump then Flags.dump_it ();
+      if !Flags.dump then Dumpglob.close_glob_file ();
       Flags.dump := dumpstate;
       Library.save_library_to ldir (long_f_dot_v ^ "o")
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2cea826a7f..d1003bd830 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -275,7 +275,7 @@ let print_located_module r =
 
 let global_with_alias r =
   let gr = global_with_alias r in
-    if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+    if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
     gr
 
 (**********)
@@ -305,49 +305,31 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let current_dirpath sec =
-  drop_dirpath_prefix (Lib.library_dp ()) 
-    (if sec then Lib.cwd () 
-      else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()))
-    
-let dump_definition (loc, id) sec s =
-  Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) 
-			(string_of_dirpath (current_dirpath sec)) (string_of_id id))
-    
-let dump_reference loc modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-		  (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty)
-
-let dump_constraint ((loc, n), _, _) sec ty =
-  match n with
-    | Name id -> dump_definition (loc, id) sec ty
-    | Anonymous -> ()
-
-let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
-  if !Flags.dump then dump_definition lid false "def";
-  match def with
-  | ProveBody (bl,t) ->   (* local binders, typ *)
-      if Lib.is_modtype () then
-	errorlabstrm "Vernacentries.VernacDefinition"
-	  (str "Proof editing mode not supported in module types")
-      else
-	let hook _ _ = () in
-	start_proof_and_print (local,DefinitionBody Definition)
-                             [Some lid,(bl,t)] hook
-  | DefineBody (bl,red_option,c,typ_opt) ->
-      let red_option = match red_option with
-        | None -> None
-        | Some r -> 
-	    let (evc,env)= Command.get_current_context () in
-	    Some (interp_redexp env evc r) in
-      declare_definition id k bl red_option c typ_opt hook
-
+let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+  if !Flags.dump then Dumpglob.dump_definition lid false "def";
+  (match def with
+    | ProveBody (bl,t) ->   (* local binders, typ *)
+ 	if Lib.is_modtype () then
+ 	  errorlabstrm "Vernacentries.VernacDefinition"
+ 	    (str "Proof editing mode not supported in module types")
+ 	else
+ 	  let hook _ _ = () in
+ 	    start_proof_and_print (local,DefinitionBody Definition) 
+	      [Some lid, (bl,t)] hook
+    | DefineBody (bl,red_option,c,typ_opt) ->
+ 	let red_option = match red_option with
+          | None -> None
+          | Some r -> 
+ 	      let (evc,env)= Command.get_current_context () in
+ 		Some (interp_redexp env evc r) in
+ 	  declare_definition id k bl red_option c typ_opt hook)
+ 	      
 let vernac_start_proof kind l lettop hook =
   if !Flags.dump then
     List.iter (fun (id, _) -> 
       match id with
-      | Some lid -> dump_definition lid false "prf"
-      | None -> ()) l;
+	| Some lid -> Dumpglob.dump_definition lid false "prf"
+	| None -> ()) l;
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
@@ -381,28 +363,28 @@ let vernac_exact_proof c =
   	
 let vernac_assumption kind l nl=
   let global = fst kind = Global in
-  List.iter (fun (is_coe,(idl,c)) -> 
-    if !dump then
-      List.iter (fun lid -> 
-	if global then dump_definition lid false "ax" 
-	else dump_definition lid true "var") idl;
-    declare_assumption idl is_coe kind [] c false false nl) l
-
+    List.iter (fun (is_coe,(idl,c)) -> 
+      if !dump then
+	List.iter (fun lid -> 
+	  if global then Dumpglob.dump_definition lid false "ax" 
+	  else Dumpglob.dump_definition lid true "var") idl;
+      declare_assumption idl is_coe kind [] c false false nl) l
+      
 let vernac_inductive f indl = 
   if !dump then
     List.iter (fun ((lid, _, _, cstrs), _) ->
-      dump_definition lid false"ind";
+      Dumpglob.dump_definition lid false"ind";
       List.iter (fun (_, (lid, _)) ->
-	dump_definition lid false "constr") cstrs)
+	Dumpglob.dump_definition lid false "constr") cstrs)
       indl;
   build_mutual indl f
 
 let vernac_fixpoint l b = 
-  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
+  List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_recursive l b
 
 let vernac_cofixpoint l b =
-  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
+  List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   build_corecursive l b
 
 let vernac_scheme = build_scheme
@@ -413,9 +395,11 @@ let vernac_combined_scheme = build_combined_scheme
 (* Modules            *)
 
 let vernac_import export refl =
-  let import ref = Library.import_module export (qualid_of_reference ref) in
-  List.iter import refl;
-  Lib.add_frozen_state ()
+  let import ref = 
+    Library.import_module export (qualid_of_reference ref)
+  in
+    List.iter import refl;
+    Lib.add_frozen_state ()
 
 let vernac_declare_module export (loc, id) binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
@@ -433,9 +417,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
     Modintern.interp_modtype Modintern.interp_modexpr
     id binders_ast (Some mty_ast_o) None
   in 
-  Modintern.dump_moddef loc mp "mod";
-  if_verbose message ("Module "^ string_of_id id ^" is declared");
-  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+    Dumpglob.dump_moddef loc mp "mod";
+    if_verbose message ("Module "^ string_of_id id ^" is declared");
+    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = 
   (* We check the state of the system (in section, in module type)
@@ -453,7 +437,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
        let mp = Declaremods.start_module Modintern.interp_modtype export
 	 id binders_ast mty_ast_o 
        in
-	 Modintern.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Interactive Module "^ string_of_id id ^" started") ;
          List.iter
@@ -473,7 +457,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o 
        in
-	 Modintern.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Module "^ string_of_id id ^" is defined");
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -481,9 +465,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 
 let vernac_end_module export (loc,id) =
   let mp = Declaremods.end_module id in
-  Modintern.dump_modref loc mp "mod";
-  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
-  Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+    Dumpglob.dump_modref loc mp "mod";
+    if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 
 let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
@@ -499,7 +483,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
        let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
-        Modintern.dump_moddef loc mp "modtype";
+        Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
@@ -509,25 +493,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
          ) argsexport
 	  
     | Some base_mty ->
-       let binders_ast = List.map
-        (fun (export,idl,ty) ->
-          if export <> None then
-           error ("Arguments of a functor definition can be imported only if" ^
-                  " the definition is interactive. Remove the \"Export\" " ^
-                  "and \"Import\" keywords from every functor argument.")
-          else (idl,ty)) binders_ast in
-       let mp = Declaremods.declare_modtype Modintern.interp_modtype 
+	let binders_ast = List.map
+          (fun (export,idl,ty) ->
+            if export <> None then
+              error ("Arguments of a functor definition can be imported only if" ^
+			" the definition is interactive. Remove the \"Export\" " ^
+			"and \"Import\" keywords from every functor argument.")
+            else (idl,ty)) binders_ast in
+	let mp = Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty in
-        Modintern.dump_moddef loc mp "modtype";
-	if_verbose message 
-	  ("Module Type "^ string_of_id id ^" is defined")
+          Dumpglob.dump_moddef loc mp "modtype";
+	  if_verbose message 
+	    ("Module Type "^ string_of_id id ^" is defined")
 
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype id in
-  Modintern.dump_modref loc mp "modtype";
-  if_verbose message 
-    ("Module Type "^ string_of_id id ^" is defined")
+    Dumpglob.dump_modref loc mp "modtype";
+    if_verbose message 
+      ("Module Type "^ string_of_id id ^" is defined")
 
 let vernac_include = function
   | CIMTE mty_ast ->
@@ -544,7 +528,7 @@ let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
-	if !dump then dump_definition lid false "constr"; id in
+	if !dump then Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -553,11 +537,11 @@ let vernac_record struc binders sort nameopt cfs =
     | Sort s -> s
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected") in
-    if !dump then (
-      dump_definition (snd struc) false "rec";
+    if !Flags.dump then (
+      Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun (_, x) ->
 	match x with
-	| AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
+	| AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
     ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
@@ -565,13 +549,13 @@ let vernac_record struc binders sort nameopt cfs =
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
-  if !Flags.dump then dump_definition lid true "sec";
+  if !Flags.dump then Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
 let vernac_end_section (loc, id) = 
   if !Flags.dump then 
-    dump_reference loc 
-      (string_of_dirpath (current_dirpath true)) "<>" "sec";
+    Dumpglob.dump_reference loc 
+      (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section id
 
 let vernac_end_segment lid =
@@ -586,7 +570,9 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  Library.require_library qidl import
+  let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in
+    List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl;
+    Library.require_library qidl import
 
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)
@@ -605,21 +591,21 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 let vernac_class id par ar sup props =
-  if !dump then (
-    dump_definition id false "class";
-    List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props);
+  if !Flags.dump then (
+      Dumpglob.dump_definition id false "class";
+      List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props);
   Classes.new_class id par ar sup props
  
 let vernac_instance glob sup inst props pri =
-  if !dump then dump_constraint inst false "inst";
+  if !Flags.dump then Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if !dump then List.iter (fun x -> dump_constraint x true "var") l;
+  if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
-  if !dump then dump_definition id false "inst";
+  if !Flags.dump then Dumpglob.dump_definition id false "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -754,7 +740,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
-  dump_definition lid false "syndef";
+  Dumpglob.dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
   
 let vernac_declare_implicits local r = function