summaryrefslogtreecommitdiff
path: root/tools/coqdoc/index.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/index.mll')
-rw-r--r--tools/coqdoc/index.mll197
1 files changed, 141 insertions, 56 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ec89da2f..9b5716ff 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*)
{
@@ -34,11 +34,14 @@ type index_entry =
| Ref of coq_module * string
| Mod of coq_module * string
-let table = Hashtbl.create 97
+let current_type = ref Library
+let current_library = ref ""
+ (** referes to the file being parsed *)
-let current_module = ref ""
+let table = Hashtbl.create 97
+ (** [table] is used to store references and definitions *)
-let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty))
+let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
@@ -46,7 +49,55 @@ let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
let find m l = Hashtbl.find table (m, l)
-let current_type = ref Library
+
+(*s Manipulating path prefixes *)
+
+type stack = string list
+
+let rec string_of_stack st =
+ match st with
+ | [] -> ""
+ | x::[] -> x
+ | x::tl -> (string_of_stack tl) ^ "." ^ x
+
+let empty_stack = []
+
+let module_stack = ref empty_stack
+let section_stack = ref empty_stack
+
+let init_stack () =
+ module_stack := empty_stack; section_stack := empty_stack
+
+let push st p = st := p::!st
+let pop st =
+ match !st with
+ | [] -> ()
+ | _::tl -> st := tl
+
+let head st =
+ match st with
+ | [] -> ""
+ | x::_ -> x
+
+let begin_module m = push module_stack m
+let begin_section s = push section_stack s
+
+let end_block id =
+ (** determines if it ends a module or a section and pops the stack *)
+ if ((String.compare (head !module_stack) id ) == 0) then
+ pop module_stack
+ else if ((String.compare (head !section_stack) id) == 0) then
+ pop section_stack
+ else
+ ()
+
+let make_fullid id =
+ (** prepends the current module path to an id *)
+ let path = string_of_stack !module_stack in
+ if String.length path > 0 then
+ path ^ "." ^ id
+ else
+ id
(* Coq modules *)
@@ -83,7 +134,7 @@ let ref_module loc s =
let n = String.length s in
let i = String.rindex s ' ' in
let id = String.sub s (i+1) (n-i-1) in
- add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id
+ add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id
with Not_found ->
()
@@ -104,25 +155,25 @@ let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
let sort_entries el =
let t = Hashtbl.create 97 in
- List.iter
- (fun c -> Hashtbl.add t c [])
- ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N';
- 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];
- List.iter
- (fun ((s,_) as e) ->
- let c = Alpha.norm_char s.[0] in
- let l = try Hashtbl.find t c with Not_found -> [] in
- Hashtbl.replace t c (e :: l))
- el;
- let res = ref [] in
- Hashtbl.iter
- (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
- List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
-
+ List.iter
+ (fun c -> Hashtbl.add t c [])
+ ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N';
+ 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];
+ List.iter
+ (fun ((s,_) as e) ->
+ let c = Alpha.norm_char s.[0] in
+ let l = try Hashtbl.find t c with Not_found -> [] in
+ Hashtbl.replace t c (e :: l))
+ el;
+ let res = ref [] in
+ Hashtbl.iter
+ (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
+ List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
+
let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
+
let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
+
let type_name = function
| Library -> "library"
| Module -> "module"
@@ -133,28 +184,28 @@ let type_name = function
| Variable -> "variable"
| Axiom -> "axiom"
| TacticDefinition -> "tactic"
-
+
let all_entries () =
let gl = ref [] in
let add_g s m t = gl := (s,(m,t)) :: !gl in
let bt = Hashtbl.create 11 in
let add_bt t s m =
let l = try Hashtbl.find bt t with Not_found -> [] in
- Hashtbl.replace bt t ((s,m) :: l)
+ Hashtbl.replace bt t ((s,m) :: l)
in
let classify (m,_) e = match e with
| Def (s,t) -> add_g s m t; add_bt t s m
| Ref _ | Mod _ -> ()
in
- Hashtbl.iter classify table;
- Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
- { idx_name = "global";
- idx_entries = sort_entries !gl;
- idx_size = List.length !gl },
- Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
+ Hashtbl.iter classify table;
+ Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
+ { idx_name = "global";
+ idx_entries = sort_entries !gl;
+ idx_size = List.length !gl },
+ Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
idx_entries = sort_entries e;
idx_size = List.length e }) :: l) bt []
-
+
}
(*s Shortcuts for regular expressions. *)
@@ -165,15 +216,14 @@ let firstchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
let identchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'
- '\'' '0'-'9']
-let ident =
- firstchar identchar*
+ '\'' '0'-'9']
+let ident = firstchar identchar*
let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
+
(*s Indexing entry point. *)
-
+
rule traverse = parse
| "Definition" space
{ current_type := Definition; index_ident lexbuf; traverse lexbuf }
@@ -192,13 +242,15 @@ rule traverse = parse
| "Record" space
{ current_type := Inductive; index_ident lexbuf; traverse lexbuf }
| "Module" (space+ "Type")? space
- { current_type := Module; index_ident lexbuf; traverse lexbuf }
+ { current_type := Module; module_ident lexbuf; traverse lexbuf }
(*i***
| "Variable" 's'? space
{ current_type := Variable; index_idents lexbuf; traverse lexbuf }
***i*)
| "Require" (space+ ("Export"|"Import"))? space+ ident
{ ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+ | "End" space+
+ { end_ident lexbuf; traverse lexbuf }
| begin_hide
{ skip_hide lexbuf; traverse lexbuf }
| "(*"
@@ -216,7 +268,16 @@ and index_ident = parse
| space+
{ index_ident lexbuf }
| ident
- { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) }
+ { let fullid =
+ let id = lexeme lexbuf in
+ match !current_type with
+ | Definition
+ | Inductive
+ | Constructor
+ | Lemma -> make_fullid id
+ | _ -> id
+ in
+ add_def (lexeme_start lexbuf) !current_type fullid }
| eof
{ () }
| _
@@ -234,12 +295,12 @@ and index_idents = parse
{ () }
| _
{ skip_until_point lexbuf }
-
+
(*s Index identifiers in an inductive definition (types and constructors). *)
-
+
and inductive = parse
| '|' | ":=" space* '|'?
- { current_type := Constructor; index_ident lexbuf; inductive lexbuf }
+ { current_type := Constructor; index_ident lexbuf; inductive lexbuf }
| "with" space
{ current_type := Inductive; index_ident lexbuf; inductive lexbuf }
| '.'
@@ -248,9 +309,9 @@ and inductive = parse
{ () }
| _
{ inductive lexbuf }
-
+
(*s Index identifiers in a Fixpoint declaration. *)
-
+
and fixpoint = parse
| "with" space
{ index_ident lexbuf; fixpoint lexbuf }
@@ -260,9 +321,9 @@ and fixpoint = parse
{ () }
| _
{ fixpoint lexbuf }
-
+
(*s Skip a possibly nested comment. *)
-
+
and comment = parse
| "*)" { () }
| "(*" { comment lexbuf; comment lexbuf }
@@ -271,25 +332,48 @@ and comment = parse
| _ { comment lexbuf }
(*s Skip a constant string. *)
-
+
and string = parse
| '"' { () }
| eof { eprintf " *** Unterminated string while indexing" }
| _ { string lexbuf }
(*s Skip everything until the next dot. *)
-
+
and skip_until_point = parse
| '.' { () }
| eof { () }
| _ { skip_until_point lexbuf }
-
+
(*s Skip everything until [(* end hide *)] *)
and skip_hide = parse
| eof | end_hide { () }
| _ { skip_hide lexbuf }
+and end_ident = parse
+ | space+
+ { end_ident lexbuf }
+ | ident
+ { let id = lexeme lexbuf in end_block id }
+ | eof
+ { () }
+ | _
+ { () }
+
+and module_ident = parse
+ | space+
+ { module_ident lexbuf }
+ | ident space* ":="
+ { () }
+ | ident
+ { let id = lexeme lexbuf in
+ begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+ | eof
+ { () }
+ | _
+ { () }
+
{
let read_glob f =
@@ -306,10 +390,11 @@ and skip_hide = parse
| 'R' ->
(try
let i = String.index s ' ' in
+ let j = String.index_from s (i+1) ' ' in
let loc = int_of_string (String.sub s 1 (i - 1)) in
- let sp = String.sub s (i + 1) (n - i - 1) in
- let m',id = split_sp sp in
- add_ref !cur_mod loc m' id
+ let lib_dp = String.sub s (i + 1) (j - i - 1) in
+ let full_id = String.sub s (j + 1) (n - j - 1) in
+ add_ref !cur_mod loc lib_dp full_id
with Not_found ->
())
| _ -> ()
@@ -317,11 +402,11 @@ and skip_hide = parse
done
with End_of_file ->
close_in c
-
+
let scan_file f m =
- current_module := m;
+ init_stack (); current_library := m;
let c = open_in f in
let lb = from_channel c in
- traverse lb;
- close_in c
+ traverse lb;
+ close_in c
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 18:16:32 +0000