schedule_transformation completed (without arguments)

src/session/controller_itp.ml

@@ -25,7 +25,13 @@ let print_status fmt st =
   | InternalFailure e -> fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e
 
 type transformation_status =
-  | TSscheduled of transID | TSdone of transID | TSfailed
+  | TSscheduled | TSdone | TSfailed
+
+let print_trans_status fmt st =
+  match st with
+  | TSscheduled -> fprintf fmt "TScheduled"
+  | TSdone -> fprintf fmt "TSdone"
+  | TSfailed -> fprintf fmt "TSfailed"
 
 type controller =
   { mutable controller_session : Session_itp.session;
@@ -137,9 +143,23 @@ let schedule_proof_attempt c id pr ~limit ~callback =
   callback Scheduled;
   run_timeout_handler ()
 
-let schedule_transformations c id name args ~callback =
-  let tid = graft_transf c.controller_session id name args in
-  callback (TSscheduled tid)
+let schedule_transformation c id name args ~callback =
+  let apply_trans () =
+    let task = get_task c.controller_session id in
+    try
+      let subtasks = Trans.apply_transform name c.controller_env task in
+      let _tid = graft_transf c.controller_session id name args subtasks in
+      callback TSdone;
+      false
+    with e when not (Debug.test_flag Debug.stack_trace) ->
+      Format.eprintf
+        "@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
+          name Exn_printer.exn_printer e;
+        callback TSfailed;
+        false
+  in
+  S.idle ~prio:0 apply_trans;
+  callback TSscheduled
 
 let read_file env ?format fn =
   let theories = Env.read_file Env.base_language env ?format fn in

src/session/controller_itp.mli

@@ -23,7 +23,9 @@ type proof_attempt_status =
 
 val print_status : Format.formatter -> proof_attempt_status -> unit
 
-type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
+type transformation_status = TSscheduled | TSdone  | TSfailed
+
+val print_trans_status : Format.formatter -> transformation_status -> unit
 
 module type Scheduler = sig
 
@@ -72,15 +74,15 @@ val schedule_proof_attempt :
    Running, then Done. If there is already a proof attempt with [p] it
    is updated. *)
 
-val schedule_transformations :
+val schedule_transformation :
   controller ->
   proofNodeID ->
   string ->
   trans_arg list ->
   callback:(transformation_status -> unit) -> unit
-(** [schedule_transformations s id cb] schedules a transformation for a
+(** [schedule_transformation c id cb] schedules a transformation for a
    goal specified by [id]; the function [cb] will be called each time
-   the transformation status changes. Typically at Scheluded, then
+   the transformation status changes. Typically at Scheduled, then
    Done tid.*)
 
 val add_file : controller -> ?format:Env.fformat -> string -> unit

src/session/session_itp.ml

@@ -52,10 +52,10 @@ type trans_arg =
   (* | ... *)
 
 type transformation_node = {
-  transf_name             : string;
-  transf_args             : trans_arg list;
-  mutable transf_subtasks : proofNodeID list;
-  transf_parent           : proofNodeID;
+  transf_name     : string;
+  transf_args     : trans_arg list;
+  transf_subtasks : proofNodeID list;
+  transf_parent   : proofNodeID;
 }
 
 type file = {
@@ -305,16 +305,11 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
   Hint.add s.trans_table node_id tn;
   pn.proofn_transformations <- node_id::pn.proofn_transformations
 
-let set_transf_tasks (s : session) (id : transID) (tl : Task.task list) =
-  let tn = get_transfNode s id in
-  assert (tn.transf_subtasks = []);
-  let sub_tasks = List.map (mk_transf_proof_node s id) tl in
-  tn.transf_subtasks <- sub_tasks
-
 let graft_transf  (s : session) (id : proofNodeID) (name : string)
-    (args : trans_arg list) =
+    (args : trans_arg list) (tl : Task.task list) =
   let tid = gen_transID s in
-  mk_transf_node s id tid name args [];
+  let sub_tasks = List.map (mk_transf_proof_node s tid) tl in
+  mk_transf_node s id tid name args sub_tasks;
   tid
 
 let remove_transformation (s : session) (id : transID) =
@@ -491,9 +486,13 @@ and load_proof_or_transf session old_provers pid a =
     | "transf" ->
         let trname = string_attribute "name" a in
         let tid = gen_transID session in
-        let subtasks_ids = List.rev (List.fold_left (fun goals th -> match th.Xml.name with
-        | "goal" -> (gen_proofNodeID session) :: goals
-        | _ -> goals) [] a.Xml.elements) in
+        let subtasks_ids =
+          List.rev (List.fold_left
+                      (fun goals th ->
+                       match th.Xml.name with
+                       | "goal" -> (gen_proofNodeID session) :: goals
+                       | _ -> goals) [] a.Xml.elements)
+        in
         mk_transf_node session pid tid trname [] subtasks_ids;
         List.iter2
           (load_goal session old_provers (Trans tid))

src/session/session_itp.mli

@@ -112,15 +112,11 @@ val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
     corresponding proof attempt with [st]. *)
 
 val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
-   transID
-(** [graft_transf s id name l] adds the transformation [name] as a
+   Task.task list -> transID
+(** [graft_transf s id name l tl] adds the transformation [name] as a
     child of the task [id] of the session [s]. [l] is the list of
-    argument of the transformation. The subtasks are initialized to
-    the empty list *)
-
-val set_transf_tasks : session -> transID -> Task.task list -> unit
-(** [set_transf_tasks s id tl] sets the tasks of the transformation node
-    [id] to [tl] *)
+    argument of the transformation, and [tl] is the list of subtasks.
+ *)
 
 val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
 (** [remove_proof_attempt s id pr] removes the proof attempt from the

src/why3shell/why3shell.ml

@@ -243,6 +243,15 @@ let test_schedule_proof_attempt fmt _args =
     cont id alt_ergo.Whyconf.prover
     ~limit ~callback
 
+let test_transformation fmt _args =
+  (* temporary : apply split on the first goal *)
+  let id = first_goal () in
+  let callback status =
+    fprintf fmt "transformation status: %a@."
+            Controller_itp.print_trans_status status
+  in
+  C.schedule_transformation cont id "split_goal_wp" [] ~callback
+
 let task_driver =
   let d = Filename.concat (Whyconf.datadir main)
                           (Filename.concat "drivers" "why3_itp.drv")
@@ -272,6 +281,7 @@ let commands =
     "t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
     "g", "prints the first goal", test_print_goal;
     "r", "reload the session (test only)", test_reload;
+    "tr", "test schedule_transformation with split_goal on the first goal", test_transformation;
   ]
 
 let commands_table = Stdlib.Hstr.create 17