Commit 8665055f authored by Clément Fumex's avatar Clément Fumex

move reload_file and add_file out of the functor in controller_itp

parent 1e1ce4c6
......@@ -203,6 +203,53 @@ module type Scheduler = sig
val idle: prio:int -> (unit -> bool) -> unit
end
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
in
List.map (fun (_,_,a) -> a) th
(** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let merge_file (old_ses : session) (c : controller) env ~use_shapes _ file =
let format = file.file_format in
let old_theories = file.file_theories in
let file_name = Filename.concat (get_dir old_ses) file.file_name in
let new_theories =
try
read_file c.controller_env file_name ?format
with _ -> (* TODO: filter only syntax error and typing errors *)
[]
in
add_file_section
c.controller_session ~use_shapes ~merge:(old_ses,old_theories,env) file_name new_theories format
let reload_files (c : controller) (env : Env.env) ~use_shapes =
let old_ses = c.controller_session in
c.controller_session <- empty_session ~shape_version:(get_shape_version old_ses) (get_dir old_ses);
Stdlib.Hstr.iter (merge_file old_ses c env ~use_shapes) (get_files old_ses)
let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section ~use_shapes:false c.controller_session fname theories format
module Make(S : Scheduler) = struct
......@@ -400,59 +447,6 @@ let run_strategy_on_goal c id strat ~callback =
in
exec_strategy 0 strat id
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
in
List.map (fun (_,_,a) -> a) th
let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section ~use_shapes:false c.controller_session fname theories format
(** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let merge_file (old_ses : session) (c : controller) env ~use_shapes _ file =
let format = file.file_format in
let old_theories = file.file_theories in
let file_name = Filename.concat (get_dir old_ses) file.file_name in
let new_theories =
try
read_file c.controller_env file_name ?format
with _ -> (* TODO: filter only syntax error and typing errors *)
[]
in
add_file_section
c.controller_session ~use_shapes ~merge:(old_ses,old_theories,env) file_name new_theories format
let reload_files (c : controller) (env : Env.env) ~use_shapes =
let old_ses = c.controller_session in
c.controller_session <- empty_session ~shape_version:(get_shape_version old_ses) (get_dir old_ses);
Stdlib.Hstr.iter (merge_file old_ses c env ~use_shapes) (get_files old_ses)
let replay_proof_attempt c pr limit (id: proofNodeID) ~callback =
(* The replay can be done on a different machine so we need
......
......@@ -90,46 +90,6 @@ val th_proved: controller -> Session_itp.theory -> bool
val print_session : Format.formatter -> controller -> unit
module Make(S : Scheduler) : sig
val schedule_proof_attempt :
controller ->
proofNodeID ->
Whyconf.prover ->
limit:Call_provers.resource_limit ->
callback:(proof_attempt_status -> unit) -> unit
(** [schedule_proof_attempt s id p ~timelimit ~callback] schedules a
proof attempt for a goal specified by [id] with the prover [p] with
time limit [timelimit]; the function [callback] will be called each
time the proof attempt status changes. Typically at Scheduled, then
Running, then Done. If there is already a proof attempt with [p] it
is updated. *)
val schedule_transformation :
controller ->
proofNodeID ->
string ->
string list ->
callback:(transformation_status -> unit) -> unit
(** [schedule_transformation c id cb] schedules a transformation for a
goal specified by [id]; the function [cb] will be called each time
the transformation status changes. Typically at Scheduled, then
Done tid.*)
val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
callback:(strategy_status -> unit) -> unit
(** [run_strategy_on_goal c id strat] executes asynchronously the
strategy [strat] on the goal [id]. TODO: add callback to get
inform of the progress *)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *)
val reload_files : controller -> Env.env -> use_shapes:bool -> unit
(** reload the files of the given session:
......@@ -179,6 +139,46 @@ val reload_files : controller -> Env.env -> use_shapes:bool -> unit
*)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *)
module Make(S : Scheduler) : sig
val schedule_proof_attempt :
controller ->
proofNodeID ->
Whyconf.prover ->
limit:Call_provers.resource_limit ->
callback:(proof_attempt_status -> unit) -> unit
(** [schedule_proof_attempt s id p ~timelimit ~callback] schedules a
proof attempt for a goal specified by [id] with the prover [p] with
time limit [timelimit]; the function [callback] will be called each
time the proof attempt status changes. Typically at Scheduled, then
Running, then Done. If there is already a proof attempt with [p] it
is updated. *)
val schedule_transformation :
controller ->
proofNodeID ->
string ->
string list ->
callback:(transformation_status -> unit) -> unit
(** [schedule_transformation c id cb] schedules a transformation for a
goal specified by [id]; the function [cb] will be called each time
the transformation status changes. Typically at Scheduled, then
Done tid.*)
val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
callback:(strategy_status -> unit) -> unit
(** [run_strategy_on_goal c id strat] executes asynchronously the
strategy [strat] on the goal [id]. TODO: add callback to get
inform of the progress *)
type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
(** Result(new_result,old_result) *)
......
......@@ -178,9 +178,9 @@ let cont_init () =
(* create the controller *)
let c = Controller_itp.create_controller env ses in
(* update the session *)
C.reload_files c env ~use_shapes;
Controller_itp.reload_files c env ~use_shapes;
(* add files to controller *)
Queue.iter (fun fname -> C.add_file c fname) files;
Queue.iter (fun fname -> Controller_itp.add_file c fname) files;
(* load provers drivers *)
Whyconf.Mprover.iter
(fun _ p ->
......@@ -538,7 +538,7 @@ let test_save_session _fmt _args =
let test_reload fmt _args =
fprintf fmt "Reloading... @?";
(* use_shapes is true since session is in memory *)
C.reload_files cont env ~use_shapes:true;
Controller_itp.reload_files cont env ~use_shapes:true;
zipper_init ();
fprintf fmt "done @."
......
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