first commit

Makefile.in

@@ -203,8 +203,8 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 	    mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
 	    mlw_main mlw_interp
 
-LIB_SESSION = compress xml termcode session session_itp			\
-              session_tools strategy strategy_parser	\
+LIB_SESSION = compress xml termcode session session_itp unix_scheduler \
+              itp_server session_tools strategy strategy_parser \
               controller_itp session_scheduler session_user_interface
 
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \

src/session/itp_server.ml

+open Call_provers
+
+type prover = string
+type transformation = string
+type strategy = string
+
+type node_ID = int
+let root_node = 0
+
+type node_type = File | Theory | Transformation | Goal | ProofAttempt of string
+
+type node_info = { proved   : bool;
+                   obsolete : bool }
+
+type session_tree = Node of node_ID * node_type * node_info * session_tree list
+
+type error_notification =
+  | Proof_error  of node_ID * string
+  | Transf_error of node_ID * string
+
+type notification =
+  | Node_change    of node_ID * node_info
+  | Subtree_change of node_ID * session_tree
+  | Remove         of node_ID
+  | Initialized    of prover list * transformation list * strategy list
+  | Session_Tree   of session_tree
+  | Error          of error_notification
+
+type request_type =
+  | Command of string
+  | Prove of prover * resource_limit
+  | Transform of transformation * string list
+  | Strategy of strategy
+  | Open of string
+  | Get_Session_Tree
+  | Save
+  | Reload
+  | Replay
+
+type ide_request = request_type * node_ID
+
+open Unix_scheduler
+open Session_itp
+open Controller_itp
+
+module C = Why3.Controller_itp.Make(Unix_Scheduler)
+
+module type Protocol = sig
+  val get_requests : unit -> request_type list
+  val notify : notification list -> unit
+end
+
+module Make (P:Protocol) = struct
+
+  let the_tree : session_tree ref = Obj.magic "tree"
+
+  (* create a new node in the_tree and send a notification about it *)
+  let new_node ~parent:node_ID node_type node_info : unit
+    = ()
+(*    ...
+        P.notify (Subtree_change (nodeID,  )) *)
+
+  let node_ID_from_pan pan = 0
+  let node_ID_from_pn  pn  = 0
+
+  (* ----------------- Schedule proof attempt -------------------- *)
+
+  (* Callback of a proof_attempt *)
+  let callback_update_tree_proof cont panid pa_status =
+    let ses = cont.controller_session in
+    let pa = get_proof_attempt_node ses panid in
+    let prover = pa.prover in
+    let name = Pp.string_of Whyconf.print_prover prover in
+    let obsolete = pa.proof_obsolete in
+    let r = match pa_status with
+      | Scheduled ->
+        begin
+          try
+            ignore (node_ID_from_pan panid)
+            (* TODO: do we notify here ? *)
+          with Not_found ->
+            let parent_id = get_proof_attempt_parent ses panid in
+            let parent = node_ID_from_pn parent_id in
+            new_node ~parent (ProofAttempt name) { proved=false; obsolete=false }
+        end
+      | Done _ ->
+        P.notify (Node_change (node_ID_from_pan panid,
+                               { proved=false; obsolete=false }))
+        let ppn = get_proof_attempt_parent cont.controller_session panid in
+        let piter = (node_ID_from_pn ppn)#iter in
+        update_status_column_from_iter cont piter;
+        (* move focus an collapse if the goal was proven and
+           the current index still corresponds to the goal *)
+        begin match !current_selected_index with
+          | IproofNode pn when pn = ppn ->
+            if pn_proved cont pn then
+              go_to_nearest_unproven_goal_and_collapse pn
+          | _ -> ()
+        end;
+        row_from_pan panid
+      | _  -> row_from_pan panid (* TODO ? *)
+    in
+    goals_model#set ~row:r#iter ~column:status_column
+      (image_of_pa_status ~obsolete pa_status)
+
+  let test_schedule_proof_attempt cont (p: Whyconf.config_prover) limit =
+    let prover = p.Whyconf.prover in
+    let callback = callback_update_tree_proof cont in
+    let rec get_goals () =
+      match !current_selected_index with
+      | IproofNode id -> [id]
+      | IproofAttempt _ ->
+        move_current_row_selection_up ();
+        get_goals ()
+      | Itransformation tn ->
+        List.rev (unproven_goals_below_tn cont [] tn)
+      | Ifile file ->
+        List.rev (unproven_goals_below_file cont file)
+      | Itheory th ->
+        List.rev (unproven_goals_below_th cont [] th)
+      | Inone -> []
+    in
+    List.iter (fun id -> C.schedule_proof_attempt cont id prover ~limit ~callback)
+      (get_goals ())
+
+
+  let treat_request r = match r with
+    | Prove (p,limit) -> schedule_proof_attempt p limit
+
+
+  let treat_requests () : bool =
+    List.iter treat_request (P.get_requests ());
+    true
+
+  let _ = Unix_Scheduler.idle ~prio:1 treat_requests
+
+
+end

src/session/itp_server.mli

+open Call_provers
+
+type prover
+type transformation
+type strategy
+
+type node_ID
+val root_node : node_ID
+
+(* --------------------------- types to be expanded on call by need --------------------------------- *)
+
+type node_type = File | Theory | Transformation | Goal | ProofAttempt
+
+type node_info = { proved   : bool; (* TODO: add more *)
+                   obsolete : bool }
+
+type session_tree = Node of node_ID * node_type * node_info * session_tree list
+
+type error_notification =
+  | Proof_error  of node_ID * string
+  | Transf_error of node_ID * string
+
+type notification =
+  | Node_change    of node_ID * node_info
+  | Subtree_change of node_ID * session_tree
+  | Remove         of node_ID
+  | Initialized    of prover list * transformation list * strategy list
+  | Session_Tree   of session_tree
+  | Error          of error_notification
+
+type request_type =
+  | Command   of string
+  | Prove     of prover * resource_limit
+  | Transform of transformation * string list
+  | Strategy  of strategy
+  | Open      of string
+  | Get_Session_Tree
+  | Save
+  | Reload
+  | Replay
+
+type ide_request = request_type * node_ID
+
+module type Protocol = sig
+
+  val get_requests : unit -> request_type list
+  val send_notifications : notification list -> unit
+
+end
+
+module Make (P:Protocol) : sig end

src/session/unix_scheduler.ml

+module Unix_scheduler = struct
+
+    (* the private list of functions to call on idle, sorted higher
+       priority first. *)
+    let idle_handler : (int * (unit -> bool)) list ref = 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
+          | [] -> [p,f]
+          | (p1,_) as hd :: rem ->
+             if p > p1 then (p,f) :: l else hd :: aux rem
+      in
+      idle_handler := aux !idle_handler
+
+    (* the private list of functions to call on timeout, sorted on
+       earliest trigger time first. *)
+    let timeout_handler : (float * float * (unit -> bool)) list ref = 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
+          | [] -> [ms,t,f]
+          | (_,t1,_) as hd :: rem ->
+             if t < t1 then (ms,t,f) :: l else hd :: aux rem
+      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
+
+     let prompt_delay = ref 0
+     let print_prompt = ref true
+     let prompt = ref "> "
+
+     (* [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
+           if !print_prompt then begin
+             prompt_delay := !prompt_delay + 1;
+             if !prompt_delay = 2 then begin
+               Format.printf "%s@?" !prompt;
+               prompt_delay := 0;
+               print_prompt := false;
+             end
+           end;
+           (* 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
+           | _ ->
+              (* 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));
+                    print_prompt := true
+                 | [] -> () (* nothing read *)
+                 | _ -> assert false);
+         done
+       with Exit -> ()
+
+end

src/session/unix_scheduler.mli

+module Unix_Scheduler : sig
+
+    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