ITP: on-going implementation of schedule_proof_attempt

examples/use_api/itp.ml

@@ -88,6 +88,7 @@ let id =
 let () =
   printf "%a@." (Session_itp.print_tree s) (Session_itp.get_tree s id)
 
+
 let pid = Session_itp.graft_proof_attempt s id alt_ergo.Whyconf.prover ~timelimit:42
 
 let () =
@@ -107,6 +108,10 @@ let () =
 
 let my_session = Session_itp.empty_session ()
 
+module M = Controller_itp
+
+let _ = M.add_file_to_session
+
 (* adds a file in the new session *)
 let () =
   let fname = "../logic/hello_proof.why" in

src/session/controller_itp.ml

+
+
+
+open Format
 open Session_itp
 
 (** State of a proof *)
@@ -10,8 +14,6 @@ type proof_attempt_status =
     | Done of Call_provers.prover_result (** external proof done *)
     | InternalFailure of exn (** external proof aborted by internal error *)
 
-open Format
-
 let print_status fmt st =
   match st with
   | Unedited -> fprintf fmt "Unedited"
@@ -25,6 +27,13 @@ let print_status fmt st =
 type transformation_status =
   | TSscheduled of transID | TSdone of transID | TSfailed
 
+type controller =
+  { controller_session : Session_itp.session;
+    (* controller_env : Env.env; *)
+    controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
+  }
+
+
 module type Scheduler = sig
   val timeout: ms:int -> (unit -> bool) -> unit
   val idle: prio:int -> (unit -> bool) -> unit
@@ -43,8 +52,9 @@ let max_number_of_running_provers = ref 1
 
 let number_of_running_provers = ref 0
 
-open Call_provers
+module Hprover = Whyconf.Hprover
 
+(*
 let dummy_result =
   {
     pr_answer = Call_provers.Unknown ("I'm dumb", None);
@@ -54,14 +64,27 @@ let dummy_result =
     pr_steps  = 42;
     pr_model  = Model_parser.default_model;
 }
+ *)
 
-let build_prover_call _s _id _pr _timelimit callback =
+let build_prover_call c id pr limit callback =
+  let (config_pr,driver) = Hprover.find c.controller_provers pr in
+  let command =
+    Whyconf.get_complete_command config_pr
+          ~with_steps:(limit.Call_provers.limit_steps <>
+                       Call_provers.empty_limit.Call_provers.limit_steps) in
+  let task = Session_itp.get_task c.controller_session id in
+  let call =
+    Driver.prove_task ?old:None ~cntexample:false ~inplace:false ~command
+                      ~limit driver task
+  in
+(*
   let c = ref 0 in
   let call () =
     incr c;
-    if !c = 1000 then Call_provers.ProverStarted else
-      if !c = 10000 then Call_provers.ProverFinished dummy_result
+    if !c = 10 then Call_provers.ProverStarted else
+      if !c = 20 then Call_provers.ProverFinished dummy_result
       else Call_provers.NoUpdates
+ *)
 (*
   match find_prover eS a with
   | None ->
@@ -109,7 +132,6 @@ let build_prover_call _s _id _pr _timelimit callback =
                             ~limit driver goal
         in
  *)
-  in
   let pa = (callback,false,call) in
   Queue.push pa prover_tasks_in_progress
 
@@ -118,7 +140,7 @@ let timeout_handler () =
   let q = Queue.create () in
   while not (Queue.is_empty prover_tasks_in_progress) do
     let (callback,started,call) as c = Queue.pop prover_tasks_in_progress in
-    match (*Call_provers.query_call*) call () with
+    match Call_provers.query_call call with
     | Call_provers.NoUpdates -> Queue.add c q
     | Call_provers.ProverStarted ->
        assert (not started);
@@ -130,18 +152,18 @@ let timeout_handler () =
        callback (Done res)
   done;
   Queue.transfer q prover_tasks_in_progress;
-  (* if the number of prover tasks in less that 3 times the maximum
+  (* if the number of prover tasks is less than 3 times the maximum
      number of running provers, then we heuristically decide to add
      more tasks *)
   try
     for _i = Queue.length prover_tasks_in_progress
         to 3 * !max_number_of_running_provers do
-      let (s,id,pr,timelimit,callback) = Queue.pop scheduled_proof_attempts in
+      let (c,id,pr,timelimit,callback) = Queue.pop scheduled_proof_attempts in
       try
-        build_prover_call s id pr timelimit callback
+        build_prover_call c id pr timelimit callback
       with e when not (Debug.test_flag Debug.stack_trace) ->
         Format.eprintf
-          "@[Exception raise in Controler_itp.build_prover_call:@ %a@.@]"
+          "@[Exception raise in Controller_itp.build_prover_call:@ %a@.@]"
           Exn_printer.exn_printer e;
         callback (InternalFailure e)
     done;
@@ -155,14 +177,14 @@ let run_timeout_handler () =
       S.timeout ~ms:125 timeout_handler;
     end
 
-let schedule_proof_attempt s id pr ~timelimit ~callback =
-  graft_proof_attempt s id pr ~timelimit;
-  Queue.add (s,id,pr,timelimit,callback) scheduled_proof_attempts;
+let schedule_proof_attempt c id pr ~limit ~callback =
+  graft_proof_attempt c.controller_session id pr ~timelimit:5;
+  Queue.add (c,id,pr,limit,callback) scheduled_proof_attempts;
   callback Scheduled;
   run_timeout_handler ()
 
-let schedule_transformations s id name args ~callback =
-  let tid = graft_transf s id name args in
+let schedule_transformations c id name args ~callback =
+  let tid = graft_transf c.controller_session id name args in
   callback (TSscheduled tid)
 
 let read_file env ?format fn =

src/session/controller_itp.mli

@@ -49,23 +49,29 @@ module type Scheduler = sig
 
 end
 
+type controller =
+  { controller_session : Session_itp.session;
+    (* controller_env : Env.env; *)
+    controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
+  }
 
 module Make(S : Scheduler) : sig
 
 val schedule_proof_attempt :
-  session ->
+  controller ->
   proofNodeID ->
   Whyconf.prover ->
-  timelimit:int ->
+  limit:Call_provers.resource_limit ->
   callback:(proof_attempt_status -> unit) -> unit
-(** [schedule_proof_attempt s id p tl cb] schedules a proof attempt for
-   a goal specified by [id] with the prover [p] with time limit [tl];
-   the function [cb] will be called each time the proof attempt status
-   changes. Typically at Scheduled, then Running, then Done. If there
-   is already a proof attempt with [p] it is updated. *)
+(** [schedule_proof_attempt s id p ~timelimit ~callback] schedules a
+   proof attempt for a goal specified by [id] with the prover [p] with
+   time limit [timelimit]; the function [callback] will be called each
+   time the proof attempt status changes. Typically at Scheduled, then
+   Running, then Done. If there is already a proof attempt with [p] it
+   is updated. *)
 
 val schedule_transformations :
-  session ->
+  controller ->
   proofNodeID ->
   string ->
   trans_arg list ->

src/session/session_itp.ml

@@ -134,6 +134,10 @@ let get_proofNode (s : session) (id : proofNodeID) =
     Hint.find s.proofNode_table id
   with Not_found -> raise BadID
 
+let get_task (s:session) (id:proofNodeID) =
+  let node = get_proofNode s id in
+  node.proofn_task
+
 let get_transfNode (s : session) (id : transID) =
   try
     Hint.find s.trans_table id

src/session/session_itp.mli

@@ -45,6 +45,8 @@ 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
@@ -70,7 +72,7 @@ val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
   timelimit:int -> unit
 (** [graft_proof_attempt s id pr t] adds a proof attempt with prover
     [pr] and timelimit [t] in the session [s] as a child of the task
-    [id]. If there allready a proof attempt with the same prover,
+    [id]. If there already a proof attempt with the same prover,
     it updates it with the new timelimit. *)
 
 val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->

src/why3shell/why3shell.ml

@@ -94,6 +94,9 @@ end
 (* parsing command line *)
 (************************)
 
+open Why3
+open Format
+
 let files = Queue.create ()
 
 let spec = Arg.align [
@@ -103,18 +106,57 @@ let usage_str = Format.sprintf
   "Usage: %s [options] <project directory>"
   (Filename.basename Sys.argv.(0))
 
-let config, base_config, env =
+
+let config, base_config, _env =
   Why3.Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
 
+let main : Whyconf.main = Whyconf.get_main config
+(* all the provers detected, from the config file *)
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers config
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
+
+(* loading the drivers *)
+let provers =
+  Whyconf.Mprover.fold
+    (fun _ p acc ->
+      try
+        let d = Driver.load_driver env p.Whyconf.driver [] in
+        (p,d)::acc
+      with e ->
+        let p = p.Whyconf.prover in
+        eprintf "Failed to load driver for %s %s: %a@."
+          p.Whyconf.prover_name p.Whyconf.prover_version
+          Exn_printer.exn_printer e;
+        acc)
+    provers
+    []
+
+(* One prover named Alt-Ergo in the config file *)
+let alt_ergo =
+  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
+  (** all provers that have the name "Alt-Ergo" *)
+  let provers = Whyconf.filter_provers config fp in
+  if Whyconf.Mprover.is_empty provers then begin
+    eprintf "Prover Alt-Ergo not installed or not configured@.";
+    exit 0
+  end else
+    snd (Whyconf.Mprover.choose provers)
+
+
 let ses =
   if Queue.is_empty files then Why3.Whyconf.Args.exit_with_usage spec usage_str;
   let fname = Queue.pop files in
   ref (Why3.Session_itp.load_session fname)
 
-module C = Why3.Controller_itp.Make(Unix_scheduler)
+let cont = Controller_itp.{
+    controller_session = !ses;
+    controller_provers = Whyconf.Hprover.create 7;
+  }
 
-open Why3
-open Format
+module C = Why3.Controller_itp.Make(Unix_scheduler)
 
 exception Error of string
 
@@ -137,7 +179,27 @@ let interp s =
        printf "ls : list current directory@\n";
        printf "p : print the session in raw form@\n";
        printf "q : exit the shell@\n";
+       printf "t : test schedule_proof_attempt on the first goal@\n";
        printf "@."
+    | "t" ->
+       let id =
+         match Session_itp.get_theories !ses with
+         | (_n, (_thn, x::_)::_)::_ -> x
+         | _ -> assert false
+       in
+       let callback status =
+         printf "status: %a@."
+                Controller_itp.print_status status
+       in
+       let limit = Call_provers.{
+           limit_time = 5 ;
+           limit_mem  = 1000;
+           limit_steps = -1;
+         }
+       in
+       C.schedule_proof_attempt
+         cont id alt_ergo.Whyconf.prover
+         ~limit ~callback
     | "a" ->
        Unix_scheduler.timeout
          ~ms:1000