why3session_latex.ml 14.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  *)
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 13 14 15

open Why3
open Why3session_lib
open Format

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

19 20
let opt_style = ref 1
let opt_output_dir = ref ""
21
let opt_longtable = ref false
22 23 24 25 26 27 28 29
let opt_elements = ref None

let add_element s =
  let l = match !opt_elements with
    | None -> [s]
    | Some r -> s :: r
  in
  opt_elements := Some l
30 31

let spec =
32
  ("-style",
33
   Arg.Set_int opt_style,
34
   "<n> set output style (1 or 2, default 1)") ::
35
  ("-o",
36
   Arg.Set_string opt_output_dir,
37
   "<dir> where to produce LaTeX files (default: session dir)") ::
Andrei Paskevich's avatar
Andrei Paskevich committed
38
  ("-e",
39 40
   Arg.String add_element,
   "<path> produce a table for the element denoted by <path>") ::
41 42
  ("-longtable",
   Arg.Set opt_longtable,
MARCHE Claude's avatar
MARCHE Claude committed
43
   " use 'longtable' environment instead of 'tabular'") ::
44
  common_options
45 46 47 48 49 50 51 52 53 54 55 56 57 58


(* Statistics in LaTeX*)

let rec transf_depth tr =
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 tr.S.transf_goals
and goal_depth g =
  S.PHstr.fold
    (fun _st tr depth -> max depth (1 + transf_depth tr))
    g.S.goal_transformations 0

let theory_depth t =
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals

59 60 61 62
let file_depth f =
  List.fold_left (fun depth t -> max depth (theory_depth t)) 0
    f.S.file_theories

63 64
let provers_latex_stats_goal provers goal =
  S.goal_iter_proof_attempt (fun a ->
65
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) goal
66 67

let provers_latex_stats provers theory =
68
  S.theory_iter_proof_attempt (fun a ->
69
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) theory
70

71 72
let provers_latex_stats_file provers file =
  S.file_iter_proof_attempt (fun a ->
73
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) file
74

75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
let protect s =
  let b = Buffer.create 7 in
  for i = 0 to String.length s - 1 do
    match s.[i] with
	'_' -> Buffer.add_string b "\\_"
      | c -> Buffer.add_char b c
  done;
  Buffer.contents b


let column n depth provers =
  if n == 1 then
    if depth > 1 then
      (List.length provers) + depth
    else
      (List.length provers) + depth + 1
  else
    (List.length provers) +  1

94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
let print_head n depth provers fmt =
  if n == 1 then
    if (depth > 1) then
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        depth
    else
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        (depth + 1)
  else
    fprintf fmt "\\hline Proof obligations ";
  List.iter (fun a -> fprintf fmt "& \\provername{%a} " Whyconf.print_prover a)
    provers;
  fprintf fmt "\\\\ @."

let print_tabular_head n depth provers fmt =
  fprintf fmt "\\begin{tabular}";
110 111 112
  fprintf fmt "{|l|";
  for _i = 0 to depth do fprintf fmt "l|" done;
  for _i = 1 to (List.length provers) do fprintf fmt "c|" done;
113 114 115 116 117 118
  fprintf fmt "}@.";
  print_head n depth provers fmt

let print_tabular_foot fmt =
  fprintf fmt "\\hline \\end{tabular}@."

119 120 121 122 123 124 125

let print_result_prov proofs prov fmt=
  List.iter (fun p ->
  try
    let pr = S.PHprover.find proofs p in
    let s = pr.S.proof_state in
      match s with
126
	| Session.Done res ->
127 128
	    begin
	      match res.Call_provers.pr_answer with
Claude Marche's avatar
Claude Marche committed
129 130 131 132 133
		| Call_provers.Valid ->
                  fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
		| Call_provers.Invalid ->
                  fprintf fmt "& \\invalid{%.2f} " res.Call_provers.pr_time
		| Call_provers.Timeout ->
134 135
                  fprintf fmt "& \\timeout{%ds} "
                    (Call_provers.get_time pr.S.proof_limit)
Claude Marche's avatar
Claude Marche committed
136
		| Call_provers.OutOfMemory ->
137 138
                  fprintf fmt "& \\outofmemory{%dM} "
                    (Call_provers.get_mem pr.S.proof_limit)
139 140
		| Call_provers.StepLimitExceeded ->
                  fprintf fmt "& \\steplimitexceeded "
Claude Marche's avatar
Claude Marche committed
141 142 143 144 145 146
		| Call_provers.Unknown _ ->
                  fprintf fmt "& \\unknown{%.2f} " res.Call_provers.pr_time
		| Call_provers.Failure _ ->
                  fprintf fmt "& \\failure "
		| Call_provers.HighFailure ->
                  fprintf fmt "& \\highfailure "
Andrei Paskevich's avatar
Andrei Paskevich committed
147

148
	    end
149
	| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
150 151 152 153
	| Session.Interrupted -> fprintf fmt "& Not yet run"
	| Session.Unedited -> fprintf fmt "& Not yet edited"
	| Session.Scheduled | Session.Running
	| Session.JustEdited -> assert false
154 155 156 157 158 159 160 161 162
  with Not_found -> fprintf fmt "& \\noresult") prov;
  fprintf fmt "\\\\ @."


let rec goal_latex_stat fmt prov depth depth_max subgoal g =
  let column = column 1 depth prov
  in
    if depth > 0 then
      if subgoal > 0 then
163
	fprintf fmt "\\cline{%d-%d}@." (depth + 1) column
164 165
      else ()
    else
166
      fprintf fmt "\\hline@.";
167 168 169 170 171
    if depth_max > 1 then
      begin
	if subgoal > 0 then
	  begin
	    if(depth < depth_max)  then
172
	      for _i = 1 to depth do
173
                fprintf fmt " & "
174 175
              done
	    else
176
	      for _i = 1 to depth - 1 do
177
                fprintf fmt " & "
178 179 180 181 182
              done
	  end
	else
	  if(depth < depth_max) then
	    if depth > 0 then
183
              fprintf fmt " & "
184 185 186 187
      end
    else
      begin
	if subgoal > 0  then
188
	  for _i = 1 to depth do fprintf fmt " & " done
189
	else
190
	  if depth > 0 then fprintf fmt " & "
191 192 193 194
      end;
    if (depth <= 1) then
      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
    else
195
      fprintf fmt " " ;
196 197 198 199 200 201
    let proofs = g.S.goal_external_proofs in
      if (S.PHprover.length proofs) > 0 then
	begin
	  if depth_max <= 1 then
	    begin
	      if depth > 0 then
202
		for _i = depth to (depth_max - depth) do
203
                  fprintf fmt "& " done
204
	      else
205
		for _i = depth to (depth_max - depth - 1) do
206
                  fprintf fmt "& " done
207 208 209
	    end
	  else
	    if depth > 0 then
210
	      for _i = depth to (depth_max - depth - 1) do
211
		fprintf fmt "& " done
212
	    else
213
	      for _i = depth to (depth_max - depth - 2) do
214
		fprintf fmt "& " done;
215 216 217 218 219
	  print_result_prov proofs prov fmt;
	end;
      let tr = g.S.goal_transformations in
	if S.PHstr.length tr > 0 then
	  if S.PHprover.length proofs > 0 then
220
	    fprintf fmt "\\cline{%d-%d}@." (depth + 2) column;
221 222 223 224 225 226 227 228
	S.PHstr.iter (fun _st tr ->
          let goals = tr.S.transf_goals in
	  let _ = List.fold_left (fun subgoal g ->
              goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
               subgoal + 1) 0 goals in
	    () ) tr


229
let style_2_row fmt ?(transf=false) depth prov subgoal expl=
230
  let column = column 2 depth prov in
231
  if depth > 0 || transf then
232
    fprintf fmt "\\cline{%d-%d}@." 2 column
233
  else
234
    fprintf fmt "\\hline@.";
235
  for _i = 1 to depth do fprintf fmt "\\quad" done;
236 237 238
  let macro = if transf then "transformation" else "explanation" in
  if depth = 0 || transf then
    fprintf fmt "\\%s{%s} " macro expl
239
  else
240
    fprintf fmt "\\subgoal{%s}{%d} " expl (subgoal + 1)
Claude Marche's avatar
Claude Marche committed
241 242

let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
243
  let proofs = g.S.goal_external_proofs in
244 245 246 247 248 249
  if S.PHprover.length proofs > 0 then
    begin
      style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
      print_result_prov proofs prov fmt
    end
 else
250
    if (*depth = 0*) true then
251 252 253 254 255
      begin
        style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
          (List.length prov)
      end;
256 257 258 259
  let tr = g.S.goal_transformations in
  if S.PHstr.length tr > 0 then
    begin
      S.PHstr.iter (fun _st tr ->
Andrei Paskevich's avatar
Andrei Paskevich committed
260
        style_2_row fmt ~transf:true (depth+1) prov subgoal
261
          (protect tr.S.transf_name);
262
	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\@."
Claude Marche's avatar
Claude Marche committed
263
          (List.length prov);
264 265 266 267 268 269
	let goals = tr.S.transf_goals in
	let _ = List.fold_left (fun subgoal g ->
	  goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g;
	  subgoal + 1) 0 goals in
	() ) tr
    end
270 271
 else
    if (S.PHprover.length proofs) == 0 && depth <> 0 then
272
      fprintf fmt "\\\\@."
273

274 275
let latex_tabular_goal n fmt depth provers g =
  print_tabular_head n depth provers fmt;
276
  if n == 1 then
277
    goal_latex_stat fmt provers 0 depth 0 g
278
  else
279 280
    goal_latex2_stat fmt provers 0 depth  0 g;
  print_tabular_foot fmt
281

282
let latex_tabular_aux n fmt depth provers t =
283 284 285
  if n == 1 then
    List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
  else
286 287 288 289 290 291 292 293 294 295 296
    List.iter (goal_latex2_stat fmt provers 0 depth  0) t.S.theory_goals

let latex_tabular n fmt depth provers t =
  print_tabular_head n depth provers fmt;
  latex_tabular_aux n fmt depth provers t;
  print_tabular_foot fmt


let latex_tabular_file n fmt depth provers f =
  print_tabular_head n depth provers fmt;
  List.iter (latex_tabular_aux n fmt depth provers) f.S.file_theories;
297
  print_tabular_foot fmt
298 299 300 301 302


let latex_longtable n fmt depth name provers t=
  fprintf fmt "\\begin{longtable}";
  fprintf fmt "{| l |";
303
  for _i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
304
  fprintf fmt "}@.";
305
  (* First head *)
306 307
  print_head n depth provers fmt;
  fprintf fmt "\\hline \\endfirsthead @.";
308
  (* Other heads : "Continued... " added *)
309 310 311 312 313
  fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ;
  fprintf fmt "\\hline @.";
  print_head n depth provers fmt;
  fprintf fmt "\\hline \\endhead @.";
314
  (* Other foots : "Continued..." added *)
315 316
  fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
317
  (* Last foot : nothing *)
318 319 320 321 322 323 324 325 326 327
  fprintf fmt "\\endfoot \\endlastfoot @.";
  if n == 1 then
    List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
  else
    List.iter (goal_latex2_stat fmt provers 0 depth  0) t.S.theory_goals;
  fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
  fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)


let theory_latex_stat n table dir t =
328
  let provers = Hprover.create 9 in
329
  provers_latex_stats provers t;
330
  let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
  let depth = theory_depth  t in
  let name = t.S.theory_name.Ident.id_string in
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
    if table = "tabular" then
      begin
      latex_tabular n fmt depth provers t
      end
    else
      latex_longtable n fmt depth name provers t;
    close_out ch

let file_latex_stat n table  dir f =
   List.iter (theory_latex_stat n table dir) f.S.file_theories

348
let standalone_goal_latex_stat n _table dir g =
349
  let provers = Hprover.create 9 in
350
  provers_latex_stats_goal provers g;
351
  let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
  let depth = goal_depth g in
  let name = g.S.goal_name.Ident.id_string in
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
  latex_tabular_goal n fmt depth provers g;
(*
  if table = "tabular" then
  begin
  latex_tabular_goal n fmt depth provers g
  end
  else
  latex_longtable_goal n fmt depth name provers g;
*)
close_out ch

369
let file_latex_stat_all n _table dir f =
370
  let provers = Hprover.create 9 in
371
  provers_latex_stats_file provers f;
372
  let provers = Hprover.fold (fun _ pr acc -> pr :: acc)
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
  let depth = file_depth f in
  let name = Filename.basename f.S.file_name in
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
  latex_tabular_file n fmt depth provers f;
(*
    if table = "tabular" then
      begin
      latex_tabular n fmt depth provers t
      end
    else
      latex_longtable n fmt depth name provers t;

*)
    close_out ch



393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
let element_latex_stat_goal g n table dir r =
  begin
    match r with
      | [] -> ()
      | _ ->
        eprintf "Warning: only main goals are supported@.:"
  end;
  standalone_goal_latex_stat n table dir g

let element_latex_stat_theory th n table dir e =
  match e with
    | [] -> theory_latex_stat n table dir th
    | g :: r ->
      try
        let goals =
Andrei Paskevich's avatar
Andrei Paskevich committed
408
          List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
409 410 411 412 413 414 415 416 417
            th.S.theory_goals
        in
        let g = List.assoc g goals in
        element_latex_stat_goal g n table dir r
      with Not_found ->
        eprintf "Warning: goal not found in path: %s@." g

let element_latex_stat_file f n table dir e =
  match e with
418
    | [] -> file_latex_stat_all n table dir f
419 420 421 422 423 424 425 426 427 428 429 430 431 432
    | th :: r ->
      try
        let ths =
          List.map (fun th -> (th.S.theory_name.Ident.id_string,th))
            f.S.file_theories
        in
        let th = List.assoc th ths in
        element_latex_stat_theory th n table dir r
      with Not_found ->
        eprintf "Warning: theory not found in path: %s@." th


let element_latex_stat files n table dir e =
  eprintf "Element %s@." e;
433
  match Strings.split '.' e with
434 435
    | [] -> ()
    | f :: r ->
436 437 438 439
      let found = ref false in
      S.PHstr.iter
        (fun fname file ->
          let fname = Filename.basename fname in
440
          let fname = List.hd (Strings.split '.' fname) in
Andrei Paskevich's avatar
Andrei Paskevich committed
441
          if fname = f then
442 443 444 445 446 447 448
            begin
              found := true;
              element_latex_stat_file file n table dir r
            end)
        files;
      if not !found then
        eprintf "Warning: file not found for element %s@." e
449

450 451
let print_latex_statistics n table dir session =
  let files = session.S.session_files in
452 453 454 455 456
  match !opt_elements with
    | None ->
      S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
    | Some l ->
      List.iter (element_latex_stat files n table dir) l
457 458 459 460 461 462 463



let table () = if !opt_longtable then "longtable" else "tabular"

let run_one fname =
  let project_dir = Session.get_project_dir fname in
464
  let session,_use_shapes = Session.read_session project_dir in
465 466 467 468
  let dir = if !opt_output_dir = "" then project_dir else
      !opt_output_dir
  in
  print_latex_statistics !opt_style (table ()) dir session
469 470

let run () =
MARCHE Claude's avatar
MARCHE Claude committed
471
  let _,_,should_exit1 = read_env_spec () in
472 473 474 475 476 477
  if should_exit1 then exit 1;
  iter_files run_one


let cmd =
  { cmd_spec = spec;
478
    cmd_desc = "output session in LaTeX format";
479
    cmd_name = "latex";
480 481
    cmd_run  = run;
  }