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

forget all dans pretty

parent 342d141c
......@@ -413,6 +413,7 @@ let print_theory fmt th =
print_th th (print_list newline2 print_tdecl) th.th_decls
let print_task fmt task =
forget_all ();
fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
(print_list newline2 print_tdecl) (task_tdecls task)
......
......@@ -38,36 +38,36 @@ let spec = Arg.align [
let usage_str = "whydb [options] <project name>"
let file = ref None
let set_file f = match !file with
| Some _ ->
| Some _ ->
raise (Arg.Bad "only one file")
| None ->
| None ->
file := Some f
let () = Arg.parse spec set_file usage_str
let fname = match !file with
| None ->
Arg.usage spec usage_str;
| None ->
Arg.usage spec usage_str;
exit 1
| Some f ->
| 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
let languages_manager =
GSourceView2.source_language_manager ~default:true
in
languages_manager#set_search_path
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;
| 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 source_text fname =
let ic = open_in fname in
let size = in_channel_length ic in
let buf = String.create size in
......@@ -79,12 +79,12 @@ let source_text fname =
(* loading WhyIDE configuration *)
(********************************)
let gconfig =
let gconfig =
let c = Gconfig.config in
let loadpath = (get_main ()).loadpath @ List.rev !includes in
c.env <- Env.create_env (Lexer.retrieve loadpath);
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <-
c.provers <-
Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
c
......@@ -93,14 +93,14 @@ let gconfig =
(* opening database *)
(********************)
let () =
let () =
if Sys.file_exists fname then
begin
if not (Sys.is_directory fname) then
begin
eprintf "'%s' is not a directory@." fname;
exit 1
end
begin
eprintf "'%s' is not a directory@." fname;
exit 1
end
end
else
begin
......@@ -113,7 +113,7 @@ let () =
with e ->
Format.eprintf "Error while opening database '%s'@." dbfname;
raise e
(****************)
......@@ -144,7 +144,7 @@ module Model = struct
{ parent : goal_parent;
task: Task.task;
goal_row : Gtk.tree_iter;
goal_db : Db.goal;
goal_db : Db.goal;
mutable proved : bool;
external_proofs: (string, proof_attempt) Hashtbl.t;
mutable transformations : transf list;
......@@ -156,27 +156,27 @@ module Model = struct
transf : Task.task Trans.trans;
*)
transf_row : Gtk.tree_iter;
transf_db : Db.transf;
transf_db : Db.transf;
mutable subgoals : goal list;
}
and theory =
{ theory : Theory.theory;
theory_row : Gtk.tree_iter;
theory_db : Db.theory;
theory_parent : file;
theory_db : Db.theory;
theory_parent : file;
mutable goals : goal list;
mutable verified : bool;
}
and file =
{ file_name : string;
file_row : Gtk.tree_iter;
file_db : Db.file;
mutable theories: theory list;
file_row : Gtk.tree_iter;
file_db : Db.file;
mutable theories: theory list;
mutable file_verified : bool;
}
type any_row =
| Row_file of file
......@@ -185,31 +185,31 @@ module Model = struct
| Row_proof_attempt of proof_attempt
| Row_transformation of transf
let all_files : file list ref = ref []
let all_files : file list ref = ref []
let toggle_hide_proved_goals = ref false
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let icon_column = cols#add Gobject.Data.gobject
let index_column : any_row GTree.column = cols#add Gobject.Data.caml
let index_column : any_row GTree.column = cols#add Gobject.Data.caml
let status_column = cols#add Gobject.Data.gobject
let time_column = cols#add Gobject.Data.string
let visible_column = cols#add Gobject.Data.boolean
(*
let bg_column = cols#add (Gobject.Data.unsafe_boxed
let bg_column = cols#add (Gobject.Data.unsafe_boxed
(Gobject.Type.from_name "GdkColor"))
*)
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
let image_renderer = GTree.cell_renderer_pixbuf [ ]
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
let image_renderer = GTree.cell_renderer_pixbuf [ ]
let icon_renderer = GTree.cell_renderer_pixbuf [ ]
let view_name_column =
let view_name_column =
GTree.view_column ~title:"Theories/Goals" ()
let () =
let () =
view_name_column#pack icon_renderer ;
view_name_column#add_attribute icon_renderer "pixbuf" icon_column ;
view_name_column#pack name_renderer;
......@@ -221,16 +221,16 @@ module Model = struct
*)
()
let view_status_column =
GTree.view_column ~title:"Status"
~renderer:(image_renderer, ["pixbuf", status_column])
let view_status_column =
GTree.view_column ~title:"Status"
~renderer:(image_renderer, ["pixbuf", status_column])
()
let view_time_column =
GTree.view_column ~title:"Time"
let view_time_column =
GTree.view_column ~title:"Time"
~renderer:(renderer, ["text", time_column]) ()
let () =
let () =
view_status_column#set_resizable false;
view_status_column#set_visible true;
view_time_column#set_resizable false;
......@@ -262,52 +262,52 @@ let exit_function () =
save_config ();
GMain.quit ()
let w = GWindow.window
let w = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:gconfig.window_width
~height:gconfig.window_height
~width:gconfig.window_width
~height:gconfig.window_height
~title:"why-db" ()
let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function
let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function
let (_ : GtkSignal.id) =
w#misc#connect#size_allocate
let (_ : GtkSignal.id) =
w#misc#connect#size_allocate
~callback:
(fun {Gtk.width=w;Gtk.height=h} ->
(fun {Gtk.width=w;Gtk.height=h} ->
gconfig.window_height <- h;
gconfig.window_width <- w)
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add ()
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add ()
(* Menu *)
let menubar = GMenu.menu_bar ~packing:vbox#pack ()
let menubar = GMenu.menu_bar ~packing:vbox#pack ()
let factory = new GMenu.factory menubar
let factory = new GMenu.factory menubar
let accel_group = factory#accel_group
let accel_group = factory#accel_group
(* horizontal paned *)
let hp = GPack.paned `HORIZONTAL ~border_width:3 ~packing:vbox#add ()
let hp = GPack.paned `HORIZONTAL ~border_width:3 ~packing:vbox#add ()
(* tree view *)
let scrollview =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
~width:gconfig.tree_width
~packing:hp#add ()
let () = scrollview#set_shadow_type `ETCHED_OUT
let (_ : GtkSignal.id) =
scrollview#misc#connect#size_allocate
let scrollview =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
~width:gconfig.tree_width
~packing:hp#add ()
let () = scrollview#set_shadow_type `ETCHED_OUT
let (_ : GtkSignal.id) =
scrollview#misc#connect#size_allocate
~callback:
(fun {Gtk.width=w;Gtk.height=_h} ->
(fun {Gtk.width=w;Gtk.height=_h} ->
gconfig.tree_width <- w)
let goals_model,filter_model,goals_view =
Model.create ~packing:scrollview#add ()
let task_checksum t =
let task_checksum t =
fprintf str_formatter "%a@." Pretty.print_task t;
let s = flush_str_formatter () in
eprintf "task = %s@." s;
......@@ -320,10 +320,10 @@ let info_window mt s =
~message_type:mt
~buttons:GWindow.Buttons.close
~title:"Why3 info or error"
~show:true ()
~show:true ()
in
let (_ : GtkSignal.id) =
d#connect#response
d#connect#response
~callback:(function `CLOSE | `DELETE_EVENT -> d#destroy ())
in
()
......@@ -337,7 +337,7 @@ module Helpers = struct
| Scheduler.Timeout -> !image_timeout
| Scheduler.Unknown -> !image_unknown
| Scheduler.HighFailure -> !image_failure
open Model
let set_file_verified f =
......@@ -347,7 +347,7 @@ module Helpers = struct
goals_model#set ~row ~column:status_column !image_yes;
if !toggle_hide_proved_goals then
goals_model#set ~row ~column:visible_column false
let set_theory_proved t =
t.verified <- true;
let row = t.theory_row in
......@@ -358,7 +358,7 @@ module Helpers = struct
let f = t.theory_parent in
if List.for_all (fun t -> t.verified) f.theories then
set_file_verified f
let rec set_proved g =
let row = g.goal_row in
g.proved <- true;
......@@ -380,12 +380,12 @@ module Helpers = struct
a.status <- s;
let row = a.proof_row in
goals_model#set ~row ~column:status_column (image_of_result s);
let t = if time > 0.0 then
let t = if time > 0.0 then
begin
a.Model.time <- time;
Format.sprintf "%.2f" time
Format.sprintf "%.2f" time
end
else ""
else ""
in
goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t
......@@ -414,15 +414,15 @@ module Helpers = struct
Hashtbl.add g.external_proofs p.prover_id a;
set_proof_status a status time;
a
let add_goal_row mth name t db_goal =
let parent = mth.theory_row in
let row = goals_model#append ~parent () in
let goal = { parent = Theory mth;
task = t ;
let goal = { parent = Theory mth;
task = t ;
goal_row = row;
goal_db = db_goal;
goal_db = db_goal;
external_proofs = Hashtbl.create 7;
transformations = [];
proved = false;
......@@ -440,12 +440,12 @@ module Helpers = struct
let tname = th.Theory.th_name.Ident.id_string in
let parent = mfile.file_row in
let row = goals_model#append ~parent () in
let mth = { theory = th;
theory_row = row;
theory_db = db_theory;
theory_parent = mfile;
goals = [] ;
verified = false }
let mth = { theory = th;
theory_row = row;
theory_db = db_theory;
theory_parent = mfile;
goals = [] ;
verified = false }
in
goals_model#set ~row ~column:name_column tname;
goals_model#set ~row ~column:icon_column !image_directory;
......@@ -461,25 +461,25 @@ module Helpers = struct
let goals =
List.fold_left
(fun acc t ->
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let sum = task_checksum t in
let db_goal = Db.add_goal db_theory name sum in
let goal = add_goal_row mth name t db_goal in
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let sum = task_checksum t in
let db_goal = Db.add_goal db_theory name sum in
let goal = add_goal_row mth name t db_goal in
goal :: acc)
[]
(List.rev tasks)
in
if goals = [] then set_theory_proved mth;
mth
let add_file_row f dbfile =
let parent = goals_model#append () in
let mfile = { file_name = f;
file_row = parent;
file_db = dbfile;
theories = [] ;
file_verified = false }
let mfile = { file_name = f;
file_row = parent;
file_db = dbfile;
theories = [] ;
file_verified = false }
in
all_files := !all_files @ [mfile];
let name = Filename.basename f in
......@@ -494,11 +494,11 @@ module Helpers = struct
let theories = Env.read_file gconfig.env f in
let dbfile = Db.add_file f in
let mfile = add_file_row f dbfile in
let theories =
Theory.Mnm.fold
let theories =
Theory.Mnm.fold
(fun thname t acc ->
eprintf "Adding theory '%s'@." thname;
let mth = add_theory mfile t in
eprintf "Adding theory '%s'@." thname;
let mth = add_theory mfile t in
mth :: acc
)
theories
......@@ -507,9 +507,9 @@ module Helpers = struct
mfile.theories <- List.rev theories;
if theories = [] then set_file_verified mfile
with e ->
fprintf str_formatter
fprintf str_formatter
"@[Error while reading file@ '%s':@ %a@]" f
Exn_printer.exn_printer e;
Exn_printer.exn_printer e;
let msg = flush_str_formatter () in
info_window `ERROR msg
......@@ -521,8 +521,8 @@ end
let () =
let files = Db.files () in
List.iter
(fun (f,fn) ->
List.iter
(fun (f,fn) ->
eprintf "Reimporting file '%s'@." fn;
let theories = Env.read_file gconfig.env fn in
let mfile = Helpers.add_file_row fn f in
......@@ -536,51 +536,51 @@ let () =
(* on pourrait retrouver l'ordre des theories dans le fichier source
en comparant les locations des idents de ces theories *)
let mth = Helpers.add_theory_row mfile th db_th in
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
(* TODO: remplacer iter2 par un parcours intelligent
en detectant d'eventuelles nouvelles tasks *)
List.iter2
List.iter2
(fun db_goal t ->
let gname = Db.goal_name db_goal in
let taskname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
if gname <> taskname then
begin
eprintf "gname = %s, taskname = %s@." gname taskname;
assert false;
end;
let sum = task_checksum t in
let db_sum = Db.task_checksum db_goal in
if sum <> db_sum then
begin
eprintf "bad checksum for %s: %s <> %s@." gname sum db_sum;
end;
let goal = Helpers.add_goal_row mth gname t db_goal in
let gname = Db.goal_name db_goal in
let taskname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
if gname <> taskname then
begin
eprintf "gname = %s, taskname = %s@." gname taskname;
assert false;
end;
let sum = task_checksum t in
let db_sum = Db.task_checksum db_goal in
if sum <> db_sum then
begin
eprintf "bad checksum for %s: %s <> %s@." gname sum db_sum;
end;
let goal = Helpers.add_goal_row mth gname t db_goal in
let external_proofs = Db.external_proofs db_goal in
Db.Hprover.iter
Db.Hprover.iter
(fun pid a ->
let p =
Util.Mstr.find (Db.prover_name pid) gconfig.provers
let p =
Util.Mstr.find (Db.prover_name pid) gconfig.provers
in
let s,t = Db.status_and_time a in
eprintf "time = %f@." t;
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success -> Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Success -> Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
in
let (_pa : Model.proof_attempt) =
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row goal p a s t
in
((* TODO *))
)
external_proofs
)
goals tasks
)
goals tasks
)
ths;
(* TODO: detecter d'eventuelles nouvelles theories, qui seraient donc
......@@ -594,11 +594,11 @@ let () =
(* set up scheduler *)
(**********************)
let () =
let () =
begin
Scheduler.async := GtkThread.async;
Scheduler.maximum_running_proofs := gconfig.max_running_processes
end
end
(*****************************************************)
(* method: run a given prover on each unproved goals *)
......@@ -624,15 +624,15 @@ let redo_external_proof g a =
(Some (open_in a.Model.edited_as))
in
Scheduler.schedule_proof_attempt
~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
?old ~command:p.command ~driver:p.driver
~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
?old ~command:p.command ~driver:p.driver
~callback
g.Model.task
let rec prover_on_goal p g =
let id = p.prover_id in
let a =
try Hashtbl.find g.Model.external_proofs id
let a =
try Hashtbl.find g.Model.external_proofs id
with Not_found ->
let db_prover = Db.prover_from_name id in
let db_pa = Db.add_proof_attempt g.Model.goal_db db_prover in
......@@ -642,7 +642,7 @@ let rec prover_on_goal p g =
List.iter
(fun t -> List.iter (prover_on_goal p) t.Model.subgoals)
g.Model.transformations
(*
let prover_on_unproved_goals p =
List.iter
......@@ -655,37 +655,37 @@ let prover_on_unproved_goals p =
*)
let rec prover_on_goal_or_children p g =
if not g.Model.proved then
if not g.Model.proved then
begin
match g.Model.transformations with
| [] -> prover_on_goal p g
| l ->
List.iter (fun t ->
List.iter (prover_on_goal_or_children p)
t.Model.subgoals) l
| [] -> prover_on_goal p g
| l ->
List.iter (fun t ->
List.iter (prover_on_goal_or_children p)
t.Model.subgoals) l
end
let prover_on_selected_goal_or_children pr row =
let row = filter_model#get_iter row in
match filter_model#get ~row ~column:Model.index_column with
| Model.Row_goal g ->
prover_on_goal_or_children pr g
| Model.Row_theory th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals
prover_on_goal_or_children pr g
| Model.Row_theory th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals
| Model.Row_file file ->
List.iter
(fun th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals)
file.Model.theories
List.iter
(fun th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals)
file.Model.theories
| Model.Row_proof_attempt a ->
prover_on_goal_or_children pr a.Model.proof_goal
prover_on_goal_or_children pr a.Model.proof_goal
| Model.Row_transformation tr ->
List.iter (prover_on_goal_or_children pr) tr.Model.subgoals
List.iter (prover_on_goal_or_children pr) tr.Model.subgoals
let prover_on_selected_goals pr =
List.iter
(prover_on_selected_goal_or_children pr)
goals_view#selection#get_selected_rows
goals_view#selection#get_selected_rows
(*****************************************************)
(* method: split all unproved goals *)
......@@ -700,7 +700,7 @@ let split_unproved_goals () =
(fun th ->