GTK IDE: command 'auto'

src/ide/why3ide.ml

@@ -420,67 +420,59 @@ let build_tree_from_session ses =
    do not want to move the current index with the computing of strategy. *)
 let current_selected_index = ref Inone
 
-(* TODO maybe an other file for callbacks *)
 (* Callback of a transformation *)
-let callback_update_tree_transform ses row_reference = fun status ->
+let callback_update_tree_transform ses status =
   match status with
   | TSdone trans_id ->
-      build_subtree_from_trans ses row_reference trans_id;
-      (match Session_itp.get_sub_tasks ses trans_id with
+     let id = get_trans_parent ses trans_id in
+     let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
+     build_subtree_from_trans ses row_ref trans_id;
+     (match Session_itp.get_sub_tasks ses trans_id with
       | first_goal :: _ ->
-          (* Put the selection on the first goal *)
-          goals_view#selection#select_iter (Hpn.find pn_id_to_gtree first_goal)#iter
+         (* Put the selection on the first goal *)
+         goals_view#selection#select_iter (Hpn.find pn_id_to_gtree first_goal)#iter
       | [] -> ())
   | _ -> ()
 
 let apply_transform ses t args =
   match !current_selected_index with
   | IproofNode id ->
-    let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
-    let callback =
-         callback_update_tree_transform ses row_ref
-       in
-       C.schedule_transformation cont id t args ~callback
-    | _ -> printf "Error: Give the name of the transformation@."
+     let callback = callback_update_tree_transform ses in
+    C.schedule_transformation cont id t args ~callback
+  | _ -> printf "Error: Give the name of the transformation@."
 
 
-let remove_children iter =
-  if (goals_model#iter_has_child iter) then
-    ignore (goals_model#remove (goals_model#iter_children (Some iter)))
-  else ()
-
 (* Callback of a proof_attempt *)
-let callback_update_tree_proof _ses row_ref _id name =
-  fun panid pa_status ->
+let callback_update_tree_proof ses panid pa_status =
+  let pa = get_proof_attempt ses panid in
+  let prover = pa.prover in
+  let name = Pp.string_of Whyconf.print_prover prover in
   match pa_status with
-    | Scheduled ->
-       begin
-       try
-         let _new_row_ref = Hpan.find pan_id_to_gtree panid in
-         () (* TODO: set icon to 'pause' *)
-       with Not_found ->
-            ignore(new_node ~parent:row_ref (name ^ " scheduled") (IproofAttempt panid))
-       end
-  | Done _pr ->
-       begin
+  | Scheduled ->
+     begin
        try
          let r = Hpan.find pan_id_to_gtree panid in
-         goals_model#set ~row:r#iter ~column:name_column (name ^ " done")
-       with Not_found -> assert false
-       end
-  | Running -> () (* TODO: set icon to 'play' *)
+         goals_model#set ~row:r#iter ~column:name_column (name ^ " scheduled")
+       with Not_found ->
+         let parent_id = get_proof_attempt_parent ses panid in
+         let parent = Hpn.find pn_id_to_gtree parent_id in
+         ignore(new_node ~parent (name ^ " scheduled") (IproofAttempt panid))
+     end
+  | Done pr ->
+     let r = Hpan.find pan_id_to_gtree panid in
+     let res = Pp.string_of Call_provers.print_prover_result pr in
+     goals_model#set ~row:r#iter ~column:name_column (name ^ " " ^ res)
+  | Running ->
+     let r = Hpan.find pan_id_to_gtree panid in
+     goals_model#set ~row:r#iter ~column:name_column (name ^ " running")
   | _ ->  () (* TODO ? *)
 
 let test_schedule_proof_attempt ses (p: Whyconf.config_prover) limit =
   match !current_selected_index with
   | IproofNode id ->
-    let row_ref = Hpn.find pn_id_to_gtree id in
     let prover = p.Whyconf.prover in
-    let printing = prover.Whyconf.prover_name ^ "(" ^ prover.Whyconf.prover_version ^ ")" in
-    let callback = callback_update_tree_proof ses row_ref id printing in
-        C.schedule_proof_attempt
-          cont id prover
-          ~limit ~callback
+    let callback = callback_update_tree_proof ses in
+    C.schedule_proof_attempt cont id prover ~limit ~callback
   | _ -> message_zone#buffer#set_text ("Must be on a proof node to use a prover.")
 
 
@@ -498,7 +490,13 @@ let run_strategy_on_task s =
           let callback sts =
             printf "Strategy status: %a@." print_strategy_status sts
           in
-          C.run_strategy_on_goal cont id st ~callback
+          let callback_pa =
+            callback_update_tree_proof cont.controller_session
+          in
+          let callback_tr st =
+            callback_update_tree_transform cont.controller_session st
+          in
+          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
     | _ -> printf "Strategy '%s' not found@." s
      end
   | _ -> ()

src/session/controller_itp.ml

@@ -396,14 +396,15 @@ let schedule_transformation c id name args ~callback =
 
 open Strategy
 
-let run_strategy_on_goal c id strat ~callback =
+let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback =
   let rec exec_strategy pc strat g =
     if pc < 0 || pc >= Array.length strat then
       callback STShalt
     else
       match Array.get strat pc with
       | Icall_prover(p,timelimit,memlimit) ->
-         let callback _panid res =
+         let callback panid res =
+           callback_pa panid res;
            match res with
            | Scheduled | Running -> (* nothing to do yet *) ()
            | Done { Call_provers.pr_answer = Call_provers.Valid } ->
@@ -425,6 +426,7 @@ let run_strategy_on_goal c id strat ~callback =
          schedule_proof_attempt c g p ~limit ~callback
       | Itransform(trname,pcsuccess) ->
          let callback ntr =
+           callback_tr ntr;
            match ntr with
            | TSfailed -> (* transformation failed *)
               callback (STSgoto (g,pc+1));
@@ -439,8 +441,7 @@ let run_strategy_on_goal c id strat ~callback =
                    exec_strategy pcsuccess strat g; false
                  in
                  S.idle ~prio:0 run_next)
-                (get_sub_tasks c.controller_session tid);
-              (*Todo._done todo*) ()
+                (get_sub_tasks c.controller_session tid)
          in
          schedule_transformation c g trname [] ~callback
       | Igoto pc ->

src/session/controller_itp.mli

@@ -169,15 +169,19 @@ val schedule_transformation :
    the transformation status changes. Typically at Scheduled, then
    Done tid.*)
 
-
 val run_strategy_on_goal :
   controller ->
   proofNodeID ->
   Strategy.t ->
+  callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
+  callback_tr:(transformation_status -> unit) ->
   callback:(strategy_status -> unit) -> unit
 (** [run_strategy_on_goal c id strat] executes asynchronously the
-    strategy [strat] on the goal [id].  TODO: add callback to get
-    inform of the progress *)
+    strategy [strat] on the goal [id].  [callback_pa] is called for
+    each proof attempted (as in [schedule_proof_attempt]) and
+    [callback_tr] is called for each transformation applied (as in
+    [schedule_transformation]). [callback] is called on each step of
+    execution of the strategy.  *)
 
 type report =
   | Result of Call_provers.prover_result * Call_provers.prover_result

src/session/session_itp.ml

@@ -207,6 +207,12 @@ let get_transformations (s : session) (id : proofNodeID) =
 let get_proof_attempt_ids (s : session) (id : proofNodeID) =
   (get_proofNode s id).proofn_attempts
 
+let get_proof_attempt (s : session) (a : proofAttemptID) =
+  (get_proofAttemptNode s a).proofa_attempt
+
+let get_proof_attempt_parent (s : session) (a : proofAttemptID) =
+  (get_proofAttemptNode s a).proofa_parent
+
 let get_proof_attempts (s : session) (id : proofNodeID) =
   Hprover.fold (fun _ a l ->
                 let pa = get_proofAttemptNode s a in

src/session/session_itp.mli

@@ -65,6 +65,8 @@ val get_task : session -> proofNodeID -> Task.task
 val get_transformations : session -> proofNodeID -> transID list
 val get_proof_attempt_ids :
   session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
+val get_proof_attempt : session -> proofAttemptID -> proof_attempt
+val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
 val get_proof_attempts : session -> proofNodeID -> proof_attempt list
 val get_sub_tasks : session -> transID -> proofNodeID list
 val get_detached_sub_tasks : session -> transID -> proofNodeID list

src/why3shell/why3shell.ml

@@ -549,7 +549,9 @@ let run_strategy _fmt args =
           let callback sts =
             printf "Strategy status: %a@." print_strategy_status sts
           in
-          C.run_strategy_on_goal cont id st ~callback
+          let callback_pa _panid _st = () in
+          let callback_tr _tr = () in
+          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
        | _ -> printf "Strategy '%s' not found@." s
      end
   | _ -> printf "Please give the strategy shortcut as argument@."