Commit 392a4d2a authored by MARCHE Claude's avatar MARCHE Claude

task is not anymore a field of proof nodes, but in a hashtable of the session

parent 9fcc1a85
......@@ -78,7 +78,6 @@ type controller =
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_tasks_for_print : (bool * Task.task * Trans.naming_table) Hpn.t;
}
......@@ -89,7 +88,6 @@ let create_controller config env ses =
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
controller_tasks_for_print = Hpn.create 7;
}
in
let provers = Whyconf.get_provers config in
......@@ -119,31 +117,6 @@ let get_undetached_children_no_pa s any : any list =
(* handling of task printing with intros *)
let goal_task_to_print ?do_intros c n =
try
let (b,t,ta) = Hpn.find c.controller_tasks_for_print n in
match do_intros with
| None -> t,ta
| Some b' -> if b <> b' then raise Not_found; t,ta
with Not_found ->
let t = get_task c.controller_session n in
let do_intros =
match do_intros with
| None -> false
| Some b -> b
in
let t =
if do_intros then Trans.apply Introduction.introduce_premises t else t
in
let ta = Args_wrapper.build_naming_tables t in
Hpn.add c.controller_tasks_for_print n (do_intros,t,ta);
t,ta
(* printing *)
module PSession = struct
......@@ -272,8 +245,7 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback =
Whyconf.get_complete_command
config_pr
~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let task = Session_itp.get_task c.controller_session id in
(* let table = Session_itp.get_table c.controller_session id in *)
let task,_table = Session_itp.get_task c.controller_session id in
let call =
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace:false ~command
~limit (*?name_table:table*) driver task
......@@ -392,7 +364,7 @@ let schedule_proof_attempt ?proof_script c id pr
let create_file_rel_path c pr pn =
let session = c.controller_session in
let driver = snd (Hprover.find c.controller_provers pr) in
let task = Session_itp.get_task session pn in
let task,_table = Session_itp.get_task session pn in
let session_dir = Session_itp.get_dir session in
let th = get_encapsulating_theory session (APn pn) in
let th_name = (Session_itp.theory_name th).Ident.id_string in
......@@ -407,7 +379,7 @@ let create_file_rel_path c pr pn =
let update_edit_external_proof c pn ?panid pr =
let session = c.controller_session in
let driver = snd (Hprover.find c.controller_provers pr) in
let task = Session_itp.get_task session pn in
let task,_table = Session_itp.get_task session pn in
let session_dir = Session_itp.get_dir session in
let file =
match panid with
......@@ -535,7 +507,7 @@ let schedule_transformation_r c id name args ~callback =
| None -> raise (Trans.Bad_name_table "Controller_itp.schedule_transformation_r")
| Some table -> table in
*)
let task,table = goal_task_to_print c id in
let task,table = get_task c.controller_session id in
begin
try
let subtasks =
......
......@@ -78,7 +78,6 @@ type controller = private
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_tasks_for_print : (bool * Task.task * Trans.naming_table) Hpn.t;
}
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
......@@ -88,10 +87,6 @@ val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> contr
val print_session : Format.formatter -> controller -> unit
(* handling of task printing with intros *)
val goal_task_to_print :
?do_intros:bool -> controller -> proofNodeID -> Task.task * Trans.naming_table
val reload_files : controller -> use_shapes:bool -> bool * bool
(** reload the files of the given session:
......
......@@ -88,7 +88,7 @@ let p s id =
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
*)
let _,tables = Controller_itp.goal_task_to_print s id in
let _,tables = Session_itp.get_task s id in
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
(Pretty.create pr apr pr pr false)
......@@ -790,7 +790,7 @@ end
let session = d.cont.Controller_itp.controller_session in
(match node with
| APn pr_node ->
let task = Session_itp.get_task session pr_node in
let task,_table = Session_itp.get_task session pr_node in
let b = label_detection task in
if b then
(focused_node := Focus_on node;
......@@ -906,7 +906,7 @@ end
let task = get_task d.cont.controller_session id in
let tables = get_table d.cont.controller_session id in
*)
let task,tables = goal_task_to_print ~do_intros d.cont id in
let task,tables = get_task ~do_intros d.cont.controller_session id in
(* This function also send source locations associated to the task *)
let loc_color_list = if loc then get_locations task else [] in
let task_text =
......@@ -1108,7 +1108,7 @@ end
let doc = try
Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
with | _ -> "" in
let msg, loc, arg_opt = get_exception_message d.cont id e in
let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
P.notify (Message (Transf_error (node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
| _ -> ()
......
......@@ -414,7 +414,7 @@ let interp commands_table config cont id s =
| None -> raise (Trans.Bad_name_table "Server_utils.interp")
| Some table -> table in
*)
let _,table = Controller_itp.goal_task_to_print cont id in
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
......
......@@ -57,8 +57,6 @@ type proof_attempt_node = {
type proof_node = {
proofn_name : Ident.ident;
proofn_expl : string;
proofn_task : Task.task;
proofn_table : Trans.naming_table option;
proofn_parent : proof_parent;
proofn_checksum : Termcode.checksum option;
proofn_shape : Termcode.shape;
......@@ -108,6 +106,9 @@ type session = {
session_files : file Hstr.t;
mutable session_shape_version : int;
session_prover_ids : int Hprover.t;
(* tasks *)
session_raw_tasks : Task.task Hpn.t;
session_tasks : (bool * Task.task * Trans.naming_table) Hpn.t;
(* proved status *)
file_state: bool Hstr.t;
th_state: bool Ident.Hid.t;
......@@ -115,6 +116,8 @@ type session = {
pn_state : bool Hpn.t;
}
let theory_parent s th =
Hstr.find s.session_files th.theory_parent_name
......@@ -206,9 +209,28 @@ let get_proofNode (s : session) (id : proofNodeID) =
Hint.find s.proofNode_table id
with Not_found -> raise BadID
let get_task (s:session) (id:proofNodeID) =
let node = get_proofNode s id in
node.proofn_task
let get_raw_task s id =
Hpn.find s.session_raw_tasks id
let get_task ?do_intros s n =
try
let (b,ti,ta) = Hpn.find s.session_tasks n in
match do_intros with
| None -> (ti,ta)
| Some b' -> if b <> b' then raise Not_found; (ti,ta)
with Not_found ->
let t = get_raw_task s n in
let do_intros =
match do_intros with
| None -> true
| Some b -> b
in
let ti =
if do_intros then Trans.apply Introduction.introduce_premises t else t
in
let ta = Args_wrapper.build_naming_tables ti in
Hpn.add s.session_tasks n (do_intros,ti,ta);
ti,ta
let get_transfNode (s : session) (id : transID) =
try
......@@ -270,17 +292,17 @@ let is_detached (s: session) (a: any) =
end
| ATn tn ->
let pn_id = get_trans_parent s tn in
let pn = get_proofNode s pn_id in
pn.proofn_task = None ||
let _pn = get_proofNode s pn_id in
(* pn.proofn_task = None || *)
List.exists (fun x -> x = tn) (get_detached_trans s pn_id)
| APn pn ->
let pn = get_proofNode s pn in
pn.proofn_task = None
let _pn = get_proofNode s pn in
(* pn.proofn_task = None *) false
| APa pa ->
let pa = get_proof_attempt_node s pa in
let pn_id = pa.parent in
let pn = get_proofNode s pn_id in
pn.proofn_task = None
let _pn = get_proofNode s pn_id in
(* pn.proofn_task = None *) false
let rec get_encapsulating_theory s any =
match any with
......@@ -492,10 +514,12 @@ let empty_session ?shape_version dir =
session_files = Hstr.create 3;
session_shape_version = shape_version;
session_prover_ids = Hprover.create 7;
session_raw_tasks = Hpn.create 97;
session_tasks = Hpn.create 97;
file_state = Hstr.create 3;
th_state = Ident.Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42;
tn_state = Htn.create 97;
pn_state = Hpn.create 97;
}
(**************************************************)
......@@ -541,26 +565,25 @@ let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.pro
of proofNodeID [id] of parent [p] of task [t] *)
let mk_proof_node ~version ~expl (s : session) (n : Ident.ident) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
let tables = Args_wrapper.build_naming_tables t in
(* let tables = Args_wrapper.build_naming_tables t in *)
let sum = Some (Termcode.task_checksum ~version t) in
let shape = Termcode.t_shape_task ~version ~expl t in
let pn = { proofn_name = n;
proofn_expl = expl;
proofn_task = t;
proofn_table = Some tables;
(* proofn_table = Some tables; *)
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
proofn_attempts = Hprover.create 7;
proofn_transformations = [] } in
Hpn.add s.session_raw_tasks node_id t;
Hint.add s.proofNode_table node_id pn
let mk_proof_node_no_task (s : session) (n : Ident.ident)
(parent : proof_parent) (node_id : proofNodeID) sum shape proved =
let pn = { proofn_name = n;
proofn_expl = "";
proofn_task = None;
proofn_table = None;
(* proofn_table = None; *)
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
......@@ -1376,10 +1399,7 @@ let add_registered_transformation s env old_tr goal_id =
tr
with Not_found ->
Debug.dprintf debug "[merge_theory] trans not found@.";
let task = goal.proofn_task in
let tables = match goal.proofn_table with
| None -> raise (Trans.Bad_name_table "Session_itp.add_registered_transformation")
| Some tables -> tables in
let task,tables = get_task s goal_id in
let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args tables task in
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
......
......@@ -84,7 +84,8 @@ val is_below: session -> any -> any -> bool
type proof_parent = Trans of transID | Theory of theory
val get_task : session -> proofNodeID -> Task.task
val get_raw_task : session -> proofNodeID -> Task.task
val get_task : ?do_intros:bool -> session -> proofNodeID -> Task.task * Trans.naming_table
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
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