summaryrefslogtreecommitdiff
path: root/interp/dumpglob.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/dumpglob.ml')
-rw-r--r--interp/dumpglob.ml114
1 files changed, 51 insertions, 63 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 5ac584a7..702c509d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dumpglob.ml 11582 2008-11-12 19:49:57Z notin $ *)
+(* $Id$ *)
(* Dump of globalization (to be used by coqdoc) *)
@@ -15,11 +15,11 @@ let glob_file = ref Pervasives.stdout
let open_glob_file f =
glob_file := Pervasives.open_out f
-
+
let close_glob_file () =
Pervasives.close_out !glob_file
-type glob_output_t =
+type glob_output_t =
| NoGlob
| StdOut
| MultFiles
@@ -39,7 +39,7 @@ let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
-let dump_string s =
+let dump_string s =
if dump () then Pervasives.output_string !glob_file s
@@ -47,28 +47,15 @@ let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state
+type coqdoc_state = Lexer.location_table
-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
+let coqdoc_freeze = Lexer.location_table
+let coqdoc_unfreeze = Lexer.restore_location_table
open Decl_kinds
let type_of_logical_kind = function
- | IsDefinition def ->
+ | IsDefinition def ->
(match def with
| Definition -> "def"
| Coercion -> "coe"
@@ -102,7 +89,7 @@ let type_of_global_ref gr =
"class"
else
match gr with
- | Libnames.ConstRef cst ->
+ | Libnames.ConstRef cst ->
type_of_logical_kind (Decls.constant_kind cst)
| Libnames.VarRef v ->
"var" ^ type_of_logical_kind (Decls.variable_kind v)
@@ -118,13 +105,13 @@ let type_of_global_ref gr =
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 ())
+ Libnames.pop_dirpath_n (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"
+ 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 =
@@ -137,41 +124,31 @@ let add_glob_gen loc sp lib_dp ty =
let ident = Names.string_of_id id in
dump_ref loc filepath modpath ident ty
-let add_glob loc ref =
+let add_glob loc ref =
if dump () && loc <> Util.dummy_loc then
- let sp = Nametab.sp_of_global ref in
+ let sp = Nametab.path_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 mp_of_kn kn =
- let mp,sec,l = Names.repr_kn kn in
- Names.MPdot (mp,l)
+
+let mp_of_kn kn =
+ let mp,sec,l = Names.repr_kn kn in
+ Names.MPdot (mp,l)
let add_glob_kn loc kn =
if dump () && loc <> Util.dummy_loc then
- let sp = Nametab.sp_of_syntactic_definition kn in
+ let sp = Nametab.path_of_syndef kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen loc sp lib_dp "syndef"
-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 = ()
-
+
let dump_definition (loc, id) sec s =
- dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+ 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"
+ 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 =
@@ -187,7 +164,7 @@ let dump_name (loc, n) sec ty =
let dump_local_binder b sec ty =
if dump () then
match b with
- | Topconstr.LocalRawAssum (nl, _, _) ->
+ | Topconstr.LocalRawAssum (nl, _, _) ->
List.iter (fun x -> dump_name x sec ty) nl
| Topconstr.LocalRawDef _ -> ()
@@ -197,7 +174,7 @@ let dump_modref loc mp ty =
let l = if l = [] then l else Util.list_drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) fp mp "<>" ty)
let dump_moddef loc mp ty =
@@ -207,22 +184,33 @@ let dump_moddef loc mp ty =
dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
let dump_libref loc dp ty =
- dump_string (Printf.sprintf "R%d %s <> <> %s\n"
+ dump_string (Printf.sprintf "R%d %s <> <> %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
-let dump_notation_location pos ((path,df),sc) =
+let cook_notation df sc =
+ let ntn = String.make (String.length df * 3) '_' in
+ let j = ref 0 in
+ let quoted = ref false in
+ for i = 0 to String.length df - 1 do
+ if df.[i] = '\'' then quoted := not !quoted;
+ if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
+ if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
+ if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
+ (ntn.[!j] <- df.[i]; incr j)
+ done;
+ let df = String.sub ntn 0 !j in
+ match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+
+let dump_notation (loc,(df,_)) sc sec =
+ (* We dump the location of the opening '"' *)
+ dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
+ (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+
+let dump_notation_location posl df (((path,secpath),_),sc) =
if dump () then
- 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 | _ -> "" in
- dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
-
-
+ let path = Names.string_of_dirpath path in
+ let secpath = Names.string_of_dirpath secpath in
+ let df = cook_notation df sc in
+ List.iter (fun (bl,el) ->
+ dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
+ posl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 18:40:27 +0000