Commit 0fce7da0 authored by MARCHE Claude's avatar MARCHE Claude

reload_session in progress

parent b38a33e9
......@@ -181,23 +181,25 @@ let read_file env ?format fn =
let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section c.controller_session fname theories None
add_file_section c.controller_session fname theories format (empty_session ()) []
(** 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) _ file =
try
let theories =
read_file c.controller_env file.file_name ?format:file.file_format
in
add_file_section c.controller_session file.file_name theories None;
with _ -> (* TODO: filter only syntax error and typing errors *)
(* TODO: copy the old session with empty tasks *)
add_file_section c.controller_session file.file_name [] None
let merge_file (old_ses : session) (c : controller) _ file =
let format = file.file_format in
let old_theories = file.file_theories in
let new_theories =
try
read_file c.controller_env file.file_name ?format
with _ -> (* TODO: filter only syntax error and typing errors *)
[]
in
add_file_section
c.controller_session file.file_name new_theories format old_ses old_theories
let reload_files (c : controller) =
let old_ses = c.controller_session in
......
......@@ -641,9 +641,7 @@ let load_session (file : string) =
else
session
(* add a why file from a session *)
let add_file_section (s:session) (fn:string) (theories:Theory.theory list) format : unit =
let add_theory acc (th : Theory.theory) =
let make_theory_section ?old (s:session) (th:Theory.theory) : theory =
let add_goal parent goal id =
let name,_expl,task = Termcode.goal_expl_task ~root:true goal in
mk_proof_node s name task parent id;
......@@ -655,9 +653,37 @@ let add_file_section (s:session) (fn:string) (theories:Theory.theory list) forma
theory_goals = goalsID; } in
let parent = Theory theory in
List.iter2 (add_goal parent) tasks goalsID;
theory::acc
begin
match old with
| None -> ()
| Some (old_ses,old_th) ->
let old_goals_table = Hstr.create 7 in
List.iter
(fun id ->
let pn = get_proofNode old_ses id in
Hstr.add old_goals_table pn.proofn_name.Ident.id_string pn)
old_th.theory_goals;
assert false (* TODO: merge with old theory *)
end;
theory
(* add a why file from a session *)
let add_file_section (s:session) (fn:string) (theories:Theory.theory list) format
(old_ses:session) (old_theories: theory list) : unit =
let old_th_table = Hstr.create 7 in
List.iter
(fun th -> Hstr.add old_th_table th.theory_name.Ident.id_string th)
old_theories;
let add_theory (th: Theory.theory) =
try
let old_th = Hstr.find old_th_table th.Theory.th_name.Ident.id_string in
Hstr.remove old_th_table th.Theory.th_name.Ident.id_string;
make_theory_section ~old:(old_ses,old_th) s th
with Not_found ->
make_theory_section s th
in
let theories = List.fold_left add_theory [] theories in
let theories = List.rev_map add_theory theories in
(* TODO : put remaining theories in old_th_table in the new session *)
let f = { file_name = fn;
file_format = format;
file_theories = List.rev theories }
......
......@@ -113,11 +113,15 @@ val get_trans_parent : session -> transID -> proofNodeID
val empty_session : ?shape_version:int -> unit -> session
val add_file_section :
session -> string -> (Theory.theory list) -> Env.fformat option -> unit
(** [add_file_section s fn ths] adds a new 'file' section in session
[s], named [fn], containing fresh theory subsections corresponding
to theories [ths]. The tasks of each theory nodes generated are
computed using [Task.split_theory] *)
session -> string -> (Theory.theory list) -> Env.fformat option ->
session -> theory list -> unit
(** [add_file_section s fn ths old_s old_ths] adds a new 'file'
section in session [s], named [fn], containing fresh theory
subsections corresponding to theories [ths]. The tasks of each
theory nodes generated are computed using [Task.split_theory]. For
each theory whose name is identical to one theory of old_ths, it
is attempted to associate the old goals, proof_attempts and transformations
to the goals of the new theory *)
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
timelimit:int -> unit
......
......@@ -17,7 +17,7 @@ module Unix_scheduler = struct
in
idle_handler := aux !idle_handler
(* the private list of functions to call on idle, sorted on
(* the private list of functions to call on timeout, sorted on
earliest trigger time first. *)
let timeout_handler = ref []
......
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