Skip to content

GitLab

Commit 9604ca5f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

newmain and runs without errors. transformations still missing

parent 2861844e
Hide whitespace changes
Inline Side-by-side
Makefile.in
View file @ 9604ca5f
......@@ -420,7 +420,7 @@ install_local: bin/why3config
ifeq (@enable_ide@,yes)
IDE_FILES = gconfig db session gmain
IDE_FILES = session gconfig db gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......
src/ide/newmain.ml
View file @ 9604ca5f
......@@ -295,6 +295,7 @@ let name_column = cols#add Gobject.Data.string
let icon_column = cols#add Gobject.Data.gobject
let status_column = cols#add Gobject.Data.gobject
let time_column = cols#add Gobject.Data.string
let index_column = cols#add Gobject.Data.int
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
......@@ -386,11 +387,6 @@ module M = Session.Make
end)
let index_column : M.any GTree.column =
eprintf "index column...@?";
let c = cols#add Gobject.Data.caml in
eprintf " done@."; c
let set_row_status row b =
if b then
begin
......@@ -415,15 +411,40 @@ let set_proof_state ~obsolete a =
let t = if obsolete then t ^ " (obsolete)" else t in
goals_model#set ~row ~column:time_column t
let init row any =
goals_model#set ~row ~column:index_column any;
goals_model#set ~row ~column:icon_column
(match any with
| M.Goal _ -> !image_file
| M.Theory _ | M.File _ -> !image_directory
| M.Proof_attempt _ -> !image_prover
| M.Transformation _ -> !image_transf)
let model_index = Hashtbl.create 17
let get_any row =
try
let row = goals_model#get_iter row in
let idx = goals_model#get ~row ~column:index_column in
Hashtbl.find model_index idx
with Not_found -> invalid_arg "Gmain.get_index"
let init =
let cpt = ref 0 in
fun row any ->
incr cpt;
Hashtbl.add model_index !cpt any;
goals_model#set ~row ~column:index_column !cpt;
goals_model#set ~row ~column:icon_column
(match any with
| M.Goal _ -> !image_file
| M.Theory _
| M.File _ -> !image_directory
| M.Proof_attempt _ -> !image_prover
| M.Transformation _ -> !image_transf);
goals_model#set ~row ~column:name_column
(match any with
| M.Goal g ->
(match g.M.goal_expl with
| None -> g.M.goal_name
| Some s -> s)
| M.Theory th -> th.M.theory.Theory.th_name.Ident.id_string
| M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a -> let p = a.M.prover in
p.prover_name ^ " " ^ p.prover_version
| M.Transformation tr -> Session.transformation_id tr.M.transf)
let notify any =
match any with
| M.Goal g ->
......@@ -892,8 +913,7 @@ let () =
let prover_on_selected_goals pr =
List.iter
(fun row ->
let row = goals_model#get_iter row in
let a = goals_model#get ~row ~column:index_column in
let a = get_any row in
M.run_prover
~context_unproved_goals_only:!context_unproved_goals_only
pr a)
......@@ -907,8 +927,7 @@ let prover_on_selected_goals pr =
let replay_obsolete_proofs () =
List.iter
(fun row ->
let row = goals_model#get_iter row in
let a = goals_model#get ~row ~column:index_column in
let a = get_any row in
M.replay ~context_unproved_goals_only:!context_unproved_goals_only a)
goals_view#selection#get_selected_rows
......@@ -1519,8 +1538,8 @@ let scroll_to_theory th =
(* to be run when a row in the tree view is selected *)
let select_row p =
let row = goals_model#get_iter p in
match goals_model#get ~row ~column:index_column with
let a = get_any p in
match a with
| M.Goal g ->
let t = g.M.task in
let t = match apply_trans intro_transformation t with
......@@ -1557,8 +1576,7 @@ let select_row p =
(*****************************)
let edit_selected_row p =
let row = goals_model#get_iter p in
match goals_model#get ~row ~column:index_column with
match get_any p with
| M.Goal _g ->
()
| M.Theory _th ->
......
src/ide/session.ml
View file @ 9604ca5f
......@@ -21,9 +21,7 @@
open Why
open Format
type prover_data = Gconfig.prover_data
(*
type prover_data =
{ prover_id : string;
prover_name : string;
prover_version : string;
......@@ -32,8 +30,66 @@ type prover_data = Gconfig.prover_data
driver : Driver.driver;
mutable editor : string;
}
type trans =
| Trans_one of Task.task Trans.trans
| Trans_list of Task.task Trans.tlist
(*
let lookup_trans name =
try
let t = Trans.lookup_transform name gconfig.env in
Trans_one t
with Trans.UnknownTrans _ ->
let t = Trans.lookup_transform_l name gconfig.env in
Trans_list t
*)
(*
let trans_list =
["split_goal"; "inline_goal" ; "introduce_premises" ]
let trans_of_name =
let h = Hashtbl.create 13 in
List.iter
(fun n -> Hashtbl.add h n (lookup_trans n))
trans_list;
Hashtbl.find h
let split_transformation = trans_of_name "split_goal"
let inline_transformation = trans_of_name "inline_goal"
let intro_transformation = trans_of_name "introduce_premises"
*)
exception Not_applicable
let apply_trans t task =
match t with
| Trans_one t ->
let t' = Trans.apply t task in
if task == t' then raise Not_applicable; [t']
| Trans_list t ->
match Trans.apply t task with
| [t'] as l -> if task == t' then raise Not_applicable; l
| l -> l
(*
let apply_transformation ~callback t task =
match t with
| Trans_one t ->
let callback t = callback [t] in
Gscheduler.apply_transformation ~callback t task
| Trans_list t ->
Gscheduler.apply_transformation_l ~callback t task
*)
type transformation_data =
{ transformation_name : string;
transformation : trans;
}
let transformation_id t = t.transformation_name
type proof_attempt_status =
| Undone
| Scheduled (** external proof attempt is scheduled *)
......@@ -78,7 +134,8 @@ and goal =
}
and transf =
{ parent_goal : goal;
{ transf : transformation_data;
parent_goal : goal;
mutable transf_proved : bool;
transf_key : O.key;
mutable subgoals : goal list;
......@@ -414,8 +471,10 @@ let raw_add_external_proof ~obsolete ~edit g p result =
edited_as = edit;
}
in
Hashtbl.add g.external_proofs p.Gconfig.prover_name a;
!notify_fun (Proof_attempt a);
Hashtbl.add g.external_proofs p.prover_name a;
let any = Proof_attempt a in
!init_fun key any;
!notify_fun any;
(* !notify_fun (Goal g) ? *)
a
......@@ -438,23 +497,29 @@ let raw_add_goal parent name expl t =
proved = false;
}
in
!notify_fun (Goal goal);
let any = Goal goal in
!init_fun key any;
!notify_fun any;
goal
(* [raw_add_transformation g name adds a transformation to the given goal g
Adds no subgoals, thus this should not be exported
*)
let raw_add_transformation g tr_name =
let raw_add_transformation g trans =
let parent = g.goal_key in
let key = O.create ~parent () in
let tr = { parent_goal = g;
let tr = { transf = trans;
parent_goal = g;
transf_proved = false;
transf_key = key;
subgoals = [];
}
in
Hashtbl.add g.transformations tr_name tr;
Hashtbl.add g.transformations trans.transformation_name tr;
let any = Transformation tr in
!init_fun key any;
!notify_fun any;
tr
let raw_add_theory mfile th =
......@@ -466,14 +531,13 @@ let raw_add_theory mfile th =
goals = [] ;
verified = false }
in
let any = Theory mth in
!init_fun key any;
!notify_fun any;
mth
let add_theory mfile th =
let tasks = List.rev (Task.split_theory th None None) in
let mth = raw_add_theory mfile th in
......@@ -493,13 +557,16 @@ let add_theory mfile th =
mth
let raw_add_file f =
let parent = O.create () in
let key = O.create () in
let mfile = { file_name = f;
file_key = parent;
file_key = key;
theories = [] ;
file_verified = false }
in
all_files := !all_files @ [mfile];
let any = File mfile in
!init_fun key any;
!notify_fun any;
mfile
let add_file f theories =
......@@ -776,12 +843,12 @@ let redo_external_proof g a =
in
schedule_proof_attempt
~debug:false ~timelimit:10 ~memlimit:0
?old ~command:p.Gconfig.command ~driver:p.Gconfig.driver
?old ~command:p.command ~driver:p.driver
~callback
g.task
let rec prover_on_goal p g =
let id = p.Gconfig.prover_id in
let id = p.prover_id in
let a =
try Hashtbl.find g.external_proofs id
with Not_found ->
......@@ -1038,7 +1105,7 @@ let edit_proof ~default_editor ~project_dir a =
else
let g = a.proof_goal in
let t = g.task in
let driver = a.prover.Gconfig.driver in
let driver = a.prover.driver in
let file =
match a.edited_as with
| "" ->
......@@ -1072,7 +1139,7 @@ let edit_proof ~default_editor ~project_dir a =
set_proof_state ~obsolete:false a res
in
let editor =
match a.prover.Gconfig.editor with
match a.prover.editor with
| "" -> default_editor
| s -> s
in
......
src/ide/session.mli
View file @ 9604ca5f
......@@ -21,9 +21,7 @@
open Why
type prover_data = Gconfig.prover_data
(*
type prover_data = private
{ prover_id : string;
prover_name : string;
prover_version : string;
......@@ -32,7 +30,10 @@ type prover_data = Gconfig.prover_data
driver : Driver.driver;
mutable editor : string;
}
*)
type transformation_data
val transformation_id : transformation_data -> string
type proof_attempt_status = private
| Undone
......@@ -85,7 +86,8 @@ module Make(O: OBSERVER) : sig
}
and transf = private
{ parent_goal : goal;
{ transf : transformation_data;
parent_goal : goal;
mutable transf_proved : bool;
transf_key : O.key;
mutable subgoals : goal list;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment