Commit dd787602 authored by Clément Fumex's avatar Clément Fumex
Browse files

load proof first attempt

parent 9e698189
......@@ -3,21 +3,27 @@ open Stdlib
module Hprover = Whyconf.Hprover
let debug = Debug.register_info_flag "session_itp"
~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
creation,@ reading@ and@ writing."
~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
creation,@ reading@ and@ writing."
type transID = int
type proofNodeID = int
type proof_parent = Trans of transID | Theory of Theory.theory
type theory = {
theory_name : Ident.ident;
theory_checksum : Termcode.checksum option;
theory_goals : proofNodeID list;
}
type proof_parent = Trans of transID | Theory of theory
type proof_attempt = {
prover : Whyconf.prover;
timelimit : int;
memlimit : int;
stepslimit : int;
proof_state : Call_provers.prover_result option; (* None means that the call was not done
or never returned *)
proof_state : Call_provers.prover_result option;
(* None means that the call was not done or never returned *)
proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
}
......@@ -49,20 +55,14 @@ type transformation_node = {
transf_parent : proofNodeID;
}
type theory = {
theory_name : Ident.ident;
theory_checksum : Termcode.checksum option;
theory_goals : proofNodeID list;
}
type file = {
file_name : string;
file_format : string option;
file_theories : theory list;
}
type session = {
task_table : proof_node Hint.t;
type session = {
proofNode_table : proof_node Hint.t;
mutable next_proofNodeID : int;
trans_table : transformation_node Hint.t;
mutable next_transID : int;
......@@ -70,7 +70,7 @@ type session = {
mutable session_shape_version : int;
session_prover_ids : int Hprover.t;
session_file_name : string;
}
}
let gen_transID (s : session) =
let id = s.next_transID in
......@@ -82,12 +82,23 @@ let gen_proofNodeID (s : session) =
s.next_proofNodeID <- id + 1;
id
exception BadID
let get_proofNode (s : session) (id : proofNodeID) =
try
Hint.find s.proofNode_table id
with Not_found -> raise BadID
let get_transfNode (s : session) (id : transID) =
try
Hint.find s.trans_table id
with Not_found -> raise BadID
let empty_session ?shape_version (file : string) =
let shape_version = match shape_version with
| Some v -> v
| None -> Termcode.current_shape_version
in
{ task_table = Hint.create 97;
{ proofNode_table = Hint.create 97;
next_proofNodeID = 0;
trans_table = Hint.create 97;
next_transID = 0;
......@@ -97,35 +108,52 @@ let empty_session ?shape_version (file : string) =
session_file_name = file;
}
exception BadID
let graft_proof_attempt (s : session) (id : proofNodeID) (pa : proof_attempt) =
try
let pn = Hint.find s.task_table id in
let node = { proofa_parent = id; proofa_attempt = pa } in
Hprover.replace pn.proofn_attempts pa.prover node
with Not_found -> raise BadID
let pn = get_proofNode s id in
let node = { proofa_parent = id; proofa_attempt = pa } in
Hprover.replace pn.proofn_attempts pa.prover node
let remove_proof_attempt (s : session) (id : proofNodeID)
(prover : Whyconf.prover) =
let pn = get_proofNode s id in
Hprover.remove pn.proofn_attempts prover
(* [mk_proof_node s t p id] register in the session [s] a proof node
of proofNodeID [id] of parent [p] of task [t] *)
let mk_proof_node (s : session) (t : Task.task) (parent : proof_parent)
(node_id : proofNodeID) =
let pn = { proofn_task = t; proofn_parent = parent;
proofn_attempts = Hprover.create 7;
proofn_transformations = []} in
Hint.add s.proofNode_table node_id pn
let mk_proof_node (s : session) (tid : int) (t : Task.task) =
let mk_transf_proof_node (s : session) (tid : int) (t : Task.task) =
let id = gen_proofNodeID s in
let pn = { proofn_task = t; proofn_parent = Trans tid;
proofn_attempts = Hprover.create 3;
proofn_transformations = []} in
Hint.add s.task_table id pn;
mk_proof_node s t (Trans tid) id;
id
let graft_transf (s : session) (id : proofNodeID) (name : string) (l : trans_arg list) (tl : Task.task list) =
try
let pn = Hint.find s.task_table id in
let tid = gen_transID s in
let sub_tasks = List.map (mk_proof_node s tid) tl in
let tn = { transf_name = name;
transf_args = l;
transf_subtasks = sub_tasks;
transf_parent = id; } in
Hint.replace s.trans_table tid tn;
pn.proofn_transformations <- tid::pn.proofn_transformations
with Not_found -> raise BadID
let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
(name : string) (args : trans_arg list) (pnl : proofNodeID list) =
let pn = get_proofNode s id in
let tn = { transf_name = name;
transf_args = args;
transf_subtasks = pnl;
transf_parent = id; } in
Hint.add s.trans_table node_id tn;
pn.proofn_transformations <- node_id::pn.proofn_transformations
let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : trans_arg list) (tl : Task.task list) =
let tid = gen_transID s in
let sub_tasks = List.map (mk_transf_proof_node s tid) tl in
mk_transf_node s id tid name args sub_tasks
let remove_transformation (s : session) (id : transID) =
let nt = get_transfNode s id in
Hint.remove s.trans_table id;
let pn = get_proofNode s nt.transf_parent in
let trans_up = List.filter (fun tid -> tid != id) pn.proofn_transformations in
pn.proofn_transformations <- trans_up;
(************************)
(* saving state on disk *)
......@@ -150,9 +178,9 @@ exception SessionFileError of string
let bool_attribute field r def =
try
match List.assoc field r.Xml.attributes with
| "true" -> true
| "false" -> false
| _ -> assert false
| "true" -> true
| "false" -> false
| _ -> assert false
with Not_found -> def
let int_attribute_def field r def =
......@@ -189,46 +217,46 @@ let string_attribute field r =
let load_result r =
match r.Xml.name with
| "result" ->
let status = string_attribute "status" r in
let answer =
match status with
| "valid" -> Call_provers.Valid
| "invalid" -> Call_provers.Invalid
| "unknown" -> Call_provers.Unknown ("", None)
| "timeout" -> Call_provers.Timeout
| "outofmemory" -> Call_provers.OutOfMemory
| "failure" -> Call_provers.Failure ""
| "highfailure" -> Call_provers.HighFailure
| "steplimitexceeded" -> Call_provers.StepLimitExceeded
| "stepslimitexceeded" -> Call_provers.StepLimitExceeded
| s ->
Warning.emit
"[Warning] Session.load_result: unexpected status '%s'@." s;
Call_provers.HighFailure
in
let time =
try float_of_string (List.assoc "time" r.Xml.attributes)
with Not_found -> 0.0
in
let steps =
try int_of_string (List.assoc "steps" r.Xml.attributes)
with Not_found -> -1
in
Some {
Call_provers.pr_answer = answer;
Call_provers.pr_time = time;
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0;
Call_provers.pr_steps = steps;
Call_provers.pr_model = Model_parser.default_model;
}
| "undone" -> None
| "unedited" -> None
| s ->
Warning.emit "[Warning] Session.load_result: unexpected element '%s'@."
s;
None
| "result" ->
let status = string_attribute "status" r in
let answer =
match status with
| "valid" -> Call_provers.Valid
| "invalid" -> Call_provers.Invalid
| "unknown" -> Call_provers.Unknown ("", None)
| "timeout" -> Call_provers.Timeout
| "outofmemory" -> Call_provers.OutOfMemory
| "failure" -> Call_provers.Failure ""
| "highfailure" -> Call_provers.HighFailure
| "steplimitexceeded" -> Call_provers.StepLimitExceeded
| "stepslimitexceeded" -> Call_provers.StepLimitExceeded
| s ->
Warning.emit
"[Warning] Session.load_result: unexpected status '%s'@." s;
Call_provers.HighFailure
in
let time =
try float_of_string (List.assoc "time" r.Xml.attributes)
with Not_found -> 0.0
in
let steps =
try int_of_string (List.assoc "steps" r.Xml.attributes)
with Not_found -> -1
in
Some {
Call_provers.pr_answer = answer;
Call_provers.pr_time = time;
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0;
Call_provers.pr_steps = steps;
Call_provers.pr_model = Model_parser.default_model;
}
| "undone" -> None
| "unedited" -> None
| s ->
Warning.emit "[Warning] Session.load_result: unexpected element '%s'@."
s;
None
let load_option attr g =
try Some (List.assoc attr g.Xml.attributes)
......@@ -237,13 +265,13 @@ let load_option attr g =
let load_ident elt =
let name = string_attribute "name" elt in
let label = List.fold_left
(fun acc label ->
match label with
| {Xml.name = "label"} ->
let lab = string_attribute "name" label in
Ident.Slab.add (Ident.create_label lab) acc
| _ -> acc
) Ident.Slab.empty elt.Xml.elements in
(fun acc label ->
match label with
| {Xml.name = "label"} ->
let lab = string_attribute "name" label in
Ident.Slab.add (Ident.create_label lab) acc
| _ -> acc
) Ident.Slab.empty elt.Xml.elements in
let preid =
try
let load_exn attr g = List.assoc attr g.Xml.attributes in
......@@ -263,96 +291,179 @@ type load_ctxt = {
let read_file_session_and_shapes dir xml_filename =
try
let compressed_shape_filename =
Filename.concat dir compressed_shape_filename
in
if Sys.file_exists compressed_shape_filename then
(* if Compress.compression_supported then
Session.ReadShapesCompress.read_xml_and_shapes
xml_filename compressed_shape_filename
else *)
let compressed_shape_filename =
Filename.concat dir compressed_shape_filename
in
if Sys.file_exists compressed_shape_filename then
(* if Compress.compression_supported then
Session.ReadShapesCompress.read_xml_and_shapes
xml_filename compressed_shape_filename
else *)
begin
Warning.emit "[Warning] could not read goal shapes because \
Why3 was not compiled with compress support@.";
Why3 was not compiled with compress support@.";
Xml.from_file xml_filename, false
end
else
let shape_filename = Filename.concat dir shape_filename in
(* if Sys.file_exists shape_filename then
ReadShapesNoCompress.read_xml_and_shapes xml_filename shape_filename
else*)
else
let shape_filename = Filename.concat dir shape_filename in
(* if Sys.file_exists shape_filename then
ReadShapesNoCompress.read_xml_and_shapes xml_filename shape_filename
else*)
begin
Warning.emit "[Warning] could not find goal shapes file@.";
Xml.from_file xml_filename, false
end
with e ->
Warning.emit "[Warning] failed to read goal shapes: %s@."
(Printexc.to_string e);
Xml.from_file xml_filename, false
let load_file session old_provers f = old_provers
(* match f.Xml.name with
| "file" ->
let ctxt = { old_provers = old_provers ; keygen = keygen } in
let fn = string_attribute "name" f in
let fmt = load_option "format" f in
let expanded = bool_attribute "expanded" f false in
let mf = raw_add_file ~keygen:ctxt.keygen ~expanded session fn fmt in
mf.file_theories <-
List.rev
(List.fold_left
(load_theory ctxt mf) [] f.Xml.elements);
mf.file_verified <- file_verified mf;
old_provers
| "prover" ->
(* The id is just for the session file *)
let id = string_attribute "id" f in
begin
try
let id = int_of_string id in
let name = string_attribute "name" f in
let version = string_attribute "version" f in
let altern = string_attribute_def "alternative" f "" in
let timelimit = int_attribute_def "timelimit" f 5 in
let steplimit = int_attribute_def "steplimit" f 1 in
let memlimit = int_attribute_def "memlimit" f 1000 in
let p = {C.prover_name = name;
prover_version = version;
prover_altern = altern} in
Mint.add id (p,timelimit,steplimit,memlimit) old_provers
with Failure _ ->
Warning.emit "[Warning] Session.load_file: unexpected non-numeric prover id '%s'@." id;
old_provers
end
with e ->
Warning.emit "[Warning] failed to read goal shapes: %s@."
(Printexc.to_string e);
Xml.from_file xml_filename, false
(* [load_goal s op p g id] loads the goal of parent [p] from the xml
[g] of nodeID [id] into the session [s] *)
let rec load_goal session old_provers parent g id =
match g.Xml.name with
| "goal" -> mk_proof_node session None parent id;
List.iter (load_proof_or_transf session old_provers id) g.Xml.elements;
| "label" -> ()
| s ->
Warning.emit "[Warning] Session.load_goal: unexpected element '%s'@." s
(* [load_proof_or_transf s op id a] load either a proof attempt or a
transformation of parent id [pid] from the xml [a] into the session
[s] *)
and load_proof_or_transf session old_provers pid a =
match a.Xml.name with
| "proof" ->
begin
let prover = string_attribute "prover" a in
try
let prover = int_of_string prover in
let (p,timelimit,steplimit,memlimit) = Mint.find prover old_provers in
let res = match a.Xml.elements with
| [r] -> load_result r
| [] -> None
| _ ->
Warning.emit "[Error] Too many result elements@.";
raise (LoadError (a,"too many result elements"))
in
let edit = load_option "edited" a in
let edit = match edit with None | Some "" -> None | _ -> edit in
let obsolete = bool_attribute "obsolete" a false in
let timelimit = int_attribute_def "timelimit" a timelimit in
let steplimit = int_attribute_def "steplimit" a steplimit in
let memlimit = int_attribute_def "memlimit" a memlimit in
let pa = { prover = p;
timelimit = timelimit;
memlimit = memlimit;
stepslimit = steplimit;
proof_state = res;
proof_obsolete = obsolete;
proof_script = edit;
} in
graft_proof_attempt session pid pa
with Failure _ | Not_found ->
Warning.emit "[Error] prover id not listed in header '%s'@." prover;
raise (LoadError (a,"prover not listing in header"))
end
| "transf" ->
let trname = string_attribute "name" a in
let tid = gen_transID session in
let subtasks = List.fold_left (fun goals th -> match th.Xml.name with
| "goal" -> (gen_proofNodeID session) :: goals
| _ -> goals) [] a.Xml.elements in
mk_transf_node session pid tid trname [] subtasks;
List.iter2
(load_goal session old_provers (Trans tid))
a.Xml.elements subtasks;
| "metas" -> ()
| "label" -> ()
| s ->
Warning.emit "[Warning] Session.load_file: unexpected element '%s'@." s;
Warning.emit
"[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
s
let load_theory session old_provers acc th =
match th.Xml.name with
| "theory" ->
let thname = load_ident th in
let csum = string_attribute_opt "sum" th in
let checksum = Opt.map Termcode.checksum_of_string csum in
let goals = List.fold_left (fun goals th -> match th.Xml.name with
| "goal" -> (gen_proofNodeID session) :: goals
| _ -> goals) [] th.Xml.elements in
let mth = { theory_name = thname;
theory_checksum = checksum;
theory_goals = goals; } in
List.iter2
(load_goal session old_provers (Theory mth))
th.Xml.elements goals;
mth::acc
| s ->
Warning.emit "[Warning] Session.load_theory: unexpected element '%s'@."
s;
acc
let load_file session old_provers f = (* old_provers *)
match f.Xml.name with
| "file" ->
let fn = string_attribute "name" f in
let fmt = load_option "format" f in
let ft = List.rev
(List.fold_left
(load_theory session old_provers) [] f.Xml.elements) in
let mf = { file_name = fn;
file_format = fmt;
file_theories = ft; } in
Hstr.add session.session_files fn mf;
old_provers
| "prover" ->
(* The id is just for the session file *)
let id = string_attribute "id" f in
begin
try
let id = int_of_string id in
let name = string_attribute "name" f in
let version = string_attribute "version" f in
let altern = string_attribute_def "alternative" f "" in
let timelimit = int_attribute_def "timelimit" f 5 in
let steplimit = int_attribute_def "steplimit" f 1 in
let memlimit = int_attribute_def "memlimit" f 1000 in
let p = {Whyconf.prover_name = name;
prover_version = version;
prover_altern = altern} in
Mint.add id (p,timelimit,steplimit,memlimit) old_provers
with Failure _ ->
Warning.emit "[Warning] Session.load_file: unexpected non-numeric prover id '%s'@." id;
old_provers
*)
end
| s ->
Warning.emit "[Warning] Session.load_file: unexpected element '%s'@." s;
old_provers
let build_session (s : session) xml =
match xml.Xml.name with
| "why3session" ->
let shape_version = int_attribute_def "shape_version" xml 1 in
s.session_shape_version <- shape_version;
Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
(* just to keep the old_provers somewhere *)
let old_provers =
List.fold_left (load_file s) Mint.empty xml.Xml.elements
in
Mint.iter
(fun id (p,_,_,_) ->
Debug.dprintf debug "prover %d: %a@." id Whyconf.print_prover p;
Hprover.replace s.session_prover_ids p id)
old_provers;
Debug.dprintf debug "[Info] load_session: done@\n"
| s ->
Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
s
| "why3session" ->
let shape_version = int_attribute_def "shape_version" xml 1 in
s.session_shape_version <- shape_version;
Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
(* just to keep the old_provers somewhere *)
let old_provers =
List.fold_left (load_file s) Mint.empty xml.Xml.elements
in
Mint.iter
(fun id (p,_,_,_) ->
Debug.dprintf debug "prover %d: %a@." id Whyconf.print_prover p;
Hprover.replace s.session_prover_ids p id)
old_provers;
Debug.dprintf debug "[Info] load_session: done@\n"
| s ->
Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
s
let load_session (file : string) =
let session = empty_session file in
let use_shapes =
(* If the xml is present we read it, otherwise we consider it empty *)
(* If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists file then
try
Termcode.reset_dict ();
......@@ -364,12 +475,12 @@ let load_session (file : string) =
with Sys_error msg ->
failwith ("Open session: sys error " ^ msg)
with
| Sys_error msg ->
| Sys_error msg ->
(* xml does not exist yet *)
raise (SessionFileError msg)
| Xml.Parse_error s ->
Warning.emit "XML database corrupted, ignored (%s)@." s;
raise (SessionFileError "XML corrupted")
else false
raise (SessionFileError msg)
| Xml.Parse_error s ->
Warning.emit "XML database corrupted, ignored (%s)@." s;
raise (SessionFileError "XML corrupted")
else false
in
session, use_shapes
......@@ -7,9 +7,11 @@ type trans_arg
(* (\** New Proof sessions ("Refectoire") *\) *)
(* note: la fonction register des transformations doit permettre de declarer les types des arguments
(* note: la fonction register des transformations doit permettre de
declarer les types des arguments
type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol | TTlsymbol | TTprsymbol
type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
| TTlsymbol | TTprsymbol
*)
......@@ -19,32 +21,36 @@ val graft_proof_attempt : session -> proofNodeID -> proof_attempt -> unit
(** [graft_proof_attempt s id pa] adds the proof attempt [pa] as a
child of the task [id] of the session [s]. *)
val graft_transf : session -> proofNodeID -> string -> trans_arg list -> Task.task list -> unit
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
Task.task list -> unit
(** [graft_transf s id name l tl] adds the transformation [name] as a
child of the task [id] of the session [s]. [l] is the list of argument
of the transformation; [tl] is the resulting list of tasks *)
child of the task [id] of the session [s]. [l] is the list of
argument of the transformation; [tl] is the resulting list of
tasks *)
val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
(** [remove_proof_attempt s id pr] removes the proof attempt from the
prover [pr] from the proof node [id] of the session [s] *)
val remove_transformation : session -> proofNodeID -> transID -> unit
(** [remove_transformation s pid tid] removes the transformation [tid] from
the proof node [pid] of the session [s] *)
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
from the session [s] *)
val save_session : string -> session -> unit
(* val save_session : string -> session -> unit *)
(** [save_session f s] Save the session [s] in file [f] *)
val load_session : string -> session
val load_session : string -> session * bool
(** [load_session f] load a session from a file [f]; all the tasks are
initialised to None *)
(*
couche au-dessus: "scheduler" cad modifications asynchrones de la session
couche au-dessus: "scheduler" cad modifications asynchrones de la
session