Commit c266cbf3 authored by MARCHE Claude's avatar MARCHE Claude

fix numbering of sub-goals

parent 6c65e7ee
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
......@@ -750,7 +750,7 @@ let notify any =
(* name is set by notify since upgrade policy may update the prover name *)
goals_model#set ~row:row#iter ~column:name_column
(match any with
| S.Goal g -> S.goal_expl_or_name g
| S.Goal g -> S.goal_user_name g
| S.Theory th -> th.S.theory_name.Ident.id_string
| S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a ->
......
......@@ -142,6 +142,7 @@ let posid_of_idpos idpos =
type 'a goal =
{ mutable goal_key : 'a;
goal_name : Ident.ident;
goal_number : int;
mutable goal_expl : string option;
goal_parent : 'a goal_parent;
mutable goal_checksum : Tc.checksum option;
......@@ -533,9 +534,9 @@ let goal_expl_lazy g =
g.goal_expl <- Some expl; expl
| None -> ""
let goal_expl_or_name g =
let goal_user_name g =
let s = goal_expl_lazy g in
if s <> "" then s else
if s <> "" then string_of_int g.goal_number ^ ". " ^ s else
try let _,_,l = restore_path g.goal_name in
String.concat "." l
with Not_found -> g.goal_name.Ident.id_string
......@@ -1031,7 +1032,8 @@ let get_edited_as_abs session pr =
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
DOES NOT record the new goal in its parent, thus this should not be exported
*)
let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum shape =
let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool)
parent name number expl sum shape =
let parent_key = match parent with
| Parent_theory mth -> mth.theory_key
| Parent_transf mtr -> mtr.transf_key
......@@ -1039,6 +1041,7 @@ let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum sh
in
let key = keygen ~parent:parent_key () in
let goal = { goal_name = name;
goal_number = number;
goal_expl = expl;
goal_parent = parent;
goal_task = None ;
......@@ -1054,7 +1057,8 @@ let raw_add_no_task ~(keygen:'a keygen) ~(expanded:bool) parent name expl sum sh
in
goal
let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl t =
let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool)
parent name number expl t =
let parent_key = match parent with
| Parent_theory mth -> mth.theory_key
| Parent_transf mtr -> mtr.transf_key
......@@ -1065,6 +1069,7 @@ let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl
(* let shape = Termcode.t_shape_buf ~version (Task.task_goal_fmla t) in *)
let shape = Termcode.t_shape_task ~version ~expl t in
let goal = { goal_name = name;
goal_number = number;
goal_expl = Some expl;
goal_parent = parent;
goal_task = Some t ;
......@@ -1269,7 +1274,7 @@ type 'key load_ctxt = {
keygen : 'key keygen;
}
let rec load_goal ctxt parent acc g =
let rec load_goal ctxt parent (acc,n) g =
match g.Xml.name with
| "goal" ->
let gname = load_ident g in
......@@ -1282,15 +1287,15 @@ let rec load_goal ctxt parent acc g =
in
let expanded = bool_attribute "expanded" g false in
let mg =
raw_add_no_task ~keygen:ctxt.keygen ~expanded parent gname expl sum shape
raw_add_no_task ~keygen:ctxt.keygen ~expanded parent gname n expl sum shape
in
List.iter (load_proof_or_transf ctxt mg) g.Xml.elements;
mg.goal_verified <- goal_verified mg;
mg::acc
| "label" -> acc
(mg::acc,n+1)
| "label" -> (acc,n)
| s ->
Warning.emit "[Warning] Session.load_goal: unexpected element '%s'@." s;
acc
(acc,n)
and load_proof_or_transf ctxt mg a =
match a.Xml.name with
......@@ -1339,10 +1344,10 @@ and load_proof_or_transf ctxt mg a =
let expanded = bool_attribute "expanded" a false in
let mtr = raw_add_transformation ~keygen:ctxt.keygen ~expanded mg trname in
mtr.transf_goals <-
List.rev
List.rev (fst
(List.fold_left
(load_goal ctxt (Parent_transf mtr))
[] a.Xml.elements);
([],1) a.Xml.elements));
(* already done by raw_add_transformation:
Hashtbl.add mg.transformations trname mtr *)
(* The attribute "proved" is required but not read *)
......@@ -1462,7 +1467,7 @@ and load_metas ctxt mg a =
| _ ->
raise (LoadError (a,"Only one goal can appear in a metas element")) in
metas.metas_goal <-
List.hd (load_goal ctxt (Parent_metas metas) [] goal);
List.hd (fst (load_goal ctxt (Parent_metas metas) ([],1) goal));
(* already done by raw_add_transformation:
Hashtbl.add mg.transformations trname mtr *)
(* The attribute "proved" is required but not read *)
......@@ -1479,10 +1484,10 @@ let load_theory ctxt mf acc th =
let checksum = Opt.map Tc.checksum_of_string csum in
let mth = raw_add_theory ~keygen:ctxt.keygen ~expanded ~checksum mf thname in
mth.theory_goals <-
List.rev
List.rev (fst
(List.fold_left
(load_goal ctxt (Parent_theory mth))
[] th.Xml.elements);
([],1) th.Xml.elements));
mth.theory_verified <- theory_verified mth;
mth::acc
| s ->
......@@ -1736,14 +1741,14 @@ let read_file env ?format fn =
let add_file ~keygen env ?format filename =
let version = env.session.session_shape_version in
let add_goal parent acc goal =
let add_goal parent (acc,n) goal =
let g =
let name,expl,task = Termcode.goal_expl_task ~root:true goal in
raw_add_task
~version
~keygen ~expanded:true
parent name expl task
in g::acc
parent name n expl task
in (g::acc,n+1)
in
let add_theory acc rfile thname theory =
let checksum = None (* Some (Tc.theory_checksum theory) *) in
......@@ -1752,7 +1757,7 @@ let add_file ~keygen env ?format filename =
in
let parent = Parent_theory rtheory in
let tasks = List.rev (Task.split_theory theory None None) in
let goals = List.fold_left (add_goal parent) [] tasks in
let goals = fst (List.fold_left (add_goal parent) ([],1) tasks) in
rtheory.theory_goals <- List.rev goals;
rtheory.theory_verified <- theory_verified rtheory;
rtheory.theory_task <- Some theory;
......@@ -1795,22 +1800,25 @@ let add_transformation ?(init=notify) ?(notify=notify) ~keygen env_session trans
let next_subgoal task =
incr i;
let gid,expl,_ = Termcode.goal_expl_task ~root:false task in
(* let expl = string_of_int !i ^ ". " ^ expl in *)
(* Format.eprintf "parent_goal_name = %s@." parent_goal_name; *)
let goal_name = parent_goal_name ^ "." ^ string_of_int !i in
let goal_name =
(* if expl = ""
then *)parent_goal_name ^ "." ^ string_of_int !i
(* else string_of_int !i ^ ". " ^ expl *)
in
let goal_name = Ident.id_register (Ident.id_derive goal_name gid) in
(* Format.eprintf "goal_name = %s@." goal_name.Ident.id_string; *)
goal_name, expl, task
in
let add_goal acc g =
let add_goal (acc,n) g =
let name,expl,task = next_subgoal g in
(* Format.eprintf "call raw_add_task with name = %s@." name.Ident.id_string; *)
let g = raw_add_task ~version:env_session.session.session_shape_version
~keygen ~expanded:false parent name expl task
~keygen ~expanded:false parent name n expl task
in
g::acc
(g::acc,n+1)
in
let goals = List.fold_left add_goal [] goals in
let goals = fst (List.fold_left add_goal ([],1) goals) in
rtransf.transf_goals <- List.rev goals;
rtransf.transf_verified <- transf_verified rtransf;
init (Transf rtransf);
......@@ -1894,7 +1902,8 @@ let add_registered_metas ~keygen env added0 g =
let metas = raw_add_metas ~keygen ~expanded:true g added idpos in
let goal =
raw_add_task ~version:env.session.session_shape_version
~keygen ~expanded:true (Parent_metas metas) g.goal_name (goal_expl_lazy g) task
~keygen ~expanded:true (Parent_metas metas) g.goal_name
1 (goal_expl_lazy g) task
in
metas.metas_goal <- goal;
metas
......@@ -2114,7 +2123,7 @@ and import_goal ~keygen parent g =
raw_add_no_task
~keygen
~expanded:g.goal_expanded
parent g.goal_name g.goal_expl g.goal_checksum g.goal_shape in
parent g.goal_name g.goal_number g.goal_expl g.goal_checksum g.goal_shape in
PHprover.iter (fun _ v -> import_proof_attempt ~keygen new_goal v)
g.goal_external_proofs;
PHstr.iter (fun k v ->
......@@ -2440,7 +2449,7 @@ and merge_metas_aux ~ctxt ~theories env to_goal _ from_metas =
let to_goal =
raw_add_task ~version:env.session.session_shape_version
~keygen:ctxt.keygen (Parent_metas to_metas) ~expanded:true
to_goal.goal_name (goal_expl_lazy to_goal) task
to_goal.goal_name 1 (goal_expl_lazy to_goal) task
in
to_metas.metas_goal <- to_goal;
Debug.dprintf debug "[Reload] metas done@\n";
......@@ -2732,7 +2741,7 @@ and add_metas_to_goal ~keygen env to_goal from_metas =
let to_goal =
raw_add_task ~version:env.session.session_shape_version
~keygen ~expanded:true (Parent_metas to_metas)
from_metas.metas_goal.goal_name
from_metas.metas_goal.goal_name 1
(goal_expl_lazy from_metas.metas_goal) task
in
to_metas.metas_goal <- to_goal;
......
......@@ -318,8 +318,8 @@ val goal_task : 'key goal -> Task.task
val goal_task_option : 'key goal -> Task.task option
(** Return the task of a goal. *)
val goal_expl_or_name : 'key goal -> string
(** Return the explication of a goal, or its name if no explanation *)
val goal_user_name : 'key goal -> string
(** Return a user-friendly name for a goal, derived from its name, its number in a sequence of sub-goals, and/or its explanation *)
val proof_verified : 'key proof_attempt -> float option
(** Return [Some t] if the proof is not obsolete and the result is
......
......@@ -191,7 +191,7 @@ let rec num_lines acc tr =
(color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_expl_or_name g);
fprintf fmt "%s</td>" (S.goal_user_name g);
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results fmt provers (goal_external_proofs g);
fprintf fmt "</tr>@\n";
......
......@@ -190,7 +190,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
if depth > 0 then fprintf fmt " & "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl_or_name g))
fprintf fmt "\\explanation{%s} " (protect (S.goal_user_name g))
else
fprintf fmt " " ;
let proofs = S.goal_external_proofs g in
......@@ -243,13 +243,13 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let proofs = S.goal_external_proofs g in
if S.PHprover.length proofs > 0 then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_expl_or_name g));
style_2_row fmt depth prov subgoal (protect (S.goal_user_name g));
print_result_prov proofs prov fmt
end
else
if (*depth = 0*) true then
begin
style_2_row fmt depth prov subgoal (protect (S.goal_expl_or_name g));
style_2_row fmt depth prov subgoal (protect (S.goal_user_name g));
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov)
end;
......
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