doc_lexer.mll 10.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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
  let newline lexbuf =
21 22
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
MARCHE Claude's avatar
MARCHE Claude committed
23
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
24

25 26 27 28
  let backtrack lexbuf =
    lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
    lexbuf.lex_curr_p <- lexbuf.lex_start_p

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

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

  let get_loc lb =
50
    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
51

52 53
  let current_file = ref ""

54
  let print_ident fmt lexbuf s =
55 56 57 58
    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
59 60 61 62 63
    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
64 65 66 67 68 69 70 71 72 73 74
        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
75 76 77 78 79
      with Not_found ->
        (* otherwise, just print it *)
        pp_print_string fmt s
    end

80 81
  type empty_line = PrevEmpty | CurrEmpty | NotEmpty

82 83
}

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

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

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

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

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

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

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


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


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

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

284 285
{

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

299 300 301 302 303 304 305
  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

306 307 308 309 310 311 312
}

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