diff options
Diffstat (limited to 'tools/coqdoc/index.mll')
| -rw-r--r-- | tools/coqdoc/index.mll | 490 |
1 files changed, 0 insertions, 490 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll deleted file mode 100644 index f8adb52b..00000000 --- a/tools/coqdoc/index.mll +++ /dev/null @@ -1,490 +0,0 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) -(************************************************************************) -(* 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 *) -(************************************************************************) - -(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*) - -{ - -open Filename -open Lexing -open Printf - -open Cdglobals - -type loc = int - -type entry_type = - | Library - | Module - | Definition - | Inductive - | Constructor - | Lemma - | Record - | Projection - | Instance - | Class - | Method - | Variable - | Axiom - | TacticDefinition - | Abbreviation - | Notation - | Section - -type index_entry = - | Def of string * entry_type - | Ref of coq_module * string * entry_type - | Mod of coq_module * string - -let current_type = ref Library -let current_library = ref "" - (** refers to the file being parsed *) - -(** [deftable] stores only definitions and is used to interpolate idents - inside comments, which are not globalized otherwise. *) - -let deftable = Hashtbl.create 97 - -(** [reftable] stores references and definitions *) -let reftable = Hashtbl.create 97 - -let full_ident sp id = - if sp <> "<>" then - if id <> "<>" then - sp ^ "." ^ id - else sp - else if id <> "<>" - then id - else "" - -let add_def loc ty sp id = - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); - Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty)) - -let add_ref m loc m' sp id ty = - if Hashtbl.mem reftable (m, loc) then () - else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); - let idx = if id = "<>" then m' else id in - if Hashtbl.mem deftable idx then () - else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty)) - -let add_mod m loc m' id = - Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable m (Mod (m', id)) - -let find m l = Hashtbl.find reftable (m, l) - -let find_string m s = Hashtbl.find deftable s - -(*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 *) - -let split_sp s = - try - let i = String.rindex s '.' in - String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1) - with - Not_found -> "", s - -let modules = Hashtbl.create 97 -let local_modules = Hashtbl.create 97 - -let add_module m = - let _,id = split_sp m in - Hashtbl.add modules id m; - Hashtbl.add local_modules m () - -type module_kind = Local | Coqlib | Unknown - -let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq." - -let find_module m = - if Hashtbl.mem local_modules m then - Local - else if coq_module m then - Coqlib - else - Unknown - - -(* Building indexes *) - -type 'a index = { - idx_name : string; - idx_entries : (char * (string * 'a) list) list; - idx_size : int } - -let map f i = - { i with idx_entries = - List.map - (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l)) - i.idx_entries } - -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 - -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" - | Definition -> "definition" - | Inductive -> "inductive" - | Constructor -> "constructor" - | Lemma -> "lemma" - | Record -> "record" - | Projection -> "projection" - | Instance -> "instance" - | Class -> "class" - | Method -> "method" - | Variable -> "variable" - | Axiom -> "axiom" - | TacticDefinition -> "tactic" - | Abbreviation -> "abbreviation" - | Notation -> "notation" - | Section -> "section" - -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) - 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 reftable; - 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. *) -let digit = ['0'-'9'] -let num = digit+ - -let space = - [' ' '\010' '\013' '\009' '\012'] -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 id = firstchar identchar* -let pfx_id = (id '.')* -let ident = id | pfx_id id - -let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" -let end_hide = "(*" space* "end" space+ "hide" space* "*)" - -(*s Indexing entry point. *) - -rule traverse = parse - | ("Program" space+)? "Definition" space - { current_type := Definition; index_ident lexbuf; traverse lexbuf } - | "Tactic" space+ "Definition" space - { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf } - | ("Axiom" | "Parameter") space - { current_type := Axiom; index_ident lexbuf; traverse lexbuf } - | ("Program" space+)? "Fixpoint" space - { current_type := Definition; index_ident lexbuf; fixpoint lexbuf; - traverse lexbuf } - | ("Program" space+)? ("Lemma" | "Theorem") space - { current_type := Lemma; index_ident lexbuf; traverse lexbuf } - | "Obligation" space num ("of" ident)? - { current_type := Lemma; index_ident lexbuf; traverse lexbuf } - | "Inductive" space - { current_type := Inductive; - index_ident lexbuf; inductive lexbuf; traverse lexbuf } - | "Record" space - { current_type := Inductive; index_ident lexbuf; traverse lexbuf } - | "Module" (space+ "Type")? space - { 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"))? - { module_refs lexbuf; traverse lexbuf } - | "End" space+ - { end_ident lexbuf; traverse lexbuf } - | begin_hide - { skip_hide lexbuf; traverse lexbuf } - | "(*" - { comment lexbuf; traverse lexbuf } - | '"' - { string lexbuf; traverse lexbuf } - | eof - { () } - | _ - { traverse lexbuf } - -(*s Index one identifier. *) - -and index_ident = parse - | space+ - { index_ident lexbuf } - | ident - { 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 - { () } - | _ - { () } - -(*s Index identifiers separated by blanks and/or commas. *) - -and index_idents = parse - | space+ | ',' - { index_idents lexbuf } - | ident - { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf); - index_idents lexbuf } - | eof - { () } - | _ - { 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 } - | "with" space - { current_type := Inductive; index_ident lexbuf; inductive lexbuf } - | '.' - { () } - | eof - { () } - | _ - { inductive lexbuf } - -(*s Index identifiers in a Fixpoint declaration. *) - -and fixpoint = parse - | "with" space - { index_ident lexbuf; fixpoint lexbuf } - | '.' - { () } - | eof - { () } - | _ - { fixpoint lexbuf } - -(*s Skip a possibly nested comment. *) - -and comment = parse - | "*)" { () } - | "(*" { comment lexbuf; comment lexbuf } - | '"' { string lexbuf; comment lexbuf } - | eof { eprintf " *** Unterminated comment while indexing" } - | _ { 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 } - | '"' { string lexbuf; module_ident lexbuf } - | ident space* ":=" - { () } - | ident - { let id = lexeme lexbuf in - begin_module id; add_def (lexeme_start lexbuf) !current_type "" id } - | eof - { () } - | _ - { () } - -(*s parse module names *) - -and module_refs = parse - | space+ - { module_refs lexbuf } - | ident - { let id = lexeme lexbuf in - (try - add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id - with - Not_found -> () - ); - module_refs lexbuf } - | eof - { () } - | _ - { () } - -{ - let type_of_string = function - | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" - | "ex" | "scheme" -> Definition - | "prf" | "thm" -> Lemma - | "ind" | "coind" -> Inductive - | "constr" -> Constructor - | "rec" | "corec" -> Record - | "proj" -> Projection - | "class" -> Class - | "meth" -> Method - | "inst" -> Instance - | "var" -> Variable - | "defax" | "prfax" | "ax" -> Axiom - | "syndef" -> Abbreviation - | "not" -> Notation - | "lib" -> Library - | "mod" | "modtype" -> Module - | "tac" -> TacticDefinition - | "sec" -> Section - | s -> raise (Invalid_argument ("type_of_string:" ^ s)) - - let read_glob f = - let c = open_in f in - let cur_mod = ref "" in - try - while true do - let s = input_line c in - let n = String.length s in - if n > 0 then begin - match s.[0] with - | 'F' -> - cur_mod := String.sub s 1 (n - 1); - current_library := !cur_mod - | 'R' -> - (try - Scanf.sscanf s "R%d %s %s %s %s" - (fun loc lib_dp sp id ty -> - add_ref !cur_mod loc lib_dp sp id (type_of_string ty)) - with _ -> ()) - | _ -> - try Scanf.sscanf s "%s %d %s %s" - (fun ty loc sp id -> add_def loc (type_of_string ty) sp id) - with Scanf.Scan_failure _ -> () - end - done; assert false - with End_of_file -> - close_in c; !cur_mod - - let scan_file f m = - init_stack (); current_library := m; - let c = open_in f in - let lb = from_channel c in - traverse lb; - close_in c -} |