why3shell.ml 2.71 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99


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