why3shell.ml 20.1 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4


module Unix_scheduler = struct

MARCHE Claude's avatar
MARCHE Claude committed
5 6
    (* the private list of functions to call on idle, sorted higher
       priority first. *)
MARCHE Claude's avatar
MARCHE Claude committed
7 8
    let idle_handler = ref []

MARCHE Claude's avatar
MARCHE Claude committed
9 10
    (* [insert_idle_handler p f] inserts [f] as a new function to call
       on idle, with priority [p] *)
MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14 15 16 17 18 19
    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

MARCHE Claude's avatar
MARCHE Claude committed
20
    (* the private list of functions to call on timeout, sorted on
MARCHE Claude's avatar
MARCHE Claude committed
21
       earliest trigger time first. *)
MARCHE Claude's avatar
MARCHE Claude committed
22 23
    let timeout_handler = ref []

MARCHE Claude's avatar
MARCHE Claude committed
24 25
    (* [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] *)
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29 30 31 32 33 34
    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

MARCHE Claude's avatar
MARCHE Claude committed
35
    (* public function to register a task to run on idle *)
MARCHE Claude's avatar
MARCHE Claude committed
36 37
    let idle ~(prio:int) f = insert_idle_handler prio f

MARCHE Claude's avatar
MARCHE Claude committed
38
    (* public function to register a task to run on timeout *)
MARCHE Claude's avatar
MARCHE Claude committed
39
    let timeout ~ms f =
MARCHE Claude's avatar
MARCHE Claude committed
40
      assert (ms > 0);
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44
      let ms = float ms /. 1000.0 in
      let time = Unix.gettimeofday () in
      insert_timeout_handler ms (time +. ms) f

MARCHE Claude's avatar
MARCHE Claude committed
45
     (* buffer for storing character read on stdin *)
MARCHE Claude's avatar
MARCHE Claude committed
46 47
     let buf = Bytes.create 256

48 49 50
     let show_prompt = ref true
     let prompt = ref "> "

MARCHE Claude's avatar
MARCHE Claude committed
51 52 53
     (* [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] *)
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
     let main_loop interp =
       try
         while true do
57 58 59 60
           if !show_prompt then begin
               Format.printf "%s@?" !prompt;
               show_prompt := false;
             end;
MARCHE Claude's avatar
MARCHE Claude committed
61 62 63
           (* attempt to run the first timeout handler *)
           let time = Unix.gettimeofday () in
           match !timeout_handler with
MARCHE Claude's avatar
MARCHE Claude committed
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
           | (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
89 90 91 92
                 | [_] ->
                    let n = Unix.read Unix.stdin buf 0 256 in
                    interp (Bytes.sub_string buf 0 (n-1));
                    show_prompt := true
MARCHE Claude's avatar
MARCHE Claude committed
93 94
                 | [] -> () (* nothing read *)
                 | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98 99 100 101
         done
       with Exit -> ()

end



MARCHE Claude's avatar
MARCHE Claude committed
102 103 104 105
(************************)
(* parsing command line *)
(************************)

106 107 108
open Why3
open Format

MARCHE Claude's avatar
MARCHE Claude committed
109 110 111 112 113 114
let files = Queue.create ()

let spec = Arg.align [
]

let usage_str = Format.sprintf
115
  "Usage: %s [options] [ <file.xml> | <f1.why> <f2.mlw> ...]"
MARCHE Claude's avatar
MARCHE Claude committed
116 117
  (Filename.basename Sys.argv.(0))

118 119

let config, base_config, _env =
MARCHE Claude's avatar
MARCHE Claude committed
120 121
  Why3.Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str

122 123 124 125 126 127 128 129
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)

130 131 132 133

module C = Why3.Controller_itp.Make(Unix_scheduler)

let cont =
134 135
  if Queue.is_empty files then Why3.Whyconf.Args.exit_with_usage spec usage_str;
  let fname = Queue.pop files in
136 137 138 139
  let ses =
    if Filename.check_suffix fname ".xml" then
      Session_itp.load_session fname
    else
140 141 142 143
      begin
        Queue.push fname files;
        Session_itp.empty_session ()
      end
144
  in
145 146 147
  let c = Controller_itp.create_controller env ses in
  Queue.iter (fun fname -> C.add_file c fname) files;
  c
148

149
(* loading the drivers *)
150 151 152
let () =
  Whyconf.Mprover.iter
    (fun _ p ->
153 154
      try
        let d = Driver.load_driver env p.Whyconf.driver [] in
155
        Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
156 157 158 159
      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
160
          Exn_printer.exn_printer e)
161 162 163 164 165 166 167 168 169 170 171 172 173
    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)

174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
let test_idle fmt _args =
  Unix_scheduler.idle
    ~prio:0
    (fun () -> fprintf fmt "idle@."; false)

let test_timeout fmt _args =
  Unix_scheduler.timeout
    ~ms:1000
    (let c = ref 10 in
     fun () -> decr c;
               if !c > 0 then
                 (fprintf fmt "%d@." !c; true)
               else
                 (fprintf fmt "boom!@."; false))

let list_provers _fmt _args =
  let l =
    Whyconf.Hprover.fold
      (fun p _ acc -> (Pp.sprintf "%a" Whyconf.print_prover p)::acc)
      cont.Controller_itp.controller_provers
      []
  in
  let l = List.sort String.compare l in
  printf "@[<hov 2>== Known provers ==@\n%a@]@."
          (Pp.print_list Pp.newline Pp.string) l
199

200
let sort_pair (x,_) (y,_) = String.compare x y
201

202 203 204 205 206 207 208 209 210 211
let list_transforms _fmt _args =
  let l =
    List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ())
  in
  let print_trans_desc fmt (x,r) =
    fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
  printf "@[<hov 2>== Known transformations ==@\n%a@]@\n@."
         (Pp.print_list Pp.newline2 print_trans_desc)
         (List.sort sort_pair l)

212 213
open Controller_itp
open Session_itp
214 215
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
216 217 218 219 220
type proof_hole =
    Th of theory list * theory * theory list |
    Pn of proofNodeID list * proofNodeID * proofNodeID list |
    Tn of transID list * transID * transID list

221
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
222

223
let ctxt = Stack.create ()
224 225 226 227 228

let zipper =
  let files =
    get_files cont.Controller_itp.controller_session
  in
229 230 231
  let file = ref None in
  Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
  let file = Opt.get !file in
232 233
  match file.file_theories with
  | th :: tail -> { cursor = (Th ([], th, tail)); ctxt }
234 235
  | _ -> assert false

236 237 238 239 240 241 242 243 244
let zipper_init () =
  let files =
    get_files cont.Controller_itp.controller_session
  in
  let file = ref None in
  Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
  let file = Opt.get !file in
  match file.file_theories with
  | th :: tail -> zipper.cursor <- (Th ([], th, tail));
245
      while not (Stack.is_empty zipper.ctxt) do ignore (Stack.pop zipper.ctxt) done
246 247 248
  | _ -> assert false


249 250 251 252 253
let zipper_down () =
  match zipper.cursor with
  | Th (_,th,_) ->
    (match theory_goals th with
    | pn::l ->
254
      Stack.push zipper.cursor zipper.ctxt;
255 256 257 258 259 260
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)
  | Pn (_,pn,_) ->
    (match get_transformations cont.controller_session pn with
    | tn::l ->
261
      Stack.push zipper.cursor zipper.ctxt;
262 263 264 265 266 267
      zipper.cursor <- Tn ([],tn,l);
      true
    | _ -> false)
  | Tn (_,tn,_) ->
    (match get_sub_tasks cont.controller_session tn with
    | pn::l ->
268
      Stack.push zipper.cursor zipper.ctxt;
269 270 271 272 273
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)

let zipper_up () =
274 275
  if not (Stack.is_empty zipper.ctxt) then begin
    zipper.cursor <- Stack.pop zipper.ctxt;
276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
    true
  end else
    false

let zipper_right () =
  match zipper.cursor with
  | Th (l,cs,hd::r) ->
    zipper.cursor <- Th (cs::l,hd,r);
    true
  | Pn (l,cs,hd::r) ->
    zipper.cursor <- Pn (cs::l,hd,r);
    true
  | Tn (l,cs,hd::r) ->
    zipper.cursor <- Tn (cs::l,hd,r);
    true
  | _ -> false

let zipper_left () =
  match zipper.cursor with
  | Th (hd::l,cs,r) ->
    zipper.cursor <- Th (l,hd,cs::r);
    true
  | Pn (hd::l,cs,r) ->
    zipper.cursor <- Pn (l,hd,cs::r);
    true
  | Tn (hd::l,cs,r) ->
    zipper.cursor <- Tn (l,hd,cs::r);
    true
  | _ -> false

306 307 308
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)

309 310 311 312 313
let rec next_node () =
  zipper_down () || zipper_right () || (zipper_up () && next_node_no_down ())
and next_node_no_down () =
  zipper_right () || (zipper_up () && next_node_no_down ())

314
let prev_node () = zipper_left () || zipper_up ()
315

316 317 318 319
(* This function try to reach a goal from the current position using
   the move function *)
let rec move_to_goal move =
  if move () then
320 321
    match zipper.cursor with
    | Pn (_,pn,_) -> Some pn
322
    | _  -> move_to_goal move
323 324 325
  else
    None

326
let move_to_goal_ret move =
327
  match
328
    (match move_to_goal move with
Sylvain Dailler's avatar
Sylvain Dailler committed
329
    | None -> Printf.printf "No more goal right; back to root@.";
330
	zipper_init(); move_to_goal next_node
331 332 333 334
    | Some id -> Some id) with
  | None -> failwith "After initialization there is no goal to go to@."
  | Some id -> id

335 336
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)

337 338
(* The cursor of the zipper is on a goal *)
let is_goal_cursor () =
339
  match zipper.cursor with
340 341 342 343 344
  | Pn (_, pn, _) -> Some pn
  | _ -> None

(* If on goal, do nothing else go to next_goal *)
let nearest_goal () =
345 346
  match is_goal_cursor () with
  | None -> move_to_goal_ret next_node
347
  | Some id -> id
348

349 350 351 352 353 354 355 356 357 358 359 360
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

let print_proof_attempt fmt pa =
  fprintf fmt "%a tl=%d %a"
          Whyconf.print_prover pa.prover
          pa.limit.Call_provers.limit_time
          (Pp.print_option Call_provers.print_prover_result) pa.proof_state

let rec print_proof_node s (fmt: Format.formatter) p =
  let parent = match get_proof_parent s p with
  | Theory t -> (theory_name t).Ident.id_string
361
  | Trans id -> get_transf_name s id
362 363 364 365 366 367
  in
  let current_goal =
    match is_goal_cursor () with
    | Some pn -> pn = p
    | _ -> false
  in
368 369 370 371 372 373
  (* TODO proved or not to be done on the whole tree. Just a test *)
  let is_proved () =
    match is_goal_cursor () with
    | Some p -> Controller_itp.find_pn cont p
    | _ -> false
  in
374 375
  if current_goal then
    fprintf fmt "**";
376 377
  if is_proved () then
    fprintf fmt "P";
378 379

  fprintf fmt
380
    "@[<hv 2> Goal %s; parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
381 382 383 384 385 386
    (get_proof_name s p).Ident.id_string parent
    (Pp.print_list Pp.semi print_proof_attempt)
    (get_proof_attempts s p)
    (Pp.print_list Pp.semi (print_trans_node s)) (get_transformations s p);

  if current_goal then
387
    fprintf fmt " **"
388 389

and print_trans_node s fmt id =
390 391
  let name = get_transf_name s id in
  let args = get_transf_args s id in
392 393
  let l = get_sub_tasks s id in
  let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
394
  fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.semi pp_print_string) args parent
395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
    (Pp.print_list Pp.semi (print_proof_node s)) l

let print_theory s fmt th : unit =
  fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
    (Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) (theory_goals th)

let print_file s fmt (file, thl) =
  fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
    (Pp.print_list Pp.semi (print_theory s)) thl

let print_s s fmt =
  fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))

let print_session fmt s =
  let l = Stdlib.Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
  fprintf fmt "%a@." (print_s s) l;;

let dump_session_raw fmt _args =
  fprintf fmt "%a@." print_session cont.Controller_itp.controller_session


let print_position (s: session) (cursor: proof_zipper) fmt: unit =
  match cursor.cursor with
  | Th (_, th, _) -> fprintf fmt "%a@." (print_theory s) th
  | Pn (_, pn, _) -> fprintf fmt "%a@." (print_proof_node s) pn
  | Tn (_, tn, _) -> fprintf fmt "%a@." (print_trans_node s) tn

let print_position_p s cursor fmt _ = print_position s cursor fmt

424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
(* Print current goal or nearest next goal if we are not on a goal *)
let test_print_goal fmt _args =
  (* temporary : get the first goal *)
  let id = nearest_goal () in
  let task = Session_itp.get_task cont.Controller_itp.controller_session id in
  fprintf fmt "@[====================== Task =====================@\n%a@]@."
          Pretty.print_task
          (* (Driver.print_task ~cntexample:false task_driver) *)
          task

(* Execute f and then print the goal *)
let then_print f fmt args =
  f fmt args;
  test_print_goal fmt []

439 440 441
(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)

442 443
let test_schedule_proof_attempt fmt _args =
  (* temporary : get the first goal *)
444
  let id = nearest_goal () in
445 446 447 448
  let callback status =
    fprintf fmt "status: %a@."
            Controller_itp.print_status status
  in
MARCHE Claude's avatar
MARCHE Claude committed
449
  let limit = Call_provers.{empty_limit with limit_time = 2} in
450 451 452 453
  C.schedule_proof_attempt
    cont id alt_ergo.Whyconf.prover
    ~limit ~callback

Sylvain Dailler's avatar
Sylvain Dailler committed
454
let apply_transform fmt args =
455
  match args with
Sylvain Dailler's avatar
Sylvain Dailler committed
456
    | tr :: tl ->
457 458 459 460 461
       let id = nearest_goal () in
       let callback status =
         fprintf fmt "transformation status: %a@."
                 Controller_itp.print_trans_status status
       in
Sylvain Dailler's avatar
Sylvain Dailler committed
462 463
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."
MARCHE Claude's avatar
MARCHE Claude committed
464 465 466

(*******)

467 468 469 470 471
let task_driver =
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver env d []
472

473 474 475 476 477 478 479
let test_save_session _fmt args =
  match args with
  | file :: _ ->
    Session_itp.save_session (file ^ ".xml") cont.Controller_itp.controller_session;
    printf "session saved@."
  | [] ->
    printf "missing session file name@."
480 481 482 483 484

let test_reload fmt _args =
  fprintf fmt "Reloading... @?";
  C.reload_files cont;
  fprintf fmt "done @."
485

Sylvain Dailler's avatar
Sylvain Dailler committed
486 487 488 489 490 491 492 493
let test_transform_and_display fmt args =
  match args with
    | tr :: tl ->
       let id = nearest_goal () in
       let callback status =
         fprintf fmt "transformation status: %a@."
                 Controller_itp.print_trans_status status;
         match status with
494
         | TSdone tid -> (ignore (move_to_goal_ret next_node);
Sylvain Dailler's avatar
Sylvain Dailler committed
495 496 497 498 499 500
             test_print_goal fmt [])
         | _ -> ()
       in
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."

MARCHE Claude's avatar
MARCHE Claude committed
501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537

(***************** strategy *****************)

let loaded_strategies = ref []

let strategies () =
  match !loaded_strategies with
    | [] ->
      let strategies = Whyconf.get_strategies config in
      let strategies =
        Stdlib.Mstr.fold_left
          (fun acc _ st ->
            let name = st.Whyconf.strategy_name in
            try
              let code = st.Whyconf.strategy_code in
              let code = Strategy_parser.parse2 env config code in
              let shortcut = st.Whyconf.strategy_shortcut in
              Format.eprintf "[Why3shell] Strategy '%s' loaded.@." name;
              (name, shortcut, st.Whyconf.strategy_desc, code) :: acc
            with Strategy_parser.SyntaxError msg ->
              Format.eprintf
                "[Why3shell warning] Loading strategy '%s' failed: %s@." name msg;
              acc)
          []
          strategies
      in
      let strategies = List.rev strategies in
      loaded_strategies := strategies;
      strategies
    | l -> l

let list_strategies _fmt _args =
  let l = strategies () in
  let pp_strat fmt (n,s,_,_) = fprintf fmt "%s: %s" s n in
  printf "@[<hov 2>== Known strategies ==@\n%a@]@."
          (Pp.print_list Pp.newline pp_strat) l

Sylvain Dailler's avatar
Sylvain Dailler committed
538
(*******)
MARCHE Claude's avatar
MARCHE Claude committed
539 540


541 542 543 544 545 546 547 548 549 550 551 552
let print_known_map _fmt _args =
  let id = nearest_goal () in
  let task = get_task cont.controller_session id in
  let km = Task.task_known task in
  Ident.Mid.iter
    (fun id _d ->
     printf "known: %s@." id.Ident.id_string)
    km

(****)


553 554
let commands =
  [
555
    "k", "list known identifiers", print_known_map;
556 557
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
MARCHE Claude's avatar
MARCHE Claude committed
558
    "list-strategies", "list available strategies", list_strategies;
Sylvain Dailler's avatar
Sylvain Dailler committed
559
    "a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
Sylvain Dailler's avatar
Sylvain Dailler committed
560
    "b", "<transname> <args>: behave like a but add function to display into the callback", test_transform_and_display;
561
    "p", "print the session in raw form", dump_session_raw;
562 563
    "t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
    "g", "prints the first goal", test_print_goal;
564
    "r", "reload the session (test only)", test_reload;
565
    "s", "[s my_session] save the current session in my_session.xml", test_save_session;
566 567 568 569 570 571
    "ng", "get to the next goal", then_print (move_to_goal_ret_p next_node);
    "pg", "get to the prev goal", then_print (move_to_goal_ret_p prev_node);
    "gu", "get to the goal up",  then_print (move_to_goal_ret_p zipper_up);
    "gd", "get to the goal down",  then_print (move_to_goal_ret_p zipper_down);
    "gr", "get to the goal right",  then_print (move_to_goal_ret_p zipper_right);
    "gl", "get to the goal left",  then_print (move_to_goal_ret_p zipper_left);
572
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
573 574 575
    "zu", "navigation up, parent", (fun _ _ -> ignore (zipper_up ()));
    "zd", "navigation down, left child", (fun _ _ -> ignore (zipper_down ()));
    "zl", "navigation left, left brother", (fun _ _ -> ignore (zipper_left ()));
Sylvain Dailler's avatar
Sylvain Dailler committed
576
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
  ]

let commands_table = Stdlib.Hstr.create 17
let () =
  List.iter
    (fun (c,_,f) -> Stdlib.Hstr.add commands_table c f)
    commands

let help () =
  printf "== Available commands ==@\n";
  let l = ("q", "exit the shell") ::
            List.rev_map (fun (c,h,_) -> (c,h)) commands
  in
  let l = List.sort sort_pair l in
  List.iter (fun (c,help) -> printf "%20s : %s@\n" c help) l;
  printf "@."
593 594


595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
let split_args s =
  let args = ref [] in
  let b = Buffer.create 17 in
  let state = ref 0 in
  for i = 0 to String.length s - 1 do
    let c = s.[i] in
    match !state, c with
    | 0,' ' -> ()
    | 0,'"' -> state := 1
    | 0,_ -> Buffer.add_char b c; state := 2
    | 1,'"' -> args := Buffer.contents b :: !args; Buffer.clear b; state := 0
    | 1,_ -> Buffer.add_char b c
    | 2,' ' -> args := Buffer.contents b :: !args; Buffer.clear b; state := 0
    | 2,_ -> Buffer.add_char b c
    | _ -> assert false
  done;
  begin
    match !state with
      | 0 -> ()
      | 1 -> args := Buffer.contents b :: !args (* TODO : report missing '"' *)
      | 2 -> args := Buffer.contents b :: !args
      | _ -> assert false
  end;
  match List.rev !args with
619
    | a::b -> a,b
620 621 622 623
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
624
  match cmd with
625 626 627 628 629 630 631 632 633 634
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
       try
         let f = Stdlib.Hstr.find commands_table cmd in
         f fmt args
       with Not_found ->
635
         printf "unknown command '%s'@." cmd
636

MARCHE Claude's avatar
MARCHE Claude committed
637 638

let () =
MARCHE Claude's avatar
MARCHE Claude committed
639
  printf "Welcome to Why3 shell. Type '?' for help.@.";
640 641 642
  let chout = open_out "why3shell.out" in
  let fmt = formatter_of_out_channel chout in
  Unix_scheduler.main_loop (interp chout fmt)