Improvements on coqdoc by adding more information into .glob

files, about definitions and type of references.
- Add missing location information on fixpoints/cofixpoint in topconstr and
syntactic definitions in vernacentries for correct dumping.
- Dump definition information in vernacentries: defs, constructors,
projections etc...
- Modify coqdoc/index.mll to use this information instead of trying to
scan the file.
- Use the type information in latex output, update coqdoc.sty accordingly.
- Use the hyperref package to do crossrefs between definition and 
  references to coq objects in latex.  

Next step is to test and debug it on bigger developments.

On the side:
- Fix Program Let which was adding a Global definition. 
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.


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

6 files changed, 213 insertions, 62 deletions

diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 2c07b9fc88..d8cc333367 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -8,20 +8,20 @@
 \NeedsTeXFormat{LaTeX2e}
 \ProvidesPackage{coqdoc}[2002/02/11]
 
-% Headings
-\usepackage{fancyhdr}
-\newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
-\newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
-\pagestyle{fancyplain}
+% % Headings
+% \usepackage{fancyhdr}
+% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
+% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
+% \pagestyle{fancyplain}
 
-%BEGIN LATEX
-\headsep 8mm
-\renewcommand{\plainheadrulewidth}{0.4pt}
-\renewcommand{\plainfootrulewidth}{0pt}
-\lhead[\coqdocleftpageheader]{\leftmark}
-\rhead[\leftmark]{\coqdocrightpageheader}
-\cfoot{}
-%END LATEX
+% %BEGIN LATEX
+% \headsep 8mm
+% \renewcommand{\plainheadrulewidth}{0.4pt}
+% \renewcommand{\plainfootrulewidth}{0pt}
+% \lhead[\coqdocleftpageheader]{\leftmark}
+% \rhead[\leftmark]{\coqdocrightpageheader}
+% \cfoot{}
+% %END LATEX
 
 % Hevea puts to much space with \medskip and \bigskip
 %HEVEA\renewcommand{\medskip}{}
@@ -36,11 +36,20 @@
 %END LATEX
 
 % macro for typesetting keywords
-\newcommand{\coqdockw}[1]{\textsf{#1}}
+\newcommand{\coqdockw}[1]{\texttt{#1}}
 
-% macro for typesetting identifiers
+% macro for typesetting variable identifiers
 \newcommand{\coqdocid}[1]{\textit{#1}}
 
+% macro for typesetting constant identifiers
+\newcommand{\coqdoccst}[1]{\textsf{#1}}
+
+% macro for typesetting inductive type identifiers
+\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}
+
+% macro for typesetting constructor identifiers
+\newcommand{\coqdocconstr}[1]{\textsf{#1}}
+
 % newline and indentation 
 %BEGIN LATEX
 \newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
@@ -53,6 +62,52 @@
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 
+\usepackage{hyperref}
+%\usepackage{color}
+%\hypersetup{colorlinks=true,linkcolor=black}
+%\usepackage{multind}
+%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
+
+\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}}
+\newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
+
+\newcommand{\coqdocvar}[1]{{\textit{#1}}}
+\newcommand{\coqdoctac}[1]{{\texttt{#1}}}
+
+\newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
+
+\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+
+\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
+\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}
+
+\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
 %HEVEA\newcommand{\lor}{\coqwkw{or}}
 %HEVEA\newcommand{\land}{\&}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 1af3945708..9f0c3d24a9 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -19,13 +19,22 @@ type entry_type =
   | Inductive
   | Constructor
   | Lemma
+  | Record
+  | Projection
+  | Instance
+  | Class
+  | Method
   | Variable
   | Axiom
   | TacticDefinition
+  | Abbreviation
+  | Notation
+
+val type_name : entry_type -> string
 
 type index_entry = 
   | Def of string * entry_type
-  | Ref of coq_module * string
+  | Ref of coq_module * string * entry_type
   | Mod of coq_module * string
 
 val find : coq_module -> loc -> index_entry
@@ -42,7 +51,7 @@ val scan_file : string -> coq_module -> unit
 
 (*s Read globalizations from a file (produced by coqc -dump-glob) *)
 
-val read_glob : string -> unit
+val read_glob : string -> coq_module
 
 (*s Indexes *)
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 9bb7bd4002..fa619a9434 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -25,13 +26,20 @@ type entry_type =
   | Inductive
   | Constructor
   | Lemma
+  | Record
+  | Projection
+  | Instance
+  | Class
+  | Method
   | Variable
   | Axiom
   | TacticDefinition
+  | Abbreviation
+  | Notation
 
 type index_entry = 
   | Def of string * entry_type
-  | Ref of coq_module * string
+  | Ref of coq_module * string * entry_type
   | Mod of coq_module * string
 
 let current_type = ref Library
@@ -43,13 +51,13 @@ let table = Hashtbl.create 97
 
 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))
+let add_ref m loc m' id ty = 
+  Hashtbl.add table (m, loc) (Ref (m', id, ty))
 
 let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
 
-
 (*s Manipulating path prefixes *) 
 
 type stack = string list 
@@ -173,9 +181,16 @@ let type_name = function
   | 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"
       
 let all_entries () =
   let gl = ref [] in
@@ -390,7 +405,26 @@ and module_refs = parse
       { () }
 
 {
-  
+  let type_of_string = function
+    | "def" | "coe" | "subclass" | "canonstruc" 
+    | "ex" | "scheme" -> Definition
+    | "prf" | "thm" -> Lemma
+    | "ind" | "coind" -> Inductive
+    | "constr" -> Constructor
+    | "rec" | "corec" -> Record
+    | "proj" -> Projection
+    | "class" -> Class
+    | "meth" -> Method
+    | "inst" -> Instance
+    | "var" -> Variable
+    | "ax" -> Axiom
+    | "syndef" -> Abbreviation
+    | "not" -> Notation
+    | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+(*   | Library *)
+(*   | Module *)
+(*   | TacticDefinition *)
+
   let read_glob f = 
     let c = open_in f in
     let cur_mod = ref "" in
@@ -401,22 +435,22 @@ and module_refs = parse
 	if n > 0 then begin
 	  match s.[0] with
 	    | 'F' -> 
-		cur_mod := String.sub s 1 (n - 1)
+		cur_mod := String.sub s 1 (n - 1);
+		current_library := !cur_mod
 	    | '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 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 -> 
-		   ())
-	    | _ -> ()
+		    Scanf.sscanf s "R%d %s %s %s"
+		      (fun loc lib_dp full_id ty ->
+			add_ref !cur_mod loc lib_dp full_id (type_of_string ty))
+		  with _ -> ())
+	    | _ -> 
+		try Scanf.sscanf s "%s %d %s"
+		  (fun ty loc id -> add_def loc (type_of_string ty) id)
+		with Scanf.Scan_failure _ -> ()
 	end
-      done
+      done; assert false
     with End_of_file -> 
-      close_in c
+      close_in c; !cur_mod
 	
   let scan_file f m = 
     init_stack (); current_library := m;
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 469db5367c..7466a6ba19 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -408,14 +409,16 @@ let gen_mult_files l =
     end 
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
-let read_glob = function
-  | Vernac_file (f,m) ->   
-      let glob = (Filename.chop_extension f) ^ ".glob" in
-	(try
-	  Index.read_glob glob
-	with 
-	    _ -> eprintf "Warning: file %s cannot be opened; links will not be available\n" glob)
-  | Latex_file _ -> ()
+let read_glob x =
+  match x with
+    | Vernac_file (f,m) ->   
+	let glob = (Filename.chop_extension f) ^ ".glob" in
+	  (try
+	      Vernac_file (f, Index.read_glob glob)
+	    with _ -> 
+	      eprintf "Warning: file %s cannot be opened; links will not be available\n" glob;
+	      x)
+  | Latex_file _ -> x
 
 let index_module = function
   | Vernac_file (f,m) ->   
@@ -426,14 +429,14 @@ let produce_document l =
   (if !target_language=HTML then
     let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
-      copy src dst;
-      List.iter read_glob l);
+      copy src dst);
   (if !target_language=LaTeX then
       let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
       let dst = if !output_dir <> "" then 
 	  Filename.concat !output_dir "coqdoc.sty" 
 	else "coqdoc.sty" in
 	copy src dst);
+  let l = List.map read_glob l in
   List.iter index_module l;
   match !out_to with
     | StdOut -> 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index fd8768fdf1..251fb23571 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -46,7 +47,7 @@ let is_keyword =
       "Delimit"; "Bind"; "Open"; "Scope";
       "Boxed"; "Unboxed";
       "Arguments";
-      "Instance"; "Class"; "where"; "Instantiation";
+      "Instance"; "Class"; "Instantiation";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -59,6 +60,15 @@ let is_keyword =
 	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
        ]
 
+let is_tactic = 
+  build_table
+    [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
+      "destruct"; "induction"; "elim"; "dependent"; 
+      "generalize"; "clear"; "rename"; "move"; "set"; "assert";
+      "cut"; "assumption"; "exact";
+      "unfold"; "red"; "compute"; "at"; "in"; "by";
+      "reflexivity"; "symmetry"; "transitivity" ]
+
 (*s Current Coq module *)
 
 let current_module = ref ""
@@ -159,6 +169,12 @@ module Latex = struct
     | _ -> 
 	output_char c
 
+  let label_char c = match c with
+    | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
+    | '^' | '~' -> ()
+    | _ -> 
+	output_char c
+
   let latex_char = output_char
   let latex_string = output_string
 
@@ -168,6 +184,9 @@ module Latex = struct
   let raw_ident s =
     for i = 0 to String.length s - 1 do char s.[i] done
 
+  let label_ident s =
+    for i = 0 to String.length s - 1 do label_char s.[i] done
+
   let start_module () = 
     if not !short then begin
       printf "\\coqdocmodule{"; 
@@ -198,11 +217,52 @@ module Latex = struct
     with Not_found -> 
       f tok
 
-  let ident s _ = 
+  let module_ref m s = 
+    printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
+      (*i
+    match find_module m with
+    | Local ->
+	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    | Coqlib | Unknown ->
+	raw_ident s
+    i*)
+
+  let ident_ref m fid typ s = 
+    match find_module m with
+      | Local ->
+	  printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+      | Coqlib when !externals ->
+	  let _m = Filename.concat !coqlib m in
+	    printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+      | Coqlib | Unknown ->
+	  raw_ident s
+
+  let defref m id ty s =
+    printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
+
+  let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
+    end else if is_tactic s then begin
+      printf "\\coqdoctac{"; raw_ident s; printf "}"
     end else begin
-      printf "\\coqdocid{"; raw_ident s; printf "}"
+      begin
+	try
+	  (match Index.find !current_module loc with
+	     | Def (fullid,typ) -> 
+		 defref !current_module fullid typ s
+             | Mod (m,s') when s = s' ->
+		 module_ref m s
+	     | Ref (m,fullid,typ) -> 
+		 ident_ref m fullid typ s
+	     | Mod _ ->
+		 printf "\\coqdocid{"; raw_ident s; printf "}")
+	with Not_found ->
+	  printf "\\coqdocvar{"; raw_ident s; printf "}"
+      end
     end
 
   let ident s l = with_latex_printing (fun s -> ident s l) s
@@ -387,7 +447,7 @@ module Html = struct
 		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
              | Mod (m,s') when s = s' ->
 		 module_ref m s
-	     | Ref (m,fullid) -> 
+	     | Ref (m,fullid,ty) -> 
 		 ident_ref m fullid s
 	     | Mod _ ->
 		 raw_ident s)
@@ -456,17 +516,6 @@ module Html = struct
 
   let rule () = printf "<hr/>\n"
 
-  let entry_type = function
-    | Library -> "library"
-    | Module -> "module"
-    | Definition -> "definition"
-    | Inductive -> "inductive"
-    | Constructor -> "constructor"
-    | Lemma -> "lemma"
-    | Variable -> "variable"
-    | Axiom -> "axiom"
-    | TacticDefinition -> "tactic definition"
-
   (* make a HTML index from a list of triples (name,text,link) *)
   let index_ref i c =
     let idxc = sprintf "%s_%c" i.idx_name c in
@@ -492,7 +541,7 @@ module Html = struct
 	 if t = Library then 
 	   "[library]", m ^ ".html"
 	 else
-	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
+	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
 	 sprintf "%s.html#%s" m s)
 
   let format_bytype_index = function
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 8774d9d2e4..2e0f46795a 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -173,6 +173,7 @@ let firstchar =
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
+  '\206' ['\177'-'\183'] |
   '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
 let identchar = 
   firstchar | ['\'' '0'-'9' '@' ]
@@ -188,6 +189,7 @@ let symbolchar_no_brackets =
   (* utf-8 symbols *) 
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
 let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token_no_brackets = symbolchar_no_brackets+
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
 let printing_token = (token | id)+
 
@@ -608,7 +610,7 @@ and body = parse
   | eof { false }
   | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
   | '.' space+ { Output.char '.'; Output.char ' '; false }
-  | '"' { Output.char '"'; notation lexbuf; body lexbuf }
+  | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(*" { let eol = comment lexbuf in 
 	     if eol 
 	     then begin Output.line_break(); body_bol lexbuf end
@@ -617,7 +619,7 @@ and body = parse
       { let s = lexeme lexbuf in 
 	  Output.ident s (lexeme_start lexbuf); 
 	  body lexbuf }
-  | printing_token
+  | token_no_brackets
       { let s = lexeme lexbuf in
 	  Output.symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
@@ -659,7 +661,6 @@ and printing_token_body = parse
 
   let coq_file f m =
     reset ();
-    Index.scan_file f m;
     Output.start_module ();
     let c = open_in f in
     let lb = from_channel c in