Commit 57ced03b authored by MARCHE Claude's avatar MARCHE Claude

load xml database, but without merge

parent e356453a
...@@ -428,7 +428,10 @@ let init = ...@@ -428,7 +428,10 @@ let init =
(match g.M.goal_expl with (match g.M.goal_expl with
| None -> g.M.goal_name | None -> g.M.goal_name
| Some s -> s) | Some s -> s)
| M.Theory th -> th.M.theory.Theory.th_name.Ident.id_string | M.Theory th -> th.M.theory_name
(*
th.M.theory.Theory.th_name.Ident.id_string
*)
| M.File f -> Filename.basename f.M.file_name | M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a -> let p = a.M.prover in | M.Proof_attempt a -> let p = a.M.prover in
p.Session.prover_name ^ " " ^ p.Session.prover_version p.Session.prover_name ^ " " ^ p.Session.prover_version
...@@ -483,6 +486,7 @@ let () = ...@@ -483,6 +486,7 @@ let () =
Unix.mkdir project_dir 0o777 Unix.mkdir project_dir 0o777
end end
let () = let () =
let dbfname = Filename.concat project_dir "project.xml" in let dbfname = Filename.concat project_dir "project.xml" in
try try
...@@ -673,6 +677,7 @@ let (_ : GMenu.image_menu_item) = ...@@ -673,6 +677,7 @@ let (_ : GMenu.image_menu_item) =
let exit_function () = let exit_function () =
eprintf "saving IDE config file@."; eprintf "saving IDE config file@.";
save_config (); save_config ();
(*
eprintf "saving session (testing only)@."; eprintf "saving session (testing only)@.";
begin begin
M.test_save (); M.test_save ();
...@@ -690,6 +695,8 @@ let exit_function () = ...@@ -690,6 +695,8 @@ let exit_function () =
end; end;
let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
if ret = 0 then eprintf "DTD validation succeeded, good!@."; if ret = 0 then eprintf "DTD validation succeeded, good!@.";
*)
M.save_session ();
GMain.quit () GMain.quit ()
let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function
...@@ -1067,22 +1074,26 @@ and color_t_locs () t = ...@@ -1067,22 +1074,26 @@ and color_t_locs () t =
Term.t_fold color_t_locs color_f_locs () t Term.t_fold color_t_locs color_f_locs () t
let scroll_to_source_goal g = let scroll_to_source_goal g =
let t = g.M.task in try
let id = (Task.task_goal t).Decl.pr_name in let t = M.get_task g in
scroll_to_id id; let id = (Task.task_goal t).Decl.pr_name in
match t with scroll_to_id id;
| Some match t with
{ Task.task_decl = | Some
{ Theory.td_node = { Task.task_decl =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} -> { Theory.td_node =
color_f_locs () f Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
| _ -> color_f_locs () f
assert false | _ ->
assert false
with Not_found -> ()
let scroll_to_theory th = let scroll_to_theory th =
let t = th.M.theory in try
let id = t.Theory.th_name in let t = M.get_theory th in
scroll_to_id id let id = t.Theory.th_name in
scroll_to_id id
with Not_found -> ()
(* to be run when a row in the tree view is selected *) (* to be run when a row in the tree view is selected *)
let select_row p = let select_row p =
...@@ -1097,7 +1108,7 @@ let select_row p = ...@@ -1097,7 +1108,7 @@ let select_row p =
scroll_to_source_goal g scroll_to_source_goal g
| _ -> assert false | _ -> assert false
in in
M.apply_transformation ~callback intro_transformation g.M.task M.apply_transformation ~callback intro_transformation (M.get_task g)
| M.Theory th -> | M.Theory th ->
task_view#source_buffer#set_text ""; task_view#source_buffer#set_text "";
......
...@@ -134,7 +134,7 @@ and goal = ...@@ -134,7 +134,7 @@ and goal =
{ goal_name : string; { goal_name : string;
goal_expl : string option; goal_expl : string option;
parent : goal_parent; parent : goal_parent;
task: Task.task; task: Task.task option;
goal_key : O.key; goal_key : O.key;
mutable proved : bool; mutable proved : bool;
external_proofs: (string, proof_attempt) Hashtbl.t; external_proofs: (string, proof_attempt) Hashtbl.t;
...@@ -150,7 +150,8 @@ and transf = ...@@ -150,7 +150,8 @@ and transf =
} }
and theory = and theory =
{ theory : Theory.theory; { theory_name : string;
theory : Theory.theory option;
theory_key : O.key; theory_key : O.key;
theory_parent : file; theory_parent : file;
mutable goals : goal list; mutable goals : goal list;
...@@ -171,10 +172,20 @@ type any = ...@@ -171,10 +172,20 @@ type any =
| Proof_attempt of proof_attempt | Proof_attempt of proof_attempt
| Transformation of transf | Transformation of transf
let get_theory t =
match t.theory with
| None -> raise Not_found
| Some t -> t
let get_task g =
match g.task with
| None -> raise Not_found
| Some t -> t
let all_files : file list ref = ref [] let all_files : file list ref = ref []
let get_all_files () = !all_files let get_all_files () = !all_files
(************************) (************************)
(* saving state on disk *) (* saving state on disk *)
(************************) (************************)
...@@ -220,7 +231,8 @@ and save_trans fmt _ t = ...@@ -220,7 +231,8 @@ and save_trans fmt _ t =
fprintf fmt "</transf>@\n" fprintf fmt "</transf>@\n"
let save_theory fmt t = let save_theory fmt t =
fprintf fmt "@[<v 1><theory name=\"%s\" verified=\"%b\">@\n" "todo" t.verified; fprintf fmt "@[<v 1><theory name=\"%s\" verified=\"%b\">@\n"
t.theory_name t.verified;
List.iter (save_goal fmt) t.goals; List.iter (save_goal fmt) t.goals;
fprintf fmt "</theory>@]@\n" fprintf fmt "</theory>@]@\n"
...@@ -246,21 +258,15 @@ let test_save () = save "essai.xml" ...@@ -246,21 +258,15 @@ let test_save () = save "essai.xml"
let test_load () = Xml.from_file "essai.xml" let test_load () = Xml.from_file "essai.xml"
(****************************)
(* session opening *)
(****************************)
let init_fun = ref (fun (_:O.key) (_:any) -> ())
let notify_fun = ref (fun (_:any) -> ())
let open_session ~init ~notify _ =
init_fun := init; notify_fun := notify
(************************) (************************)
(* actions *) (* actions *)
(************************) (************************)
let init_fun = ref (fun (_:O.key) (_:any) -> ())
let notify_fun = ref (fun (_:any) -> ())
let check_file_verified f = let check_file_verified f =
let b = List.for_all (fun t -> t.verified) f.theories in let b = List.for_all (fun t -> t.verified) f.theories in
if f.file_verified <> b then if f.file_verified <> b then
...@@ -564,7 +570,7 @@ let raw_add_external_proof ~obsolete ~edit g p result = ...@@ -564,7 +570,7 @@ let raw_add_external_proof ~obsolete ~edit g p result =
(* [raw_add_goal parent name expl t] adds a goal to the given parent (* [raw_add_goal parent name expl t] adds a goal to the given parent
DOES NOT record the new goal in its parent, thus this should not be exported DOES NOT record the new goal in its parent, thus this should not be exported
*) *)
let raw_add_goal parent name expl t = let raw_add_goal parent name expl topt =
let parent_key = match parent with let parent_key = match parent with
| Parent_theory mth -> mth.theory_key | Parent_theory mth -> mth.theory_key
| Parent_transf mtr -> mtr.transf_key | Parent_transf mtr -> mtr.transf_key
...@@ -573,7 +579,7 @@ let raw_add_goal parent name expl t = ...@@ -573,7 +579,7 @@ let raw_add_goal parent name expl t =
let goal = { goal_name = name; let goal = { goal_name = name;
goal_expl = expl; goal_expl = expl;
parent = parent; parent = parent;
task = t ; task = topt ;
goal_key = key; goal_key = key;
external_proofs = Hashtbl.create 7; external_proofs = Hashtbl.create 7;
transformations = Hashtbl.create 3; transformations = Hashtbl.create 3;
...@@ -605,10 +611,11 @@ let raw_add_transformation g trans = ...@@ -605,10 +611,11 @@ let raw_add_transformation g trans =
!notify_fun any; !notify_fun any;
tr tr
let raw_add_theory mfile th = let raw_add_theory mfile thopt thname =
let parent = mfile.file_key in let parent = mfile.file_key in
let key = O.create ~parent () in let key = O.create ~parent () in
let mth = { theory = th; let mth = { theory_name = thname;
theory = thopt;
theory_key = key; theory_key = key;
theory_parent = mfile; theory_parent = mfile;
goals = [] ; goals = [] ;
...@@ -621,16 +628,16 @@ let raw_add_theory mfile th = ...@@ -621,16 +628,16 @@ let raw_add_theory mfile th =
let add_theory mfile th = let add_theory mfile name th =
let tasks = List.rev (Task.split_theory th None None) in let tasks = List.rev (Task.split_theory th None None) in
let mth = raw_add_theory mfile th in let mth = raw_add_theory mfile (Some th) name in
let goals = let goals =
List.fold_left List.fold_left
(fun acc t -> (fun acc t ->
let id = (Task.task_goal t).Decl.pr_name in let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in let name = id.Ident.id_string in
let expl = get_explanation id (Task.task_goal_fmla t) in let expl = get_explanation id (Task.task_goal_fmla t) in
let goal = raw_add_goal (Parent_theory mth) name expl t in let goal = raw_add_goal (Parent_theory mth) name expl (Some t) in
goal :: acc) goal :: acc)
[] []
tasks tasks
...@@ -668,8 +675,8 @@ let add_file f theories = ...@@ -668,8 +675,8 @@ let add_file f theories =
let mfile = raw_add_file f in let mfile = raw_add_file f in
let mths = let mths =
List.fold_left List.fold_left
(fun acc (_,_,t) -> (fun acc (_,name,t) ->
let mth = add_theory mfile t in let mth = add_theory mfile name t in
mth :: acc) mth :: acc)
[] theories [] theories
in in
...@@ -682,6 +689,8 @@ let file_exists fn = ...@@ -682,6 +689,8 @@ let file_exists fn =
(**********************************) (**********************************)
(* reload a file *) (* reload a file *)
(**********************************) (**********************************)
...@@ -896,6 +905,58 @@ let () = ...@@ -896,6 +905,58 @@ let () =
*) *)
(****************************)
(* session opening *)
(****************************)
let load_goal mth acc g =
assert (g.Xml.name = "goal");
let gname =
try List.assoc "name" g.Xml.attributes
with Not_found -> assert false
in
let expl =
try Some (List.assoc "expl" g.Xml.attributes)
with Not_found -> None
in
let mg = raw_add_goal (Parent_theory mth) gname expl None in
(* TODO add proofs and transformations *)
mg::acc
let load_theory mf acc th =
assert (th.Xml.name = "theory");
let thname =
try List.assoc "name" th.Xml.attributes
with Not_found -> assert false
in
let mth = raw_add_theory mf None thname in
mth.goals <- List.rev (List.fold_left (load_goal mth) [] th.Xml.elements);
mth::acc
let load_file f =
assert (f.Xml.name = "file");
let fn =
try List.assoc "name" f.Xml.attributes
with Not_found -> assert false
in
let mf = raw_add_file fn in
mf.theories <- List.rev (List.fold_left (load_theory mf) [] f.Xml.elements)
let db_file = ref ""
let open_session ~init ~notify file =
init_fun := init; notify_fun := notify; db_file := file;
try
let l = Xml.from_file file in
List.iter load_file l;
(* TODO reload the files *)
()
with Sys_error _ ->
(* xml does not exist yet *)
()
let save_session () = save !db_file
(*****************************************************) (*****************************************************)
(* method: run a given prover on each unproved goals *) (* method: run a given prover on each unproved goals *)
(*****************************************************) (*****************************************************)
...@@ -928,7 +989,7 @@ let redo_external_proof g a = ...@@ -928,7 +989,7 @@ let redo_external_proof g a =
~debug:false ~timelimit:10 ~memlimit:0 ~debug:false ~timelimit:10 ~memlimit:0
?old ~command:p.command ~driver:p.driver ?old ~command:p.command ~driver:p.driver
~callback ~callback
g.task (get_task g)
let rec prover_on_goal p g = let rec prover_on_goal p g =
let id = p.prover_id in let id = p.prover_id in
...@@ -1047,7 +1108,7 @@ let transformation_on_goal g tr = ...@@ -1047,7 +1108,7 @@ let transformation_on_goal g tr =
let b = let b =
match subgoals with match subgoals with
| [task] -> | [task] ->
let s1 = task_checksum g.task in let s1 = task_checksum (get_task g) in
let s2 = task_checksum task in let s2 = task_checksum task in
(* (*
eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task); eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task);
...@@ -1071,7 +1132,7 @@ let transformation_on_goal g tr = ...@@ -1071,7 +1132,7 @@ let transformation_on_goal g tr =
in in
let goal = let goal =
raw_add_goal (Parent_transf tr) raw_add_goal (Parent_transf tr)
subgoal_name expl subtask subgoal_name expl (Some subtask)
in in
(goal :: acc, count+1) (goal :: acc, count+1)
in in
...@@ -1080,7 +1141,7 @@ let transformation_on_goal g tr = ...@@ -1080,7 +1141,7 @@ let transformation_on_goal g tr =
in in
tr.subgoals <- List.rev goals tr.subgoals <- List.rev goals
in in
apply_transformation ~callback tr g.task apply_transformation ~callback tr (get_task g)
let rec transform_goal_or_children ~context_unproved_goals_only tr g = let rec transform_goal_or_children ~context_unproved_goals_only tr g =
if not g.proved then if not g.proved then
...@@ -1119,7 +1180,11 @@ let transform ~context_unproved_goals_only tr a = ...@@ -1119,7 +1180,11 @@ let transform ~context_unproved_goals_only tr a =
let ft_of_th th = let ft_of_th th =
(Filename.basename th.theory_parent.file_name, (Filename.basename th.theory_parent.file_name,
th.theory.Theory.th_name.Ident.id_string) (*
th.theory.Theory.th_name.Ident.id_string
*)
th.theory_name
)
let rec ft_of_goal g = let rec ft_of_goal g =
match g.parent with match g.parent with
...@@ -1141,7 +1206,7 @@ let edit_proof ~default_editor ~project_dir a = ...@@ -1141,7 +1206,7 @@ let edit_proof ~default_editor ~project_dir a =
*) *)
else else
let g = a.proof_goal in let g = a.proof_goal in
let t = g.task in let t = (get_task g) in
let driver = a.prover.driver in let driver = a.prover.driver in
let file = let file =
match a.edited_as with match a.edited_as with
......
...@@ -84,7 +84,7 @@ module Make(O: OBSERVER) : sig ...@@ -84,7 +84,7 @@ module Make(O: OBSERVER) : sig
{ goal_name : string; { goal_name : string;
goal_expl : string option; goal_expl : string option;
parent : goal_parent; parent : goal_parent;
task: Task.task; task: Task.task option;
goal_key : O.key; goal_key : O.key;
mutable proved : bool; mutable proved : bool;
external_proofs: (string, proof_attempt) Hashtbl.t; external_proofs: (string, proof_attempt) Hashtbl.t;
...@@ -100,7 +100,8 @@ module Make(O: OBSERVER) : sig ...@@ -100,7 +100,8 @@ module Make(O: OBSERVER) : sig
} }
and theory = private and theory = private
{ theory : Theory.theory; { theory_name : string;
theory : Theory.theory option;
theory_key : O.key; theory_key : O.key;
theory_parent : file; theory_parent : file;
mutable goals : goal list; mutable goals : goal list;
...@@ -122,6 +123,10 @@ module Make(O: OBSERVER) : sig ...@@ -122,6 +123,10 @@ module Make(O: OBSERVER) : sig
| Transformation of transf | Transformation of transf
val get_theory : theory -> Theory.theory
val get_task : goal -> Task.task
(*****************************) (*****************************)
(* *) (* *)
(* save/load state *) (* save/load state *)
...@@ -149,11 +154,11 @@ module Make(O: OBSERVER) : sig ...@@ -149,11 +154,11 @@ module Make(O: OBSERVER) : sig
val test_save : unit -> unit val test_save : unit -> unit
val test_load : unit -> Xml.element list val test_load : unit -> Xml.element list
(*
val save_session : unit -> unit val save_session : unit -> unit
(** enforces to save the session state on disk. *) (** enforces to save the session state on disk.
this is not necessary since the session manager handles this itself this it supposed to be called only at exit,
using add_timeout *) since the session manager also performs automatic saving
some time to time *)
val file_exists : string -> bool val file_exists : string -> bool
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
type element = type element =
{ name : string; { name : string;
attributes : (string * Why.Rc.rc_value) list; attributes : (string * string) list;
elements : element list; elements : element list;
} }
......
...@@ -4,11 +4,9 @@ ...@@ -4,11 +4,9 @@
open Lexing open Lexing
open Why.Rc
type element = type element =
{ name : string; { name : string;
attributes : (string * rc_value) list; attributes : (string * string) list;
elements : element list; elements : element list;
} }
...@@ -97,27 +95,32 @@ and attributes groupe_stack element_stack elem acc = parse ...@@ -97,27 +95,32 @@ and attributes groupe_stack element_stack elem acc = parse
and value = parse and value = parse
| space+ | space+
{ value lexbuf } { value lexbuf }
(*
| integer as i | integer as i
{ RCint (int_of_string i) } { RCint (int_of_string i) }
| real as r | real as r
{ RCfloat (float_of_string r) } { RCfloat (float_of_string r) }
*)
| '"' | '"'
{ Buffer.clear buf; { Buffer.clear buf;
string_val lexbuf } string_val lexbuf }
(*
| "true" | "true"
{ RCbool true } { RCbool true }
| "false" | "false"
{ RCbool false } { RCbool false }
| ident as id | ident as id
{ RCident id } { RCident id }
*)
| _ as c | _ as c
{ failwith ("[Xml error] invalid value starting with " ^ String.make 1 c) } { failwith ("[Xml error] invalid value starting with "
^ String.make 1 c) }
| eof | eof
{ failwith "[Xml error] unterminated keyval pair" } { failwith "[Xml error] unterminated keyval pair" }
and string_val = parse and string_val = parse
| '"' | '"'
{ RCstring (Buffer.contents buf) } { Buffer.contents buf }
| [^ '\\' '"'] as c | [^ '\\' '"'] as c
{ Buffer.add_char buf c; { Buffer.add_char buf c;
string_val lexbuf } string_val lexbuf }
......
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