why3 session with new sessions: restored basic usage of why3 session info

supported options of 'why3 session info: --stats, --graph, --provers
not supported: --tree, --edited-files, --dir

Makefile.in

@@ -821,10 +821,10 @@ install_local:: bin/why3webserver
 # Session
 ###############
 
-SESSION_FILES = why3session_lib why3session_copy why3session_info \
-		why3session_latex why3session_html why3session_rm \
-		why3session_output why3session_run why3session_csv \
+SESSION_FILES = why3session_lib why3session_info \
 		why3session_main
+# TODO: why3session_copy why3session_rm why3session_csv why3session_run
+#       why3session_latex why3session_html  why3session_output
 
 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 

src/session/session_itp.ml

@@ -431,19 +431,15 @@ let rec fold_all_sub_goals_of_proofn s f acc pnid =
 let fold_all_sub_goals_of_theory s f acc th =
   List.fold_left (fold_all_sub_goals_of_proofn s f) acc th.theory_goals
 
-(*
 let theory_iter_proofn s f th =
   fold_all_sub_goals_of_theory s (fun _ -> f) () th
-*)
 
-(*
 let theory_iter_proof_attempt s f th =
   theory_iter_proofn s
     (fun pn -> Hprover.iter (fun _ pan ->
                              let pan = get_proof_attempt_node s pan in
                              f pan)
          pn.proofn_attempts) th
-*)
 
 (**************)
 (* Copy/Paste *)

src/why3session/why3session_copy.ml

@@ -76,6 +76,16 @@ type action =
   | CopyArchive
   | Mod
 
+let print_external_proof fmt p =
+  fprintf fmt "%a - %a (%i, %i, %i)%s%s"
+    Whyconf.print_prover p.prover
+    (Pp.print_option Call_provers.print_prover_result) p.proof_state
+    (p.limit.Call_provers.limit_time)
+    (p.limit.Call_provers.limit_steps)
+    (p.limit.Call_provers.limit_mem)
+    (if p.proof_obsolete then " obsolete" else "")
+    (if false (* p.proof_edited_as <> None*) then " edited" else "")
+
 let rec interactive to_remove =
   eprintf "Do you want to replace the external proof %a (y/n)@."
     print_external_proof to_remove;
@@ -92,6 +102,17 @@ type to_prover =
   | To_prover of prover
   | SameProver
 
+let unknown_to_known_provers provers pu =
+  Mprover.fold (fun pk _ (others,name,version) ->
+    match
+      pk.prover_name = pu.prover_name,
+      pk.prover_version = pu.prover_version,
+      pk.prover_altern = pu.prover_altern with
+        | false, _, _ -> pk::others, name, version
+        | _, false, _ -> others, pk::name, version
+        | _           -> others, name, pk::version
+  ) provers ([],[],[])
+
 let get_to_prover pk session config =
   match pk with
     | Some pk -> To_prover pk
@@ -103,7 +124,7 @@ let get_to_prover pk session config =
       let unknown_provers = Mprover.set_diff provers known_provers in
       let map pu () =
         let _,name,version =
-          Session_tools.unknown_to_known_provers known_provers pu in
+          unknown_to_known_provers known_provers pu in
         match name,version with
           | _,a::_ -> Some a
           | a::_,_ -> Some a
@@ -114,17 +135,18 @@ let get_to_prover pk session config =
 exception NoAlt
 
 let run_one ~action env config filters pk fname =
-  let env_session,_,_ =
+  let cont,_,_ =
     read_update_session ~allow_obsolete:!opt_force_obsolete env config fname in
-  let to_prover = get_to_prover pk env_session.session config in
+  let ses = cont.Controller_itp.controller_session in
+  let to_prover = get_to_prover pk ses config in
   let s = Stack.create () in
-  session_iter_proof_attempt_by_filter filters
-    (fun pr -> Stack.push pr s) env_session.session;
+  session_iter_proof_attempt_by_filter cont filters
+    (fun pr -> Stack.push pr s) ses;
   Stack.iter (fun pr ->
     try
       let prover = match to_prover with To_prover pk -> Some pk
         | Convert mprover ->
-          Some (Mprover.find_exn NoAlt pr.proof_prover mprover)
+          Some (Mprover.find_exn NoAlt pr.prover mprover)
         | SameProver -> None
       in
       let prn = match prover with
@@ -132,7 +154,7 @@ let run_one ~action env config filters pk fname =
         | Some prover ->
       (* If such a prover already exists on the goal *)
           let exists =
-            (PHprover.mem pr.proof_parent.goal_external_proofs prover) in
+            (Hprover.mem pr.parent.goal_external_proofs prover) in
           let replace = not exists || match !opt_replace with
             | Always -> true | Never -> false
             | Interactive ->
@@ -145,7 +167,7 @@ let run_one ~action env config filters pk fname =
               not (Opt.inhabited (proof_verified rm))
           in
           if not replace then raise Exit;
-          copy_external_proof ~keygen ~prover ~env_session pr
+          copy_external_proof ~keygen ~prover ~env_session:cont pr
       in
       if !tobe_obsolete then set_obsolete prn;
       begin match !tobe_archived with

src/why3session/why3session_info.ml

@@ -142,30 +142,30 @@ let update_perf_stats stats ((_,t) as prover_and_time) =
 
 let string_of_prover p = Pp.string_of_wnl print_prover p
 
-let rec stats_of_goal ~root prefix_name stats goal =
+let rec stats_of_goal ~root prefix_name stats cont goal =
+  let ses = cont.Controller_itp.controller_session in
   if root
   then stats.nb_root_goals <- stats.nb_root_goals + 1
   else stats.nb_sub_goals <- stats.nb_sub_goals + 1;
   let proof_list =
-    PHprover.fold
-      (fun prover proof_attempt acc ->
-        match proof_attempt.proof_state with
-          | Done result ->
+    List.fold_left
+      (fun acc pa ->
+        match pa.proof_state with
+          | Some result ->
             begin
               match result.Call_provers.pr_answer with
                 | Call_provers.Valid ->
-                  (prover, result.Call_provers.pr_time) :: acc
+                  (pa.prover, result.Call_provers.pr_time) :: acc
                 | _ ->
                   acc
             end
           | _ -> acc)
-      goal.goal_external_proofs
-      []
+      [] (get_proof_attempts ses goal)
   in
   List.iter (update_perf_stats stats) proof_list;
-  PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations;
-  if not (Opt.inhabited goal.goal_verified) then
-    let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
+  List.iter (stats_of_transf prefix_name stats cont) (get_transformations ses goal);
+  let goal_name = prefix_name ^ (get_proof_name ses goal).Ident.id_string in
+  if not (Controller_itp.pn_proved cont goal) then
     stats.no_proof <- Sstr.add goal_name stats.no_proof
   else
     begin
@@ -175,7 +175,6 @@ let rec stats_of_goal ~root prefix_name stats goal =
         stats.nb_proved_sub_goals <- stats.nb_proved_sub_goals + 1;
       match proof_list with
       | [ (prover, _) ] ->
-        let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
         stats.only_one_proof <-
           Sstr.add
           (goal_name ^ " : " ^ (string_of_prover prover))
@@ -183,77 +182,79 @@ let rec stats_of_goal ~root prefix_name stats goal =
       | _ -> ()
     end
 
-and stats_of_transf prefix_name stats _ transf =
-  let prefix_name = prefix_name ^ transf.transf_name  ^ " / " in
-  List.iter (stats_of_goal ~root:false prefix_name stats) transf.transf_goals
+and stats_of_transf prefix_name stats cont transf =
+  let ses = cont.Controller_itp.controller_session in
+  let prefix_name = prefix_name ^ (get_transf_name ses transf) ^
+                    (String.concat "" (get_transf_args ses transf)) ^ " / " in
+  List.iter (stats_of_goal ~root:false prefix_name stats cont) (get_sub_tasks ses transf)
 
-let stats_of_theory file stats theory =
-  let goals = theory.theory_goals in
-  let prefix_name = file.file_name ^ " / " ^ theory.theory_name.Ident.id_string
+let stats_of_theory file stats cont theory =
+  let goals = theory_goals theory in
+  let prefix_name = file.file_name ^ " / " ^ (theory_name theory).Ident.id_string
     ^  " / " in
-  List.iter (stats_of_goal ~root:true prefix_name stats) goals
+  List.iter (stats_of_goal ~root:true prefix_name stats cont) goals
 
-let stats_of_file stats _ file =
+let stats_of_file stats cont _ file =
   let theories = file.file_theories in
-  List.iter (stats_of_theory file stats) theories
+  List.iter (stats_of_theory file stats cont) theories
 
 
 
-type 'a goal_stat =
-  | No of ('a transf * ('a goal * 'a goal_stat) list) list
-  | Yes of (prover * float) list * ('a transf * ('a goal * 'a goal_stat) list) list
+type goal_stat =
+  | No of (transID * (proofNodeID * goal_stat) list) list
+  | Yes of (prover * float) list * (transID * (proofNodeID * goal_stat) list) list
 
-let rec stats2_of_goal ~nb_proofs g : 'a goal_stat =
+let rec stats2_of_goal ~nb_proofs cont g : goal_stat =
+  let ses = cont.Controller_itp.controller_session in
   let proof_list =
-    PHprover.fold
-      (fun prover proof_attempt acc ->
+    List.fold_left
+      (fun acc proof_attempt ->
         match proof_attempt.proof_state with
-          | Done result ->
+          | Some result ->
             begin
               match result.Call_provers.pr_answer with
                 | Call_provers.Valid ->
-                  (prover, result.Call_provers.pr_time) :: acc
+                  (proof_attempt.prover, result.Call_provers.pr_time) :: acc
                 | _ ->
                   acc
             end
           | _ -> acc)
-      g.goal_external_proofs
-      []
+      [] (get_proof_attempts ses g)
   in
   let l =
-    PHstr.fold
-      (fun _ tr acc ->
-        match stats2_of_transf ~nb_proofs tr with
+    List.fold_left
+      (fun acc tr ->
+        match stats2_of_transf ~nb_proofs cont tr with
           | [] -> acc
           | r -> (tr,List.rev r)::acc)
-      g.goal_transformations
-      []
+      [] (get_transformations ses g)
   in
   if match nb_proofs with
-    | 0 -> not (Opt.inhabited g.goal_verified)
+    | 0 -> not (Controller_itp.pn_proved cont g)
     | 1 -> List.length proof_list = 1
     | _ -> assert false
       then Yes(proof_list,l) else No(l)
 
-and stats2_of_transf ~nb_proofs tr : ('a goal * 'a goal_stat) list =
+and stats2_of_transf ~nb_proofs cont tr : (proofNodeID * goal_stat) list =
+  let ses = cont.Controller_itp.controller_session in
   List.fold_left
     (fun acc g ->
-      match stats2_of_goal ~nb_proofs g with
+      match stats2_of_goal ~nb_proofs cont g with
         | No [] -> acc
         | r -> (g,r)::acc)
-    [] tr.transf_goals
+    [] (get_sub_tasks ses tr)
 
 let print_res ~time fmt (p,t) =
   fprintf fmt "%a" print_prover p;
   if time then fprintf fmt " (%.2f)" t
 
-let rec print_goal_stats ~time depth (g,l) =
+let rec print_goal_stats ~time depth ses (g,l) =
   for _i=1 to depth do printf "  " done;
-  printf "+-- goal %s" g.goal_name.Ident.id_string;
+  printf "+-- goal %s" (get_proof_name ses g).Ident.id_string;
   match l with
     | No l ->
       printf "@\n";
-      List.iter (print_transf_stats ~time (depth+1)) l
+      List.iter (print_transf_stats ~time (depth+1) ses) l
     | Yes(pl,l) ->
       begin
         match pl with
@@ -261,46 +262,49 @@ let rec print_goal_stats ~time depth (g,l) =
           | _ -> printf ": %a@\n"
             (Pp.print_list pp_print_space (print_res ~time)) pl
       end;
-      List.iter (print_transf_stats ~time (depth+1)) l
+      List.iter (print_transf_stats ~time (depth+1) ses) l
 
-and print_transf_stats ~time depth (tr,l) =
+and print_transf_stats ~time depth ses (tr,l) =
   for _i=1 to depth do printf "  " done;
-  printf "+-- transformation %s@\n" tr.transf_name;
-  List.iter (print_goal_stats ~time (depth+1)) l
+  let name = (get_transf_name ses tr) ^
+               (String.concat "" (get_transf_args ses tr)) in
+  printf "+-- transformation %s@\n" name;
+  List.iter (print_goal_stats ~time (depth+1) ses) l
 
-let stats2_of_theory ~nb_proofs th =
+let stats2_of_theory ~nb_proofs cont th =
   List.fold_left
     (fun acc g ->
-      match stats2_of_goal ~nb_proofs g with
+      match stats2_of_goal ~nb_proofs cont g with
         | No [] -> acc
         | r -> (g,r)::acc)
-    [] th.theory_goals
+    [] (theory_goals th)
 
-let print_theory_stats ~time (th,r) =
-  printf "  +-- theory %s@\n" th.theory_name.Ident.id_string;
-  List.iter (print_goal_stats ~time 2) r
+let print_theory_stats ~time ses (th,r) =
+  printf "  +-- theory %s@\n" (theory_name th).Ident.id_string;
+  List.iter (print_goal_stats ~time 2 ses) r
 
-let stats2_of_file ~nb_proofs file =
+let stats2_of_file ~nb_proofs cont file =
   List.fold_left
     (fun acc th ->
-      match stats2_of_theory ~nb_proofs th with
+      match stats2_of_theory ~nb_proofs cont th with
         | [] -> acc
         | r -> (th,List.rev r)::acc)
     [] file.file_theories
 
-let stats2_of_session ~nb_proofs s acc =
-  PHstr.fold
+let stats2_of_session ~nb_proofs cont acc =
+  let ses = cont.Controller_itp.controller_session in
+  Hstr.fold
     (fun _ f acc ->
-      match stats2_of_file ~nb_proofs f with
+      match stats2_of_file ~nb_proofs cont f with
         | [] -> acc
         | r -> (f,List.rev r)::acc)
-    s.session_files acc
+    (get_files ses) acc
 
-let print_file_stats ~time (f,r) =
+let print_file_stats ~time ses (f,r) =
   printf "+-- file %s@\n" f.file_name;
-  List.iter (print_theory_stats ~time) r
+  List.iter (print_theory_stats ~time ses) r
 
-let print_session_stats ~time = List.iter (print_file_stats ~time)
+let print_session_stats ~time ses = List.iter (print_file_stats ~time ses)
 
 
 (*
@@ -322,7 +326,7 @@ let finalize_stats stats =
     stats.prover_avg_time
 *)
 
-let print_stats r0 r1 stats =
+let print_stats ses r0 r1 stats =
   printf "== Number of root goals ==@\n  total: %d  proved: %d@\n@\n"
     stats.nb_root_goals stats.nb_proved_root_goals;
 
@@ -330,12 +334,12 @@ let print_stats r0 r1 stats =
     stats.nb_sub_goals stats.nb_proved_sub_goals;
 
   printf "== Goals not proved ==@\n  @[";
-  print_session_stats ~time:false r0;
+  print_session_stats ~time:false ses r0;
   (* Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof; *)
   printf "@]@\n";
 
   printf "== Goals proved by only one prover ==@\n  @[";
-  print_session_stats ~time:false r1;
+  print_session_stats ~time:false ses r1;
   (* Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof; *)
   printf "@]@\n";
 
@@ -351,29 +355,42 @@ let print_stats r0 r1 stats =
   printf "@]@\n"
 
 
-let run_one stats r0 r1 fname =
-  let project_dir = Server_utils.get_project_dir fname in
-  if !opt_project_dir then printf "%s@." project_dir;
-  let session,_use_shapes = S.read_session project_dir in
+let run_one env config stats r0 r1 fname =
+  let cont,_,_ =
+    read_update_session ~allow_obsolete:false env config fname in
+  let ses = cont.Controller_itp.controller_session in
   let sep = if !opt_print0 then Pp.print0 else Pp.newline in
   if !opt_print_provers then
     printf "%a@."
       (Pp.print_iter1 Sprover.iter sep print_prover)
-      (get_used_provers session);
-  if !opt_print_edited then
-    session_iter_proof_attempt
+      (get_used_provers ses);
+  if !opt_print_edited then begin
+      failwith "option print_edited non implemented" (* TODO *)
+(*    session_iter_proof_attempt
       (fun pr ->
         Opt.iter (fun s -> printf "%s%a" s sep ())
           (get_edited_as_abs session pr))
       session;
+ *)
+    end;
   if !opt_tree_print then
-    printf "%a@." print_session session;
+    begin
+      failwith "option print_tree not implemented"
+(*
+      printf "%a@." print_session ses;
+ *)
+    end;
   if !opt_stats_print || !opt_hist_print then
     begin
       (* fill_prover_data stats session; *)
-      PHstr.iter (stats_of_file stats) session.session_files;
-      r0 := stats2_of_session ~nb_proofs:0 session !r0;
-      r1 := stats2_of_session ~nb_proofs:1 session !r1
+      Hstr.iter (stats_of_file stats cont) (get_files ses);
+      r0 := stats2_of_session ~nb_proofs:0 cont !r0;
+      r1 := stats2_of_session ~nb_proofs:1 cont !r1
+    end;
+  if !opt_stats_print then
+    begin
+      (* finalize_stats stats; *)
+      print_stats ses !r0 !r1 stats
     end
 
 (**** print histograms ******)
@@ -437,16 +454,11 @@ let print_hist stats =
 (****** run on all files  ******)
 
 let run () =
-  let _,_,should_exit1 = read_env_spec () in
+  let env,config,should_exit1 = read_env_spec () in
   if should_exit1 then exit 1;
   let stats = new_proof_stats () in
   let r0 = ref [] and r1 = ref [] in
-  iter_files (run_one stats r0 r1);
-  if !opt_stats_print then
-    begin
-      (* finalize_stats stats; *)
-      print_stats !r0 !r1 stats
-    end;
+  iter_files (run_one env config stats r0 r1);
   if !opt_hist_print then print_hist stats
 
 

src/why3session/why3session_lib.ml

@@ -296,3 +296,11 @@ let ask_yn_nonblock ~callback =
             Buffer.clear b;
             true
       end
+
+
+let get_used_provers session =
+  let sprover = ref Whyconf.Sprover.empty in
+  Session_itp.session_iter_proof_attempt
+    (fun _ pa -> sprover := Whyconf.Sprover.add pa.Session_itp.prover !sprover)
+     session;
+  !sprover

src/why3session/why3session_lib.mli

@@ -88,3 +88,7 @@ val ask_yn : unit -> bool
 val ask_yn_nonblock : callback:(bool -> unit) -> (unit -> bool)
 (** call the callback when an answer have been given,
     return true if it must be retried *)
+
+(**)
+
+val get_used_provers : Session_itp.session -> Whyconf.Sprover.t

src/why3session/why3session_main.ml

@@ -16,6 +16,7 @@ open Why3session_lib
 let cmds =
   [|
     Why3session_info.cmd;
+(*
     Why3session_latex.cmd;
     Why3session_html.cmd;
     Why3session_csv.cmd;
@@ -25,6 +26,7 @@ let cmds =
     Why3session_rm.cmd;
     Why3session_output.cmd;
     Why3session_run.cmd;
+*)
   |]
 
 let exec_name = Filename.basename Sys.argv.(0)