why3shell in progress

src/session/controller_itp.ml

@@ -27,15 +27,139 @@ type transformation_status =
 
 module type Scheduler = sig
   val timeout: ms:int -> (unit -> bool) -> unit
-  val idle: (unit -> bool) -> unit
+  val idle: prio:int -> (unit -> bool) -> unit
 end
 
 
 module Make(S : Scheduler) = struct
 
+let scheduled_proof_attempts = Queue.create ()
+
+let prover_tasks_in_progress = Queue.create ()
+
+let timeout_handler_running = ref false
+
+let max_number_of_running_provers = ref 1
+
+let number_of_running_provers = ref 0
+
+open Call_provers
+
+let dummy_result =
+  {
+    pr_answer = Call_provers.Unknown ("I'm dumb", None);
+    pr_status = Unix.WEXITED 0;
+    pr_output = "";
+    pr_time   = 3.14;
+    pr_steps  = 42;
+    pr_model  = Model_parser.default_model;
+}
+
+let build_prover_call s id pr timelimit callback =
+  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
+      else Call_provers.NoUpdates
+(*
+  match find_prover eS a with
+  | None ->
+    callback a a.proof_prover Call_provers.empty_limit None Starting;
+    (* nothing to do *)
+    callback a a.proof_prover Call_provers.empty_limit None MissingProver
+  | Some(ap,npc,a) ->
+    callback a ap Call_provers.empty_limit None Starting;
+    let itp = npc.prover_config.Whyconf.interactive in
+    if itp && a.proof_edited_as = None then begin
+      callback a ap Call_provers.empty_limit None (MissingFile "unedited")
+    end else begin
+      let previous_result = a.proof_state in
+      let limit = adapt_limits ~interactive:itp ~use_steps a in
+      let inplace = npc.prover_config.Whyconf.in_place in
+      let command =
+        Whyconf.get_complete_command npc.prover_config
+          ~with_steps:(limit.Call_provers.limit_steps <>
+                       Call_provers.empty_limit.Call_provers.limit_steps) in
+      let cb result =
+        let result = fuzzy_proof_time result previous_result in
+        callback a ap limit
+          (match previous_result with Done res -> Some res | _ -> None)
+          (StatusChange result) in
+      try
+        let old =
+          match get_edited_as_abs eS.session a with
+          | None -> None
+          | Some f ->
+            if Sys.file_exists f then Some f
+            else raise (NoFile f) in
+        schedule_proof_attempt
+          ~cntexample ~limit
+          ?old ~inplace ~command
+          ~driver:npc.prover_driver
+          ~callback:cb
+          eT
+          (goal_task_or_recover eS a.proof_parent)
+      with NoFile f ->
+        callback a ap Call_provers.empty_limit None (MissingFile f)
+    end
+
+        let call =
+          Driver.prove_task ?old:None ~cntexample:false ~inplace:false ~command
+                            ~limit driver goal
+        in
+ *)
+  in
+  let pa = (callback,false,call) in
+  Queue.push pa prover_tasks_in_progress
+
+let timeout_handler () =
+  (* examine all the prover tasks in progress *)
+  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
+    | Call_provers.NoUpdates -> Queue.add c q
+    | Call_provers.ProverStarted ->
+       assert (not started);
+       callback Running;
+       incr number_of_running_provers;
+       Queue.add (callback,true,call) q
+    | Call_provers.ProverFinished res ->
+       if started then decr number_of_running_provers;
+       callback (Done res)
+  done;
+  Queue.transfer q prover_tasks_in_progress;
+  (* if the number of prover tasks in less that 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
+      try
+        build_prover_call s 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@.@]"
+          Exn_printer.exn_printer e;
+        callback (InternalFailure e)
+    done;
+    true
+  with Queue.Empty -> true
+
+let run_timeout_handler () =
+  if not !timeout_handler_running then
+    begin
+      timeout_handler_running := true;
+      S.timeout ~ms:125 timeout_handler;
+    end
+
 let schedule_proof_attempt s id pr ~timelimit ~callback =
   graft_proof_attempt s id pr ~timelimit;
-  callback Scheduled
+  Queue.add (s,id,pr,timelimit,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

src/session/controller_itp.mli

@@ -26,8 +26,27 @@ val print_status : Format.formatter -> proof_attempt_status -> unit
 type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
 
 module type Scheduler = sig
-  val timeout: ms:int -> (unit -> bool) -> unit
-  val idle: (unit -> bool) -> unit
+
+    (** Any module of this signature should implement a scheduler,
+    that allows the register functions to call, and call them
+    depending on some time constraints: after a given delay, or simply
+    when there is no more tasks with higher priority. *)
+
+    val timeout: ms:int -> (unit -> bool) -> unit
+    (** [timeout ~ms f] registers the function [f] as a function to be
+    called every [ms] milliseconds. The function is called repeatedly
+    until it returns false. the [ms] delay is not strictly guaranteed:
+    it is only a minimum delay between the end of the last call and
+    the beginning of the next call.  Several functions can be
+    registered at the same time. *)
+
+    val idle: prio:int -> (unit -> bool) -> unit
+    (** [idle prio f] registers the function [f] as a function to be
+    called whenever there is nothing else to do. Several functions can
+    be registered at the same time.  Several functions can be
+    registered at the same time. Functions registered with higher
+    priority will be called first. *)
+
 end
 
 

src/session/session_itp.mli

@@ -2,7 +2,18 @@ type session
 type transID
 type proofNodeID
 type proof_attempt
-type trans_arg
+
+type trans_arg =
+  | TAint      of int
+  | TAstring   of string
+  | TAterm     of Term.term
+  | TAty       of Ty.ty
+  | TAtysymbol of Ty.tysymbol
+  (* | ... *)
+
+
+
+
 
 (* New Proof sessions ("Refectoire") *)
 
@@ -17,12 +28,17 @@ type trans_arg
 type tree =
     Tree of
       (proofNodeID * string
-       * proof_attempt list (* proof attempts in this node *)
-       * (transID * string * tree list) list) (* transformation in this node *)
+       * proof_attempt list (* proof attempts on this node *)
+       * (transID * string * tree list) list) (* transformations on this node *)
+(* a tree is a complete proof whenever at least one proof_attempf or
+  one transformation proves the goal, where a transformation proves a
+  goal when all subgoals have a complete proof.  In other word, the
+  list of proof_attempt and transformation are "disjunctive" but the
+  list of tree below a transformation is "conjunctive" *)
 
 val get_theories : session -> (string * (string * proofNodeID list) list) list
 (** [get_theories s] returns a list of pairs [name,l] where [name] is a
-    file name and [l] is a list of pairs [thnmae,l'] where [thname] is
+    file name and [l] is a list of pairs [thname,l'] where [thname] is
     a theory name and [l'] is the list of goal ids *)
 
 val get_tree : session -> proofNodeID -> tree

src/why3shell/why3shell.ml

@@ -2,8 +2,12 @@
 
 module Unix_scheduler = struct
 
+    (* the private list of functions to call on idle, sorted higher
+       priority first. *)
     let idle_handler = ref []
 
+    (* [insert_idle_handler p f] inserts [f] as a new function to call
+       on idle, with priority [p] *)
     let insert_idle_handler p f =
       let rec aux l =
         match l with
@@ -13,8 +17,12 @@ module Unix_scheduler = struct
       in
       idle_handler := aux !idle_handler
 
+    (* the private list of functions to call on idle, sorted on
+       earliest trigger time first. *)
     let timeout_handler = ref []
 
+    (* [insert_timeout_handler ms t f] inserts [f] as a new function to call
+       on timeout, with time step of [ms] and first call time as [t] *)
     let insert_timeout_handler ms t f =
       let rec aux l =
         match l with
@@ -24,47 +32,57 @@ module Unix_scheduler = struct
       in
       timeout_handler := aux !timeout_handler
 
-
+    (* public function to register a task to run on idle *)
     let idle ~(prio:int) f = insert_idle_handler prio f
 
+    (* public function to register a task to run on timeout *)
     let timeout ~ms f =
+      assert (ms > 0);
       let ms = float ms /. 1000.0 in
       let time = Unix.gettimeofday () in
       insert_timeout_handler ms (time +. ms) f
 
+     (* buffer for storing character read on stdin *)
      let buf = Bytes.create 256
 
+     (* [main_loop interp] starts the scheduler. On idle, standard input is
+        read.  When a complete line is read from stdin, it is passed
+        as a string to the function [interp] *)
      let main_loop interp =
        try
          while true do
            (* attempt to run the first timeout handler *)
            let time = Unix.gettimeofday () in
            match !timeout_handler with
-             | (ms,t,f) :: rem when t <= time ->
-                timeout_handler := rem;
-                let b = f () in
-                let time = Unix.gettimeofday () in
-                if b then insert_timeout_handler ms (ms +. time) f
-             | _ ->
-                (* attempt to run the first idle handler *)
-                match !idle_handler with
-                | (p,f) :: rem ->
-                   idle_handler := rem;
-                   let b = f () in
-                   if b then insert_idle_handler p f
-                | [] ->
-                   (* check stdin for a some delay *)
-                   let delay =
-                     match !timeout_handler with
-                       | [] -> 0.1
-                       | (_,t,_) :: _ -> t -. time
-                   in
-                   let a,_,_ = Unix.select [Unix.stdin] [] [] delay in
-                   match a with
-                   | [_] -> let n = Unix.read Unix.stdin buf 0 256 in
-                            interp (Bytes.sub_string buf 0 (n-1))
-                   | [] -> ()
-                   | _ -> assert false
+           | (ms,t,f) :: rem when t <= time ->
+              timeout_handler := rem;
+              let b = f () in
+              let time = Unix.gettimeofday () in
+              if b then insert_timeout_handler ms (ms +. time) f
+           | _ ->
+              (* time is not yet passed *)
+              (* attempt to run the first idle handler *)
+              match !idle_handler with
+              | (p,f) :: rem ->
+                 idle_handler := rem;
+                 let b = f () in
+                 if b then insert_idle_handler p f
+              | [] ->
+                 (* no idle handler *)
+                 (* check stdin for a some delay *)
+                 let delay =
+                   match !timeout_handler with
+                   | [] -> 0.125
+                   (* 1/8 second by default *)
+                   | (_,t,_) :: _ -> t -. time
+                   (* or the time left until the next timeout otherwise *)
+                 in
+                 let a,_,_ = Unix.select [Unix.stdin] [] [] delay in
+                 match a with
+                 | [_] -> let n = Unix.read Unix.stdin buf 0 256 in
+                          interp (Bytes.sub_string buf 0 (n-1))
+                 | [] -> () (* nothing read *)
+                 | _ -> assert false
          done
        with Exit -> ()
 
@@ -72,17 +90,17 @@ end
 
 
 
-(*
 module C = Why3.Controller_itp.Make(Unix_scheduler)
- *)
+
+open Why3.Session_itp
 
 let interp s =
   match s with
     | "a" ->
-       let c = ref 10 in
        Unix_scheduler.timeout
          ~ms:1000
-         (fun () -> decr c;
+         (let c = ref 10 in
+          fun () -> decr c;
                     if !c > 0 then
                       (Format.printf "%d@." !c; true)
                     else
@@ -91,7 +109,14 @@ let interp s =
        Unix_scheduler.idle
          ~prio:0
          (fun () -> Format.printf "idle@."; false)
-    | _ -> Format.printf "unknowm command `%s`@." s
+(*
+    | "p" ->
+       let s = empty_session () in
+       C.schedule_proof_attempt
+         s (get_node s 0)
+*)
+
+    | _ -> Format.printf "unknown command `%s`@." s