Merge branch 'experimental/upstream' into upstream

1 files changed, 217 insertions, 75 deletions

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index eefcfd11..0dc86bc8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 open Index
 
@@ -32,24 +29,27 @@ let build_table l =
 
 let is_keyword =
   build_table
-    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+    [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
-      "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+      "Guarded"; "Goal"; "Hint"; "Debug"; "On";
       "Hypothesis"; "Hypotheses";
-      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+      "Implicit"; "Import"; "Inductive";
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
-      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
+      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+      "Search"; "SearchAbout"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed"; "Inline";
+      "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal";
-      "Opaque"; "Transparent";
+      "subgoal"; "subgoals"; "vm_compute";
+      "Opaque"; "Transparent"; "Time";
+      "Extraction"; "Extract";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -57,14 +57,20 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      (* Notations *)
+      "level"; "associativity"; "no"
        ]
 
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite";
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
       "set"; "assert"; "do"; "repeat";
@@ -73,8 +79,10 @@ let is_tactic =
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
       "pattern"; "intuition"; "congruence"; "fail"; "fresh";
-      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+      "trivial"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+      "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+      "eval"; "instantiate"; "until" ]
 
 (*s Current Coq module *)
 
@@ -118,9 +126,12 @@ let initialize_texmacs () =
 
 let token_tree_texmacs = ref (initialize_texmacs ())
 
+let token_tree_latex = ref Tokens.empty_ttree
+let token_tree_html = ref Tokens.empty_ttree
+
 let initialize_tex_html () =
   let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
-    List.fold_right (fun (s,l,l') (tt,tt') ->
+  let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
       (Tokens.ttree_add tt s l,
        match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
       [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
@@ -143,10 +154,9 @@ let initialize_tex_html () =
 	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
 	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
-      ] (Tokens.empty_ttree,Tokens.empty_ttree)
-
-let token_tree_latex = ref (fst (initialize_tex_html ()))
-let token_tree_html = ref (snd (initialize_tex_html ()))
+      ] (Tokens.empty_ttree,Tokens.empty_ttree) in
+  token_tree_latex := tree_latex;
+  token_tree_html  := tree_html
 
 let add_printing_token s (t1,t2) =
   (match t1 with None -> () | Some t1 ->
@@ -182,10 +192,20 @@ module Latex = struct
 
   let push_in_preamble s = Queue.add s preamble
 
+  let utf8x_extra_support () =
+    printf "\n";
+    printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
+    printf "%%interpret utf8 characters but extra packages might have to be added\n";
+    printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
+    printf "%%Use coqdoc's option -p to add new packages.\n";
+    printf "\\usepackage{tipa}\n";
+    printf "\n"
+
   let header () =
     if !header_trailer then begin
       printf "\\documentclass[12pt]{report}\n";
       if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+      if !inputenc = "utf8x" then utf8x_extra_support ();
       printf "\\usepackage[T1]{fontenc}\n";
       printf "\\usepackage{fullpage}\n";
       printf "\\usepackage{coqdoc}\n";
@@ -255,6 +275,12 @@ module Latex = struct
 	| '^' | '~' as c ->
 	    Buffer.add_char buff '\\'; Buffer.add_char buff c;
 	    Buffer.add_string buff "{}"
+        | '\'' ->
+            if i < String.length s - 1 && s.[i+1] = '\'' then begin
+              Buffer.add_char buff '\''; Buffer.add_char buff '{';
+              Buffer.add_char buff '}'
+            end else
+              Buffer.add_char buff '\''
 	| c ->
 	    Buffer.add_char buff c
       done;
@@ -276,9 +302,23 @@ module Latex = struct
 
   let stop_latex_math () = output_char '$'
 
-  let start_verbatim () = printf "\\begin{verbatim}"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
+    
+  let start_verbatim inline = 
+    if inline then printf "\\texttt{"
+    else printf "\\begin{verbatim}"
 
-  let stop_verbatim () = printf "\\end{verbatim}\n"
+  let stop_verbatim inline =
+    if inline then printf "}"
+    else printf "\\end{verbatim}\n"
+
+  let url addr name = 
+    printf "%s\\footnote{\\url{%s}}"
+      (match name with
+       | None -> ""
+       | Some n -> n)
+      addr
 
   let indentation n =
     if n == 0 then
@@ -287,9 +327,6 @@ module Latex = struct
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
 
-  let module_ref m s =
-    printf "\\coqdocmodule{%s}{%s}" m (escaped s)
-
   let ident_ref m fid typ s =
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
@@ -306,18 +343,20 @@ module Latex = struct
 	  printf "\\coqdoc%s{%s}" (type_name typ) s
 
   let defref m id ty s =
-    printf "\\coqdef{"; label_ident (m ^ "." ^ id);
-    printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s
+    if ty <> Notation then
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s)
+    else
+      (* Glob file still not able to say the exact extent of the definition *)
+      (* so we currently renounce to highlight the notation location *)
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{%s}" s s)
 
   let reference s = function
     | Def (fullid,typ) ->
 	defref (get_module false) 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 "\\coqdocvar{%s}" (escaped s)
 
   (*s The sublexer buffers symbol characters and attached
        uninterpreted ident and try to apply special translation such as,
@@ -330,13 +369,22 @@ module Latex = struct
     | Some ref -> reference s ref
     | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
 
+  let last_was_in = ref false
+
   let sublexer c loc =
-    let tag =
-      try Some (Index.find (get_module false) loc) with Not_found -> None
-    in
-    Tokens.output_tagged_symbol_char tag c
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else begin
+      let tag =
+        try Some (Index.find (get_module false) loc) with Not_found -> None
+      in
+      Tokens.output_tagged_symbol_char tag c
+    end;
+    last_was_in := false
 
   let initialize () =
+    initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
     Tokens.outfun := output_sublexer_string
 
@@ -345,7 +393,11 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "\\coqdockw{%s}" (translate s)
+
   let ident s loc =
+    last_was_in := s = "in";
     try
       let tag = Index.find (get_module false) loc in
       reference (translate s) tag
@@ -478,8 +530,7 @@ module Html = struct
 	end
 
   let trailer () =
-    if !header_trailer then
-      if !footer_file_spec then
+    if !header_trailer && !footer_file_spec then
 	let cin = Pervasives.open_in !footer_file in
 	  try
 	    while true do
@@ -487,14 +538,14 @@ module Html = struct
 		printf "%s\n" s
 	    done
 	  with End_of_file -> Pervasives.close_in cin
-      else
-	begin
-	  if !index && (get_module false) <> "Index" then
-	    printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
-	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
-	  printf "</div>\n\n</div>\n\n</body>\n</html>"
-	end
+    else
+      begin
+        if !index && (get_module false) <> "Index" then
+          printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+	printf "<hr/>This page has been generated by ";
+	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+	printf "</div>\n\n</div>\n\n</body>\n</html>"
+      end
 
   let start_module () =
     let ln = !lib_name in
@@ -547,17 +598,22 @@ module Html = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = printf "<pre>"
-  let stop_verbatim () = printf "</pre>\n"
+  let start_quote () = char '"'
+  let stop_quote () = start_quote ()
 
-  let module_ref m s =
-    match find_module m with
-      | Local ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External m when !externals ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External _ | Unknown ->
-	  output_string s
+  let start_verbatim inline = 
+    if inline then printf "<tt>"
+    else printf "<pre>"
+
+  let stop_verbatim inline = 
+    if inline then printf "</tt>" 
+    else printf "</pre>\n"
+
+  let url addr name = 
+    printf "<a href=\"%s\">%s</a>" addr 
+      (match name with
+       | Some n -> n
+       | None -> addr)
 
   let ident_ref m fid typ s =
     match find_module m with
@@ -575,12 +631,8 @@ module Html = struct
     | Def (fullid,ty) ->
 	printf "<a name=\"%s\">" fullid;
 	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
-    | Mod _ ->
-	printf "<span class=\"id\" type=\"mod\">%s</span>" s
 
   let output_sublexer_string doescape issymbchar tag s =
     let s = if doescape then escaped s else s in
@@ -597,12 +649,16 @@ module Html = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
+    initialize_tex_html();
     Tokens.token_tree := token_tree_html;
     Tokens.outfun := output_sublexer_string
 
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+
   let ident s loc =
     if is_keyword s then begin
       printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -624,7 +680,7 @@ module Html = struct
 
   let rec reach_item_level n =
     if !item_level < n then begin
-      printf "<ul>\n<li>"; incr item_level;
+      printf "<ul class=\"doclist\">\n<li>"; incr item_level;
       reach_item_level n
     end else if !item_level > n then begin
       printf "\n</li>\n</ul>\n"; decr item_level;
@@ -662,7 +718,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<span class=\"inlinecode\">"
+  let start_inline_coq () = 
+    if !inline_notmono then printf "<span class=\"inlinecodenm\">"
+                       else printf "<span class=\"inlinecode\">"
 
   let end_inline_coq () = printf "</span>"
 
@@ -670,7 +728,50 @@ module Html = struct
 
   let end_inline_coq_block () = end_inline_coq ()
 
-  let paragraph () = printf "\n<br/> <br/>\n"
+  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" 
+
+  (* inference rules *)
+  let inf_rule assumptions (_,_,midnm) conclusions =
+    (* this first function replaces any occurance of 3 or more spaces
+       in a row with "&nbsp;"s.  We do this to the assumptions so that
+       people can put multiple rules on a line with nice formatting *)
+    let replace_spaces str =
+      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in 
+      let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
+      let strs = List.map (fun r -> match r with
+                                    | Str.Text s  -> [s]
+                                    | Str.Delim s -> 
+                                        copy "&nbsp;" (String.length s))  
+                          results
+      in
+        String.concat "" (List.concat strs)
+    in
+    let start_assumption line =
+          (printf "<tr class=\"infruleassumption\">\n";
+           printf "  <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in
+    let end_assumption () =
+          (printf "  <td></td>\n";
+           printf "</td>\n") in
+    let rec print_assumptions hyps = 
+          match hyps with
+          | []                 -> start_assumption "&nbsp;&nbsp;"
+          | [(_,hyp)]          -> start_assumption hyp
+          | ((_,hyp) :: hyps') -> (start_assumption hyp;
+                                   end_assumption ();
+                                   print_assumptions hyps') in
+    printf "<center><table class=\"infrule\">\n";
+    print_assumptions assumptions;
+    printf "  <td class=\"infrulenamecol\" rowspan=\"3\">\n";
+    (match midnm with
+     | None   -> printf "    &nbsp;\n  </td>" 
+     | Some s -> printf "    %s &nbsp;\n  </td>" s);
+    printf "</tr>\n";
+    printf "<tr class=\"infrulemiddle\">\n";
+    printf "  <td class=\"infrule\"><hr /></td>\n";
+    printf "</tr>\n";
+    print_assumptions conclusions;
+    end_assumption ();
+    printf "</table></center>"
 
   let section lev f =
     let lab = new_label () in
@@ -858,19 +959,28 @@ module TeXmacs = struct
 
   let stop_latex_math () = output_char '>'
 
-  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+  let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+  let stop_verbatim inline = in_doc := false; printf "</verbatim>"
+
+  let url addr name = 
+    printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+      (match name with
+       | None -> ""
+       | Some n -> n)
 
-  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
 
   let indentation n = ()
 
+  let keyword s =
+    printf "<kw|"; raw_ident s; printf ">"
+
   let ident_true s =
-    if is_keyword s then begin
-      printf "<kw|"; raw_ident s; printf ">"
-    end else begin
-      raw_ident s
-    end
+    if is_keyword s then keyword s
+    else raw_ident s
 
+  let keyword s loc = keyword s
   let ident s _ = if !in_doc then ident_true s else raw_ident s
 
   let output_sublexer_string doescape issymbchar tag s =
@@ -985,13 +1095,21 @@ module Raw = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = ()
+  let start_verbatim inline = ()
+  let stop_verbatim inline = ()
 
-  let stop_verbatim () = ()
+  let url addr name = 
+    match name with
+    | Some n -> printf "%s (%s)" n addr
+    | None -> printf "%s" addr
+
+  let start_quote () = printf "\""
+  let stop_quote () = printf "\""
 
   let indentation n =
       for i = 1 to n do printf " " done
 
+  let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
@@ -1105,6 +1223,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
 let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 let char = select Latex.char Html.char TeXmacs.char Raw.char
+let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
@@ -1132,10 +1251,33 @@ let start_verbatim =
   select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
 let stop_verbatim =
   select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
-  select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+  select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let url = 
+  select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+  select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+  select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
+  start_verbatim false;
+  let dumb_line = 
+       function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
+                            char '\n')
+  in 
+    (List.iter dumb_line assumptions;
+     dumb_line (midsp, midln ^ (match midnm with 
+                                | Some s -> " " ^ s 
+                                | None -> ""));
+     List.iter dumb_line conclusions);
+  stop_verbatim false
+
+let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
+
 let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
 let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
 let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc