why3session_latex.ml 14.1 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

MARCHE Claude's avatar
MARCHE Claude committed
12
open Format
13
open Why3
MARCHE Claude's avatar
MARCHE Claude committed
14
open Session_itp
15 16
open Why3session_lib

17
module Hprover = Whyconf.Hprover
18

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


(* Statistics in LaTeX*)

MARCHE Claude's avatar
MARCHE Claude committed
49
(*
50
let provers_latex_stats_goal provers goal =
MARCHE Claude's avatar
MARCHE Claude committed
51
  goal_iter_proof_attempt (fun a ->
52
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) goal
53 54

let provers_latex_stats provers theory =
55
  S.theory_iter_proof_attempt (fun a ->
56
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) theory
57

58 59
let provers_latex_stats_file provers file =
  S.file_iter_proof_attempt (fun a ->
60
    Hprover.replace provers a.S.proof_prover a.S.proof_prover) file
MARCHE Claude's avatar
MARCHE Claude committed
61
 *)
62

63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
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

82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
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}";
98 99 100
  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;
101 102 103 104 105 106
  fprintf fmt "}@.";
  print_head n depth provers fmt

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

107

MARCHE Claude's avatar
MARCHE Claude committed
108
let print_result_prov s proofs prov fmt=
109 110
  List.iter (fun p ->
  try
MARCHE Claude's avatar
MARCHE Claude committed
111 112
    let pr = get_proof_attempt_node s (Hprover.find proofs p) in
    let s = pr.proof_state in
113
      match s with
MARCHE Claude's avatar
MARCHE Claude committed
114
	| Some res ->
115 116
	    begin
	      match res.Call_provers.pr_answer with
Claude Marche's avatar
Claude Marche committed
117 118 119 120 121
		| 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 ->
122
                  fprintf fmt "& \\timeout{%ds} "
MARCHE Claude's avatar
MARCHE Claude committed
123
                    pr.limit.Call_provers.limit_time
Claude Marche's avatar
Claude Marche committed
124
		| Call_provers.OutOfMemory ->
125
                  fprintf fmt "& \\outofmemory{%dM} "
MARCHE Claude's avatar
MARCHE Claude committed
126
                    pr.limit.Call_provers.limit_mem
127 128
		| Call_provers.StepLimitExceeded ->
                  fprintf fmt "& \\steplimitexceeded "
Claude Marche's avatar
Claude Marche committed
129 130 131 132 133 134
		| 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
135

136
	    end
MARCHE Claude's avatar
MARCHE Claude committed
137
	| None -> fprintf fmt "(no result)"
138 139 140 141
  with Not_found -> fprintf fmt "& \\noresult") prov;
  fprintf fmt "\\\\ @."


MARCHE Claude's avatar
MARCHE Claude committed
142
let rec goal_latex_stat s fmt prov depth depth_max subgoal g =
143 144 145 146
  let column = column 1 depth prov
  in
    if depth > 0 then
      if subgoal > 0 then
147
	fprintf fmt "\\cline{%d-%d}@." (depth + 1) column
148 149
      else ()
    else
150
      fprintf fmt "\\hline@.";
151 152 153 154 155
    if depth_max > 1 then
      begin
	if subgoal > 0 then
	  begin
	    if(depth < depth_max)  then
156
	      for _i = 1 to depth do
157
                fprintf fmt " & "
158 159
              done
	    else
160
	      for _i = 1 to depth - 1 do
161
                fprintf fmt " & "
162 163 164 165 166
              done
	  end
	else
	  if(depth < depth_max) then
	    if depth > 0 then
167
              fprintf fmt " & "
168 169 170 171
      end
    else
      begin
	if subgoal > 0  then
172
	  for _i = 1 to depth do fprintf fmt " & " done
173
	else
174
	  if depth > 0 then fprintf fmt " & "
175 176
      end;
    if (depth <= 1) then
MARCHE Claude's avatar
MARCHE Claude committed
177 178
      fprintf fmt "\\explanation{%s} "
              (protect (get_proof_name s g).Ident.id_string)
179
    else
180
      fprintf fmt " " ;
MARCHE Claude's avatar
MARCHE Claude committed
181 182
    let proofs = get_proof_attempt_ids s g in
      if (Hprover.length proofs) > 0 then
183 184 185 186
	begin
	  if depth_max <= 1 then
	    begin
	      if depth > 0 then
187
		for _i = depth to (depth_max - depth) do
188
                  fprintf fmt "& " done
189
	      else
190
		for _i = depth to (depth_max - depth - 1) do
191
                  fprintf fmt "& " done
192 193 194
	    end
	  else
	    if depth > 0 then
195
	      for _i = depth to (depth_max - depth - 1) do
196
		fprintf fmt "& " done
197
	    else
198
	      for _i = depth to (depth_max - depth - 2) do
199
		fprintf fmt "& " done;
MARCHE Claude's avatar
MARCHE Claude committed
200
	  print_result_prov s proofs prov fmt;
201
	end;
MARCHE Claude's avatar
MARCHE Claude committed
202 203 204
      let tr = get_transformations s g in
	if List.length tr > 0 then
	  if Hprover.length proofs > 0 then
205
	    fprintf fmt "\\cline{%d-%d}@." (depth + 2) column;
MARCHE Claude's avatar
MARCHE Claude committed
206 207
	List.iter (fun tr ->
          let goals = get_sub_tasks s tr in
208
	  let _ = List.fold_left (fun subgoal g ->
MARCHE Claude's avatar
MARCHE Claude committed
209
              goal_latex_stat s fmt prov (depth + 1) depth_max (subgoal) g;
210 211 212 213
               subgoal + 1) 0 goals in
	    () ) tr


214
let style_2_row fmt ?(transf=false) depth prov subgoal expl=
215
  let column = column 2 depth prov in
216
  if depth > 0 || transf then
217
    fprintf fmt "\\cline{%d-%d}@." 2 column
218
  else
219
    fprintf fmt "\\hline@.";
220
  for _i = 1 to depth do fprintf fmt "\\quad" done;
221 222 223
  let macro = if transf then "transformation" else "explanation" in
  if depth = 0 || transf then
    fprintf fmt "\\%s{%s} " macro expl
224
  else
225
    fprintf fmt "\\subgoal{%s}{%d} " expl (subgoal + 1)
Claude Marche's avatar
Claude Marche committed
226

MARCHE Claude's avatar
MARCHE Claude committed
227 228 229
let rec goal_latex2_stat s fmt prov depth depth_max subgoal g =
  let proofs = get_proof_attempt_ids s g in
  if Hprover.length proofs > 0 then
230
    begin
MARCHE Claude's avatar
MARCHE Claude committed
231 232 233
      style_2_row fmt depth prov subgoal
                  (protect (get_proof_name s g).Ident.id_string);
      print_result_prov s proofs prov fmt
234 235
    end
 else
236
    if (*depth = 0*) true then
237
      begin
MARCHE Claude's avatar
MARCHE Claude committed
238 239
        style_2_row fmt depth prov subgoal
                    (protect (get_proof_name s g).Ident.id_string);
240 241 242
	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
          (List.length prov)
      end;
MARCHE Claude's avatar
MARCHE Claude committed
243 244
  let tr = get_transformations s g in
  if List.length tr > 0 then
245
    begin
MARCHE Claude's avatar
MARCHE Claude committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259
      List.iter
        (fun tr ->
         let name = (get_transf_name s tr) ^
                      (String.concat "" (get_transf_args s tr)) in
         style_2_row fmt ~transf:true (depth+1) prov subgoal
                     (protect name);
	 fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\@."
                 (List.length prov);
	 let goals = get_sub_tasks s tr in
	 let _ = List.fold_left
                   (fun subgoal g ->
	            goal_latex2_stat s fmt prov (depth + 1) depth_max (subgoal) g;
	            subgoal + 1) 0 goals in
	 () ) tr
260
    end
261
 else
MARCHE Claude's avatar
MARCHE Claude committed
262 263
   if (Hprover.length proofs) == 0 && depth <> 0 then
     fprintf fmt "\\\\@."
264

MARCHE Claude's avatar
MARCHE Claude committed
265
let latex_tabular_goal n s fmt depth provers g =
266
  print_tabular_head n depth provers fmt;
267
  if n == 1 then
MARCHE Claude's avatar
MARCHE Claude committed
268
    goal_latex_stat s fmt provers 0 depth 0 g
269
  else
MARCHE Claude's avatar
MARCHE Claude committed
270
    goal_latex2_stat s fmt provers 0 depth  0 g;
271
  print_tabular_foot fmt
272

MARCHE Claude's avatar
MARCHE Claude committed
273
let latex_tabular_aux n s fmt depth provers t =
274
  if n == 1 then
MARCHE Claude's avatar
MARCHE Claude committed
275
    List.iter (goal_latex_stat s fmt provers 0 depth 0) (theory_goals t)
276
  else
MARCHE Claude's avatar
MARCHE Claude committed
277
    List.iter (goal_latex2_stat s fmt provers 0 depth  0) (theory_goals t)
278

MARCHE Claude's avatar
MARCHE Claude committed
279
let latex_tabular n s fmt depth provers t =
280
  print_tabular_head n depth provers fmt;
MARCHE Claude's avatar
MARCHE Claude committed
281
  latex_tabular_aux n s fmt depth provers t;
282 283 284
  print_tabular_foot fmt


MARCHE Claude's avatar
MARCHE Claude committed
285
let latex_tabular_file n s fmt depth provers f =
286
  print_tabular_head n depth provers fmt;
MARCHE Claude's avatar
MARCHE Claude committed
287
  List.iter (latex_tabular_aux n s fmt depth provers) (file_theories f);
288
  print_tabular_foot fmt
289 290


MARCHE Claude's avatar
MARCHE Claude committed
291
let latex_longtable n s fmt depth name provers t=
292 293
  fprintf fmt "\\begin{longtable}";
  fprintf fmt "{| l |";
294
  for _i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
295
  fprintf fmt "}@.";
296
  (* First head *)
297 298
  print_head n depth provers fmt;
  fprintf fmt "\\hline \\endfirsthead @.";
299
  (* Other heads : "Continued... " added *)
300 301 302 303 304
  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 @.";
305
  (* Other foots : "Continued..." added *)
306 307
  fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
308
  (* Last foot : nothing *)
309 310
  fprintf fmt "\\endfoot \\endlastfoot @.";
  if n == 1 then
MARCHE Claude's avatar
MARCHE Claude committed
311
    List.iter (goal_latex_stat s fmt provers 0 depth 0) (theory_goals t)
312
  else
MARCHE Claude's avatar
MARCHE Claude committed
313
    List.iter (goal_latex2_stat s fmt provers 0 depth  0) (theory_goals t);
314 315 316 317
  fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
  fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)


MARCHE Claude's avatar
MARCHE Claude committed
318 319 320
let theory_latex_stat n s table dir t =
  let provers = get_used_provers_theory s t in
  let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
321 322
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
MARCHE Claude's avatar
MARCHE Claude committed
323 324
  let depth = theory_depth s t in
  let name = (theory_name t).Ident.id_string in
325 326 327 328
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
    if table = "tabular" then
      begin
MARCHE Claude's avatar
MARCHE Claude committed
329
      latex_tabular n s fmt depth provers t
330 331
      end
    else
MARCHE Claude's avatar
MARCHE Claude committed
332
      latex_longtable n s fmt depth name provers t;
333 334
    close_out ch

MARCHE Claude's avatar
MARCHE Claude committed
335 336
let file_latex_stat n s table  dir f =
   List.iter (theory_latex_stat n s table dir) (file_theories f)
337

MARCHE Claude's avatar
MARCHE Claude committed
338 339 340
let standalone_goal_latex_stat n s _table dir g =
  let provers = get_used_provers_goal s g in
  let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
341 342
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
MARCHE Claude's avatar
MARCHE Claude committed
343 344 345
  let depth = goal_depth s g in
  let name = (get_proof_name s g).Ident.id_string in
  let ch = open_out (Filename.concat dir (name^".tex")) in
346
  let fmt = formatter_of_out_channel ch in
MARCHE Claude's avatar
MARCHE Claude committed
347
  latex_tabular_goal n s fmt depth provers g;
348 349 350 351 352 353 354 355
(*
  if table = "tabular" then
  begin
  latex_tabular_goal n fmt depth provers g
  end
  else
  latex_longtable_goal n fmt depth name provers g;
*)
MARCHE Claude's avatar
MARCHE Claude committed
356
  close_out ch
357

MARCHE Claude's avatar
MARCHE Claude committed
358 359 360
let file_latex_stat_all n s _table dir f =
  let provers = get_used_provers_file s f in
  let provers = Whyconf.Sprover.fold (fun pr acc -> pr :: acc)
361 362
    provers [] in
  let provers = List.sort Whyconf.Prover.compare provers in
MARCHE Claude's avatar
MARCHE Claude committed
363 364
  let depth = file_depth s f in
  let name = Filename.basename (file_name f) in
365 366
  let ch = open_out (Filename.concat dir(name^".tex")) in
  let fmt = formatter_of_out_channel ch in
MARCHE Claude's avatar
MARCHE Claude committed
367
  latex_tabular_file n s fmt depth provers f;
368 369 370 371 372 373 374 375 376 377 378 379 380
(*
    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



MARCHE Claude's avatar
MARCHE Claude committed
381
let element_latex_stat_goal g n s table dir r =
382 383 384 385 386 387
  begin
    match r with
      | [] -> ()
      | _ ->
        eprintf "Warning: only main goals are supported@.:"
  end;
MARCHE Claude's avatar
MARCHE Claude committed
388
  standalone_goal_latex_stat n s table dir g
389

MARCHE Claude's avatar
MARCHE Claude committed
390
let element_latex_stat_theory s th n table dir e =
391
  match e with
MARCHE Claude's avatar
MARCHE Claude committed
392
    | [] -> theory_latex_stat n s table dir th
393 394 395
    | g :: r ->
      try
        let goals =
MARCHE Claude's avatar
MARCHE Claude committed
396 397 398
          List.map (fun g ->
                    (get_proof_name s g).Ident.id_string,g)
            (theory_goals th)
399 400
        in
        let g = List.assoc g goals in
MARCHE Claude's avatar
MARCHE Claude committed
401
        element_latex_stat_goal g n s table dir r
402 403 404
      with Not_found ->
        eprintf "Warning: goal not found in path: %s@." g

MARCHE Claude's avatar
MARCHE Claude committed
405
let element_latex_stat_file f n s table dir e =
406
  match e with
MARCHE Claude's avatar
MARCHE Claude committed
407
    | [] -> file_latex_stat_all n s table dir f
408 409 410
    | th :: r ->
      try
        let ths =
MARCHE Claude's avatar
MARCHE Claude committed
411 412
          List.map (fun th -> (theory_name th).Ident.id_string,th)
            (file_theories f)
413 414
        in
        let th = List.assoc th ths in
MARCHE Claude's avatar
MARCHE Claude committed
415
        element_latex_stat_theory s th n table dir r
416 417 418 419
      with Not_found ->
        eprintf "Warning: theory not found in path: %s@." th


MARCHE Claude's avatar
MARCHE Claude committed
420
let element_latex_stat files n s table dir e =
421
  eprintf "Element %s@." e;
422
  match Strings.split '.' e with
423 424
    | [] -> ()
    | f :: r ->
425
      let found = ref false in
MARCHE Claude's avatar
MARCHE Claude committed
426
      Stdlib.Hstr.iter
427 428
        (fun fname file ->
          let fname = Filename.basename fname in
429
          let fname = List.hd (Strings.split '.' fname) in
Andrei Paskevich's avatar
Andrei Paskevich committed
430
          if fname = f then
431 432
            begin
              found := true;
MARCHE Claude's avatar
MARCHE Claude committed
433
              element_latex_stat_file file n s table dir r
434 435 436 437
            end)
        files;
      if not !found then
        eprintf "Warning: file not found for element %s@." e
438

439
let print_latex_statistics n table dir session =
MARCHE Claude's avatar
MARCHE Claude committed
440
  let files = get_files session in
441 442
  match !opt_elements with
    | None ->
MARCHE Claude's avatar
MARCHE Claude committed
443
      Stdlib.Hstr.iter (fun _ f -> file_latex_stat n session table dir f) files
444
    | Some l ->
MARCHE Claude's avatar
MARCHE Claude committed
445
      List.iter (element_latex_stat files n session table dir) l
446 447 448 449 450 451



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

let run_one fname =
MARCHE Claude's avatar
MARCHE Claude committed
452 453
  let ses,_ = read_session fname in
  let project_dir = get_dir ses in
454 455 456
  let dir = if !opt_output_dir = "" then project_dir else
      !opt_output_dir
  in
MARCHE Claude's avatar
MARCHE Claude committed
457
  print_latex_statistics !opt_style (table ()) dir ses
458 459

let run () =
MARCHE Claude's avatar
MARCHE Claude committed
460
  let _,_,should_exit1 = read_env_spec () in
461 462 463 464 465 466
  if should_exit1 then exit 1;
  iter_files run_one


let cmd =
  { cmd_spec = spec;
467
    cmd_desc = "output session in LaTeX format";
468
    cmd_name = "latex";
469 470
    cmd_run  = run;
  }