doc_lexer.mll 10.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16

(* Why3 to HTML *)

{

  open Format
17 18
  open Lexing
  open Why3
19

MARCHE Claude's avatar
MARCHE Claude committed
20 21
  let output_comments = ref true

MARCHE Claude's avatar
MARCHE Claude committed
22
  let newline lexbuf =
23 24
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
MARCHE Claude's avatar
MARCHE Claude committed
25
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
26

27
  let make_table l =
28
    let ht = Hashtbl.create 97 in
29 30 31
    List.iter (fun s -> Hashtbl.add ht s ()) l;
    Hashtbl.mem ht

32
  let is_keyword1 = make_table [ "as"; "axiom"; "clone"; "coinductive";
33 34 35 36
    "constant"; "else"; "end"; "epsilon"; "exists"; "export"; "false";
    "forall"; "function"; "goal"; "if"; "import"; "in"; "inductive";
    "lemma"; "let"; "match"; "meta"; "namespace"; "not"; "predicate";
    "prop"; "then"; "theory"; "true"; "type"; "use"; "with";
37 38 39 40 41 42 43 44
    (* programs *) "abstract"; "any";
    "begin"; "do"; "done"; "downto"; "exception";
    "for"; "fun"; "ghost"; "loop"; "model"; "module";
    "mutable"; "private"; "raise"; "rec";
    "to"; "try"; "val"; "while"; ]

  let is_keyword2 = make_table [ "absurd"; "assert"; "assume";
    "ensures"; "check"; "invariant"; "raises"; "reads"; "requires";
45
    "returns"; "variant"; "writes"; "diverges"; ]
46 47

  let get_loc lb =
48
    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
49

50 51 52 53 54 55
  let html_char fmt c =
    pp_print_string fmt (match c with
      | '<' -> "&lt;"
      | '>' -> "&gt;"
      | '&' -> "&amp;"
      | _ -> assert false)
56

57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
  let html_escape s =
    let len = ref 0 in
    String.iter (function '<' | '>' -> len := !len + 4
      | '&' -> len := !len + 5 | _ -> incr len) s;
    let len' = !len in
    let len = String.length s in
    if len = len' then s else begin
      let t = String.create len' in
      let j = ref 0 in
      let app u =
        let l = String.length u in
        String.blit u 0 t !j l;
        j := !j + l in
      for i = 0 to len - 1 do
        match s.[i] with
        | '<' -> app "&lt;"
        | '>' -> app "&gt;"
        | '&' -> app "&amp;"
        | c -> t.[!j] <- c; incr j
      done;
      t
    end

80 81
  let current_file = ref ""

82
  let print_ident fmt lexbuf s =
83 84 85 86
    if is_keyword1 s then
      fprintf fmt "<span class=\"keyword1\">%s</span>" s
    else if is_keyword2 s then
      fprintf fmt "<span class=\"keyword2\">%s</span>" s
87 88 89 90
    else begin
      let (* f,l,c as *) loc = get_loc lexbuf in
      (* Format.eprintf "  IDENT %s/%d/%d@." f l c; *)
      (* is this a def point? *)
91
      let s = html_escape s in
92
      try
93 94 95 96 97 98 99
        match Glob.find loc with
        | id, Glob.Def ->
          let t = Doc_def.anchor id in
          fprintf fmt "<a name=\"%s\">%s</a>" t s
        | id, Glob.Use ->
          let url = Doc_def.locate id in
          fprintf fmt "<a href=\"%s\">%s</a>" url s
100 101 102 103 104
      with Not_found ->
        (* otherwise, just print it *)
        pp_print_string fmt s
    end

105 106
  type empty_line = PrevEmpty | CurrEmpty | NotEmpty

107 108
}

109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
let prefix_op =
    op_char_1234* op_char_1 op_char_1234*
  | op_char_234*  op_char_2 op_char_234*
  | op_char_34* op_char_3 op_char_34*
  | op_char_4+
let operator =
    op_char_pref op_char_4*
  | prefix_op
  | prefix_op '_'
  | "[]"
  | "[<-]"
  | "[]<-"

130
let space = [' ' '\t']
131
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
132
let special = ['<' '>' '&']
133

134
rule scan fmt empty = parse
MARCHE Claude's avatar
MARCHE Claude committed
135
  | "(*)" as s
136
          { pp_print_string fmt s;
137 138
            scan fmt NotEmpty lexbuf }
  | space* "(***"
139
          { comment fmt false lexbuf;
140 141 142 143 144
            scan fmt empty lexbuf }
  | space* "(**"
          { pp_print_string fmt "</pre>\n";
            if empty <> PrevEmpty then
              pp_print_string fmt "<div class=\"info\">";
145
            doc fmt false [] lexbuf;
146 147 148
            if empty <> PrevEmpty then pp_print_string fmt "</div>";
            pp_print_string fmt "<pre>";
            scan fmt CurrEmpty lexbuf }
149 150 151
  | "(**)"
          { pp_print_string fmt "<span class=\"comment\">(**)</span>";
            scan fmt NotEmpty lexbuf }
152
  | "(*"
153
          { pp_print_string fmt "<span class=\"comment\">(*";
154
            comment fmt true lexbuf;
155 156
            pp_print_string fmt "</span>";
            scan fmt NotEmpty lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
157
  | eof   { () }
158
  | ident as s
159
          { print_ident fmt lexbuf s;
160 161 162 163 164 165 166 167 168
            scan fmt NotEmpty lexbuf }
  | space* '\n'
          { newline lexbuf;
            if empty <> PrevEmpty then pp_print_char fmt '\n';
            let e = if empty = NotEmpty then CurrEmpty else PrevEmpty in
            scan fmt e lexbuf }
  | '"'   { pp_print_string fmt "&quot;";
            string fmt true lexbuf;
            scan fmt NotEmpty lexbuf }
169
  | "'\"'"
170 171 172
  | _ as s
          { pp_print_string fmt s;
            scan fmt NotEmpty lexbuf }
173 174 175 176 177 178 179 180 181 182 183 184 185

and scan_embedded fmt depth = parse
  | '['   { pp_print_char fmt '[';
            scan_embedded fmt (depth + 1) lexbuf }
  | ']'   { if depth > 0 then begin
              pp_print_char fmt ']';
              scan_embedded fmt (depth - 1) lexbuf
            end }
  | eof   { () }
  | ident as s
          { print_ident fmt lexbuf s;
            scan_embedded fmt depth lexbuf }
  | "\n"   { newline lexbuf;
186
             pp_print_char fmt '\n';
187
             scan_embedded fmt depth lexbuf }
188
  | '"'    { pp_print_string fmt "&quot;";
189 190
             string fmt true lexbuf;
             scan_embedded fmt depth lexbuf }
191
  | "'\"'"
192 193
  | _ as s { pp_print_string fmt s;
             scan_embedded fmt depth lexbuf }
194

MARCHE Claude's avatar
MARCHE Claude committed
195
and comment fmt do_output = parse
196
  | "(*"   { if do_output then pp_print_string fmt "(*";
MARCHE Claude's avatar
MARCHE Claude committed
197 198
             comment fmt do_output lexbuf;
             comment fmt do_output lexbuf }
199
  | "*)"   { if do_output then pp_print_string fmt "*)" }
200
  | eof    { () }
MARCHE Claude's avatar
MARCHE Claude committed
201
  | "\n"   { newline lexbuf;
202
             if do_output then pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
203
             comment fmt do_output lexbuf }
204
  | '"'    { if do_output then pp_print_string fmt "&quot;";
MARCHE Claude's avatar
MARCHE Claude committed
205 206
             string fmt do_output lexbuf;
             comment fmt do_output lexbuf }
207 208
  | special as c
           { if do_output then html_char fmt c;
MARCHE Claude's avatar
MARCHE Claude committed
209
             comment fmt do_output lexbuf }
210
  | "'\"'"
MARCHE Claude's avatar
MARCHE Claude committed
211
  | _ as s { if do_output then pp_print_string fmt s;
MARCHE Claude's avatar
MARCHE Claude committed
212 213 214
             comment fmt do_output lexbuf }

and string fmt do_output = parse
MARCHE Claude's avatar
MARCHE Claude committed
215
  | "\n"   { newline lexbuf;
216
             if do_output then pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
217
             string fmt do_output lexbuf }
218
  | '"'    { if do_output then pp_print_string fmt "&quot;" }
219 220
  | special as c
           { if do_output then html_char fmt c;
MARCHE Claude's avatar
MARCHE Claude committed
221
             string fmt do_output lexbuf }
222
  | "\\" _
MARCHE Claude's avatar
MARCHE Claude committed
223
  | _ as s { if do_output then pp_print_string fmt s;
MARCHE Claude's avatar
MARCHE Claude committed
224
             string fmt do_output lexbuf }
225

226
and doc fmt block headings = parse
227 228
  | ' '* "*)"
           { if block then pp_print_string fmt "</p>\n" }
MARCHE Claude's avatar
MARCHE Claude committed
229
  | eof    { () }
230
  | "\n" space* "\n" { newline lexbuf;
231 232
             newline lexbuf;
             if block then pp_print_string fmt "</p>";
233
             pp_print_char fmt '\n';
234
             doc fmt false headings lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
235
  | "\n"   { newline lexbuf;
236
             pp_print_char fmt '\n';
237
             doc fmt block headings lexbuf }
238
  | '{' (['1'-'6'] as c) ' '*
239
           { if block then pp_print_string fmt "</p>\n";
240
             let n = Char.code c - Char.code '0' in
MARCHE Claude's avatar
MARCHE Claude committed
241
             fprintf fmt "<h%d>" n;
242 243 244 245 246 247 248 249
             doc fmt true (n::headings) lexbuf }
  | '{''h' { if not block then pp_print_string fmt "<p>";
             raw_html fmt 0 lexbuf; doc fmt true headings lexbuf }
  | '{'    { if not block then pp_print_string fmt "<p>";
             pp_print_char fmt '{';
             doc fmt true (0::headings) lexbuf }
  | '}'    { let brace r =
               if not block then pp_print_string fmt "<p>";
250
               pp_print_char fmt '}';
251
               doc fmt true r lexbuf
252
             in
253 254
             match headings with
              | [] -> brace headings
MARCHE Claude's avatar
MARCHE Claude committed
255
              | n :: r ->
256
                if n >= 1 then begin
257
                  fprintf fmt "</h%d>" n;
258 259
                  doc fmt (r <> []) r lexbuf
                end else brace r
MARCHE Claude's avatar
MARCHE Claude committed
260
           }
261 262
  | '['    { if not block then pp_print_string fmt "<p>";
             pp_print_string fmt "<code>";
263
             scan_embedded fmt 0 lexbuf;
MARCHE Claude's avatar
MARCHE Claude committed
264
             pp_print_string fmt "</code>";
265 266 267
             doc fmt true headings lexbuf }
  | ' '    { if block then pp_print_char fmt ' ';
             doc fmt block headings lexbuf }
268
  | special as c
269 270 271 272 273 274
           { if not block then pp_print_string fmt "<p>";
             html_char fmt c;
             doc fmt true headings lexbuf }
  | _ as c { if not block then pp_print_string fmt "<p>";
             pp_print_char fmt c;
             doc fmt true headings lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
275 276 277 278 279


and raw_html fmt depth = parse
  | eof    { () }
  | "\n"   { newline lexbuf;
280
             pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
281
             raw_html fmt depth lexbuf }
282
  | '{'    { pp_print_char fmt '{'; raw_html fmt (succ depth) lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
283 284
  | '}'    { if depth = 0 then () else
               begin
285
                 pp_print_char fmt '}';
MARCHE Claude's avatar
MARCHE Claude committed
286 287 288 289 290
                 raw_html fmt (pred depth) lexbuf
               end }
  | _ as c { pp_print_char fmt c; raw_html fmt depth lexbuf }


291 292 293 294 295 296 297 298 299
and extract_header = parse
  | "(**" space* "{" ['1'-'6'] ([^ '}']* as header) "}"
      { header }
  | space+ | "\n"
      { extract_header lexbuf }
  | "(*"
      { skip_comment lexbuf; extract_header lexbuf }
  | eof | _
      { "" }
MARCHE Claude's avatar
MARCHE Claude committed
300

301 302 303 304 305
and skip_comment = parse
  | "*)" { () }
  | "(*" { skip_comment lexbuf; skip_comment lexbuf }
  | eof  { () }
  | _    { skip_comment lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
306

307 308
{

309
  let do_file fmt fname =
310
    current_file := fname;
311 312 313
    (* input *)
    let cin = open_in fname in
    let lb = Lexing.from_channel cin in
314 315
    lb.Lexing.lex_curr_p <-
      { lb.Lexing.lex_curr_p with Lexing.pos_fname = fname };
316
    (* output *)
317 318 319
    pp_print_string fmt "<div class=\"why3doc\">\n<pre>";
    scan fmt PrevEmpty lb;
    pp_print_string fmt "</pre>\n</div>\n";
320
    close_in cin
321

322 323 324 325 326 327 328
  let extract_header fname =
    let cin = open_in fname in
    let lb = Lexing.from_channel cin in
    let h = extract_header lb in
    close_in cin;
    h

329 330 331 332 333 334 335 336
}

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3doc.opt"
End:
*)