Request to locate next unproven node.

src/ide/ide_utils.ml

@@ -68,33 +68,3 @@ module History = struct
     h.tr <- false
 
 end
-
-(***********************)
-(* First Unproven goal *)
-(***********************)
-
-(* Children should not give the proof attempts *)
-let rec unproven_goals_below_node ~proved ~children ~is_goal acc node =
-  if proved node then
-    acc
-  else
-    let nodes = children node in
-    if is_goal node && nodes = [] then
-      node :: acc
-    else
-      List.fold_left (unproven_goals_below_node ~proved ~children ~is_goal)
-        acc nodes
-
-let get_first_unproven_goal_around ~proved ~children ~get_parent ~is_goal node =
-  let rec look_around node =
-    match get_parent node with
-    | None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
-    | Some parent ->
-        if proved parent then
-          look_around parent
-        else
-          unproven_goals_below_node ~proved ~children ~is_goal [] parent
-  in
-  match look_around node with
-  | [] -> None
-  | hd :: _tl  -> Some hd

src/ide/ide_utils.mli

@@ -9,9 +9,3 @@ module History : sig
   val add_command: history -> string -> unit
 
 end
-
-val get_first_unproven_goal_around:
-    proved:('a -> bool) ->
-      children:('a -> 'a list) ->
-        get_parent:('a -> 'a option) ->
-          is_goal:('a -> bool) -> 'a -> 'a option

src/ide/why3ide.ml

@@ -939,7 +939,7 @@ let if_selected_alone id f =
   match get_selected_row_references () with
   | [r] ->
      let i = get_node_id r#iter in
-     if i = id || Some i = get_parent id  then f id
+     if i = id || Some i = get_parent id then f id
   | _ -> ()
 
 let treat_notification n = match n with
@@ -947,29 +947,22 @@ let treat_notification n = match n with
      begin
        match uinfo with
        | Proved b ->
-          Hint.replace node_id_proved id b;
-          set_status_column (get_node_row id)#iter
+           Hint.replace node_id_proved id b;
+           set_status_column (get_node_row id)#iter;
+           (* Trying to move cursor on first unproven goal around on all cases
+              but not when proofAttempt is updated because ad hoc debugging. *)
+           send_request (Get_first_unproven_node id)
        | Proof_status_change (pa, obs, l) ->
           let r = get_node_row id in
           Hint.replace node_id_pa id (pa, obs, l);
           goals_model#set ~row:r#iter ~column:status_column
                           (image_of_pa_status ~obsolete:obs pa)
-     end;
-     (* Moving cursor on first unproved goal around *)
-     if_selected_alone
-       id
-       (fun _ ->
-        let node =
-          get_first_unproven_goal_around
-            ~proved:proved
-            ~children:children ~get_parent:get_parent ~is_goal:is_goal id
-        in
-        match node with
-        | None -> ()
-        | Some node ->
-           let iter = (get_node_row node)#iter in
-           goals_view#selection#select_iter iter)
-
+     end
+  | Next_Unproven_Node_Id (asked_id, next_unproved_id) ->
+      if_selected_alone asked_id
+          (fun _ ->
+            let iter = (get_node_row next_unproved_id)#iter in
+            goals_view#selection#select_iter iter)
   | New_node (id, parent_id, typ, name, detached) ->
      begin
        try

src/session/controller_itp.ml

@@ -101,6 +101,25 @@ let file_proved c f =
   else
     List.for_all (fun th -> th_proved c th) f.file_theories
 
+let any_proved cont any : bool =
+  match any with
+  | AFile file -> file_proved cont file
+  | ATh th -> th_proved cont th
+  | ATn tn -> tn_proved cont tn
+  | APn pn -> pn_proved cont pn
+  | APa pa ->
+      begin
+        let pa = get_proof_attempt_node cont.controller_session pa in
+        match pa.proof_state with
+        | None -> false
+        | Some pa ->
+          begin
+            match pa.Call_provers.pr_answer with
+            | Call_provers.Valid -> true
+            | _ -> false
+          end
+      end
+
 (* Update the result of the theory according to its children *)
 let update_theory_proof_state notification ps th =
   let goals = theory_goals th in
@@ -152,7 +171,7 @@ and update_proof notification c id =
 (* [update_proof_node c id b] Update the whole proof_state
    of c according to the result (id, b) *)
 let update_proof_node notification c id b =
-  if (Hpn.mem c.proof_state.pn_state id) then
+  if Hpn.mem c.proof_state.pn_state id then
   begin
     let b' = Hpn.find_def c.proof_state.pn_state false id in
     if b != b' then
@@ -172,7 +191,7 @@ let update_proof_node notification c id b =
 (* [update_trans_node c id b] Update the proof_state of c to take the result of
    (id,b). Then propagates it to its parents *)
 let update_trans_node notification c id b =
-  if (Htn.mem c.proof_state.tn_state id) then
+  if Htn.mem c.proof_state.tn_state id then
   begin
     let b' = Htn.find_def c.proof_state.tn_state false id in
     if b != b' then
@@ -215,6 +234,15 @@ let reload_theory_proof_state c th =
   Hid.replace ps.th_state (theory_name th)
     proved
 
+(* Get children of any without proofattempts *)
+let get_undetached_children_no_pa s any : any list =
+  match any with
+  | AFile f -> List.map (fun th -> ATh th) f.file_theories
+  | ATh th  -> List.map (fun g -> APn g) (theory_goals th)
+  | ATn tn  -> List.map (fun pn -> APn pn) (get_sub_tasks s tn)
+  | APn pn  -> List.map (fun tn -> ATn tn) (get_transformations s pn)
+  | APa pa -> []
+
 (* printing *)
 
 module PSession = struct

src/session/controller_itp.mli

@@ -89,6 +89,7 @@ val tn_proved: controller -> Session_itp.transID -> bool
 val pn_proved: controller -> Session_itp.proofNodeID -> bool
 val th_proved: controller -> Session_itp.theory -> bool
 val file_proved: controller -> Session_itp.file -> bool
+val any_proved: controller -> any -> bool
 
 val print_session : Format.formatter -> controller -> unit
 
@@ -145,6 +146,8 @@ 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 get_undetached_children_no_pa: Session_itp.session -> any -> any list
+
 module Make(S : Scheduler) : sig
 
 val set_max_tasks : int -> unit

src/session/itp_communication.ml

@@ -59,6 +59,9 @@ type notification =
   (* inform that the data of the given node changed *)
   | Remove       of node_ID
   (* the given node was removed *)
+  | Next_Unproven_Node_Id of node_ID * node_ID
+  (* Next_Unproven_Node_Id (asked_id, next_unproved_id). Returns a node and the
+     next unproven node from this node *)
   | Initialized  of global_information
   (* initial global data *)
   | Saved
@@ -73,18 +76,19 @@ type notification =
   (* contents of the file *)
 
 type ide_request =
-  | Command_req       of node_ID * string
-  | Prove_req         of node_ID * prover * Call_provers.resource_limit
-  | Transform_req     of node_ID * transformation * string list
-  | Strategy_req      of node_ID * strategy
-  | Open_session_req  of string
-  | Add_file_req      of string
-  | Set_max_tasks_req of int
-  | Get_file_contents of string
-  | Get_task          of node_ID
-  | Remove_subtree    of node_ID
-  | Copy_paste        of node_ID * node_ID
-  | Copy_detached     of node_ID
+  | Command_req             of node_ID * string
+  | Prove_req               of node_ID * prover * Call_provers.resource_limit
+  | Transform_req           of node_ID * transformation * string list
+  | Strategy_req            of node_ID * strategy
+  | Open_session_req        of string
+  | Add_file_req            of string
+  | Set_max_tasks_req       of int
+  | Get_file_contents       of string
+  | Get_task                of node_ID
+  | Remove_subtree          of node_ID
+  | Copy_paste              of node_ID * node_ID
+  | Copy_detached           of node_ID
+  | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
   | Save_req
   | Reload_req

src/session/itp_communication.mli

@@ -64,6 +64,9 @@ type notification =
   (* inform that the data of the given node changed *)
   | Remove       of node_ID
   (* the given node was removed *)
+  | Next_Unproven_Node_Id of node_ID * node_ID
+  (* Next_Unproven_Node_Id (asked_id, next_unproved_id). Returns a node and the
+     next unproven node from this node *)
   | Initialized  of global_information
   (* initial global data *)
   | Saved
@@ -78,18 +81,19 @@ type notification =
   (* contents of the file *)
 
 type ide_request =
-  | Command_req       of node_ID * string
-  | Prove_req         of node_ID * prover * Call_provers.resource_limit
-  | Transform_req     of node_ID * transformation * string list
-  | Strategy_req      of node_ID * strategy
-  | Open_session_req  of string
-  | Add_file_req      of string
-  | Set_max_tasks_req of int
-  | Get_file_contents of string
-  | Get_task          of node_ID
-  | Remove_subtree    of node_ID
-  | Copy_paste        of node_ID * node_ID
-  | Copy_detached     of node_ID
+  | Command_req             of node_ID * string
+  | Prove_req               of node_ID * prover * Call_provers.resource_limit
+  | Transform_req           of node_ID * transformation * string list
+  | Strategy_req            of node_ID * strategy
+  | Open_session_req        of string
+  | Add_file_req            of string
+  | Set_max_tasks_req       of int
+  | Get_file_contents       of string
+  | Get_task                of node_ID
+  | Remove_subtree          of node_ID
+  | Copy_paste              of node_ID * node_ID
+  | Copy_detached           of node_ID
+  | Get_first_unproven_node of node_ID
   | Get_Session_Tree_req
   | Save_req
   | Reload_req

src/session/itp_server.ml

@@ -283,6 +283,7 @@ let print_request fmt r =
   | Add_file_req f                  -> fprintf fmt "open file %s" f
   | Set_max_tasks_req i             -> fprintf fmt "set max tasks %i" i
   | Get_file_contents _f            -> fprintf fmt "get file contents"
+  | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
   | Get_task _nid                   -> fprintf fmt "get task"
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
   | Copy_paste _                    -> fprintf fmt "copy paste"
@@ -313,6 +314,7 @@ let print_notify fmt n =
   | Node_change (_ni, _nf)             -> fprintf fmt "node change"
   | New_node (ni, _pni, _nt,  _nf, _d) -> fprintf fmt "new node %d" ni
   | Remove _ni                         -> fprintf fmt "remove"
+  | Next_Unproven_Node_Id (_ni, _nj)   -> fprintf fmt "next unproven node_id"
   | Initialized _gi                    -> fprintf fmt "initialized"
   | Saved                              -> fprintf fmt "saved"
   | Message msg                        ->
@@ -530,7 +532,6 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
     | APn pn     -> node_ID_from_pn pn
     | APa pan    -> node_ID_from_pan pan
 
-
   let get_prover p =
     let d = get_server_data () in
     match return_prover p d.config with
@@ -871,8 +872,29 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
     (* TODO make replay print *)
     C.replay ~use_steps:false d.cont ~callback:callback ~remove_obsolete:false
 
+  (* ----------------- locate next unproven node -------------------- *)
+
+  let notify_first_unproven_node d ni =
+    let any = any_from_node_ID ni in
+      let unproven_any =
+        get_first_unproven_goal_around
+          ~proved:(Controller_itp.any_proved d.cont)
+          ~children:(get_undetached_children_no_pa d.cont.controller_session)
+          ~get_parent:(get_any_parent d.cont.controller_session)
+          ~is_goal:(fun any -> match any with | APn _ -> true | _ -> false)
+          ~is_pa:(fun any -> match any with | APa _ -> true | _ -> false)
+          any in
+      begin
+        match unproven_any with
+        | None -> () (* If no node is found we don't tell IDE to move *)
+        | Some any ->
+            P.notify (Next_Unproven_Node_Id (ni, node_ID_from_any any))
+      end
+
+
   (* ----------------- treat_request -------------------- *)
 
+
   let get_proof_node_id nid =
     try
       match any_from_node_ID nid with
@@ -898,6 +920,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
     | Save_req                     -> save_session ()
     | Reload_req                   -> reload_session ()
     | Get_Session_Tree_req         -> resend_the_tree ()
+    | Get_first_unproven_node ni   ->
+      notify_first_unproven_node d ni
     | Remove_subtree nid           ->
         let n = any_from_node_ID nid in
         begin

src/session/server_utils.ml

@@ -282,3 +282,36 @@ let interp commands commands_table config cont id s =
       Transform (cmd,t,args)
     with Trans.UnknownTrans _ ->
       interp_others commands config cmd args
+
+
+(***********************)
+(* First Unproven goal *)
+(***********************)
+
+(* Children should not give the proof attempts *)
+let rec unproven_goals_below_node ~proved ~children ~is_goal acc node =
+  if proved node then
+    acc
+  else
+    let nodes = children node in
+    if is_goal node && nodes = [] then
+      node :: acc
+    else
+      List.fold_left (unproven_goals_below_node ~proved ~children ~is_goal)
+        acc nodes
+
+let get_first_unproven_goal_around
+    ~proved ~children ~get_parent ~is_goal ~is_pa node =
+  let rec look_around node =
+    match get_parent node with
+    | None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
+    | Some parent ->
+        if proved parent then
+          look_around parent
+        else
+          unproven_goals_below_node ~proved ~children ~is_goal [] parent
+  in
+  let node = if is_pa node then Opt.get (get_parent node) else node in
+  match List.rev (look_around node) with
+  | [] -> None
+  | hd :: _tl  -> Some hd

src/session/server_utils.mli

@@ -53,3 +53,11 @@ val interp: (string * string * 'a) list ->
     Whyconf.config ->
       Controller_itp.controller ->
         Session_itp.proofNodeID option -> string -> command
+
+
+val get_first_unproven_goal_around:
+    proved:('a -> bool) ->
+      children:('a -> 'a list) ->
+        get_parent:('a -> 'a option) ->
+          is_goal:('a -> bool) ->
+            is_pa:('a -> bool) -> 'a -> 'a option