Commented out references to tree which should not be used.

Adapted work on nearest_goal_right to be able to use it why3shell.
Now should be able to apply transformation and proof on current goal. Also
able to print the current tree and goal. Requires testing.

src/session/session_itp.ml

@@ -86,6 +86,7 @@ let session_iter_proof_attempt f =
          (fun _ pan -> f pan.proofa_attempt)
         pn.proofn_attempts)
 
+(* This is not needed. Keeping it as information on the structure
 type tree = {
     tree_node_id : proofNodeID;
     tree_goal_name : string;
@@ -93,7 +94,9 @@ type tree = {
     tree_transformations : (transID * string * tree list) list;
                                 (* transformations on this node *)
   }
+*)
 
+(*
 let rec get_tree s id : tree =
   let t = Hint.find s.proofNode_table id in
   let pal =
@@ -109,6 +112,7 @@ let rec get_tree s id : tree =
 and get_trans s id =
   let tr = Hint.find s.trans_table id in
   (id, tr.transf_name, List.map (get_tree s) tr.transf_subtasks)
+*)
 
 (*
 let get_theories s =
@@ -125,11 +129,13 @@ let get_theories s =
 
 let get_files s = s.session_files
 
+(*
 let get_node (s : session) (n : int) =
   let _ = Hint.find s.proofNode_table n in n
 
 let get_trans (s : session) (n : int) =
   let _ = Hint.find s.trans_table n in n
+*)
 
 let gen_transID (s : session) =
   let id = s.next_transID in
@@ -194,6 +200,30 @@ let print_proof_attempt fmt pa =
           pa.limit.Call_provers.limit_time
           (Pp.print_option Call_provers.print_prover_result) pa.proof_state
 
+let rec print_proof_node s (fmt: Format.formatter) p =
+  let pn = get_proofNode s p in
+  let parent = match pn.proofn_parent with
+  | Theory t -> t.theory_name.id_string
+  | Trans id -> (get_transfNode s id).transf_name
+  in
+  fprintf fmt
+    "@[<hv 2> Goal %s;@ parent %s;@ sum %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
+    pn.proofn_name.id_string parent
+    (Opt.fold (fun _ a -> Termcode.string_of_checksum a) "None" pn.proofn_checksum)
+    (Pp.print_list Pp.semi print_proof_attempt)
+      (Hprover.fold (fun _key e l -> e.proofa_attempt :: l) pn.proofn_attempts [])
+    (Pp.print_list Pp.semi (print_trans_node s)) pn.proofn_transformations
+
+and print_trans_node s fmt id =
+  let tn = get_transfNode s id in
+  let name = tn.transf_name in
+  let l = tn.transf_subtasks in
+  let parent = (get_proofNode s tn.transf_parent).proofn_name.id_string in
+  fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent
+    (Pp.print_list Pp.semi (print_proof_node s)) l
+
+
+(*
 let rec print_tree s fmt t =
   let pn = get_proofNode s t.tree_node_id in
   let parent = match pn.proofn_parent with
@@ -212,19 +242,20 @@ and print_trans s fmt (id, name, l) =
   let parent = (get_proofNode s tn.transf_parent).proofn_name.id_string in
   fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent
     (Pp.print_list Pp.semi (print_tree s)) l
+*)
+
+let print_theory s fmt th : unit =
+  fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" th.theory_name.Ident.id_string
+    (Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) th.theory_goals
+
+let print_file s fmt (file, thl) =
+  fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
+    (Pp.print_list Pp.semi (print_theory s)) thl
+
+let print_s s fmt =
+  fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
 
 let print_session fmt s =
-  let print_theory s fmt th =
-    fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" th.theory_name.Ident.id_string
-      (Pp.print_list Pp.semi (fun fmt a -> print_tree s fmt (get_tree s a))) th.theory_goals
-  in
-  let print_file s fmt (file, thl) =
-    fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
-      (Pp.print_list Pp.semi (print_theory s)) thl
-  in
-  let print_s s fmt =
-    fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
-  in
   let l = Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
   fprintf fmt "%a@." (print_s s) l;;
 

src/session/session_itp.mli

@@ -61,6 +61,7 @@ type trans_arg =
 
 type proof_parent = Trans of transID | Theory of theory
 
+(* This is not needed
 type tree = {
     tree_node_id : proofNodeID;
     tree_goal_name : string;
@@ -73,18 +74,33 @@ type tree = {
   goal when all subgoals have a complete proof.  In other word, the
   list of proof_attempt and transformation are "disjunctive" but the
   list of tree below a transformation is "conjunctive" *)
+*)
 
-
+(*
 val get_tree : session -> proofNodeID -> tree
 (** [get_tree s id] returns the proof tree of the goal identified by
     [id] *)
+*)
 
 val get_task : session -> proofNodeID -> Task.task
 
 (* temp *)
+(*
 val get_node : session -> int -> proofNodeID
 val get_trans : session -> int -> transID
-val print_tree : session -> Format.formatter -> tree -> unit
+*)
+
+(* [print_proof_node s fmt t]: From definition of s, print on fmt the tree
+   rooted at element t *)
+val print_proof_node : session -> Format.formatter -> proofNodeID -> unit
+
+(* [print_theory s fmt t]: From definition of s, print on fmt the theory t *)
+val print_theory : session -> Format.formatter -> theory -> unit
+
+(* [print_trans s fmt tn]: From definition of s, print on fmt the tree originating
+   from transformation tn *)
+val print_trans_node : session -> Format.formatter -> transID -> unit
+
 val print_session : Format.formatter -> session -> unit
 
 (* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)

src/why3shell/why3shell.ml

@@ -237,6 +237,19 @@ let zipper =
   | th :: tail -> { cursor = (Th ([], th, tail)); ctxt }
   | _ -> assert false
 
+let zipper_init () =
+  let files =
+    get_files cont.Controller_itp.controller_session
+  in
+  let file = ref None in
+  Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
+  let file = Opt.get !file in
+  match file.file_theories with
+  | th :: tail -> zipper.cursor <- (Th ([], th, tail));
+      while not (Queue.is_empty zipper.ctxt) do ignore (Queue.pop zipper.ctxt) done
+  | _ -> assert false
+
+
 let zipper_down () =
   match zipper.cursor with
   | Th (_,th,_) ->
@@ -301,18 +314,52 @@ and next_node_no_down () =
 
 let prev_node = zipper_left () || zipper_up ()
 
+(* This function always move from current position to the next goal even when on a goal *)
 let rec nearest_goal_right () =
+  if next_node () then
+    match zipper.cursor with
+    | Pn (_,pn,_) -> Some pn
+    | _  -> nearest_goal_right ()
+  else
+    None
+
+let print_position (s: session) (cursor: proof_zipper) fmt: unit =
+  match cursor.cursor with
+  | Th (_, th, _) -> fprintf fmt "%a@." (print_theory s) th
+  | Pn (_, pn, _) -> fprintf fmt "%a@." (print_proof_node s) pn
+  | Tn (_, tn, _) -> fprintf fmt "%a@." (print_trans_node s) tn
+
+let print_position_p s cursor fmt _ = print_position s cursor fmt
+
+(* This function try to get the id of the nearest goal right. If it can't, it tries
+   to get you to the first goal of the session. If this is still not possible,
+   it returns an error. *)
+let ngr_ret () =
+  match
+    (match nearest_goal_right () with
+    | None -> Printf.eprintf "No more goal right. You might want to go back to the root@.";
+	zipper_init(); nearest_goal_right ()
+    | Some id -> Some id) with
+  | None -> failwith "After initialization there is no goal to go to@."
+  | Some id -> id
+
+(* The cursor of the zipper is on a goal *)
+let is_goal_cursor () =
   match zipper.cursor with
-  | Pn (_,pn,_) -> Some pn
-  | _  ->
-    if next_node () then
-      nearest_goal_right ()
-    else
-      None
+  | Pn (_, pn, _) -> Some pn
+  | _ -> None
+
+let ngr_ret_p _ _ = ignore (ngr_ret ())
+
+(* If on goal, do nothing else go to next_goal *)
+let nearest_goal () =
+  match (is_goal_cursor ()) with
+  | None -> ngr_ret ()
+  | Some id -> id
 
 let test_schedule_proof_attempt fmt _args =
   (* temporary : get the first goal *)
-  let Some id = nearest_goal_right () in
+  let id = nearest_goal () in
   let callback status =
     fprintf fmt "status: %a@."
             Controller_itp.print_status status
@@ -324,7 +371,7 @@ let test_schedule_proof_attempt fmt _args =
 
 let test_transformation fmt _args =
   (* temporary : apply split on the first goal *)
-  let Some id = nearest_goal_right () in
+  let id = nearest_goal () in
   let callback status =
     fprintf fmt "transformation status: %a@."
             Controller_itp.print_trans_status status
@@ -337,9 +384,10 @@ let task_driver =
   in
   Driver.load_driver env d []
 
+(* Print current goal or nearest next goal if we are not on a goal *)
 let test_print_goal fmt _args =
   (* temporary : get the first goal *)
-  let Some id = nearest_goal_right () in
+  let id = nearest_goal () in
   let task = Session_itp.get_task cont.Controller_itp.controller_session id in
   fprintf fmt "@[====================== Task =====================@\n%a@]@."
     (Driver.print_task ~cntexample:false task_driver) task
@@ -369,7 +417,9 @@ let commands =
     "g", "prints the first goal", test_print_goal;
     "r", "reload the session (test only)", test_reload;
     "s", "[s my_session] save the current session in my_session.xml", test_save_session;
-    "tr", "test schedule_transformation with split_goal on the first goal", test_transformation;
+    "tr", "test schedule_transformation with split_goal on the current or next right goal (or on the top goal if there is none", test_transformation;
+    "ngr", "get to the next goal right", ngr_ret_p;
+    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper)
   ]
 
 let commands_table = Stdlib.Hstr.create 17