Commit 19294391 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

removed type proof_result of IDE and use Call_provers.result instead

parent d165681f
......@@ -39,6 +39,9 @@
* Encodings and transformations (Andrei+Francois, CADE 2011,
deadline January 2011) DONE
* Why presentation at the IVL workshop of CADE:
(http://research.microsoft.com/en-us/um/people/moskal/boogie2011/)
deadline: May 1st
* Caml code ?
* logic language for talking to provers
** FOL + poly + alg + ind + rec ? + theories
......@@ -58,16 +61,17 @@
* IDE: implement "inline" (use transformation inline_goal)
** partially done
** problem 1: detect that transformation did nothing
** problem 2: reimport form db does apply inline correctly
* IDE: debug "hide proved goals" feature
** suggested solution: replace model + filter_model by a custom model
* IDE: ajouter "invalid" comme cas de resultats de preuve
(utiliser call_provers.proof_result dans gmain)
DONE
* IDE, file names in DB: use only file names relative to the db file (DONE)
=== Roadmap for second release, as early as possible in 2011 ================
=== Roadmap for second release 0.64 ================
* fix local installation
** fix local executables names (DONE)
......@@ -83,6 +87,8 @@
why.conf if they correspond to the default value.
* IDE, file names in DB: use only file names relative to the db file
DONE
=== Roadmap for December 2010 ================================================
......
theory FSet
type elt
type t
logic single elt : t
logic union t t : t
logic mem elt t
(* triggers needed by Alt-Ergo but not Simplify, Z3 or CVC3 *)
axiom Mem_single : forall x y:elt [mem x (single y)].
mem x (single y) <-> x=y
axiom Mem_union : forall x:elt, s1 s2:t [mem x (union s1 s2)].
mem x (union s1 s2) <-> mem x s1 or mem x s2
end
theory Switch
(* useless
type enum_POSITION = Normal | Reverse | Void
*)
use import int.Int
logic in_1_3 (x:int) = 1 <= x <= 3
clone import FSet as S with type elt = int
logic f2 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in previous components'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3
logic f3 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in this component'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3 and
"`Local hypotheses'"
not (m1 = 2) and m1 = 1 and m2 = 2
logic f4 (m1:int) (m2:int) (m3:int) =
"`Check that the invariant (pos$1 = pos & pos$1 = pos) is preserved by the operation - ref 4.4, 5.5'" true
logic f5 (m1:int) (m2:int) (m3:int) =
(mem 1 (union (union (single m1) (single m2)) (single m3)) and
not 2 = m1 and not 2 = m2 and not 2 = m3 and
3 = 1)
or
(mem 2 (union (union (single m1) (single m2)) (single m3)) and
not 1 = m1 and not 1 = m2 and not 1 = m3 and
3=2)
or
((mem 1 (union (union (single m1) (single m2)) (single m3)) ->
mem 2 (union (union (single m1) (single m2)) (single m3))) and
(mem 2 (union (union (single m1) (single m2)) (single m3)) ->
mem 1 (union (union (single m1) (single m2)) (single m3))))
goal estimate1 : forall m1 m2 m3: int (* * POSITION *).
f2 m1 m2 m3 and f3 m1 m2 m3 -> f5 m1 m2 m3
logic f6 (m1:int) (m2:int) (m3:int) =
"`estimate preconditions in this component'"
in_1_3 m1 and in_1_3 m2 and in_1_3 m3 and
"`Local hypotheses'"
not(m1 = 2) and m1 = 1 and m3 = 2
goal estimate2 : forall m1 m2 m3: int (* * POSITION *).
f2 m1 m2 m3 and f6 m1 m2 m3 -> f5 m1 m2 m3
end
\ No newline at end of file
......@@ -468,15 +468,6 @@ let transf_from_name n =
with Not_found -> TransfId.add db n
let status_array = [|
Undone;
Done Call_provers.Valid;
Done Call_provers.Timeout;
Done (Call_provers.Unknown "");
Done (Call_provers.Failure "");
Done Call_provers.Invalid;
Done Call_provers.HighFailure; |]
let int64_from_status = function
| Undone -> 0L
| Done Call_provers.Valid -> 1L
......@@ -486,6 +477,14 @@ let int64_from_status = function
| Done Call_provers.Invalid -> 5L
| Done Call_provers.HighFailure -> 6L
let status_array = [|
Undone;
Done Call_provers.Valid;
Done Call_provers.Timeout;
Done (Call_provers.Unknown "");
Done (Call_provers.Failure "");
Done Call_provers.Invalid;
Done Call_provers.HighFailure; |]
let status_from_int64 i =
try
......
......@@ -73,10 +73,12 @@ val image_remove : GdkPixbuf.pixbuf ref
val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref
val image_invalid : GdkPixbuf.pixbuf ref
val image_timeout : GdkPixbuf.pixbuf ref
val image_unknown : GdkPixbuf.pixbuf ref
val image_failure : GdkPixbuf.pixbuf ref
val image_valid_obs : GdkPixbuf.pixbuf ref
val image_invalid_obs : GdkPixbuf.pixbuf ref
val image_timeout_obs : GdkPixbuf.pixbuf ref
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
......
......@@ -227,23 +227,19 @@ let read_file fn =
module Model = struct
(* TODO: remove, see below *)
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_answer (** external proof attempt done *)
type proof_attempt =
{ prover : prover_data;
proof_goal : goal;
proof_row : Gtk.tree_iter;
proof_db : Db.proof_attempt;
(*
mutable status : proof_attempt_status;
mutable time : float;
mutable output : string;
(* TODO: replace the 3 fields above with
mutable proof_result : Call_provers.prover_result
*)
(* TODO: replace the 3 fields above with *)
mutable proof_state : Scheduler.proof_attempt_status;
(**)
mutable proof_obsolete : bool;
mutable edited_as : string;
}
......@@ -536,23 +532,26 @@ let info_window ?(callback=(fun () -> ())) mt s =
module Helpers = struct
open Model
open Scheduler
let image_of_result ~obsolete result =
match obsolete,result with
| _, Scheduled -> !image_scheduled
| _, Running -> !image_running
| false, Done Call_provers.Valid -> !image_valid
| false, Done Call_provers.Invalid -> !image_unknown (** TODO change *)
| false, Done Call_provers.Timeout -> !image_timeout
| false, Done (Call_provers.Unknown _) -> !image_unknown
| false, Done (Call_provers.Failure _) -> !image_failure
| false, Done Call_provers.HighFailure -> !image_failure
| true, Done Call_provers.Valid -> !image_valid_obs
| true, Done Call_provers.Invalid -> !image_unknown_obs (** TODO change *)
| true, Done Call_provers.Timeout -> !image_timeout_obs
| true, Done (Call_provers.Unknown _) -> !image_unknown_obs
| true, Done (Call_provers.Failure _) -> !image_failure_obs
| true, Done Call_provers.HighFailure -> !image_failure_obs
match result with
| Scheduled -> !image_scheduled
| Running -> !image_running
| InternalFailure _ -> !image_failure
| Done r -> match r.Call_provers.pr_answer with
| Call_provers.Valid ->
if obsolete then !image_valid else !image_valid_obs
| Call_provers.Invalid ->
if obsolete then !image_invalid else !image_invalid_obs
| Call_provers.Timeout ->
if obsolete then !image_timeout else !image_timeout_obs
| Call_provers.Unknown _ ->
if obsolete then !image_unknown else !image_unknown_obs
| Call_provers.Failure _ ->
if obsolete then !image_failure else !image_failure_obs
| Call_provers.HighFailure ->
if obsolete then !image_failure else !image_failure_obs
let set_row_status b row =
if b then
......@@ -588,8 +587,10 @@ module Helpers = struct
let rec check_goal_proved g =
let b1 = Hashtbl.fold
(fun _ a acc -> acc || a.status = Done Call_provers.Valid)
g.external_proofs false
(fun _ a acc -> acc ||
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid} -> true
| _ -> false) g.external_proofs false
in
let b = Hashtbl.fold
(fun _ t acc -> acc || t.transf_proved) g.transformations b1
......@@ -658,23 +659,22 @@ module Helpers = struct
set_proved ~propagate t.parent_goal;
end
let set_proof_status ~obsolete a s time =
a.status <- s;
let set_proof_state ~obsolete a res =
a.proof_state <- res;
let row = a.proof_row in
goals_model#set ~row ~column:status_column
(image_of_result ~obsolete s);
let t = if time > 0.0 then
begin
a.Model.time <- time;
Format.sprintf "%.2f" time
end
else ""
(image_of_result ~obsolete res);
let t = match res with
| Done { Call_provers.pr_time = time } ->
Format.sprintf "%.2f" time
| _ -> ""
in
let t = if obsolete then t ^ " (obsolete)" else t in
goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t
let add_external_proof_row ~obsolete ~edit g p db_proof status time =
let add_external_proof_row ~obsolete ~edit g p db_proof result (*_time*) =
let parent = g.goal_row in
let name = p.prover_name in
let row = goals_model#prepend ~parent () in
......@@ -687,16 +687,21 @@ module Helpers = struct
proof_goal = g;
proof_row = row;
proof_db = db_proof;
(*
status = status;
*)
proof_obsolete = obsolete;
(*
time = time;
output = "";
*)
proof_state = result;
edited_as = edit;
}
in
goals_model#set ~row ~column:index_column (Row_proof_attempt a);
Hashtbl.add g.external_proofs p.prover_id a;
set_proof_status ~obsolete a status time;
set_proof_state ~obsolete a result;
a
......@@ -860,14 +865,20 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Model.Done Call_provers.HighFailure
| Db.Done Call_provers.Valid ->
if not obsolete then proved := true;
Model.Done Call_provers.Valid
| Db.Done a -> Model.Done a
| Db.Undone -> Call_provers.HighFailure
| Db.Done r ->
if r = Call_provers.Valid then
if not obsolete then proved := true;
r
in
let r = { Call_provers.pr_answer = s;
Call_provers.pr_output = "";
Call_provers.pr_time = t;
}
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete ~edit goal p a s t
Helpers.add_external_proof_row ~obsolete ~edit goal p a
(Scheduler.Done r)
in
((* something TODO ?*))
with Not_found ->
......@@ -1078,6 +1089,7 @@ let () =
(* method: run a given prover on each unproved goals *)
(*****************************************************)
(*
let callback_of_callback callback = function
| Scheduler.Scheduled -> callback Model.Scheduled 0. ""
| Scheduler.Running -> callback Model.Running 0. ""
......@@ -1086,10 +1098,12 @@ let callback_of_callback callback = function
| Scheduler.Done r ->
let res = Model.Done r.Call_provers.pr_answer in
callback res r.Call_provers.pr_time r.Call_provers.pr_output
*)
(* q is a queue of proof attempt where to put the new one *)
let redo_external_proof q g a =
let p = a.Model.prover in
(*
let callback result time output =
a.Model.output <- output;
Helpers.set_proof_status ~obsolete:false a result time ;
......@@ -1098,6 +1112,22 @@ let redo_external_proof q g a =
let db_res = match result with
| Model.Scheduled | Model.Running -> Db.Undone
| Model.Done a -> Db.Done a
*)
let callback result (* time output *) =
(* useless: done by set_proof_status
a.Model.proof_state <- result;
*)
Helpers.set_proof_state ~obsolete:false a result (*time*) ;
let db_res, time =
match result with
| Scheduler.Scheduled | Scheduler.Running ->
Db.Undone, 0.0
| Scheduler.InternalFailure _ ->
Db.Done Call_provers.HighFailure, 0.0
| Scheduler.Done r ->
if r.Call_provers.pr_answer = Call_provers.Valid then
Helpers.set_proved ~propagate:true a.Model.proof_goal;
Db.Done r.Call_provers.pr_answer, r.Call_provers.pr_time
in
Db.set_status a.Model.proof_db db_res time
in
......@@ -1110,7 +1140,7 @@ let redo_external_proof q g a =
Scheduler.schedule_some_proof_attempts
~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
?old ~command:p.command ~driver:p.driver
~callback:(callback_of_callback callback)
~callback
g.Model.task q
let rec prover_on_goal q p g =
......@@ -1122,7 +1152,7 @@ let rec prover_on_goal q p g =
let db_prover = Db.prover_from_name id in
let db_pa = Db.add_proof_attempt g.Model.goal_db db_prover in
Helpers.add_external_proof_row ~obsolete:false ~edit:""
g p db_pa Model.Scheduled 0.0) ()
g p db_pa Scheduler.Scheduled) ()
in
redo_external_proof q g a;
Hashtbl.iter
......@@ -1779,7 +1809,12 @@ let select_row p =
task_view#source_buffer#set_text "";
(* scroll_to_file file *)
| Model.Row_proof_attempt a ->
task_view#source_buffer#set_text a.Model.output;
let o =
match a.Model.proof_state with
| Scheduler.Done r -> r.Call_provers.pr_output;
| _ -> "No information available"
in
task_view#source_buffer#set_text o;
scroll_to_source_goal a.Model.proof_goal
| Model.Row_transformation tr ->
task_view#source_buffer#set_text "";
......@@ -1843,10 +1878,10 @@ let edit_selected_row p =
file
| f -> f
in
let old_status = a.Model.status in
Helpers.set_proof_status ~obsolete:false a Model.Running 0.0;
let old_status = a.Model.proof_state in
Helpers.set_proof_state ~obsolete:false a Scheduler.Running;
let callback () =
Helpers.set_proof_status ~obsolete:false a old_status 0.0;
Helpers.set_proof_state ~obsolete:false a old_status;
in
let editor =
match a.Model.prover.editor with
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* TODO:
* when proof attempt is finished and is it the one currently selected,
the new output should be displayed on upper-right window
* when returning from edited proofs: should we run the prover again
immediately ?
* bug trouve par Johannes:
Pour reproduire le bug :
1) Partir d'un répértoire sans fichier de projet
2) Lancer why3db, ajouter un fichier
3) Prouver quelques buts (pas tous)
4) Choisir "Hide Proved Goals"
5) Prouver le reste des buts, la fênetre devient vide
6) Décocher "Hide Proved Goals"
Maintenant, le fichier réapparait dans la liste, mais on ne peut pas le
déplier, donc accéder au sous-buts, stats des appels de prouvers etc ...
Ce n'est pas un bug très grave, parce qu'il suffit de quitter l'ide,
puis le relancer, et là on peut de nouveau déplier le fichier.
* Francois :
- Les temps indiqués sont très bizarre, mais cela doit-être un bug
plus profond, au niveau de l'appel des prouveurs (wall time au lieu
de cpu time?)
- Si on modifie le fichier à droite, les buts ne sont pas marqués
obsolètes ou ajouté à gauche.
*)
open Format
let () =
eprintf "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
eprintf " done.@."
open Why
open Whyconf
open Gconfig
(************************)
(* parsing command line *)
(************************)
let includes = ref []
let file = ref None
let opt_version = ref false
let spec = Arg.align [
("-I",
Arg.String (fun s -> includes := s :: !includes),
"<s> add s to loadpath") ;
(*
("-f",
Arg.String (fun s -> input_files := s :: !input_files),
"<f> add file f to the project (ignored if it is already there)") ;
*)
("-v",
Arg.Set opt_version,
" print version information") ;
]
let version_msg = sprintf "Why3 IDE, version %s (build date: %s)"
Config.version Config.builddate
let usage_str = sprintf
"Usage: %s [options] [<file.why>|<project directory>]"
(Filename.basename Sys.argv.(0))
let set_file f = match !file with
| Some _ ->
raise (Arg.Bad "only one parameter")
| None ->
file := Some f
let () = Arg.parse spec set_file usage_str
let () =
if !opt_version then begin
printf "%s@." version_msg;
exit 0
end
let fname = match !file with
| None ->
Arg.usage spec usage_str;
exit 1
| Some f ->
f
let lang =
let main = get_main () in
let load_path = Filename.concat (datadir main) "lang" in
let languages_manager =
GSourceView2.source_language_manager ~default:true
in
languages_manager#set_search_path
(load_path :: languages_manager#search_path);
match languages_manager#language "why" with
| None ->
Format.eprintf "language file for 'why' not found in directory %s@."
load_path;
exit 1
| Some _ as l -> l
let source_text fname =
let ic = open_in fname in
let size = in_channel_length ic in
let buf = String.create size in
really_input ic buf 0 size;
close_in ic;
buf
(********************************)
(* loading WhyIDE configuration *)
(********************************)
let gconfig =
let c = Gconfig.config in
let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
c.env <- Lexer.create_env loadpath;
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <-
Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
c
let () =
Whyconf.load_plugins (get_main ())
(********************)
(* opening database *)
(********************)
let project_dir, file_to_read =
if Sys.file_exists fname then
begin
if Sys.is_directory fname then
begin
eprintf "Info: found directory '%s' for the project@." fname;
fname, None
end
else
begin
eprintf "Info: found regular file '%s'@." fname;
let d =
try Filename.chop_extension fname
with Invalid_argument _ -> fname
in
eprintf "Info: using '%s' as directory for the project@." d;
d, Some (Filename.concat Filename.parent_dir_name
(Filename.basename fname))
end
end
else
fname, None
let () =
if not (Sys.file_exists project_dir) then
begin
eprintf "Info: '%s' does not exists. Creating directory of that name \
for the project@." project_dir;
Unix.mkdir project_dir 0o777
end
let () =
let dbfname = Filename.concat project_dir "project.db" in
try
Db.init_base dbfname
with e ->
eprintf "Error while opening database '%s'@." dbfname;
eprintf "Aborting...@.";
raise e
let read_file fn =
let fn = Filename.concat project_dir fn in
let theories = Env.read_file gconfig.env fn in
let theories =
Theory.Mnm.fold
(fun name th acc ->
match th.Theory.th_name.Ident.id_origin with
| Ident.User l -> (Loc.extract l,name,th)::acc
| _ -> (Loc.dummy_floc,name,th)::acc)
theories []
in
let theories = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
theories
in theories
(****************)
(* goals widget *)
(****************)
module Model = struct
(* TODO: remove, see below *)