why3 shell

.gitignore

@@ -83,6 +83,9 @@ why3.conf
 /bin/why3session.opt
 /bin/why3session.byte
 /bin/why3session
+/bin/why3shell.opt
+/bin/why3shell.byte
+/bin/why3shell
 /bin/why3wc.opt
 /bin/why3wc.byte
 /bin/why3wc

Makefile.in

@@ -786,6 +786,52 @@ install_no_local::
 
 install_local:: bin/why3session
 
+###############
+# Why3 Shell
+###############
+
+SHELL_FILES = why3shell
+
+SHELLMODULES = $(addprefix src/why3shell/, $(SHELL_FILES))
+
+SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
+SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
+SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))
+
+$(SHELLDEP): DEPFLAGS += -I src/why3shell
+$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/why3shell
+
+# build targets
+
+byte: bin/why3shell.byte
+opt:  bin/why3shell.opt
+
+bin/why3shell.opt: lib/why3/why3.cmxa $(SHELLCMX)
+	$(SHOW) 'Linking  $@'
+	$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
+
+bin/why3shell.byte: lib/why3/why3.cma $(SHELLCMO)
+	$(SHOW) 'Linking  $@'
+	$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
+
+# depend and clean targets
+
+ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
+-include $(SHELLDEP)
+endif
+
+depend: $(SHELLDEP)
+
+CLEANDIRS += src/why3shell
+
+clean_old_install::
+	rm -f $(BINDIR)/why3shell$(EXE)
+
+install_no_local::
+	$(INSTALL) bin/why3shell.@OCAMLBEST@ $(TOOLDIR)/why3shell$(EXE)
+
+install_local:: bin/why3shell
+
 
 ##############
 # Coq plugin

src/session/controller_itp.ml

@@ -68,71 +68,3 @@ let reload_session_files (_s : session)  =
   failwith "Controller_itp.reload_session_files not yet implemented"
 
 end
-
-
-
-let usleep t = ignore (Unix.select [] [] [] t)
-
-module Unix_scheduler = struct
-
-    let idle_handler = ref None
-    let timeout_handler = ref None
-
-    let verbose = ref true
-
-     let idle f =
-       match !idle_handler with
-         | None -> idle_handler := Some f;
-         | Some _ -> failwith "Unix_scheduler.idle: already one handler installed"
-
-     let timeout ~ms f =
-       match !timeout_handler with
-         | None -> timeout_handler := Some(float ms /. 1000.0 ,f);
-         | Some _ -> failwith "Unix_scheduler.timeout: already one handler installed"
-
-     let notify_timer_state w s r =
-       if !verbose then
-         Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
-
-     let main_loop () =
-       let last = ref (Unix.gettimeofday ()) in
-       try while true do
-           let time = Unix.gettimeofday () -. !last in
-           (* attempt to run timeout handler *)
-           let timeout =
-             match !timeout_handler with
-               | None -> false
-               | Some(ms,f) ->
-                 if time > ms then
-                   let b = f () in
-                   if b then true else
-                     begin
-                       timeout_handler := None;
-                       true
-                     end
-                 else false
-           in
-           if timeout then
-             last := Unix.gettimeofday ()
-           else
-      (* attempt to run the idle handler *)
-             match !idle_handler with
-               | None ->
-                 begin
-                   let ms =
-                     match !timeout_handler with
-                       | None -> raise Exit
-                       | Some(ms,_) -> ms
-                   in
-                   usleep (ms -. time)
-                 end
-               | Some f ->
-                 let b = f () in
-                 if b then () else
-                   begin
-                     idle_handler := None;
-                   end
-         done
-       with Exit -> ()
-
-end

src/session/controller_itp.mli

@@ -30,11 +30,6 @@ module type Scheduler = sig
   val idle: (unit -> bool) -> unit
 end
 
-module Unix_scheduler : sig
-  include Scheduler
-  val main_loop : unit -> unit
-end
-
 
 module Make(S : Scheduler) : sig
 

src/why3shell/why3shell.ml

+
+
+module Unix_scheduler = struct
+
+    let idle_handler = ref []
+
+    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
+
+    let timeout_handler = ref []
+
+    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
+
+
+    let idle ~(prio:int) f = insert_idle_handler prio f
+
+    let timeout ~ms f =
+      let ms = float ms /. 1000.0 in
+      let time = Unix.gettimeofday () in
+      insert_timeout_handler ms (time +. ms) f
+
+     let buf = Bytes.create 256
+
+     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
+         done
+       with Exit -> ()
+
+end
+
+
+
+(*
+module C = Why3.Controller_itp.Make(Unix_scheduler)
+ *)
+
+let interp s =
+  match s with
+    | "a" ->
+       let c = ref 10 in
+       Unix_scheduler.timeout
+         ~ms:1000
+         (fun () -> decr c;
+                    if !c > 0 then
+                      (Format.printf "%d@." !c; true)
+                    else
+                      (Format.printf "boom!@."; false))
+    | "i" ->
+       Unix_scheduler.idle
+         ~prio:0
+         (fun () -> Format.printf "idle@."; false)
+    | _ -> Format.printf "unknowm command `%s`@." s
+
+
+
+let () =
+  Unix_scheduler.main_loop interp