Skip to content

GitLab

why3
why3
Commit e9992947 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

more robust XML loading

parent 2506cf61
Hide whitespace changes
Inline Side-by-side
Showing with 240 additions and 141 deletions
src/ide/newmain.ml
View file @ e9992947
......@@ -491,7 +491,8 @@ let () =
let dbfname = Filename.concat project_dir "project.xml" in
try
eprintf "Opening session...@?";
M.open_session ~provers:gconfig.provers ~init ~notify dbfname;
M.open_session ~env:gconfig.env ~provers:gconfig.provers
~init ~notify dbfname;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf " done@."
with e ->
......@@ -1074,26 +1075,22 @@ and color_t_locs () t =
Term.t_fold color_t_locs color_f_locs () t
let scroll_to_source_goal g =
try
let t = M.get_task g in
let id = (Task.task_goal t).Decl.pr_name in
scroll_to_id id;
match t with
| Some
{ Task.task_decl =
{ Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
color_f_locs () f
| _ ->
assert false
with Not_found -> ()
let t = M.get_task g in
let id = (Task.task_goal t).Decl.pr_name in
scroll_to_id id;
match t with
| Some
{ Task.task_decl =
{ Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
color_f_locs () f
| _ ->
assert false
let scroll_to_theory th =
try
let t = M.get_theory th in
let id = t.Theory.th_name in
scroll_to_id id
with Not_found -> ()
let t = M.get_theory th in
let id = t.Theory.th_name in
scroll_to_id id
(* to be run when a row in the tree view is selected *)
let select_row p =
......
src/ide/session.ml
View file @ e9992947
......@@ -174,12 +174,16 @@ type any =
let get_theory t =
match t.theory with
| None -> raise Not_found
| None ->
eprintf "Session: theory not yet reimported, this should not happen@.";
assert false
| Some t -> t
let get_task g =
match g.task with
| None -> raise Not_found
| None ->
(* TODO: recompute the task from the parent transformation *)
assert false
| Some t -> t
let all_files : file list ref = ref []
......@@ -191,7 +195,7 @@ let get_all_files () = !all_files
(************************)
let save_result fmt r =
fprintf fmt "<result status=\"%s\" time=\"%.2f\"/>@\n"
fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
(match r.Call_provers.pr_answer with
| Call_provers.Valid -> "valid"
| Call_provers.Failure _ -> "failure"
......@@ -207,51 +211,49 @@ let save_status fmt s =
| Done r -> save_result fmt r
let save_proof_attempt fmt _key a =
fprintf fmt "@[<v 1><proof prover=\"%s\" edited=\"%s\">@\n"
fprintf fmt "@\n@[<v 1><proof prover=\"%s\" edited=\"%s\">"
a.prover.prover_id
a.edited_as;
save_status fmt a.proof_state;
fprintf fmt "</proof>@]@\n"
fprintf fmt "@]@\n</proof>"
let opt lab fmt = function
| None -> ()
| Some s -> fprintf fmt "%s=\"%s\" " lab s
let rec save_goal fmt g =
fprintf fmt "@[<v 1><goal name=\"%s\" %aproved=\"%b\">@\n"
fprintf fmt "@\n@[<v 1><goal name=\"%s\" %aproved=\"%b\">"
g.goal_name (opt "expl") g.goal_expl g.proved;
Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
Hashtbl.iter (save_trans fmt) g.transformations;
fprintf fmt "</goal>@]@\n"
fprintf fmt "@]@\n</goal>"
and save_trans fmt _ t =
fprintf fmt "<transf name=\"%s\" proved=\"%b\">@\n"
fprintf fmt "@\n@[<v 1><transf name=\"%s\" proved=\"%b\">"
t.transf.transformation_name t.transf_proved;
List.iter (save_goal fmt) t.subgoals;
fprintf fmt "</transf>@\n"
fprintf fmt "@]@\n</transf>"
let save_theory fmt t =
fprintf fmt "@[<v 1><theory name=\"%s\" verified=\"%b\">@\n"
fprintf fmt "@\n@[<v 1><theory name=\"%s\" verified=\"%b\">"
t.theory_name t.verified;
List.iter (save_goal fmt) t.goals;
fprintf fmt "</theory>@]@\n"
fprintf fmt "@]@\n</theory>"
let save_file fmt f =
fprintf fmt "@[<v 1><file name=\"%s\" verified=\"%b\">@\n" f.file_name f.file_verified;
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\">" f.file_name f.file_verified;
List.iter (save_theory fmt) f.theories;
fprintf fmt "</file>@]@\n"
fprintf fmt "@]@\n</file>"
let save fname =
let ch = open_out fname in
let fmt = formatter_of_out_channel ch in
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
(*
fprintf fmt "@[<v 1><project name=\"%s\">@\n" (Filename.basename fname);
*)
fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
fprintf fmt "@[<v 1><why3session name=\"%s\">" fname;
List.iter (save_file fmt) (get_all_files());
(*
fprintf fmt "</project>@]@.";
*)
fprintf fmt "@]@\n</why3session>";
fprintf fmt "@.";
close_out ch
let test_save () = save "essai.xml"
......@@ -924,7 +926,9 @@ let load_result r =
| "timeout" -> Call_provers.Timeout
| "failure" -> Call_provers.Failure ""
| "highfailure" -> Call_provers.Failure ""
| _ -> assert false
| s ->
eprintf "Session.load_result: unexpected status '%s'@." s;
assert false
in
let time =
try float_of_string (List.assoc "time" r.Xml.attributes)
......@@ -935,24 +939,30 @@ let load_result r =
Call_provers.pr_output = "";
}
| s ->
failwith ("Session.load_result: unexpected element " ^ s)
eprintf "Session.load_result: unexpected element '%s'@." s;
assert false
let rec load_goal ~provers 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
List.iter (load_proof_or_transf ~provers mg) g.Xml.elements;
mg::acc
let rec load_goal ~env ~provers parent acc g =
match g.Xml.name with
| "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 gname expl None in
List.iter (load_proof_or_transf ~env ~provers mg) g.Xml.elements;
mg::acc
| s ->
eprintf "Session.load_goal: unexpected element '%s'@." s;
assert false
and load_proof_or_transf ~provers mg a =
and load_proof_or_transf ~env ~provers mg a =
match a.Xml.name with
| "proof" ->
let prover =
......@@ -969,54 +979,115 @@ and load_proof_or_transf ~provers mg a =
| [] -> Undone
| _ -> assert false
in
let pa = raw_add_external_proof ~obsolete:false
~edit:"" (* TODO *)
mg p res
let edit =
try List.assoc "edited" a.Xml.attributes
with Not_found -> assert false
in
let _pa = raw_add_external_proof ~obsolete:false
~edit mg p res
in
Hashtbl.add mg.external_proofs prover pa
(* already done by raw_add_external_proof
Hashtbl.add mg.external_proofs prover pa *)
()
| "transf" ->
let trname =
try List.assoc "name" a.Xml.attributes
with Not_found -> assert false
in
let tr =
try
lookup_transformation env trname
with Not_found -> assert false (* TODO *)
in
let _proved =
try List.assoc "proved" a.Xml.attributes
with Not_found -> assert false
in
let mtr = raw_add_transformation mg tr in
mtr.subgoals <-
List.rev
(List.fold_left
(load_goal ~env ~provers (Parent_transf mtr))
[] a.Xml.elements);
(* already done by raw_add_transformation
Hashtbl.add mg.transformations trname mtr *)
()
(* TODO *)
(*
Hashtbl.add mg.transformations tr_name tr
*)
| _ -> assert false
let load_theory ~provers 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 ~provers mth) [] th.Xml.elements);
mth::acc
let load_file ~provers 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 ~provers mf) [] f.Xml.elements)
| s ->
eprintf "Session.load_proof_or_transf: unexpected element '%s'@." s;
assert false
let load_theory ~env ~provers mf acc th =
match th.Xml.name with
| "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 ~env ~provers (Parent_theory mth))
[] th.Xml.elements);
mth::acc
| s ->
eprintf "Session.load_theory: unexpected element '%s'@." s;
assert false
let load_file ~env ~provers f =
match f.Xml.name with
| "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 ~env ~provers mf) [] f.Xml.elements)
| s ->
eprintf "Session.load_file: unexpected element '%s'@." s;
assert false
let load_session ~env ~provers xml =
let cont = xml.Xml.content in
match cont.Xml.name with
| "why3session" ->
List.iter (load_file ~env ~provers) cont.Xml.elements
| s ->
eprintf "Session.load_session: unexpected element '%s'@." s;
assert false
let db_file = ref ""
let open_session ~provers ~init ~notify file =
init_fun := init; notify_fun := notify; db_file := file;
try
let l = Xml.from_file file in
List.iter (load_file ~provers) l;
(* TODO reload the files *)
()
with Sys_error _ ->
(* xml does not exist yet *)
()
let save_session () = save !db_file
let db_file = ref None
let open_session ~env ~provers ~init ~notify file =
match !db_file with
| None ->
init_fun := init; notify_fun := notify;
db_file := Some file;
begin try
let xml = Xml.from_file file in
load_session ~env ~provers xml;
(* TODO reload the files *)
()
with
| Sys_error _ ->
(* xml does not exist yet *)
()
| Xml.Parse_error s ->
Format.eprintf "XML database corrupted, ignored (%s)@." s;
()
end
| _ ->
eprintf "Session.open_session: session already opened@.";
assert false
let save_session () =
match !db_file with
| Some f -> save f
| None ->
eprintf "Session.save_session: no session opened@.";
assert false
(*****************************************************)
(* method: run a given prover on each unproved goals *)
......
src/ide/session.mli
View file @ e9992947
......@@ -134,6 +134,7 @@ module Make(O: OBSERVER) : sig
(*****************************)
val open_session :
env:Env.env ->
provers:prover_data Util.Mstr.t ->
init:(O.key -> any -> unit) ->
notify:(any -> unit) -> string -> unit
......@@ -152,8 +153,10 @@ module Make(O: OBSERVER) : sig
val maximum_running_proofs : int ref
(*
val test_save : unit -> unit
val test_load : unit -> Xml.element list
val test_load : unit -> Xml.t
*)
val save_session : unit -> unit
(** enforces to save the session state on disk.
......
src/ide/xml.mli
View file @ e9992947
......@@ -6,6 +6,19 @@ type element =
elements : element list;
}
val from_file : string -> element list
type t =
{ version : string;
encoding : string;
doctype : string;
dtd : string;
content : element;
}
exception Parse_error of string
val from_file : string -> t
(** returns the list of XML elements from the given file.
raise [Sys_error] if the file cannot be opened.
raise [Parse_error] if the file does not follow XML syntax
*)
src/ide/xml.mll
View file @ e9992947
......@@ -10,6 +10,14 @@
elements : element list;
}
type t =
{ version : string;
encoding : string;
doctype : string;
dtd : string;
content : element;
}
let buf = Buffer.create 17
let rec pop_all group_stack element_stack =
......@@ -22,6 +30,11 @@
elements = List.rev element_stack;
}
in pop_all g (e::elems)
exception Parse_error of string
let parse_error s = raise (Parse_error s)
}
let space = [' ' '\t' '\r' '\n']
......@@ -34,11 +47,35 @@ let mantissa = ['e''E'] sign? digit+
let real = sign? digit* '.' digit* mantissa?
let escape = ['\\''"''n''t''r']
rule xml_header = parse
| "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
{ elements [] [] lexbuf }
rule xml_prolog = parse
| space+
{ xml_prolog lexbuf }
| "<?xml" space+ "version=\"1.0\"" space+ "?>"
{ xml_doctype "1.0" "" lexbuf }
| "<?xml" space+ "version=\"1.0\"" space+ "encoding=\"UTF-8\"" space+ "?>"
{ xml_doctype "1.0" "" lexbuf }
| "<?xml" ([^'?']|'?'[^'>'])* "?>"
{ Format.eprintf "[Xml warning] prolog ignored@.";
xml_doctype "1.0" "" lexbuf }
| _
{ failwith "[Xml error] wrong header" }
{ parse_error "wrong prolog" }
and xml_doctype version encoding = parse
| space+
{ xml_doctype version encoding lexbuf }
| "<!DOCTYPE" space+ (ident as doctype) space+ [^'>']* ">"
{ match elements [] [] lexbuf with
| [x] ->
{ version = version;
encoding = encoding;
doctype = doctype;
dtd = "";
content = x;
}
| _ -> parse_error "there should be exactly one root element"
}
| _
{ parse_error "wrong DOCTYPE" }
and elements group_stack element_stack = parse
| space+
......@@ -48,11 +85,15 @@ and elements group_stack element_stack = parse
| "</" (ident as celem) space* '>'
{ match group_stack with
| [] ->
Format.eprintf "[Xml warning] unexpected closing Xml element `%s'@." celem;
Format.eprintf
"[Xml warning] unexpected closing Xml element `%s'@."
celem;
elements group_stack element_stack lexbuf
| (elem,att,stack)::g ->
if celem <> elem then
Format.eprintf "[Xml warning] Xml element `%s' closed by `%s'@." elem celem;
Format.eprintf
"[Xml warning] Xml element `%s' closed by `%s'@."
elem celem;
let e = {
name = elem;
attributes = att;
......@@ -71,7 +112,7 @@ and elements group_stack element_stack = parse
pop_all group_stack element_stack
}
| _ as c
{ failwith ("[Xml error] invalid element starting with " ^ String.make 1 c) }
{ parse_error ("invalid element starting with " ^ String.make 1 c) }
and attributes groupe_stack element_stack elem acc = parse
| space+
......@@ -88,35 +129,20 @@ and attributes groupe_stack element_stack elem acc = parse
in
elements groupe_stack (e::element_stack) lexbuf }
| _ as c
{ failwith ("[Xml error] `>' expected, got " ^ String.make 1 c) }
{ parse_error ("'>' expected, got " ^ String.make 1 c) }
| eof
{ failwith ("[Xml error] unclosed element, `>' expected") }
{ parse_error "unclosed element, `>' expected" }
and value = parse
| space+
{ value lexbuf }
(*
| integer as i
{ RCint (int_of_string i) }
| real as r
{ RCfloat (float_of_string r) }
*)
| '"'
{ Buffer.clear buf;
string_val lexbuf }
(*
| "true"
{ RCbool true }
| "false"
{ RCbool false }
| ident as id
{ RCident id }
*)
| _ as c
{ failwith ("[Xml error] invalid value starting with "
^ String.make 1 c) }
{ parse_error ("invalid value starting with " ^ String.make 1 c) }
| eof
{ failwith "[Xml error] unterminated keyval pair" }
{ parse_error "unterminated keyval pair" }
and string_val = parse
| '"'
......@@ -135,26 +161,15 @@ and string_val = parse
Buffer.add_char buf c;
string_val lexbuf }
| eof
{ failwith "[Xml error] unterminated string" }
{ parse_error "unterminated string" }
{
let from_file f =
let c =
(*
try
*)
open_in f
(*
with Sys_error _ ->
Format.eprintf "Cannot open file %s@." f;
exit 1
*)
in
let c = open_in f in
let lb = Lexing.from_channel c in
let l = xml_header lb in
let t = xml_prolog lb in
close_in c;
List.rev l
t
}
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