From 261103b5bfd89335d028bf800af3f0a1ab1b70e5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 9 Mar 2010 15:13:00 +0000 Subject: New HTML documentation generator git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/coq2html.mll | 447 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 447 insertions(+) create mode 100644 doc/coq2html.mll (limited to 'doc/coq2html.mll') diff --git a/doc/coq2html.mll b/doc/coq2html.mll new file mode 100644 index 00000000..da2e602f --- /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 "" (section_level sect) +let end_section sect = + fprintf !oc "\n" (section_level sect) + +let start_doc_right () = + fprintf !oc "(* " +let end_doc_right () = + fprintf !oc " *)" + +let enum_depth = ref 0 + +let rec set_enum_depth d = + if !enum_depth < d then begin + fprintf !oc "\n"; + decr enum_depth; + end + else if !enum_depth > 0 then begin + fprintf !oc "\n"; + fprintf !oc "
  • \n" + end + +let start_doc () = + fprintf !oc "
    " +let end_doc () = + set_enum_depth 0; + fprintf !oc "
    \n" + +let ident pos id = + if StringSet.mem id coq_keywords then + fprintf !oc "%s" id + else if StringSet.mem id coq_tactics then + fprintf !oc "%s" id + else match crossref !current_module pos with + | Nolink -> + fprintf !oc "%s" id + | Link p -> + fprintf !oc "%s" p id + | Anchor p -> + fprintf !oc "%s" p id + +let space s = + for i = 1 to String.length s do fprintf !oc " " done + +let newline () = + fprintf !oc "
    \n" + +let dashes = function + | "-" -> set_enum_depth 1 + | "--" -> set_enum_depth 2 + | "---" -> set_enum_depth 3 + | "----" -> set_enum_depth 4 + | _ -> fprintf !oc "
    \n" + +let start_verbatim () = + fprintf !oc "
    \n"
+
+let end_verbatim () =
+  fprintf !oc "
    \n" + +let start_bracket () = + fprintf !oc "" + +let end_bracket () = + fprintf !oc "" + +let proof_counter = ref 0 + +let start_proof kwd = + incr proof_counter; + fprintf !oc + "
    %s
    \n" + !proof_counter kwd; + fprintf !oc "
    \n" !proof_counter + +let end_proof kwd = + fprintf !oc "%s
    \n" kwd + +let start_html_page modname = + fprintf !oc "\ + + + + + +Module %s + + + + + + +

    Module %s

    +
    +" modname modname modname + +let end_html_page () = + fprintf !oc "\ +
    +
    Generated by coq2html
    + + +" + +} + +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), + " Set output file ('%' replaced by module name)" + ] process_file + "Usage: coq2html [options] file.v\nOptions are:" +} -- cgit