[run strategy] allow the user to provide callbacks

src/session/session_scheduler.ml

@@ -926,10 +926,10 @@ let convert_unknown_prover =
 
   open Strategy
 
-  let rec exec_strategy es sched pc strat g =
+  let rec exec_strategy ~todo es sched pc strat g =
     if pc < 0 || pc >= Array.length strat then
       (* halt the strategy *)
-      ()
+      Todo._done todo ()
     else
       match Array.get strat pc with
         | Icall_prover(p,timelimit,memlimit) ->
@@ -940,10 +940,10 @@ let convert_unknown_prover =
                 ()
               | Done { Call_provers.pr_answer = Call_provers.Valid } ->
                 (* proof succeeded, nothing more to do *)
-                ()
+                Todo._done todo ()
               | Interrupted | InternalFailure _ | Done _ ->
                 (* proof did not succeed, goto to next step *)
-                let callback () = exec_strategy es sched (pc+1) strat g in
+                let callback () = exec_strategy ~todo es sched (pc+1) strat g in
                 schedule_delayed_action sched callback
               | Unedited | JustEdited ->
                 (* should not happen *)
@@ -954,25 +954,34 @@ let convert_unknown_prover =
           let callback ntr =
             match ntr with
               | None -> (* transformation failed *)
-                let callback () = exec_strategy es sched (pc+1) strat g in
+                let callback () = exec_strategy ~todo es sched (pc+1) strat g in
                 schedule_delayed_action sched callback
               | Some tr ->
                 List.iter
                   (fun g ->
+                    Todo.start todo;
                     let callback () =
-                      exec_strategy es sched pcsuccess strat g
+                      exec_strategy ~todo es sched pcsuccess strat g
                     in
                     schedule_delayed_action sched callback
                   )
-                tr.transf_goals
+                tr.transf_goals;
+                Todo._done todo ()
           in
           transform_goal es sched ~callback trname g
         | Igoto pc ->
-          exec_strategy es sched pc strat g
+          exec_strategy ~todo es sched pc strat g
 
 
-  let run_strategy_on_goal es sched strat g =
-    let callback () = exec_strategy es sched 0 strat g in
+  let run_strategy_on_goal
+      ?(intermediate_callback=fun () -> ())
+      ?(final_callback=fun () -> ())
+      es sched strat g =
+    let todo =
+      Todo.create () (fun () -> intermediate_callback) final_callback
+    in
+    Todo.start todo;
+    let callback () = exec_strategy ~todo es sched 0 strat g in
     schedule_delayed_action sched callback
 
 

src/session/session_scheduler.mli

@@ -296,6 +296,8 @@ module Make(O: OBSERVER) : sig
     (** Same as {!Session_tools.convert_unknown_prover} *)
 
   val run_strategy_on_goal:
+    ?intermediate_callback: (unit -> unit) ->
+    ?final_callback: (unit -> unit) ->
     O.key Session.env_session -> t ->
     Strategy.t -> O.key Session.goal -> unit