New option for why3session latex

src/why3session/why3session_latex.ml

@@ -29,6 +29,14 @@ module S = Session
 let opt_style = ref 1
 let opt_output_dir = ref ""
 let opt_longtable = ref false
+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
 
 let spec =
   ("-style",
@@ -36,7 +44,10 @@ let spec =
    "<n> sets output style (1 or 2, default 1)") ::
   ("-o",
    Arg.Set_string opt_output_dir,
-   "<path> where to produce LaTeX files (default: session dir)") ::
+   "<dir> where to produce LaTeX files (default: session dir)") ::
+  ("-e", 
+   Arg.String add_element,
+   "<path> produce a table for the element denoted by <path>") ::
   ("-longtable",
    Arg.Set opt_longtable,
    " use 'longtable' environment instead of 'tabular'") ::
@@ -55,7 +66,11 @@ and goal_depth g =
 let theory_depth t =
   List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
 
-let rec provers_latex_stats provers theory =
+let provers_latex_stats_goal provers goal =
+  S.goal_iter_proof_attempt (fun a ->
+    Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) goal
+
+let provers_latex_stats provers theory =
   S.theory_iter_proof_attempt (fun a ->
     Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
 
@@ -78,6 +93,30 @@ let column n depth provers =
   else
     (List.length provers) +  1
 
+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}";
+  fprintf fmt "{| l |";
+  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
+  fprintf fmt "}@.";
+  print_head n depth provers fmt
+
+let print_tabular_foot fmt =
+  fprintf fmt "\\hline \\end{tabular}@."
+
 
 let print_result_prov proofs prov fmt=
   List.iter (fun p ->
@@ -174,64 +213,52 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
 
 
 let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
-  let column = column 2 depth prov
-  in
-    if depth > 0 then
-      fprintf fmt "\\cline{%d-%d} @." 2 column
-    else
-      fprintf fmt "\\hline @.";
-    for i = 1 to depth do fprintf fmt "\\quad" done;
-    if (depth <= 1) then
-      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
-    else
-      fprintf fmt "\\explanation{%d} " (subgoal + 1);
-    let proofs = g.S.goal_external_proofs in
-      if (S.PHprover.length proofs) > 0 then
-	print_result_prov proofs prov fmt;
-      let tr = g.S.goal_transformations in
-	if S.PHstr.length tr > 0 then
-	  begin
-	    if (S.PHprover.length proofs == 0) then
-	      fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
-                (List.length prov);
-	    S.PHstr.iter (fun _st tr ->
-		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
-	else
-	  if (S.PHprover.length proofs) == 0 then
-	    fprintf fmt "\\\\ @."
+  let column = column 2 depth prov in
+  if depth > 0 then
+    fprintf fmt "\\cline{%d-%d} @." 2 column
+  else
+    fprintf fmt "\\hline @.";
+  for i = 1 to depth do fprintf fmt "\\quad" done;
+  if (depth <= 1) then
+    fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
+  else
+    fprintf fmt "\\explanation{%d} " (subgoal + 1);
+  let proofs = g.S.goal_external_proofs in
+  if (S.PHprover.length proofs) > 0 then
+    print_result_prov proofs prov fmt;
+  let tr = g.S.goal_transformations in
+  if S.PHstr.length tr > 0 then
+    begin
+      if (S.PHprover.length proofs == 0) then
+	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
+          (List.length prov);
+      S.PHstr.iter (fun _st tr ->
+	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
+  else
+    if (S.PHprover.length proofs) == 0 then
+      fprintf fmt "\\\\ @."
 
 
-let print_head n depth provers fmt =
+let latex_tabular_goal n fmt depth provers g =
+  print_tabular_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)
+    goal_latex_stat fmt provers 0 depth 0 g
   else
-    fprintf fmt "\\hline Proof obligations ";
-  List.iter (fun a -> fprintf fmt "& \\provername{%a} " Whyconf.print_prover a)
-    provers;
-  fprintf fmt "\\\\ @."
-
+    goal_latex2_stat fmt provers 0 depth  0 g;
+  print_tabular_foot fmt
 
 let latex_tabular n fmt depth provers t =
-fprintf fmt "\\begin{tabular}";
-fprintf fmt "{| l |";
-  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
-  fprintf fmt "}@.";
-  print_head n depth provers fmt;
+  print_tabular_head n depth provers fmt;
   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 \\end{tabular}@."
+  print_tabular_foot fmt
 
 
 let latex_longtable n fmt depth name provers t=
@@ -282,9 +309,83 @@ let theory_latex_stat n table dir t =
 let file_latex_stat n table  dir f =
    List.iter (theory_latex_stat n table dir) f.S.file_theories
 
+let standalone_goal_latex_stat n _table dir g =
+  let provers = Hashtbl.create 9 in
+  provers_latex_stats_goal provers g;
+  let provers = Hashtbl.fold (fun _ pr acc -> pr :: acc)
+    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
+
+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 =
+          List.map (fun g -> (g.S.goal_name.Ident.id_string,g)) 
+            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
+    | [] -> file_latex_stat n table dir f
+    | 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;
+  match Str.split (Str.regexp "|") e with
+    | [] -> ()
+    | f :: r ->
+      try
+        let f = S.PHstr.find files f in
+        element_latex_stat_file f n table dir r
+      with Not_found ->
+        eprintf "Warning: file not found in path: %s@." f
+
 let print_latex_statistics n table dir session =
   let files = session.S.session_files in
-  S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
+  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