why3session_html.ml 10.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Format
13
open Why3
14
open Why3session_lib
15

16
module Hprover = Whyconf.Hprover
17
module S = Session_itp
18

19
let output_dir = ref ""
20
let opt_context = ref false
21

22
type style = SimpleTree | Table
23

24 25
let opt_style = ref Table
let default_style = "table"
26 27

let set_opt_style = function
28
  | "simpletree" -> opt_style := SimpleTree
29
  | "table" -> opt_style := Table
Andrei Paskevich's avatar
Andrei Paskevich committed
30
  | _ ->
31 32 33
    eprintf "Unknown html style, ignored@."

let () = set_opt_style default_style
34

35 36 37 38 39 40 41 42 43
let opt_pp = ref []

let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
  let suf = ref "" in
  let cmd = ref "" in
  (fun s -> suf := s),
  (fun s -> cmd := s),
  (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)

44
let spec =
45 46
  ("-o",
   Arg.Set_string output_dir,
MARCHE Claude's avatar
MARCHE Claude committed
47
   "<path> output directory ('-' for stdout)") ::
48
  ("--context", Arg.Set opt_context,
49
   " add context around the generated HTML code") ::
50
  ("--style", Arg.Symbol (["simpletree";"table"], set_opt_style),
MARCHE Claude's avatar
MARCHE Claude committed
51
   " style to use, defaults to '" ^ default_style ^ "'."
52
) ::
53
  ("--add_pp", Arg.Tuple
54 55 56
    [Arg.String set_opt_pp_in;
     Arg.String set_opt_pp_cmd;
     Arg.String set_opt_pp_out],
57
  "<suffix> <cmd> <out_suffix> declare a pretty-printer for edited proofs") ::
58 59
  ("--coqdoc",
   Arg.Unit (fun ()->
60
    opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
MARCHE Claude's avatar
MARCHE Claude committed
61
  " use coqdoc to print Coq proofs") ::
62
  common_options
63

64
open Session_itp
65

66
type context =
67
    (string ->
MARCHE Claude's avatar
MARCHE Claude committed
68
     (formatter -> session -> unit) -> session
69 70
     -> unit, formatter, unit) format

71
let run_file (context : context) print_session fname =
MARCHE Claude's avatar
MARCHE Claude committed
72 73
  let ses,_ = read_session fname in
  let project_dir = get_dir ses in
74 75 76 77 78 79
  let output_dir =
    if !output_dir = "" then project_dir else !output_dir
  in
  let basename = Filename.basename project_dir in
  let cout =
    if output_dir = "-" then stdout else
80
      open_out (Filename.concat output_dir ("why3session.html"))
81
  in
82 83
  let fmt = formatter_of_out_channel cout in
  if !opt_context
MARCHE Claude's avatar
MARCHE Claude committed
84 85
  then fprintf fmt context basename (print_session basename) ses
  else print_session basename fmt ses;
86 87 88 89
  pp_print_flush fmt ();
  if output_dir <> "-" then close_out cout


90 91 92 93
module Table =
struct


MARCHE Claude's avatar
MARCHE Claude committed
94
  let rec transf_depth s tr =
95
    List.fold_left
MARCHE Claude's avatar
MARCHE Claude committed
96 97 98 99 100
      (fun depth g -> max depth (goal_depth s g)) 0 (get_sub_tasks s tr)
  and goal_depth s g =
    List.fold_left
      (fun depth tr -> max depth (1 + transf_depth s tr))
      1 (get_transformations s g)
101

MARCHE Claude's avatar
MARCHE Claude committed
102
  let theory_depth s t =
103
    List.fold_left
MARCHE Claude's avatar
MARCHE Claude committed
104
      (fun depth g -> max depth (goal_depth s g)) 0 (theory_goals t)
105

MARCHE Claude's avatar
MARCHE Claude committed
106 107 108
  let provers_stats s provers theory =
    theory_iter_proof_attempt s (fun a ->
      Hprover.replace provers a.prover a.prover) theory
109 110 111 112

  let print_prover = Whyconf.print_prover


Andrei Paskevich's avatar
Andrei Paskevich committed
113 114 115
  let color_of_status ?(dark=false) fmt b =
    fprintf fmt "%s" (if b then
        if dark then "008000" else "C0FFC0"
116 117
      else "FF0000")

MARCHE Claude's avatar
MARCHE Claude committed
118
let print_results fmt s provers proofs =
119 120 121 122
  List.iter (fun p ->
    fprintf fmt "<td bgcolor=\"#";
    begin
      try
MARCHE Claude's avatar
MARCHE Claude committed
123 124
        let pr = get_proof_attempt_node s (Hprover.find proofs p) in
        let s = pr.proof_state in
125 126
        begin
          match s with
MARCHE Claude's avatar
MARCHE Claude committed
127
	  | Some res ->
128 129 130 131 132 133 134
	    begin
	      match res.Call_provers.pr_answer with
		| Call_provers.Valid ->
                  fprintf fmt "C0FFC0\">%.2f" res.Call_provers.pr_time
		| Call_provers.Invalid ->
                  fprintf fmt "FF0000\">Invalid"
		| Call_provers.Timeout ->
MARCHE Claude's avatar
MARCHE Claude committed
135
                  fprintf fmt "FF8000\">Timeout (%ds)"
MARCHE Claude's avatar
MARCHE Claude committed
136
                    pr.limit.Call_provers.limit_time
137
		| Call_provers.OutOfMemory ->
MARCHE Claude's avatar
MARCHE Claude committed
138
                  fprintf fmt "FF8000\">Out Of Memory (%dM)"
MARCHE Claude's avatar
MARCHE Claude committed
139
                    pr.limit.Call_provers.limit_mem
140 141
		| Call_provers.StepLimitExceeded ->
                  fprintf fmt "FF8000\">Step limit exceeded"
142
		| Call_provers.Unknown _ ->
MARCHE Claude's avatar
MARCHE Claude committed
143
                  fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
144
		| Call_provers.Failure _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
145 146 147
                  fprintf fmt "FF8000\">Failure"
		| Call_provers.HighFailure ->
                  fprintf fmt "FF8000\">High Failure"
148
	    end
MARCHE Claude's avatar
MARCHE Claude committed
149
	  | None -> fprintf fmt "E0E0E0\">result missing"
150
        end;
151
        if pr.S.proof_obsolete then fprintf fmt " (obsolete)"
MARCHE Claude's avatar
MARCHE Claude committed
152
      with Not_found -> fprintf fmt "E0E0E0\">---"
153 154 155
    end;
    fprintf fmt "</td>") provers

MARCHE Claude's avatar
MARCHE Claude committed
156
let rec num_lines s acc tr =
MARCHE Claude's avatar
MARCHE Claude committed
157
  List.fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
158
    (fun acc g -> 1 +
MARCHE Claude's avatar
MARCHE Claude committed
159 160 161
      List.fold_left (fun acc tr -> 1 + num_lines s acc tr)
      acc (get_transformations s g))
    acc (get_sub_tasks s tr)
MARCHE Claude's avatar
MARCHE Claude committed
162

MARCHE Claude's avatar
MARCHE Claude committed
163
  let rec print_transf fmt s depth max_depth provers tr =
164
    fprintf fmt "<tr>";
165
    for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
Andrei Paskevich's avatar
Andrei Paskevich committed
166
    fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
MARCHE Claude's avatar
MARCHE Claude committed
167
      (color_of_status ~dark:false) (tn_proved s tr)
MARCHE Claude's avatar
MARCHE Claude committed
168 169
      (max_depth - depth + 1);
    (* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
MARCHE Claude's avatar
MARCHE Claude committed
170 171 172
    let name = (get_transf_name s tr) ^
                 (String.concat "" (get_transf_args s tr)) in
    fprintf fmt "%s</td>" name ;
173
    for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
174 175 176
      fprintf fmt "<td bgcolor=\"#E0E0E0\"></td>"
    done;
    fprintf fmt "</tr>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
177
    fprintf fmt "<td rowspan=\"%d\">&nbsp;&nbsp;</td>" (num_lines s 0 tr);
MARCHE Claude's avatar
MARCHE Claude committed
178 179
    let (_:bool) = List.fold_left
      (fun is_first g ->
MARCHE Claude's avatar
MARCHE Claude committed
180
        print_goal fmt s is_first (depth+1) max_depth provers g;
MARCHE Claude's avatar
MARCHE Claude committed
181
        false)
MARCHE Claude's avatar
MARCHE Claude committed
182
      true (get_sub_tasks s tr)
MARCHE Claude's avatar
MARCHE Claude committed
183 184
    in ()

MARCHE Claude's avatar
MARCHE Claude committed
185
  and print_goal fmt s is_first depth max_depth provers g =
MARCHE Claude's avatar
MARCHE Claude committed
186 187
    if not is_first then fprintf fmt "<tr>";
    (* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
188
    fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
MARCHE Claude's avatar
MARCHE Claude committed
189
      (color_of_status ~dark:false) (pn_proved s g)
190
      (max_depth - depth + 1);
MARCHE Claude's avatar
MARCHE Claude committed
191
    (* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
MARCHE Claude's avatar
MARCHE Claude committed
192
    fprintf fmt "%s</td>" (get_proof_name s g).Ident.id_string;
193
(*    for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
MARCHE Claude's avatar
MARCHE Claude committed
194
    print_results fmt s provers (get_proof_attempt_ids s g);
195
    fprintf fmt "</tr>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
196 197 198
    List.iter
      (print_transf fmt s depth max_depth provers)
      (get_transformations s g)
199

MARCHE Claude's avatar
MARCHE Claude committed
200 201
  let print_theory s fn fmt th =
    let depth = theory_depth s th in
202
    if depth > 0 then
203
    let provers = Hprover.create 9 in
MARCHE Claude's avatar
MARCHE Claude committed
204
    provers_stats s provers th;
205
    let provers =
206
      Hprover.fold (fun _ pr acc -> pr :: acc) provers []
207 208
    in
    let provers = List.sort Whyconf.Prover.compare provers in
209 210
    let name =
      try
MARCHE Claude's avatar
MARCHE Claude committed
211
        let (l,t,_) = Theory.restore_path (theory_name th) in
212
        String.concat "." ([fn]@l@[t])
MARCHE Claude's avatar
MARCHE Claude committed
213
      with Not_found -> fn ^ "." ^ (theory_name th).Ident.id_string
214 215
    in
    fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": "
MARCHE Claude's avatar
MARCHE Claude committed
216
      (color_of_status ~dark:true) (th_proved s th)
217
      name;
MARCHE Claude's avatar
MARCHE Claude committed
218 219 220
    if th_proved s th then
      fprintf fmt "fully verified in %%.02f s"
    else fprintf fmt "not fully verified";
221
    fprintf fmt "</font></h2>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
222

223
    fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
MARCHE Claude's avatar
MARCHE Claude committed
224
    (* fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>"; *)
225 226 227 228
    List.iter
      (fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
      provers;
    fprintf fmt "</td></tr>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
229
    List.iter (print_goal fmt s true 1 depth provers) (theory_goals th);
230 231
    fprintf fmt "</table>@\n"

MARCHE Claude's avatar
MARCHE Claude committed
232
  let print_file s fmt f =
233
    (* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
MARCHE Claude's avatar
MARCHE Claude committed
234
    let fn = Filename.basename (file_name f) in
235
    let fn = Filename.chop_extension fn in
236
    fprintf fmt "%a"
MARCHE Claude's avatar
MARCHE Claude committed
237
      (Pp.print_list Pp.newline (print_theory s fn)) (file_theories f)
238 239 240 241

  let print_session name fmt s =
    fprintf fmt "<h1>Why3 Proof Results for Project \"%s\"</h1>@\n" name;
    fprintf fmt "%a"
MARCHE Claude's avatar
MARCHE Claude committed
242 243
      (Pp.print_iter2 Stdlib.Hstr.iter Pp.newline Pp.nothing Pp.nothing
         (print_file s)) (get_files s)
244 245


246 247 248 249 250 251 252 253 254 255 256
  let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\
<title>Why3 session of %s</title>\
</head>\
<body>\
%a\
</body>\
</html>\
257 258 259 260 261 262 263 264
"

  let run_one = run_file context print_session

end



265 266 267
module Simple =
struct

268
  let print_prover = Whyconf.print_prover
269 270

  let print_proof_status fmt = function
MARCHE Claude's avatar
MARCHE Claude committed
271 272 273 274 275
    | None -> fprintf fmt "No result"
    | Some res -> fprintf fmt "Done: %a" Call_provers.print_prover_result res

  let print_proof_attempt s fmt pa =
    let pa = get_proof_attempt_node s pa in
276
    fprintf fmt "<li>%a : %a</li>"
MARCHE Claude's avatar
MARCHE Claude committed
277
      print_prover pa.prover
278 279
      print_proof_status pa.proof_state

MARCHE Claude's avatar
MARCHE Claude committed
280 281 282
  let rec print_transf s fmt tr =
    let name = (get_transf_name s tr) ^
                 (String.concat "" (get_transf_args s tr)) in
283
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
MARCHE Claude's avatar
MARCHE Claude committed
284 285
      name
      (Pp.print_list Pp.newline (print_goal s)) (get_sub_tasks s tr)
286

MARCHE Claude's avatar
MARCHE Claude committed
287
  and print_goal s fmt g =
288
    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
MARCHE Claude's avatar
MARCHE Claude committed
289 290 291 292 293 294 295 296
      (get_proof_name s g).Ident.id_string
      (Pp.print_iter2 Hprover.iter Pp.newline Pp.nothing
         Pp.nothing (print_proof_attempt s))
      (get_proof_attempt_ids s g)
      (Pp.print_iter1 List.iter Pp.newline (print_transf s))
      (get_transformations s g)

  let print_theory s fmt th =
297
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
MARCHE Claude's avatar
MARCHE Claude committed
298 299
      (theory_name th).Ident.id_string
      (Pp.print_list Pp.newline (print_goal s)) (theory_goals th)
300

MARCHE Claude's avatar
MARCHE Claude committed
301
  let print_file s fmt f =
302
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
MARCHE Claude's avatar
MARCHE Claude committed
303 304
      (file_name f)
      (Pp.print_list Pp.newline (print_theory s)) (file_theories f)
305 306 307

  let print_session _name fmt s =
    fprintf fmt "<ul>%a</ul>"
MARCHE Claude's avatar
MARCHE Claude committed
308 309
      (Pp.print_iter2 Stdlib.Hstr.iter Pp.newline Pp.nothing Pp.nothing
         (print_file s)) (get_files s)
310 311


312 313 314 315 316 317 318 319 320 321 322
  let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\
<title>Why3 session of %s</title>\
</head>\
<body>\
%a\
</body>\
</html>\
323
"
324

325
  let run_one = run_file context print_session
326

327
end
328

329

330
let run () =
331
  let _,_,should_exit1 = read_env_spec () in
332
  if should_exit1 then exit 1;
333 334 335
  match !opt_style with
    | Table -> iter_files Table.run_one
    | SimpleTree -> iter_files Simple.run_one
336 337 338

let cmd =
  { cmd_spec = spec;
339
    cmd_desc = "output session in HTML format";
340 341 342
    cmd_name = "html";
    cmd_run  = run;
  }
343 344 345 346 347 348 349


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