diff options
| -rw-r--r-- | Makefile | 26 | ||||
| -rw-r--r-- | doc/coq2html.css | 88 | ||||
| -rw-r--r-- | doc/coq2html.js | 24 | ||||
| -rw-r--r-- | doc/coq2html.mll | 447 | ||||
| -rw-r--r-- | doc/removeproofs.mll | 35 |
5 files changed, 570 insertions, 50 deletions
@@ -110,22 +110,18 @@ all: $(MAKE) ccomp $(MAKE) runtime -documentation: doc/removeproofs documentation-link - @mkdir -p doc/html - cd doc; $(COQDOC) --html -d html \ - $(FILES:%.v=--glob-from %.glob) $(FILES) - @cd doc; rm -f $(FILES) - cp doc/coqdoc.css doc/html/coqdoc.css - doc/removeproofs doc/html/*.html +documentation: doc/coq2html $(FILES) + mkdir -p doc/html + rm -f doc/html/*.html + doc/coq2html -o 'doc/html/%.html' doc/*.glob \ + $(filter-out doc/coq2html, $^) + cp doc/coq2html.css doc/coq2html.js doc/html/ -documentation-link: $(FILES) - @ln -f $^ doc/ +doc/coq2html: doc/coq2html.ml + ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml -doc/removeproofs: doc/removeproofs.ml - ocamlopt -o doc/removeproofs doc/removeproofs.ml - -doc/removeproofs.ml: doc/removeproofs.mll - ocamllex doc/removeproofs.mll +doc/coq2html.ml: doc/coq2html.mll + ocamllex doc/coq2html.mll latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -163,7 +159,7 @@ clean: rm -f ccomp ccomp.byte rm -rf _build rm -rf doc/html doc/*.glob - rm -f doc/removeproofs.ml doc/removeproofs + rm -f doc/coq2html.ml doc/coq2html rm -f driver/Configuration.ml rm -f extraction/*.ml extraction/*.mli $(MAKE) -C runtime clean diff --git a/doc/coq2html.css b/doc/coq2html.css new file mode 100644 index 0000000..5a326a3 --- /dev/null +++ b/doc/coq2html.css @@ -0,0 +1,88 @@ +/* Classes: + h1.title the title of the page + div.coq encloses all generated body + div.doc contents of (** *) comments + div.footer footer + div.togglescript "Proof." line + div.proofscript contents of proof script + span.docright contents of (**r *) comments + span.bracket contents of [ ] within comments + span.kwd Coq keyword + span.tactic Coq tactic + span.id any other identifier +*/ + +body { + color: black; + background: white; +} + +h1.title { + font-size: 2em; + text-align: center +} + +h1 { + font-size: 1.5em; +} +h2 { + font-size: 1.17em; +} +h3 { + font-size: 1em; +} + +h1, h2, h3 { + font-family: sans-serif; + margin-left: -5%; +} + +div.coq { + margin-left: 15%; + margin-right: 5%; + font-family: monospace; +} + +div.doc { + margin-left: -5%; + margin-top: 0.2em; + margin-bottom: 0.5em; + font-family: serif; +} + +div.toggleproof { + font-size: 0.8em; + text-decoration: underline; +} + +div.proofscript { + font-size: 0.8em; +} + +div.footer { + margin-top: 1em; + margin-bottom: 1em; + font-size: 0.8em; + font-style: italic; +} + +span.docright { + position: absolute; + left: 60%; + width: 40%; + font-family: serif; +} + +span.bracket { + font-family: monospace; + color: #008000; +} + +span.kwd { + color: #cf1d1d; +} + +a:visited {color : #416DFF; text-decoration : none; } +a:link {color : #416DFF; text-decoration : none; } +a:hover {text-decoration : none; } +a:active {text-decoration : none; } diff --git a/doc/coq2html.js b/doc/coq2html.js new file mode 100644 index 0000000..a840b00 --- /dev/null +++ b/doc/coq2html.js @@ -0,0 +1,24 @@ +function toggleDisplay(id) +{ + var elt = document.getElementById(id); + if (elt.style.display == 'none') { + elt.style.display = 'block'; + } else { + elt.style.display = 'none'; + } +} + +function hideAll(cls) +{ + var testClass = new RegExp("(^|s)" + cls + "(s|$)"); + var tag = tag || "*"; + var elements = document.getElementsByTagName("div"); + var current; + var length = elements.length; + for(var i=0; i<length; i++){ + current = elements[i]; + if(testClass.test(current.className)) { + current.style.display = 'none'; + } + } +} diff --git a/doc/coq2html.mll b/doc/coq2html.mll new file mode 100644 index 0000000..da2e602 --- /dev/null +++ b/doc/coq2html.mll @@ -0,0 +1,447 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +{ +open Printf + +(** Cross-referencing *) + +let current_module = ref "" + +type xref = + | Def of string * string (* path, type *) + | Ref of string * string * string (* unit, path, type *) + +let xref_table : (string * int, xref) Hashtbl.t = Hashtbl.create 273 +let xref_modules : (string, unit) Hashtbl.t = Hashtbl.create 29 + +let path sp id = + match sp, id with + | "<>", "<>" -> "" + | "<>", _ -> id + | _ , "<>" -> sp + | _ , _ -> sp ^ "." ^ id + +let add_module m = + Hashtbl.add xref_modules m () + +let add_reference curmod pos dp sp id ty = + if not (Hashtbl.mem xref_table (curmod, pos)) + then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty)) + +let add_definition curmod pos sp id ty = + if not (Hashtbl.mem xref_table (curmod, pos)) + then Hashtbl.add xref_table (curmod, pos) (Def(path sp id, ty)) + +(* +let read_glob_file f = + let ic = open_in f in + let curmod = ref "" in + try + while true do + let s = input_line ic in + try + Scanf.sscanf s "F%s" + (fun m -> curmod := m; add_module m) + with Scanf.Scan_failure _ -> + try + Scanf.sscanf s "R%d %s %s %s %s" + (fun pos dp sp id ty -> add_reference !curmod pos dp sp id ty) + with Scanf.Scan_failure _ -> + try + Scanf.sscanf s "%s %d %s %s" + (fun ty pos sp id -> add_definition !curmod pos sp id ty) + with Scanf.Scan_failure _ -> + () + done + with End_of_file -> + close_in ic +*) + +type link = Link of string | Anchor of string | Nolink + +let coqlib_url = "http://coq.inria.fr/library/" + +let re_coqlib = Str.regexp "Coq\\." +let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$" + +let crossref m pos = + try match Hashtbl.find xref_table (m, pos) with + | Def(p, ty) -> + Anchor p + | Ref(m', p, ty) -> + let url = + if Hashtbl.mem xref_modules m' then + m' ^ ".html" + else if Str.string_match re_coqlib m' 0 then + coqlib_url ^ m' ^ ".html" + else + raise Not_found in + if p = "" then + Link url + else if Str.string_match re_sane_path p 0 then + Link(url ^ "#" ^ p) + else + Nolink + with Not_found -> + Nolink + +(** Keywords, etc *) + +module StringSet = Set.Make(String) + +let mkset l = List.fold_right StringSet.add l StringSet.empty + +let coq_keywords = mkset [ + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; + "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; + "where"; "struct"; "wf"; "measure"; + "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; + "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; + "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; + "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; + "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; + "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; + "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; + "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; + "Qed"; "Record"; "Recursive"; "Remark"; "Require"; + "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; + "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; + "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; + "Notation"; "Reserved"; "Tactic"; "Delimit"; "Bind"; "Open"; + "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add"; + "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; + "Instantiation"; "subgoal"; "Program"; "Example"; "Obligation"; + "Obligations"; "Solve"; "using"; "Next"; "Instance"; "Equations"; + "Equations_nocomp" +] + +let coq_tactics = mkset [ + "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; + "injection"; "elimtype"; "progress"; "setoid_rewrite"; "destruct"; + "destruction"; "destruct_call"; "dependent"; "elim"; + "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; + "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact"; + "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; + "compute"; "at"; "in"; "by"; "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" +] + +(** HTML generation *) + +let oc = ref stdout + +let character = function + | '<' -> output_string !oc "<" + | '>' -> output_string !oc ">" + | '&' -> output_string !oc "&" + | c -> output_char !oc c + +let section_level = function + | "*" -> 1 + | "**" -> 2 + | _ -> 3 + +let start_section sect = + fprintf !oc "<h%d>" (section_level sect) +let end_section sect = + fprintf !oc "</h%d>\n" (section_level sect) + +let start_doc_right () = + fprintf !oc "<span class=\"docright\">(* " +let end_doc_right () = + fprintf !oc " *)</span>" + +let enum_depth = ref 0 + +let rec set_enum_depth d = + if !enum_depth < d then begin + fprintf !oc "<ul>\n"; + fprintf !oc "<li>\n"; + incr enum_depth; + end + else if !enum_depth > d then begin + fprintf !oc "</li>\n"; + fprintf !oc "</ul>\n"; + decr enum_depth; + end + else if !enum_depth > 0 then begin + fprintf !oc "</li>\n"; + fprintf !oc "<li>\n" + end + +let start_doc () = + fprintf !oc "<div class=\"doc\">" +let end_doc () = + set_enum_depth 0; + fprintf !oc "</div>\n" + +let ident pos id = + if StringSet.mem id coq_keywords then + fprintf !oc "<span class=\"kwd\">%s</span>" id + else if StringSet.mem id coq_tactics then + fprintf !oc "<span class=\"tactic\">%s</span>" id + else match crossref !current_module pos with + | Nolink -> + fprintf !oc "<span class=\"id\">%s</span>" id + | Link p -> + fprintf !oc "<span class=\"id\"><a href=\"%s\">%s</a></span>" p id + | Anchor p -> + fprintf !oc "<span class=\"id\"><a name=\"%s\">%s</a></span>" p id + +let space s = + for i = 1 to String.length s do fprintf !oc " " done + +let newline () = + fprintf !oc "<br/>\n" + +let dashes = function + | "-" -> set_enum_depth 1 + | "--" -> set_enum_depth 2 + | "---" -> set_enum_depth 3 + | "----" -> set_enum_depth 4 + | _ -> fprintf !oc "<hr/>\n" + +let start_verbatim () = + fprintf !oc "<pre>\n" + +let end_verbatim () = + fprintf !oc "</pre>\n" + +let start_bracket () = + fprintf !oc "<span class=\"bracket\">" + +let end_bracket () = + fprintf !oc "</span>" + +let proof_counter = ref 0 + +let start_proof kwd = + incr proof_counter; + fprintf !oc + "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" + !proof_counter kwd; + fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter + +let end_proof kwd = + fprintf !oc "%s</div>\n" kwd + +let start_html_page modname = + fprintf !oc "\ +<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\"> +<html xmlns=\"http://www.w3.org/1999/xhtml\"> + +<head> +<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\" /> +<title>Module %s</title> +<meta name=\"description\" content=\"Documentation of Coq module %s\" /> +<link href=\"coq2html.css\" rel=\"stylesheet\" type=\"text/css\" /> +<script type=\"text/javascript\" src=\"coq2html.js\"> </script> +</head> + +<body onload=\"hideAll('proofscript')\"> +<h1 class=\"title\">Module %s</h1> +<div class=\"coq\"> +" modname modname modname + +let end_html_page () = + fprintf !oc "\ +</div> +<div class=\"footer\"><hr/>Generated by coq2html</div> +</body> +</html> +" + +} + +let space = [' ' '\t'] +let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* +let path = ident ("." ident)* +let start_proof = "Proof." | ("Next" space+ "Obligation.") +let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort." + +let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>" +let integer = ['0'-'9']+ + +rule coq_bol = parse + | space* (start_proof as sp) + { start_proof sp; + skip_newline lexbuf } + | space* "(** " ("*"+ as sect) + { start_section sect; + doc lexbuf; + end_section sect; + skip_newline lexbuf } + | space* "(** " + { start_doc(); + doc lexbuf; + end_doc(); + skip_newline lexbuf } + | space* "(*" + { comment lexbuf; + skip_newline lexbuf } + | eof + { () } + | space* as s + { space s; + coq lexbuf } + +and skip_newline = parse + | space* "\n" + { coq_bol lexbuf } + | "" + { coq lexbuf } + +and coq = parse + | end_proof as ep + { end_proof ep; + skip_newline lexbuf } + | "(**r " + { start_doc_right(); + doc lexbuf; + end_doc_right(); + coq lexbuf } + | "(*" + { comment lexbuf; + coq lexbuf } + | path as id + { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } + | "\n" + { newline(); coq_bol lexbuf } + | eof + { () } + | _ as c + { character c; coq lexbuf } + +and bracket = parse + | ']' + { () } + | '[' + { character '['; bracket lexbuf; character ']'; bracket lexbuf } + | path as id + { ident (Lexing.lexeme_start lexbuf) id; bracket lexbuf } + | eof + { () } + | _ as c + { character c; bracket lexbuf } + +and comment = parse + | "*)" + { () } + | "(*" + { comment lexbuf; comment lexbuf } + | eof + { () } + | _ + { comment lexbuf } + +and doc_bol = parse + | "<<" space* "\n" + { start_verbatim(); + verbatim lexbuf; + end_verbatim(); + doc_bol lexbuf } + | "-"+ as d + { dashes d; doc lexbuf } + | "\n" + { set_enum_depth 0; doc_bol lexbuf } + | "" + { doc lexbuf } + +and doc = parse + | "*)" + { () } + | "\n" + { character '\n'; doc_bol lexbuf } + | "[" + { start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf } + | eof + { () } + | _ as c + { character c; doc lexbuf } + +and verbatim = parse + | "\n>>" space* "\n" + { () } + | eof + { () } + | _ as c + { character c; verbatim lexbuf } + +and globfile = parse + | eof + { () } + | "F" (ident as m) space* "\n" + { current_module := m; add_module m; + globfile lexbuf } + | "R" (integer as pos) + space+ (xref as dp) + space+ (xref as sp) + space+ (xref as id) + space+ (ident as ty) + space* "\n" + { add_reference !current_module (int_of_string pos) dp sp id ty; + globfile lexbuf } + | (ident as ty) + space+ (integer as pos) + space+ (xref as sp) + space+ (xref as id) + space* "\n" + { add_definition !current_module (int_of_string pos) sp id ty; + globfile lexbuf } + | [^ '\n']* "\n" + { globfile lexbuf } + +{ + +let output_name = ref "-" + +let process_file f = + if Filename.check_suffix f ".v" then begin + current_module := Filename.chop_suffix (Filename.basename f) ".v"; + let ic = open_in f in + if !output_name = "-" then + oc := stdout + else + oc := open_out (Str.global_replace (Str.regexp "%") !current_module + !output_name); + start_html_page !current_module; + coq_bol (Lexing.from_channel ic); + end_html_page(); + if !output_name <> "-" then (close_out !oc; oc := stdout); + close_in ic + end else + if Filename.check_suffix f ".glob" then begin + current_module := ""; + let ic = open_in f in + globfile (Lexing.from_channel ic); + close_in ic + end else begin + eprintf "Don't know what to do with file %s\n" f; + exit 2 + end + +let _ = + Arg.parse [ + "-o", Arg.String (fun s -> output_name := s), + " <output> Set output file ('%' replaced by module name)" + ] process_file + "Usage: coq2html [options] <file.glob> file.v\nOptions are:" +} diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll deleted file mode 100644 index 7fb37bb..0000000 --- a/doc/removeproofs.mll +++ /dev/null @@ -1,35 +0,0 @@ -rule process inproof oc = parse - | "<span class=\"keyword\">Proof</span>" ' '* '.' - { process true oc lexbuf } - | "<span class=\"keyword\">" ("Qed" | "Defined") "</span>" ' '* '.' - { process false oc lexbuf } -(* - | "<a class=\"idref\" href=\"" - [^ '"'] + '#' '"' [^ '\n' '>']* '"' '"' '>' - ([^ '<' '\n']+ as ident) - "</a>" - { if not inproof then output_string oc ident; - process inproof oc lexbuf } -*) - | _ - { if not inproof then output_char oc (Lexing.lexeme_char lexbuf 0); - process inproof oc lexbuf } - | eof - { () } - -{ - -let process_file name = - let ic = open_in name in - Sys.remove name; - let oc = open_out name in - process false oc (Lexing.from_channel ic); - close_out oc; - close_in ic - -let _ = - for i = 1 to Array.length Sys.argv - 1 do - process_file Sys.argv.(i) - done -} - |