doc_lexer.mll 10.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
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 28 29 30
  let backtrack lexbuf =
    lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
    lexbuf.lex_curr_p <- lexbuf.lex_start_p

31
  let make_table l =
32
    let ht = Hashtbl.create 97 in
33 34 35
    List.iter (fun s -> Hashtbl.add ht s ()) l;
    Hashtbl.mem ht

36
  let is_keyword1 = make_table [ "as"; "axiom"; "clone"; "coinductive";
37 38 39 40
    "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";
41 42 43 44 45 46 47 48
    (* 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";
49
    "returns"; "variant"; "writes"; "diverges"; ]
50 51

  let get_loc lb =
52
    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
53

54 55
  let current_file = ref ""

56
  let print_ident fmt lexbuf s =
57 58 59 60
    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
61 62 63 64 65
    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? *)
      try
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69 70 71 72 73 74 75 76
        let id, def = Glob.find loc in
        match id.Ident.id_loc with
        | None -> raise Not_found
        | Some _ ->
          match def with
          | Glob.Def ->
            fprintf fmt "<a name=\"%a\">%a</a>"
              Doc_def.pp_anchor id Pp.html_string s
          | Glob.Use ->
            fprintf fmt "<a href=\"%a\">%a</a>"
              Doc_def.pp_locate id Pp.html_string s
77 78 79 80 81
      with Not_found ->
        (* otherwise, just print it *)
        pp_print_string fmt s
    end

82 83
  type empty_line = PrevEmpty | CurrEmpty | NotEmpty

84 85
}

86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
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 '_'
  | "[]"
  | "[<-]"
  | "[]<-"

107
let space = [' ' '\t']
108
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
109
let special = ['\'' '"' '<' '>' '&']
110

111
rule scan fmt empty = parse
MARCHE Claude's avatar
MARCHE Claude committed
112
  | "(*)" as s
113
          { pp_print_string fmt s;
114 115
            scan fmt NotEmpty lexbuf }
  | space* "(***"
116
          { comment fmt false lexbuf;
117 118 119 120 121
            scan fmt empty lexbuf }
  | space* "(**"
          { pp_print_string fmt "</pre>\n";
            if empty <> PrevEmpty then
              pp_print_string fmt "<div class=\"info\">";
122
            doc fmt false [] lexbuf;
123 124 125
            if empty <> PrevEmpty then pp_print_string fmt "</div>";
            pp_print_string fmt "<pre>";
            scan fmt CurrEmpty lexbuf }
126 127 128
  | "(**)"
          { pp_print_string fmt "<span class=\"comment\">(**)</span>";
            scan fmt NotEmpty lexbuf }
129
  | "(*"
130
          { pp_print_string fmt "<span class=\"comment\">(*";
131
            comment fmt true lexbuf;
132 133
            pp_print_string fmt "</span>";
            scan fmt NotEmpty lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
134
  | eof   { () }
135
  | ident as s
136
          { print_ident fmt lexbuf s;
137 138 139 140 141 142 143 144 145
            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 }
146
  | "'\"'"
147 148 149
  | _ as s
          { pp_print_string fmt s;
            scan fmt NotEmpty lexbuf }
150 151 152 153 154 155 156 157

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 }
158
  | "*)"  { backtrack lexbuf }
159 160 161 162 163
  | eof   { () }
  | ident as s
          { print_ident fmt lexbuf s;
            scan_embedded fmt depth lexbuf }
  | "\n"   { newline lexbuf;
164
             pp_print_char fmt '\n';
165
             scan_embedded fmt depth lexbuf }
166
  | '"'    { pp_print_string fmt "&quot;";
167 168
             string fmt true lexbuf;
             scan_embedded fmt depth lexbuf }
169
  | "'\"'"
170 171
  | _ as s { pp_print_string fmt s;
             scan_embedded fmt depth lexbuf }
172

MARCHE Claude's avatar
MARCHE Claude committed
173
and comment fmt do_output = parse
174
  | "(*"   { if do_output then pp_print_string fmt "(*";
MARCHE Claude's avatar
MARCHE Claude committed
175 176
             comment fmt do_output lexbuf;
             comment fmt do_output lexbuf }
177
  | "*)"   { if do_output then pp_print_string fmt "*)" }
178
  | eof    { () }
MARCHE Claude's avatar
MARCHE Claude committed
179
  | "\n"   { newline lexbuf;
180
             if do_output then pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
181
             comment fmt do_output lexbuf }
182
  | '"'    { if do_output then pp_print_string fmt "&quot;";
MARCHE Claude's avatar
MARCHE Claude committed
183 184
             string fmt do_output lexbuf;
             comment fmt do_output lexbuf }
185
  | special as c
186
           { if do_output then Pp.html_char fmt c;
MARCHE Claude's avatar
MARCHE Claude committed
187
             comment fmt do_output lexbuf }
188
  | "'\"'"
MARCHE Claude's avatar
MARCHE Claude committed
189
  | _ as s { if do_output then pp_print_string fmt s;
MARCHE Claude's avatar
MARCHE Claude committed
190 191 192
             comment fmt do_output lexbuf }

and string fmt do_output = parse
MARCHE Claude's avatar
MARCHE Claude committed
193
  | "\n"   { newline lexbuf;
194
             if do_output then pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
195
             string fmt do_output lexbuf }
196
  | '"'    { if do_output then pp_print_string fmt "&quot;" }
197
  | special as c
198
           { if do_output then Pp.html_char fmt c;
MARCHE Claude's avatar
MARCHE Claude committed
199
             string fmt do_output lexbuf }
200
  | "\\" _
MARCHE Claude's avatar
MARCHE Claude committed
201
  | _ as s { if do_output then pp_print_string fmt s;
MARCHE Claude's avatar
MARCHE Claude committed
202
             string fmt do_output lexbuf }
203

204
and doc fmt block headings = parse
205 206
  | ' '* "*)"
           { if block then pp_print_string fmt "</p>\n" }
MARCHE Claude's avatar
MARCHE Claude committed
207
  | eof    { () }
208
  | "\n" space* "\n" { newline lexbuf;
209 210
             newline lexbuf;
             if block then pp_print_string fmt "</p>";
211
             pp_print_char fmt '\n';
212
             doc fmt false headings lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
213
  | "\n"   { newline lexbuf;
214
             pp_print_char fmt '\n';
215
             doc fmt block headings lexbuf }
216
  | '{' (['1'-'6'] as c) ' '*
217
           { if block then pp_print_string fmt "</p>\n";
218
             let n = Char.code c - Char.code '0' in
MARCHE Claude's avatar
MARCHE Claude committed
219
             fprintf fmt "<h%d>" n;
220 221 222 223 224 225 226 227
             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>";
228
               pp_print_char fmt '}';
229
               doc fmt true r lexbuf
230
             in
231 232
             match headings with
              | [] -> brace headings
MARCHE Claude's avatar
MARCHE Claude committed
233
              | n :: r ->
234
                if n >= 1 then begin
235
                  fprintf fmt "</h%d>" n;
236 237
                  doc fmt (r <> []) r lexbuf
                end else brace r
MARCHE Claude's avatar
MARCHE Claude committed
238
           }
239 240
  | '['    { if not block then pp_print_string fmt "<p>";
             pp_print_string fmt "<code>";
241
             scan_embedded fmt 0 lexbuf;
MARCHE Claude's avatar
MARCHE Claude committed
242
             pp_print_string fmt "</code>";
243 244 245
             doc fmt true headings lexbuf }
  | ' '    { if block then pp_print_char fmt ' ';
             doc fmt block headings lexbuf }
246
  | special as c
247
           { if not block then pp_print_string fmt "<p>";
248
             Pp.html_char fmt c;
249 250 251 252
             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
253 254 255


and raw_html fmt depth = parse
256
  | "*)"  { backtrack lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
257 258
  | eof    { () }
  | "\n"   { newline lexbuf;
259
             pp_print_char fmt '\n';
MARCHE Claude's avatar
MARCHE Claude committed
260
             raw_html fmt depth lexbuf }
261
  | '{'    { pp_print_char fmt '{'; raw_html fmt (succ depth) lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
262 263
  | '}'    { if depth = 0 then () else
               begin
264
                 pp_print_char fmt '}';
MARCHE Claude's avatar
MARCHE Claude committed
265 266 267 268 269
                 raw_html fmt (pred depth) lexbuf
               end }
  | _ as c { pp_print_char fmt c; raw_html fmt depth lexbuf }


270 271 272 273 274 275 276 277 278
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
279

280 281 282 283 284
and skip_comment = parse
  | "*)" { () }
  | "(*" { skip_comment lexbuf; skip_comment lexbuf }
  | eof  { () }
  | _    { skip_comment lexbuf }
MARCHE Claude's avatar
MARCHE Claude committed
285

286 287
{

288
  let do_file fmt fname =
289
    current_file := fname;
290 291 292
    (* input *)
    let cin = open_in fname in
    let lb = Lexing.from_channel cin in
293 294
    lb.Lexing.lex_curr_p <-
      { lb.Lexing.lex_curr_p with Lexing.pos_fname = fname };
295
    (* output *)
296 297 298
    pp_print_string fmt "<div class=\"why3doc\">\n<pre>";
    scan fmt PrevEmpty lb;
    pp_print_string fmt "</pre>\n</div>\n";
299
    close_in cin
300

301 302 303 304 305 306 307
  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

308 309 310 311 312 313 314
}

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