(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Hashtbl.add h key ()) l; function s -> try Hashtbl.find h s; true with Not_found -> false let is_keyword = build_table [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; "CoInductive"; "Defined"; "Definition"; "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Immediate"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Unset"; "Variable"; "Variables"; "Notation"; (* Program *) "Program Definition"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; (*i (* correctness *) "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if"; "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; "while"; i*) (*i (* coq terms *) *) "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=" ] (*s Current Coq module *) let current_module = ref "" let set_module m = current_module := m; page_title := m (*s Common to both LaTeX and HTML *) let item_level = ref 0 (*s Customized pretty-print *) let token_pp = Hashtbl.create 97 let add_printing_token = Hashtbl.replace token_pp let find_printing_token tok = try Hashtbl.find token_pp tok with Not_found -> None, None let remove_printing_token = Hashtbl.remove token_pp (* predefined pretty-prints *) let _ = List.iter (fun (s,l) -> Hashtbl.add token_pp s (Some l, None)) [ "*" , "\\ensuremath{\\times}"; "->", "\\ensuremath{\\rightarrow}"; "->~", "\\ensuremath{\\rightarrow\\lnot}"; "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; "<-", "\\ensuremath{\\leftarrow}"; "<->", "\\ensuremath{\\leftrightarrow}"; "=>", "\\ensuremath{\\Rightarrow}"; "<=", "\\ensuremath{\\le}"; ">=", "\\ensuremath{\\ge}"; "<>", "\\ensuremath{\\not=}"; "~", "\\ensuremath{\\lnot}"; "/\\", "\\ensuremath{\\land}"; "\\/", "\\ensuremath{\\lor}"; "|-", "\\ensuremath{\\vdash}"; "forall", "\\ensuremath{\\forall}"; "exists", "\\ensuremath{\\exists}"; (* "fun", "\\ensuremath{\\lambda}" ? *) ] (*s Table of contents *) type toc_entry = | Toc_library of string | Toc_section of int * (unit -> unit) * string let (toc_q : toc_entry Queue.t) = Queue.create () let add_toc_entry e = Queue.add e toc_q let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r (*s LaTeX output *) module Latex = struct (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () let push_in_preamble s = Queue.add s preamble let header () = if !header_trailer then begin printf "\\documentclass[12pt]{report}\n"; if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; Queue.iter (fun s -> printf "%s\n" s) preamble; printf "\\begin{document}\n" end; output_string "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; output_string "%% This file has been automatically generated with the command\n"; output_string "%% "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf "\n"; output_string "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n" let trailer () = if !header_trailer then begin printf "\\end{document}\n" end let char c = match c with | '\\' -> printf "\\symbol{92}" | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> output_char '\\'; output_char c | '^' | '~' -> output_char '\\'; output_char c; printf "{}" | _ -> output_char c let latex_char = output_char let latex_string = output_string let html_char _ = () let html_string _ = () let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done let start_module () = if not !short then begin printf "\\coqdocmodule{"; raw_ident !current_module; printf "}\n\n" end let start_latex_math () = output_char '$' let stop_latex_math () = output_char '$' let start_verbatim () = printf "\\begin{verbatim}" let stop_verbatim () = printf "\\end{verbatim}\n" let indentation n = if n == 0 then printf "\\noindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space let with_latex_printing f tok = try (match Hashtbl.find token_pp tok with | Some s, _ -> output_string s | _ -> f tok) with Not_found -> f tok let ident s _ = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin printf "\\coqdocid{"; raw_ident s; printf "}" end let ident s l = with_latex_printing (fun s -> ident s l) s let symbol = with_latex_printing raw_ident let rec reach_item_level n = if !item_level < n then begin printf "\n\\begin{itemize}\n\\item "; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n\\end{itemize}\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\\item " let stop_item () = reach_item_level 0 let start_doc () = printf "\n\n\n\\noindent\n" let end_doc () = stop_item (); printf "\n\n\n" let start_coq () = () let end_coq () = () let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () let section_kind = function | 1 -> "\\section{" | 2 -> "\\subsection{" | 3 -> "\\subsubsection{" | 4 -> "\\paragraph{" | _ -> assert false let section lev f = stop_item (); output_string (section_kind lev); f (); printf "}\n\n" let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" let paragraph () = stop_item (); printf "\n\n\\medskip\n" let line_break () = printf "\\coqdoceol\n" let empty_line_of_code () = printf "\n\n\\medskip\n" let start_inline_coq () = () let end_inline_coq () = () let make_multi_index () = () let make_index () = () let make_toc () = printf "\\tableofcontents\n" end (*s HTML output *) module Html = struct let header () = if !header_trailer then begin printf "\n"; printf "\n\n"; printf "\n" !charset; printf "\n"; printf "%s\n\n\n" !page_title; printf "\n\n
\n\n
\n
\n\n"; printf "
\n\n" end let self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then printf "
\n\n
\n
Index"; if !header_trailer then begin printf "
This page has been generated by "; printf "coqdoc\n" self; printf "
\n\n
\n\n\n" end let start_module () = if not !short then begin (* add_toc_entry (Toc_library !current_module); *) printf "

Library %s

\n\n" !current_module end let indentation n = for i = 1 to n do printf " " done let line_break () = printf "
\n" let empty_line_of_code () = printf "\n
\n" let char = function | '<' -> printf "<" | '>' -> printf ">" | '&' -> printf "&" | c -> output_char c let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done let latex_char _ = () let latex_string _ = () let html_char = output_char let html_string = output_string let start_latex_math () = () let stop_latex_math () = () let start_verbatim () = printf "
"
  let stop_verbatim () = printf "
\n" let module_ref m s = printf "" m; raw_ident s; printf "" (*i match find_module m with | Local -> printf "" m; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in printf "" m; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s i*) let ident_ref m fid s = match find_module m with | Local -> printf "" m fid; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in printf "" m fid; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s let ident s loc = if is_keyword s then begin printf ""; raw_ident s; printf "" end else begin try (match Index.find !current_module loc with | Def (fullid,_) -> printf "" fullid; raw_ident s | Mod (m,s') when s = s' -> module_ref m s | Ref (m,fullid) -> ident_ref m fullid s | Mod _ | Ref _ -> raw_ident s) with Not_found -> raw_ident s end let with_html_printing f tok = try (match Hashtbl.find token_pp tok with | _, Some s -> output_string s | _ -> f tok) with Not_found -> f tok let ident s l = with_html_printing (fun s -> ident s l) s let symbol = with_html_printing raw_ident let rec reach_item_level n = if !item_level < n then begin printf "\n\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\n
  • " let stop_item () = reach_item_level 0 let start_coq () = if not !raw_comments then printf "\n" let end_coq () = if not !raw_comments then printf "\n" let start_doc () = if not !raw_comments then printf "\n
    \n" let end_doc () = stop_item (); if not !raw_comments then printf "\n
    \n" let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () let start_inline_coq () = printf "" let end_inline_coq () = printf "" let paragraph () = stop_item (); printf "\n

    \n" let section lev f = let lab = new_label () in let r = sprintf "%s.html#%s" !current_module lab in add_toc_entry (Toc_section (lev, f, r)); stop_item (); printf "" lab lev; f (); printf "\n" lev let rule () = printf "
    \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 if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc let letter_index category idx (c,l) = if l <> [] then begin let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in printf "

    %c %s

    \n" idx c c cat; List.iter (fun (id,(text,link)) -> printf "%s %s
    \n" link id text) l; printf "

    " end let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries (* Construction d'une liste des index (1 index global, puis 1 index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> if t = Library then "[library]", m ^ ".html" else sprintf "[%s, in %s]" (entry_type t) m m , sprintf "%s.html#%s" m s) let format_bytype_index = function | Library, idx -> Index.map (fun id m -> "", m ^ ".html") idx | (t,idx) -> Index.map (fun s m -> let text = sprintf "[in %s]" m m in (text, sprintf "%s.html#%s" m s)) idx (* Impression de la table d'index *) let print_index_table_item i = printf "\n%s Index\n" (String.capitalize i.idx_name); List.iter (fun (c,l) -> if l <> [] then printf "%c\n" (index_ref i c) c else printf "%c\n" c) i.idx_entries; let n = i.idx_size in printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); printf "\n" let print_index_table idxl = printf "\n"; List.iter print_index_table_item idxl; printf "
    \n" let make_one_multi_index prt_tbl i = (* Attn: make_one_multi_index créé un nouveau fichier... *) let idx = i.idx_name in let one_letter ((c,l) as cl) = open_out_file (sprintf "index_%s_%c.html" idx c); if (!header_trailer) then header (); prt_tbl (); printf "
    "; letter_index true idx cl; if List.length l > 30 then begin printf "
    "; prt_tbl () end; if (!header_trailer) then trailer (); close_out_file () in List.iter one_letter i.idx_entries let make_multi_index () = let all_index = let glob,bt = Index.all_entries () in (format_global_index glob) :: (List.map format_bytype_index bt) in let print_table () = print_index_table all_index in List.iter (make_one_multi_index print_table) all_index let make_index () = let all_index = let glob,bt = Index.all_entries () in (format_global_index glob) :: (List.map format_bytype_index bt) in let print_table () = print_index_table all_index in let print_one_index i = if i.idx_size > 0 then begin printf "
    \n

    %s Index

    \n" (String.capitalize i.idx_name); all_letters i end in current_module := "Index"; if !title <> "" then printf "

    %s

    \n" !title; print_table (); if not (!multi_index) then begin List.iter print_one_index all_index; printf "
    "; print_table () end let make_toc () = let make_toc_entry = function | Toc_library m -> stop_item (); printf "

    Library %s

    \n" m m | Toc_section (n, f, r) -> item n; printf "" r; f (); printf "\n" in Queue.iter make_toc_entry toc_q; stop_item (); end (*s TeXmacs-aware output *) module TeXmacs = struct (*s Latex preamble *) let in_doc = ref false let (preamble : string Queue.t) = in_doc := false; Queue.create () let push_in_preamble s = Queue.add s preamble let header () = output_string "(*i This file has been automatically generated with the command \n"; output_string " "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n" let trailer () = () let char_true c = match c with | '\\' -> printf "\\\\" | '<' -> printf "\\<" | '|' -> printf "\\|" | '>' -> printf "\\>" | _ -> output_char c let char c = if !in_doc then char_true c else output_char c let latex_char = char_true let latex_string = String.iter latex_char let html_char _ = () let html_string _ = () let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done let start_module () = () let start_latex_math () = printf "' let start_verbatim () = in_doc := true; printf "<\\verbatim>" let stop_verbatim () = in_doc := false; printf "" let indentation n = () let ident_true s = if is_keyword s then begin printf "" end else begin raw_ident s end let ident s _ = if !in_doc then ident_true s else raw_ident s let symbol_true s = let ensuremath x = printf ">" x in match s with | "*" -> ensuremath "times" | "->" -> ensuremath "rightarrow" | "<-" -> ensuremath "leftarrow" | "<->" ->ensuremath "leftrightarrow" | "=>" -> ensuremath "Rightarrow" | "<=" -> ensuremath "le" | ">=" -> ensuremath "ge" | "<>" -> ensuremath "noteq" | "~" -> ensuremath "lnot" | "/\\" -> ensuremath "land" | "\\/" -> ensuremath "lor" | "|-" -> ensuremath "vdash" | s -> raw_ident s let symbol s = if !in_doc then symbol_true s else raw_ident s let rec reach_item_level n = if !item_level < n then begin printf "\n<\\itemize>\n"; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n"; decr item_level; reach_item_level n end let item n = let old_level = !item_level in reach_item_level n; if n <= old_level then printf "\n\n" let stop_item () = reach_item_level 0 let start_doc () = in_doc := true; printf "(** texmacs: " let end_doc () = stop_item (); in_doc := false; printf " *)" let start_coq () = () let end_coq () = () let start_code () = in_doc := true; printf "<\\code>\n" let end_code () = in_doc := false; printf "\n" let section_kind = function | 1 -> "section" | 2 -> "subsection" | 3 -> "subsubsection" | 4 -> "paragraph" | _ -> assert false let section lev f = stop_item (); printf "<"; output_string (section_kind lev); printf "|"; f (); printf ">\n\n" let rule () = printf "\n\n" let paragraph () = stop_item (); printf "\n\n" let line_break_true () = printf "" let line_break () = printf "\n" let empty_line_of_code () = printf "\n" let start_inline_coq () = printf "" let make_multi_index () = () let make_index () = () let make_toc () = () end (*s Generic output *) let select f1 f2 f3 x = match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x let push_in_preamble = Latex.push_in_preamble let header = select Latex.header Html.header TeXmacs.header let trailer = select Latex.trailer Html.trailer TeXmacs.trailer let start_module = select Latex.start_module Html.start_module TeXmacs.start_module let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq let start_code = select Latex.start_code Html.start_code TeXmacs.start_code let end_code = select Latex.end_code Html.end_code TeXmacs.end_code let start_inline_coq = select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq let end_inline_coq = select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq let indentation = select Latex.indentation Html.indentation TeXmacs.indentation let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph let line_break = select Latex.line_break Html.line_break TeXmacs.line_break let empty_line_of_code = select Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code let section = select Latex.section Html.section TeXmacs.section let item = select Latex.item Html.item TeXmacs.item let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item let rule = select Latex.rule Html.rule TeXmacs.rule let char = select Latex.char Html.char TeXmacs.char let ident = select Latex.ident Html.ident TeXmacs.ident let symbol = select Latex.symbol Html.symbol TeXmacs.symbol let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char let latex_string = select Latex.latex_string Html.latex_string TeXmacs.latex_string let html_char = select Latex.html_char Html.html_char TeXmacs.html_char let html_string = select Latex.html_string Html.html_string TeXmacs.html_string let start_latex_math = select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math let stop_latex_math = select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math let start_verbatim = select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim let verbatim_char = select output_char Html.char TeXmacs.char let hard_verbatim_char = output_char let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index let make_index = select Latex.make_index Html.make_index TeXmacs.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc