From dd787602f5af1fcdca870f8a8f4ad762d0e2cf9c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Fumex?= Date: Wed, 2 Mar 2016 15:11:17 +0100 Subject: [PATCH] load proof first attempt --- src/session/session_itp.ml | 447 ++++++++++++++++++++++-------------- src/session/session_itp.mli | 30 ++- 2 files changed, 297 insertions(+), 180 deletions(-) diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index 4affa3893..a33bd1d32 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -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 diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index c8fe7daa0..9ada5af38 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -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 - gere une file de travaux de modifications a faire - - recupere les resultats de travaux , et les applique s'ils sont encore valides + - recupere les resultats de travaux , et les applique s'ils sont + encore valides *) (* type theory = -- GitLab