Commit 174542f3 authored by Clément Fumex's avatar Clément Fumex

+ add a field theory_parent_name to theory

+ complete get_first_unproven_goal_around_pn function.
parent 3d629643
......@@ -747,7 +747,7 @@ let callback_update_tree_proof cont panid pa_status =
| Some iter -> update_status_column_from_iter cont iter
| None -> ()
end;
begin match get_first_unproven_goal_around_pn_in_th cont pa.parent with
begin match get_first_unproven_goal_around_pn cont pa.parent with
| Some next_pn ->
goals_view#selection#select_iter (row_from_pn next_pn)#iter
| None -> ()
......
......@@ -16,6 +16,7 @@ let print_proofNodeID fmt id =
type theory = {
theory_name : Ident.ident;
theory_goals : proofNodeID list;
theory_parent_name : string;
mutable theory_detached_goals : proofNodeID list;
mutable theory_checksum : Termcode.checksum option;
}
......@@ -46,7 +47,6 @@ type proof_node = {
mutable proofn_transformations : transID list;
}
type transformation_node = {
transf_name : string;
transf_args : string list;
......@@ -93,6 +93,9 @@ type session = {
session_prover_ids : int Hprover.t;
}
let theory_parent s th =
Hstr.find s.session_files th.theory_parent_name
(* TODO replace *)
let init_Hpn (s : session) (h: 'a Hpn.t) (d: 'a) : unit =
Hint.iter (fun k _pn -> Hpn.replace h k d) s.proofNode_table
......@@ -629,7 +632,7 @@ and load_proof_or_transf session old_provers pid a =
"[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
s
let load_theory session old_provers acc th =
let load_theory session parent_name old_provers acc th =
match th.Xml.name with
| "theory" ->
let thname = load_ident th in
......@@ -641,6 +644,7 @@ let load_theory session old_provers acc th =
let mth = { theory_name = thname;
theory_checksum = checksum;
theory_goals = goals;
theory_parent_name = parent_name;
theory_detached_goals = [] } in
List.iter2
(load_goal session old_provers (Theory mth))
......@@ -658,7 +662,7 @@ let load_file session old_provers f =
let fmt = load_option "format" f in
let ft = List.rev
(List.fold_left
(load_theory session old_provers) [] f.Xml.elements) in
(load_theory session fn old_provers) [] f.Xml.elements) in
let mf = { file_name = fn;
file_format = fmt;
file_theories = ft;
......@@ -903,13 +907,14 @@ let save_detached_goals old_s detached_goals_id s parent =
id)
detached_goals_id
let save_detached_theory old_s detached_theory s =
let save_detached_theory parent_name old_s detached_theory s =
let goalsID =
save_detached_goals old_s detached_theory.theory_goals s (Theory detached_theory) in
(* List.map (fun _ -> gen_proofNodeID s) detached_theory.theory_goals in *)
{ theory_name = detached_theory.theory_name;
theory_checksum = None;
theory_goals = goalsID;
theory_parent_name = parent_name;
theory_detached_goals = [] }
let merge_proof new_s obsolete new_goal _ old_pa_n =
......@@ -1050,7 +1055,8 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
(* add a theory and its goals to a session. if a previous theory is
provided in merge try to merge the new theory with the previous one *)
let make_theory_section ~use_shapes ?merge (s:session) (th:Theory.theory) : theory =
let make_theory_section ~use_shapes ?merge (s:session) parent_name (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 ~version:s.session_shape_version s name task parent id;
......@@ -1060,6 +1066,7 @@ let make_theory_section ~use_shapes ?merge (s:session) (th:Theory.theory) : the
let theory = { theory_name = th.Theory.th_name;
theory_checksum = None;
theory_goals = goalsID;
theory_parent_name = parent_name;
theory_detached_goals = [] } in
let parent = Theory theory in
List.iter2 (add_goal parent) tasks goalsID;
......@@ -1077,7 +1084,7 @@ let add_file_section ~use_shapes (s:session) (fn:string) (theories:Theory.theory
if Hstr.mem s.session_files fn then
Debug.dprintf debug "[session] file %s already in database@." fn
else
let theories = List.map (make_theory_section ~use_shapes s) theories in
let theories = List.map (make_theory_section ~use_shapes s fn) theories in
let f = { file_name = fn;
file_format = format;
file_theories = theories;
......@@ -1106,16 +1113,16 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
(* if we found one, we remove it from the table and merge it *)
let old_th = Hstr.find old_th_table theory_name in
Hstr.remove old_th_table theory_name;
make_theory_section ~use_shapes ~merge:(old_ses,old_th,env) s th
make_theory_section ~use_shapes ~merge:(old_ses,old_th,env) s fn th
with Not_found ->
(* if no theory was found we make a new theory section *)
make_theory_section ~use_shapes s th
make_theory_section ~use_shapes s fn th
in
let theories = List.map add_theory theories in
(* we save the remaining, detached *)
let detached = Hstr.fold
(fun _key th tl ->
(save_detached_theory old_ses th s) :: tl)
(save_detached_theory fn old_ses th s) :: tl)
old_th_table [] in
theories, detached
in
......
......@@ -31,10 +31,6 @@ val init_Htn: session ->'a Htn.t -> 'a -> unit
type theory
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
type file = private {
file_name : string;
file_format : string option;
......@@ -42,11 +38,15 @@ type file = private {
file_detached_theories : theory list;
}
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file
val get_files : session -> file Stdlib.Hstr.t
val get_dir : session -> string
val get_shape_version : session -> int
type proof_attempt_node = {
parent : proofNodeID;
prover : Whyconf.prover;
......
......@@ -59,6 +59,9 @@ let cont_from_files spec usage_str env files provers =
(* list unproven goal and related *)
(**********************************)
(* If the transformation is proved, return acc.
Else, return the concatenation of the reversed list of unproven
goals below the transformation and acc *)
let rec unproven_goals_below_tn cont acc tn =
if tn_proved cont tn then
acc (* we ignore "dead" goals *)
......@@ -66,8 +69,8 @@ let rec unproven_goals_below_tn cont acc tn =
let sub_tasks = get_sub_tasks cont.controller_session tn in
List.fold_left (unproven_goals_below_pn cont) acc sub_tasks
(* note that if goal is not proved and there is no transformation goal
is returned *)
(* Same as unproven_goals_below_tn; note that if goal is not proved
and there is no transformation, goal is returned (else it is not) *)
and unproven_goals_below_pn cont acc goal =
if pn_proved cont goal then
acc (* we ignore "dead" transformations *)
......@@ -76,6 +79,7 @@ and unproven_goals_below_pn cont acc goal =
| [] -> goal :: acc
| tns -> List.fold_left (unproven_goals_below_tn cont) acc tns
(* Same as unproven_goals_below_tn *)
let unproven_goals_below_th cont acc th =
if th_proved cont th then
acc
......@@ -83,6 +87,7 @@ let unproven_goals_below_th cont acc th =
let goals = theory_goals th in
List.fold_left (unproven_goals_below_pn cont) acc goals
(* Same as unproven_goals_below_tn *)
let unproven_goals_below_file cont file =
if file_proved cont file then
[]
......@@ -90,6 +95,7 @@ let unproven_goals_below_file cont file =
let theories = file.file_theories in
List.fold_left (unproven_goals_below_th cont) [] theories
(* returns the list of unproven goals in the controller session *)
let unproven_goals_in_session cont =
let files = get_files cont.controller_session in
Stdlib.Hstr.fold (fun _key file acc ->
......@@ -97,23 +103,27 @@ let unproven_goals_in_session cont =
List.rev_append file_goals acc)
files []
(*
[get_first_unproven_goal_around_pn_in_th cont pn]
(* [get_first_unproven_goal_around_pn cont pn]
returns the `first unproven goal' 'after' [pn]. Precisely:
(1) it finds the youngest ancestor a of [pn] that is not proved
(2) it returns the first unproved leaf of a
it returns None if all ancestors are proved (in the theory)
*)
let get_first_unproven_goal_around_pn_in_th cont pn : proofNodeID option =
it returns None if all ancestors are proved *)
let get_first_unproven_goal_around_pn cont pn =
let ses = cont.controller_session in
let rec look_around pn =
match get_proof_parent ses pn with
| Trans tn ->
begin match unproven_goals_below_tn cont [] tn with
| [] -> look_around (get_trans_parent ses tn)
| l -> l
end
| Theory th -> unproven_goals_below_th cont [] th
if tn_proved cont tn
then look_around (get_trans_parent ses tn)
else unproven_goals_below_tn cont [] tn
| Theory th ->
if th_proved cont th then begin
let parent = (theory_parent ses th) in
if file_proved cont parent
then unproven_goals_in_session cont
else unproven_goals_below_file cont parent
end else
unproven_goals_below_th cont [] th
in
match look_around pn with
| [] -> None
......
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