summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile26
-rw-r--r--doc/coq2html.css88
-rw-r--r--doc/coq2html.js24
-rw-r--r--doc/coq2html.mll447
-rw-r--r--doc/removeproofs.mll35
5 files changed, 570 insertions, 50 deletions
diff --git a/Makefile b/Makefile
index d50a478..e3eb246 100644
--- a/Makefile
+++ b/Makefile
@@ -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 "&lt;"
+ | '>' -> output_string !oc "&gt;"
+ | '&' -> output_string !oc "&amp;"
+ | 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 "&nbsp;" 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
-}
-