diff --git a/Makefile.in b/Makefile.in index af92aec5f28b6b0efe1675734b2c61558ae9dffe..6fe109bbeec33ba6df4804cc6a61c79967037fd1 100644 --- a/Makefile.in +++ b/Makefile.in @@ -822,9 +822,10 @@ install_local:: bin/why3webserver ############### SESSION_FILES = why3session_lib why3session_info \ + why3session_html \ why3session_main # TODO: why3session_copy why3session_rm why3session_csv why3session_run -# why3session_latex why3session_html why3session_output +# why3session_latex why3session_output SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES)) diff --git a/examples/dijkstra/why3session.xml b/examples/dijkstra/why3session.xml index e824d7cd7e53d47ee53df7dd5093ee4c1632b67f..e9054b7f20c9be16119955e4ed5ac4e9f2ec317e 100644 --- a/examples/dijkstra/why3session.xml +++ b/examples/dijkstra/why3session.xml @@ -3,69 +3,69 @@ "http://why3.lri.fr/why3session.dtd"> - + - - - - - - + + + + + + - - - + + + - + - + - - - - - - + + + + + + - + - + - - - + + + - + - - - + + + - - - - - + + + + + - + @@ -74,141 +74,129 @@ - - - + + + - + - + - - + + - + - + - - - - - + + + + + - + - + - + - + - + - + - - - + + + - + - - + + - + - - - - - + + + + + - + - + - - - - - + + - + - + - - - - - + + + + + - - - + + + - - - - - + + + + + - - - - - + + + + + - + - - - - - - - - - - + @@ -223,19 +211,19 @@ - - - - - - - + + + + + + + - + - + - + @@ -243,50 +231,50 @@ - + - + - + - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - + + + + + + + + + - + @@ -299,7 +287,7 @@ - + @@ -312,30 +300,30 @@ - + - + - + - + - + - + diff --git a/examples/dijkstra/why3shapes.gz b/examples/dijkstra/why3shapes.gz index 3f0597052e8d7c33a80cba57af6586d85679184f..54d021b579c17c3da590b74563fb0661424c2491 100644 Binary files a/examples/dijkstra/why3shapes.gz and b/examples/dijkstra/why3shapes.gz differ diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml index c444184db1162e5142b140ed79043ee44b734d29..b5bf383c83d75fff6e1111fd18ff8a59c27ebb34 100644 --- a/src/why3session/why3session_html.ml +++ b/src/why3session/why3session_html.ml @@ -65,12 +65,12 @@ open Session_itp type context = (string -> - (formatter -> unit session -> unit) -> unit session + (formatter -> session -> unit) -> session -> unit, formatter, unit) format let run_file (context : context) print_session fname = - let project_dir = S.get_project_dir fname in - let session,_use_shapes = S.read_session project_dir in + let ses,_ = read_session fname in + let project_dir = get_dir ses in let output_dir = if !output_dir = "" then project_dir else !output_dir in @@ -81,8 +81,8 @@ let run_file (context : context) print_session fname = in let fmt = formatter_of_out_channel cout in if !opt_context - then fprintf fmt context basename (print_session basename) session - else print_session basename fmt session; + then fprintf fmt context basename (print_session basename) ses + else print_session basename fmt ses; pp_print_flush fmt (); if output_dir <> "-" then close_out cout @@ -91,21 +91,21 @@ module Table = struct - let rec transf_depth tr = + let rec transf_depth s 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)) - (S.goal_transformations g) 1 + (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) - let theory_depth t = + let theory_depth s t = List.fold_left - (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals + (fun depth g -> max depth (goal_depth s g)) 0 (theory_goals t) - let provers_stats provers theory = - S.theory_iter_proof_attempt (fun a -> - Hprover.replace provers a.S.proof_prover a.S.proof_prover) theory + let provers_stats s provers theory = + theory_iter_proof_attempt s (fun a -> + Hprover.replace provers a.prover a.prover) theory let print_prover = Whyconf.print_prover @@ -115,16 +115,16 @@ struct if dark then "008000" else "C0FFC0" else "FF0000") -let print_results fmt provers proofs = +let print_results fmt s provers proofs = List.iter (fun p -> fprintf fmt " + | Some res -> begin match res.Call_provers.pr_answer with | Call_provers.Valid -> @@ -133,10 +133,10 @@ let print_results fmt provers proofs = fprintf fmt "FF0000\">Invalid" | Call_provers.Timeout -> fprintf fmt "FF8000\">Timeout (%ds)" - pr.S.proof_limit.Call_provers.limit_time + pr.limit.Call_provers.limit_time | Call_provers.OutOfMemory -> fprintf fmt "FF8000\">Out Of Memory (%dM)" - pr.S.proof_limit.Call_provers.limit_mem + pr.limit.Call_provers.limit_mem | Call_provers.StepLimitExceeded -> fprintf fmt "FF8000\">Step limit exceeded" | Call_provers.Unknown _ -> @@ -146,81 +146,78 @@ let print_results fmt provers proofs = | Call_provers.HighFailure -> fprintf fmt "FF8000\">High Failure" end - | S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure" - | S.Interrupted -> fprintf fmt "E0E0E0\">Not yet run" - | S.Unedited -> fprintf fmt "E0E0E0\">Not yet edited" - | S.Scheduled | S.Running - | S.JustEdited -> assert false + | None -> fprintf fmt "E0E0E0\">result missing" end; if pr.S.proof_obsolete then fprintf fmt " (obsolete)" with Not_found -> fprintf fmt "E0E0E0\">---" end; fprintf fmt "") provers -let rec num_lines acc tr = +let rec num_lines s acc tr = List.fold_left (fun acc g -> 1 + - PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr) - (goal_transformations g) acc) - acc tr.transf_goals + List.fold_left (fun acc tr -> 1 + num_lines s acc tr) + acc (get_transformations s g)) + acc (get_sub_tasks s tr) - let rec print_transf fmt depth max_depth provers tr = + let rec print_transf fmt s depth max_depth provers tr = fprintf fmt ""; for _i=1 to 0 (* depth-1 *) do fprintf fmt "" done; fprintf fmt "" - (color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified) + (color_of_status ~dark:false) (tn_proved s tr) (max_depth - depth + 1); (* for i=1 to depth-1 do fprintf fmt "    " done; *) - fprintf fmt "%s" tr.transf_name ; + let name = (get_transf_name s tr) ^ + (String.concat "" (get_transf_args s tr)) in + fprintf fmt "%s" name ; for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do fprintf fmt "" done; fprintf fmt "@\n"; - fprintf fmt "  " (num_lines 0 tr); + fprintf fmt "  " (num_lines s 0 tr); let (_:bool) = List.fold_left (fun is_first g -> - print_goal fmt is_first (depth+1) max_depth provers g; + print_goal fmt s is_first (depth+1) max_depth provers g; false) - true tr.transf_goals + true (get_sub_tasks s tr) in () - and print_goal fmt is_first depth max_depth provers g = + and print_goal fmt s is_first depth max_depth provers g = if not is_first then fprintf fmt ""; (* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "" done; *) fprintf fmt "" - (color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g)) + (color_of_status ~dark:false) (pn_proved s g) (max_depth - depth + 1); (* for i=1 to depth-1 do fprintf fmt "    " done; *) - fprintf fmt "%s" (S.goal_user_name g); + fprintf fmt "%s" (get_proof_name s g).Ident.id_string; (* for i=depth to max_depth-1 do fprintf fmt "" done; *) - print_results fmt provers (goal_external_proofs g); + print_results fmt s provers (get_proof_attempt_ids s g); fprintf fmt "@\n"; - PHstr.iter - (fun _ tr -> print_transf fmt depth max_depth provers tr) - (goal_transformations g) + List.iter + (print_transf fmt s depth max_depth provers) + (get_transformations s g) - let print_theory fn fmt th = - let depth = theory_depth th in + let print_theory s fn fmt th = + let depth = theory_depth s th in if depth > 0 then let provers = Hprover.create 9 in - provers_stats provers th; + provers_stats s provers th; let provers = Hprover.fold (fun _ pr acc -> pr :: acc) provers [] in let provers = List.sort Whyconf.Prover.compare provers in let name = try - let (l,t,_) = Theory.restore_path th.theory_name in + let (l,t,_) = Theory.restore_path (theory_name th) in String.concat "." ([fn]@l@[t]) - with Not_found -> fn ^ "." ^ th.theory_name.Ident.id_string + with Not_found -> fn ^ "." ^ (theory_name th).Ident.id_string in fprintf fmt "

Theory \"%s\": " - (color_of_status ~dark:true) (Opt.inhabited th.S.theory_verified) + (color_of_status ~dark:true) (th_proved s th) name; - begin match th.S.theory_verified with - | Some t -> fprintf fmt "fully verified in %.02f s" t - | None -> fprintf fmt "not fully verified" - end; + if th_proved s th then + fprintf fmt "fully verified in %%.02f s" + else fprintf fmt "not fully verified"; fprintf fmt "

@\n"; fprintf fmt "" depth; @@ -229,21 +226,21 @@ let rec num_lines acc tr = (fun pr -> fprintf fmt "" print_prover pr) provers; fprintf fmt "@\n"; - List.iter (print_goal fmt true 1 depth provers) th.theory_goals; + List.iter (print_goal fmt s true 1 depth provers) (theory_goals th); fprintf fmt "
Obligations%a
@\n" - let print_file fmt f = + let print_file s fmt f = (* fprintf fmt "

File %s

@\n" f.file_name; *) - let fn = Filename.basename f.file_name in + let fn = Filename.basename (file_name f) in let fn = Filename.chop_extension fn in fprintf fmt "%a" - (Pp.print_list Pp.newline (print_theory fn)) f.file_theories + (Pp.print_list Pp.newline (print_theory s fn)) (file_theories f) let print_session name fmt s = fprintf fmt "

Why3 Proof Results for Project \"%s\"

@\n" name; fprintf fmt "%a" - (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing - print_file) s.session_files + (Pp.print_iter2 Stdlib.Hstr.iter Pp.newline Pp.nothing Pp.nothing + (print_file s)) (get_files s) let context : context = " fprintf fmt "Not yet run" - | Unedited -> fprintf fmt "Not yet edited" - | JustEdited | Scheduled | Running -> assert false - | Done pr -> fprintf fmt "Done: %a" Call_provers.print_prover_result pr - | InternalFailure exn -> - fprintf fmt "Failure: %a"Exn_printer.exn_printer exn - - let print_proof_attempt fmt pa = + | 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 fprintf fmt "
  • %a : %a
    • " - print_prover pa.proof_prover + print_prover pa.prover print_proof_status pa.proof_state - let rec print_transf fmt tr = + let rec print_transf s fmt tr = + let name = (get_transf_name s tr) ^ + (String.concat "" (get_transf_args s tr)) in fprintf fmt "
  • %s :
      %a
    • " - tr.transf_name - (Pp.print_list Pp.newline print_goal) tr.transf_goals + name + (Pp.print_list Pp.newline (print_goal s)) (get_sub_tasks s tr) - and print_goal fmt g = + and print_goal s fmt g = fprintf fmt "
  • %s :
      %a%a
    • " - (goal_name g).Ident.id_string - (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing - Pp.nothing print_proof_attempt) - (goal_external_proofs g) - (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing - Pp.nothing print_transf) - (goal_transformations g) - - let print_theory fmt th = + (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 = fprintf fmt "
  • %s :
      %a
    • " - th.theory_name.Ident.id_string - (Pp.print_list Pp.newline print_goal) th.theory_goals + (theory_name th).Ident.id_string + (Pp.print_list Pp.newline (print_goal s)) (theory_goals th) - let print_file fmt f = + let print_file s fmt f = fprintf fmt "
  • %s :
      %a
    • " - f.file_name - (Pp.print_list Pp.newline print_theory) f.file_theories + (file_name f) + (Pp.print_list Pp.newline (print_theory s)) (file_theories f) let print_session _name fmt s = fprintf fmt "
      %a
    " - (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing - print_file) s.session_files + (Pp.print_iter2 Stdlib.Hstr.iter Pp.newline Pp.nothing Pp.nothing + (print_file s)) (get_files s) let context : context = "