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

1 files changed, 220 insertions, 0 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
new file mode 100644
index 0000000000..8cc6371f5e
--- /dev/null
+++ b/interp/dumpglob.ml
@@ -0,0 +1,220 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+let glob_file = ref Pervasives.stdout
+
+let open_glob_file f =
+  glob_file := Pervasives.open_out(f ^ ".glob")
+  
+let close_glob_file () =
+  Pervasives.close_out !glob_file
+
+let dump_string s = 
+  Pervasives.output_string !glob_file s
+
+
+
+(**********************************************************************)
+(* Dump of globalization (to be used by coqdoc)                       *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+  let lt = Lexer.location_table() in
+  let state = (lt,!token_number,!last_pos) in
+    token_number := 0;
+    last_pos := 0;
+    state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+  Lexer.restore_location_table lt;
+  token_number := tn;
+  last_pos := lp
+
+open Decl_kinds
+
+let type_of_logical_kind = function
+  | IsDefinition def -> 
+      (match def with
+      | Definition -> "def"
+      | Coercion -> "coe"
+      | SubClass -> "subclass"
+      | CanonicalStructure -> "canonstruc"
+      | Example -> "ex"
+      | Fixpoint -> "def"
+      | CoFixpoint -> "def"
+      | Scheme -> "scheme"
+      | StructureComponent -> "proj"
+      | IdentityCoercion -> "coe"
+      | Instance -> "inst"
+      | Method -> "meth")
+  | IsAssumption a ->
+      (match a with
+      | Definitional -> "defax"
+      | Logical -> "prfax"
+      | Conjectural -> "prfax")
+  | IsProof th ->
+      (match th with
+      | Theorem
+      | Lemma
+      | Fact
+      | Remark
+      | Property
+      | Proposition
+      | Corollary -> "thm")
+
+let type_of_global_ref gr =
+  if Typeclasses.is_class gr then
+    "class"
+  else
+    match gr with
+    | Libnames.ConstRef cst -> 
+	type_of_logical_kind (Decls.constant_kind cst)
+    | Libnames.VarRef v ->
+	"var" ^ type_of_logical_kind (Decls.variable_kind v)
+    | Libnames.IndRef ind ->
+	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+	  if mib.Declarations.mind_record then
+	    if mib.Declarations.mind_finite then "rec"
+	    else "corec"
+	  else if mib.Declarations.mind_finite then "ind"
+	  else "coind"
+    | Libnames.ConstructRef _ -> "constr"
+
+let remove_sections dir =
+  if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+    (* Not yet (fully) discharged *)
+    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+  else
+    (* Theorem/Lemma outside its outer section of definition *)
+    dir
+
+let dump_ref loc filepath modpath ident ty =
+  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		  (fst (Util.unloc loc)) filepath modpath ident ty)
+
+let add_glob_gen loc sp lib_dp ty =
+  let mod_dp,id = Libnames.repr_path sp in
+  let mod_dp = remove_sections mod_dp in
+  let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+  let filepath = Names.string_of_dirpath lib_dp in
+  let modpath = Names.string_of_dirpath mod_dp_trunc in
+  let ident = Names.string_of_id id in
+    dump_ref loc filepath modpath ident ty
+
+let add_glob loc ref = 
+  let sp = Nametab.sp_of_global ref in
+  let lib_dp = Lib.library_part ref in
+  let ty = type_of_global_ref ref in
+    add_glob_gen loc sp lib_dp ty
+      
+let add_glob loc ref =
+  if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref
+
+let mp_of_kn kn = 
+  let mp,sec,l = Names.repr_kn kn in 
+    Names.MPdot (mp,l) 
+
+let add_glob_kn loc kn =
+  let sp = Nametab.sp_of_syntactic_definition kn in
+  let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
+    add_glob_gen loc sp lib_dp "syndef"
+
+let add_glob_kn loc ref =
+  if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref
+
+let add_local loc id = ()
+(*   let mod_dp,id = repr_path sp in *)
+(*   let mod_dp = remove_sections mod_dp in *)
+(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
+(*   let filepath = string_of_dirpath lib_dp in *)
+(*   let modpath = string_of_dirpath mod_dp_trunc in *)
+(*   let ident = string_of_id id in *)
+(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
+(* 		    (fst (unloc loc)) filepath modpath ident ty) *)
+
+let dump_binding loc id = ()
+      
+(* BEGIN obsolete *)
+
+let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented")
+  
+let dump_def loc ref = 
+  let curr_mp, _ = Lib.current_prefix() in
+  let lib_dp, curr_dp = Lib.split_mp curr_mp in
+  let mod_dp_trunc =  Libnames.drop_dirpath_prefix lib_dp curr_dp in
+
+  let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in
+  let filepath = Names.string_of_dirpath lib_dp in
+    dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname)
+
+(* END obsolete *)
+
+let dump_definition (loc, id) sec s =
+  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) 
+			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
+    
+let dump_reference loc modpath ident ty =
+  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+
+let dump_constraint ((loc, n), _, _) sec ty =
+  match n with
+    | Names.Name id -> dump_definition (loc, id) sec ty
+    | Names.Anonymous -> ()
+
+let dump_modref loc mp ty =
+  if !Flags.dump then
+    let (dp, l) = Lib.split_modpath mp in
+    let fp = Names.string_of_dirpath dp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
+      dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+			    (fst (Util.unloc loc)) fp mp "<>" ty)
+
+let dump_moddef loc mp ty =
+  if !Flags.dump then
+    let (dp, l) = Lib.split_modpath mp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+
+let dump_libref loc dp ty =
+  if !Flags.dump then
+    dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
+			     (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+
+let loc_of_notation f loc args ntn =
+  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
+  else snd (Util.unloc (f (List.hd args)))
+
+let ntn_loc = loc_of_notation Topconstr.constr_loc
+let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc
+
+let dump_notation_location pos ((path,df),sc) =
+  let rec next growing =
+    let loc = Lexer.location_function !token_number in
+    let (bp,_) = Util.unloc loc in
+      if growing then if bp >= pos then loc else (incr token_number; next true)
+      else if bp = pos then loc
+      else if bp > pos then (decr token_number;next false)
+      else (incr token_number;next true) in
+  let loc = next (pos >= !last_pos) in
+    last_pos := pos;
+    let path = Names.string_of_dirpath path in
+    let _sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
+
+