From 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Jun 2018 10:40:04 +0200 Subject: Use the standalone coq2html tool to generate the HTML documentation coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq. --- doc/coq2html.mll | 454 ------------------------------------------------------- 1 file changed, 454 deletions(-) delete mode 100644 doc/coq2html.mll (limited to 'doc/coq2html.mll') diff --git a/doc/coq2html.mll b/doc/coq2html.mll deleted file mode 100644 index cdc844dc..00000000 --- a/doc/coq2html.mll +++ /dev/null @@ -1,454 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 = - (*eprintf "add_module %s\n" m;*) - Hashtbl.add xref_modules m () - -let add_reference curmod pos dp sp id ty = - (*eprintf "add_reference %s %d %s %s %s %s\n" 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)) - -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 re_shortname = Str.regexp "^.*\\." - -let shortname m = Str.replace_first re_shortname "" m - -let crossref m pos = - (*eprintf "crossref %s %d\n" m pos;*) - try match Hashtbl.find xref_table (m, pos) with - | Def(p, _) -> - Anchor p - | Ref(m', p, _) -> - let url = - if Hashtbl.mem xref_modules m' then - shortname 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 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 _ = 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_comment () = - fprintf !oc "(*" - -let end_comment () = - fprintf !oc "*)" - -let start_bracket () = - fprintf !oc "" - -let end_bracket () = - fprintf !oc "" - -let in_proof = ref false -let proof_counter = ref 0 - -let start_proof kwd = - in_proof := true; - incr proof_counter; - fprintf !oc - "
    %s
    \n" - !proof_counter kwd; - fprintf !oc "
    \n" !proof_counter - -let end_proof kwd = - fprintf !oc "%s
    \n" kwd; - in_proof := false - -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" space* ".") | ("Proof" space+ "with") | ("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 } - | "(*" - { if !in_proof then start_comment(); - 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 - | "*)" - { if !in_proof then end_comment() } - | "(*" - { if !in_proof then start_comment(); - comment lexbuf; comment lexbuf } - | eof - { () } - | "\n" - { if !in_proof then newline(); - comment lexbuf } - | space* as s - { if !in_proof then space s; - comment lexbuf } - | eof - { () } - | _ as c - { if !in_proof then character c; - 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 } - | "$" [^ '\n' '$']* "$" - { doc lexbuf } - | "#" ([^ '\n' '#']* as html) "#" - { output_string !oc html; 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" (path as m) space* "\n" - { current_module := m; add_module m; - globfile lexbuf } - | "R" (integer as pos) ":" (integer) - 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) ":" (integer) - 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 - let pref_f = Filename.chop_suffix f ".v" in - let base_f = Filename.basename pref_f in - current_module := - "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f; - let ic = open_in f in - if !output_name = "-" then - oc := stdout - else - oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name); - start_html_page base_f; - 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