why3shell.ml 20.7 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2 3
(* TODO *)
let proof_general = true
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6

module Unix_scheduler = struct

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

MARCHE Claude's avatar
MARCHE Claude committed
11 12
    (* [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
13 14 15 16 17 18 19 20 21
    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
22
    (* the private list of functions to call on timeout, sorted on
MARCHE Claude's avatar
MARCHE Claude committed
23
       earliest trigger time first. *)
MARCHE Claude's avatar
MARCHE Claude committed
24 25
    let timeout_handler = ref []

MARCHE Claude's avatar
MARCHE Claude committed
26 27
    (* [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
28 29 30 31 32 33 34 35 36
    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
37
    (* public function to register a task to run on idle *)
MARCHE Claude's avatar
MARCHE Claude committed
38 39
    let idle ~(prio:int) f = insert_idle_handler prio f

MARCHE Claude's avatar
MARCHE Claude committed
40
    (* public function to register a task to run on timeout *)
MARCHE Claude's avatar
MARCHE Claude committed
41
    let timeout ~ms f =
MARCHE Claude's avatar
MARCHE Claude committed
42
      assert (ms > 0);
MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46
      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
47
     (* buffer for storing character read on stdin *)
MARCHE Claude's avatar
MARCHE Claude committed
48 49
     let buf = Bytes.create 256

50
     let show_prompt = ref 0
51 52
     let prompt = ref "> "

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

end



MARCHE Claude's avatar
MARCHE Claude committed
105 106 107 108
(************************)
(* parsing command line *)
(************************)

109 110 111
open Why3
open Format

MARCHE Claude's avatar
MARCHE Claude committed
112 113 114 115 116 117
let files = Queue.create ()

let spec = Arg.align [
]

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

121 122

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

125 126 127 128 129 130 131 132
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)

133 134 135 136

module C = Why3.Controller_itp.Make(Unix_scheduler)

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

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

177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
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
202

203
let sort_pair (x,_) (y,_) = String.compare x y
204

205 206 207 208 209 210 211 212 213 214
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)

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

224
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
225

226
let ctxt = Stack.create ()
227 228 229 230 231

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

239 240 241 242 243 244 245 246 247
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));
248
      while not (Stack.is_empty zipper.ctxt) do ignore (Stack.pop zipper.ctxt) done
249 250 251
  | _ -> assert false


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

let zipper_up () =
277 278
  if not (Stack.is_empty zipper.ctxt) then begin
    zipper.cursor <- Stack.pop zipper.ctxt;
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 306 307 308
    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

309 310 311
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)

312 313 314 315 316
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 ())

317
let prev_node () = zipper_left () || zipper_up ()
318

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

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

338 339
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)

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

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

352 353 354 355 356 357 358 359 360 361 362 363
(* _____________________________________________________________________ *)
(* -------------------- 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
364
  | Trans id -> get_transf_name s id
365 366 367 368 369 370 371 372
  in
  let current_goal =
    match is_goal_cursor () with
    | Some pn -> pn = p
    | _ -> false
  in
  if current_goal then
    fprintf fmt "**";
Clément Fumex's avatar
Clément Fumex committed
373
  if Controller_itp.pn_proved cont p then
374
    fprintf fmt "P";
375 376

  fprintf fmt
377
    "@[<hv 2> Goal %s; parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
378 379 380 381 382 383
    (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
384
    fprintf fmt " **"
385 386

and print_trans_node s fmt id =
387 388
  let name = get_transf_name s id in
  let args = get_transf_args s id in
389 390
  let l = get_sub_tasks s id in
  let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
Clément Fumex's avatar
Clément Fumex committed
391 392
  if Controller_itp.tn_proved cont id then
    fprintf fmt "P";
393
  fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.semi pp_print_string) args parent
394 395 396
    (Pp.print_list Pp.semi (print_proof_node s)) l

let print_theory s fmt th : unit =
Clément Fumex's avatar
Clément Fumex committed
397 398
  if Controller_itp.th_proved cont (theory_name th) then
    fprintf fmt "P";
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 424
  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

Sylvain Dailler's avatar
Sylvain Dailler committed
425 426 427 428 429 430
let task_driver =
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver env d []

431 432 433 434 435 436
(* 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@]@."
Sylvain Dailler's avatar
Sylvain Dailler committed
437 438
          (*Pretty.print_task*)
          (Driver.print_task ~cntexample:false task_driver)
439 440 441 442 443 444 445
          task

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

446 447 448
(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)

449 450
let test_schedule_proof_attempt fmt _args =
  (* temporary : get the first goal *)
451
  let id = nearest_goal () in
452 453 454 455
  let callback status =
    fprintf fmt "status: %a@."
            Controller_itp.print_status status
  in
MARCHE Claude's avatar
MARCHE Claude committed
456
  let limit = Call_provers.{empty_limit with limit_time = 2} in
457 458 459 460
  C.schedule_proof_attempt
    cont id alt_ergo.Whyconf.prover
    ~limit ~callback

Sylvain Dailler's avatar
Sylvain Dailler committed
461
let apply_transform fmt args =
462
  match args with
Sylvain Dailler's avatar
Sylvain Dailler committed
463
    | tr :: tl ->
464 465 466 467 468
       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
469 470
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."
MARCHE Claude's avatar
MARCHE Claude committed
471 472 473

(*******)

474 475 476 477 478 479 480
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@."
481 482 483 484 485

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

Sylvain Dailler's avatar
Sylvain Dailler committed
487 488 489 490 491 492 493 494
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
495
         | TSdone _tid -> (ignore (move_to_goal_ret next_node);
496
             dump_session_raw fmt []; test_print_goal fmt [])
Sylvain Dailler's avatar
Sylvain Dailler committed
497 498 499 500 501
         | _ -> ()
       in
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."

MARCHE Claude's avatar
MARCHE Claude committed
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 538

(***************** 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
539
(*******)
MARCHE Claude's avatar
MARCHE Claude committed
540 541


542 543 544 545 546 547 548 549 550 551 552 553
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

(****)


554 555
let commands =
  [
556
    "k", "list known identifiers", print_known_map;
557 558
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
MARCHE Claude's avatar
MARCHE Claude committed
559
    "list-strategies", "list available strategies", list_strategies;
Sylvain Dailler's avatar
Sylvain Dailler committed
560
    "a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
Sylvain Dailler's avatar
Sylvain Dailler committed
561
    "b", "<transname> <args>: behave like a but add function to display into the callback", test_transform_and_display;
562
    "p", "print the session in raw form", dump_session_raw;
563 564
    "t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
    "g", "prints the first goal", test_print_goal;
565
    "r", "reload the session (test only)", test_reload;
566
    "s", "[s my_session] save the current session in my_session.xml", test_save_session;
567 568 569 570 571 572
    "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);
573
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
574 575 576 577 578 579 580 581 582 583
    "test", "test register known_map",
    (fun _ _ ->
      try
        let id = nearest_goal () in
        let task = get_task cont.controller_session id in
        let _ = Args_wrapper.build_name_tables task in
        ()
      with e when not (Debug.test_flag Debug.stack_trace) ->
        Format.eprintf
          "@[Exception raised :@ %a@.@]" Exn_printer.exn_printer e);
584 585 586
    "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
587
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603
  ]

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 "@."
604 605


606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629
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
630
    | a::b -> a,b
631 632 633 634
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
635
  match cmd with
636 637 638 639 640 641
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
Clément Fumex's avatar
Clément Fumex committed
642 643 644 645 646 647 648 649 650
      let f =
        try
          Some (Stdlib.Hstr.find commands_table cmd)
        with Not_found ->
          None
      in
      match f with
      | Some f -> f fmt args
      | None -> printf "unknown command '%s'@." cmd
MARCHE Claude's avatar
MARCHE Claude committed
651 652

let () =
MARCHE Claude's avatar
MARCHE Claude committed
653
  printf "Welcome to Why3 shell. Type '?' for help.@.";
654
  let chout = open_out "why3shell.out" in
655
  let fmt = if proof_general then formatter_of_out_channel stdout else formatter_of_out_channel chout in
656
  Unix_scheduler.main_loop (interp chout fmt)