why3shell.ml 23.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 51
     let prompt_delay = ref 0
     let print_prompt = ref true
52 53
     let prompt = ref "> "

MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
     (* [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
57 58 59
     let main_loop interp =
       try
         while true do
60 61 62 63 64 65 66
           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
67
           end;
MARCHE Claude's avatar
MARCHE Claude committed
68
           (* attempt to run the first timeout handler *)
69
           (let time = Unix.gettimeofday () in
MARCHE Claude's avatar
MARCHE Claude committed
70
           match !timeout_handler with
MARCHE Claude's avatar
MARCHE Claude committed
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
           | (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
96 97 98
                 | [_] ->
                    let n = Unix.read Unix.stdin buf 0 256 in
                    interp (Bytes.sub_string buf 0 (n-1));
99
                    print_prompt := true
MARCHE Claude's avatar
MARCHE Claude committed
100
                 | [] -> () (* nothing read *)
101
                 | _ -> assert false);
MARCHE Claude's avatar
MARCHE Claude committed
102 103 104 105 106 107 108
         done
       with Exit -> ()

end



MARCHE Claude's avatar
MARCHE Claude committed
109 110 111 112
(************************)
(* parsing command line *)
(************************)

113 114 115
open Why3
open Format

116
(* files of the current task *)
MARCHE Claude's avatar
MARCHE Claude committed
117 118
let files = Queue.create ()

119
let spec = Arg.align []
MARCHE Claude's avatar
MARCHE Claude committed
120

121
(* --help *)
MARCHE Claude's avatar
MARCHE Claude committed
122
let usage_str = Format.sprintf
123
  "Usage: %s [options] [ <file.xml> | <f1.why> <f2.mlw> ...]"
MARCHE Claude's avatar
MARCHE Claude committed
124 125
  (Filename.basename Sys.argv.(0))

126
(* build command line *)
127
let config, base_config, env =
MARCHE Claude's avatar
MARCHE Claude committed
128 129
  Why3.Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str

130 131 132 133 134 135
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] *)
136
(*let env : Env.env = Env.create_env (Whyconf.loadpath main)*)
137

138 139
(* -- declare provers -- *)

140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
(* Return the prover corresponding to given name. name is of the form
  | name
  | name, version
  | name, altern
  | name, version, altern *)
let return_prover fmt name =
  let fp = Whyconf.parse_filter_prover name in
  (** all provers that have the name/version/altern name *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
    fprintf fmt "Prover corresponding to %s has not been found@." name;
    None
  end else
    Some (snd (Whyconf.Mprover.choose provers))

155
(* -- init controller -- *)
156

MARCHE Claude's avatar
MARCHE Claude committed
157 158 159
let cont =
  Session_user_interface.cont_from_files spec usage_str env files provers

160 161
module C = Why3.Controller_itp.Make(Unix_scheduler)

162 163

(* --  -- *)
164

165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
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
190

191
let sort_pair (x,_) (y,_) = String.compare x y
192

193 194 195 196 197 198 199 200 201 202
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)

203 204
open Controller_itp
open Session_itp
205

206 207
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
208

209 210 211 212 213
type proof_hole =
    Th of theory list * theory * theory list |
    Pn of proofNodeID list * proofNodeID * proofNodeID list |
    Tn of transID list * transID * transID list

214
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
215

216
let ctxt = Stack.create ()
217 218 219 220 221

let zipper =
  let files =
    get_files cont.Controller_itp.controller_session
  in
222 223 224
  let file = ref None in
  Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
  let file = Opt.get !file in
225 226
  match file.file_theories with
  | th :: tail -> { cursor = (Th ([], th, tail)); ctxt }
227 228
  | _ -> assert false

229 230 231 232 233 234 235 236 237
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));
238
      while not (Stack.is_empty zipper.ctxt) do ignore (Stack.pop zipper.ctxt) done
239 240
  | _ -> assert false

241 242 243 244 245
let zipper_down () =
  match zipper.cursor with
  | Th (_,th,_) ->
    (match theory_goals th with
    | pn::l ->
246
      Stack.push zipper.cursor zipper.ctxt;
247 248 249 250 251 252
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)
  | Pn (_,pn,_) ->
    (match get_transformations cont.controller_session pn with
    | tn::l ->
253
      Stack.push zipper.cursor zipper.ctxt;
254 255 256 257 258 259
      zipper.cursor <- Tn ([],tn,l);
      true
    | _ -> false)
  | Tn (_,tn,_) ->
    (match get_sub_tasks cont.controller_session tn with
    | pn::l ->
260
      Stack.push zipper.cursor zipper.ctxt;
261 262 263 264 265
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)

let zipper_up () =
266 267
  if not (Stack.is_empty zipper.ctxt) then begin
    zipper.cursor <- Stack.pop zipper.ctxt;
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
    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

298 299 300
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)

301 302 303 304 305
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 ())

306
let prev_node () = zipper_left () || zipper_up ()
307

308 309 310 311
(* This function try to reach a goal from the current position using
   the move function *)
let rec move_to_goal move =
  if move () then
312 313
    match zipper.cursor with
    | Pn (_,pn,_) -> Some pn
314
    | _  -> move_to_goal move
315 316 317
  else
    None

318
let move_to_goal_ret move =
319
  match
320
    (match move_to_goal move with
Sylvain Dailler's avatar
Sylvain Dailler committed
321
    | None -> Printf.printf "No more goal right; back to root@.";
322
	zipper_init(); move_to_goal next_node
323 324 325 326
    | Some id -> Some id) with
  | None -> failwith "After initialization there is no goal to go to@."
  | Some id -> id

327 328
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)

329 330
(* The cursor of the zipper is on a goal *)
let is_goal_cursor () =
331
  match zipper.cursor with
332 333 334 335 336
  | Pn (_, pn, _) -> Some pn
  | _ -> None

(* If on goal, do nothing else go to next_goal *)
let nearest_goal () =
337 338
  match is_goal_cursor () with
  | None -> move_to_goal_ret next_node
339
  | Some id -> id
340

341 342 343 344
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

let print_proof_attempt fmt pa =
Clément Fumex's avatar
Clément Fumex committed
345
  fprintf fmt "%a tl=%d %a obsolete=%a"
346 347 348
          Whyconf.print_prover pa.prover
          pa.limit.Call_provers.limit_time
          (Pp.print_option Call_provers.print_prover_result) pa.proof_state
Clément Fumex's avatar
Clément Fumex committed
349
          pp_print_bool pa.proof_obsolete
350 351 352 353

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
354
  | Trans id -> get_transf_name s id
355 356 357 358 359 360 361 362
  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
363
  if Controller_itp.pn_proved cont p then
364
    fprintf fmt "P";
365 366

  fprintf fmt
MARCHE Claude's avatar
MARCHE Claude committed
367
    "@[<hv 2>{ Goal=%s;@ parent=%s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@] }@]"
368 369 370 371 372 373
    (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
374
    fprintf fmt " **"
375 376

and print_trans_node s fmt id =
377 378
  let name = get_transf_name s id in
  let args = get_transf_args s id in
379
  let l = get_sub_tasks s id in
Clément Fumex's avatar
Clément Fumex committed
380
  let ll = get_detached_sub_tasks s id in
381
  let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
Clément Fumex's avatar
Clément Fumex committed
382 383
  if Controller_itp.tn_proved cont id then
    fprintf fmt "P";
Clément Fumex's avatar
Clément Fumex committed
384 385
  fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a];@ detached[%a] }@]" name
    (Pp.print_list Pp.semi pp_print_string) args parent
386
    (Pp.print_list Pp.semi (print_proof_node s)) l
Clément Fumex's avatar
Clément Fumex committed
387
    (Pp.print_list Pp.semi (print_proof_node s)) ll
388 389

let print_theory s fmt th : unit =
390
  if Controller_itp.th_proved cont th then
Clément Fumex's avatar
Clément Fumex committed
391
    fprintf fmt "P";
Clément Fumex's avatar
Clément Fumex committed
392 393 394
  fprintf fmt "@[<hv 1> Theory %s;@ [%a];@ detached[%a]@]" (theory_name th).Ident.id_string
    (Pp.print_list Pp.semi (print_proof_node s)) (theory_goals th)
    (Pp.print_list Pp.semi (print_proof_node s)) (theory_detached_goals th)
395

Clément Fumex's avatar
Clément Fumex committed
396 397
let print_file s fmt (file, thl, detached) =
  fprintf fmt "@[<hv 1> File %s;@ [%a];@ detached[%a]@]" file.file_name
398
    (Pp.print_list Pp.semi (print_theory s)) thl
Clément Fumex's avatar
Clément Fumex committed
399
    (Pp.print_list Pp.semi (print_theory s)) detached
400 401 402 403 404

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

let print_session fmt s =
Clément Fumex's avatar
Clément Fumex committed
405 406 407
  let l = Stdlib.Hstr.fold
      (fun _ f acc -> (f,f.file_theories,f.file_detached_theories) :: acc) (get_files s) [] in
  fprintf fmt "folder %a %a@." pp_print_string (Session_itp.get_dir s) (print_s s) l;;
408 409 410 411

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

412 413
let display_session fmt _args =
  fprintf fmt "%a@." Controller_itp.print_session cont
414 415 416 417 418 419 420 421 422

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
423 424 425 426 427 428
let task_driver =
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver env d []

429 430 431 432 433 434
(* 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
435 436
          (*Pretty.print_task*)
          (Driver.print_task ~cntexample:false task_driver)
437 438 439 440 441 442 443
          task

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

444 445 446
(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)

447
let test_schedule_proof_attempt fmt (args: string list) =
448
  (* temporary : get the first goal *)
449
  let id = nearest_goal () in
450
  let callback _panid status =
451
    match status with
452
    | Done _prover_result -> (display_session fmt []; test_print_goal fmt [];
453 454 455 456 457 458 459 460 461
                              fprintf fmt "status: %a@."
                                Controller_itp.print_status status)
    | Scheduled | Running -> ()
    | _ ->
        fprintf fmt "status: %a@."
          Controller_itp.print_status status
  in
  let name, limit = match args with
  | [name] ->
Sylvain Dailler's avatar
Sylvain Dailler committed
462 463 464 465
      let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
                                        limit_mem = Whyconf.memlimit main;
                                        limit_steps = 0} in
      name, default_limit
466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482
  | [name; timeout] -> name, Call_provers.{empty_limit with
                                           limit_time = int_of_string timeout}
  | [name; timeout; oom ] ->
      name, Call_provers.{limit_time = int_of_string timeout;
                          limit_mem = int_of_string oom;
                          limit_steps = 0}
  | _ -> printf "Bad arguments prover_name, version timeout memlimit@.";
      "", Call_provers.empty_limit
  in
  let np = return_prover fmt name in
  (match np with
  | None -> ()
  | Some p ->
      C.schedule_proof_attempt
        cont id p.Whyconf.prover
        ~limit ~callback)
(*    | _ -> printf "Give the prover name@."*)
483

Sylvain Dailler's avatar
Sylvain Dailler committed
484
let apply_transform fmt args =
485
  match args with
Sylvain Dailler's avatar
Sylvain Dailler committed
486
    | tr :: tl ->
487 488 489 490 491
       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
492 493
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."
MARCHE Claude's avatar
MARCHE Claude committed
494 495 496

(*******)

Clément Fumex's avatar
Clément Fumex committed
497 498
let test_save_session _fmt _args =
  Session_itp.save_session cont.Controller_itp.controller_session
499 500 501

let test_reload fmt _args =
  fprintf fmt "Reloading... @?";
Clément Fumex's avatar
Clément Fumex committed
502
  (* use_shapes is true since session is in memory *)
503
  Controller_itp.reload_files cont env ~use_shapes:true;
504
  zipper_init ();
505
  fprintf fmt "done @."
506

507 508 509 510 511 512
let test_replay fmt _args =
  fprintf fmt "Replaying... @?";
  let callback = C.replay_print in
  C.replay ~use_steps:false cont ~callback:callback ~remove_obsolete:false;
  zipper_init ()

Sylvain Dailler's avatar
Sylvain Dailler committed
513 514 515 516 517 518 519 520
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
521
         | TSdone _tid -> (ignore (move_to_goal_ret next_node);
522
             display_session fmt []; test_print_goal fmt [])
Sylvain Dailler's avatar
Sylvain Dailler committed
523 524 525 526 527
         | _ -> ()
       in
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."

MARCHE Claude's avatar
MARCHE Claude committed
528 529

let list_strategies _fmt _args =
530 531 532
  let l = Session_user_interface.strategies
            cont.Controller_itp.controller_env config
  in
MARCHE Claude's avatar
MARCHE Claude committed
533
  let pp_strat fmt (n,s,desc,_) = fprintf fmt "%s (%s): %s" s n desc in
MARCHE Claude's avatar
MARCHE Claude committed
534 535 536
  printf "@[<hov 2>== Known strategies ==@\n%a@]@."
          (Pp.print_list Pp.newline pp_strat) l

MARCHE Claude's avatar
MARCHE Claude committed
537 538 539
let run_strategy _fmt args =
  match args with
  | [s] ->
540 541 542
     let l = Session_user_interface.strategies
            cont.Controller_itp.controller_env config
     in
MARCHE Claude's avatar
MARCHE Claude committed
543 544 545 546 547 548 549 550 551 552 553 554 555 556
     let st = List.filter (fun (_,c,_,_) -> c=s) l in
     begin
       match st with
       | [(n,_,_,st)] ->
          printf "running strategy '%s'@." n;
          let id = nearest_goal () in
          let callback sts =
            printf "Strategy status: %a@." print_strategy_status sts
          in
          C.run_strategy_on_goal cont id st ~callback
       | _ -> printf "Strategy '%s' not found@." s
     end
  | _ -> printf "Please give the strategy shortcut as argument@."

Sylvain Dailler's avatar
Sylvain Dailler committed
557
(*******)
MARCHE Claude's avatar
MARCHE Claude committed
558 559


560 561 562 563 564 565 566 567 568
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

569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591
let find_any_id nt s =
  try (Stdlib.Mstr.find s nt.Theory.ns_pr).Decl.pr_name with
  | Not_found -> try (Stdlib.Mstr.find s nt.Theory.ns_ls).Term.ls_name with
    | Not_found -> (Stdlib.Mstr.find s nt.Theory.ns_ts).Ty.ts_name

let print_id s task fmt =
  let tables = Args_wrapper.build_name_tables task in
  let km = tables.Args_wrapper.known_map in
  let id = try Some (find_any_id tables.Args_wrapper.namespace s) with
  | Not_found -> Format.fprintf fmt "Does not exists @."; None in
  if id = None then () else
  let id = Opt.get id in
  let d =
    try Some (Ident.Mid.find id km) with
    | Not_found -> None in
  if d = None then () else Format.fprintf fmt "%a @." (Why3printer.print_decl tables) (Opt.get d)

let test_print_id fmt args =
  let id = nearest_goal () in
  let task = get_task cont.controller_session id in
  match args with
  | [s] -> print_id s task fmt
  | _ -> Format.fprintf fmt "Wrong number of arguments"
592

Sylvain Dailler's avatar
Sylvain Dailler committed
593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615

let search s fmt task =
  let tables = Args_wrapper.build_name_tables task in
  let id_decl = tables.Args_wrapper.id_decl in
  let id = try Some (find_any_id tables.Args_wrapper.namespace s) with
  | Not_found -> Format.fprintf fmt "Does not exists @."; None in
  if id = None then () else
  let id = Opt.get id in
  let l =
    try Some (Ident.Mid.find id id_decl) with
    | Not_found -> None in
  if l = None then () else
  Format.fprintf fmt "%a @."
    (Pp.print_list (fun fmt _ -> Format.fprintf fmt "\n")
       (Why3printer.print_decl tables)) (Opt.get l)

let test_search_id fmt args =
  let id = nearest_goal () in
  let task = get_task cont.controller_session id in
  match args with
  | [s] -> search s fmt task
  | _ -> Format.fprintf fmt "Wrong number of arguments"

616
(****)
617

618 619
let commands =
  [
620
    "k", "list known identifiers", print_known_map;
621 622
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
MARCHE Claude's avatar
MARCHE Claude committed
623
    "list-strategies", "list available strategies", list_strategies;
Sylvain Dailler's avatar
Sylvain Dailler committed
624
    "a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
MARCHE Claude's avatar
MARCHE Claude committed
625
    "t", "<transname> <args>: behave like 'a' but add function to display into the callback", test_transform_and_display;
626 627
    "pr", "print the session in raw form", dump_session_raw;
    "p", "print the session", display_session;
MARCHE Claude's avatar
MARCHE Claude committed
628 629
    "c", "<provername> [timelimit [memlimit]] run a prover on the current goal", test_schedule_proof_attempt;
    "st", "<c> apply the strategy whose shortcut is 'c'", run_strategy;
630
    "print", "<s> print the declaration where s was defined", test_print_id;
Sylvain Dailler's avatar
Sylvain Dailler committed
631
    "search", "<s> print some declarations where s appear", test_search_id;
MARCHE Claude's avatar
MARCHE Claude committed
632
    "g", "prints the current goal", test_print_goal;
633
    "r", "reload the session (test only)", test_reload;
634
    "rp", "replay", test_replay;
Clément Fumex's avatar
Clément Fumex committed
635
    "s", "save the current session", test_save_session;
MARCHE Claude's avatar
MARCHE Claude committed
636 637 638 639 640 641
    "ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
    "pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
    "gu", "go to the goal up",  then_print (move_to_goal_ret_p zipper_up);
    "gd", "go to the goal down",  then_print (move_to_goal_ret_p zipper_down);
    "gr", "go to the goal right",  then_print (move_to_goal_ret_p zipper_right);
    "gl", "go to the goal left",  then_print (move_to_goal_ret_p zipper_left);
642
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
643 644 645 646 647 648 649 650 651 652
    "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);
653 654 655
    "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
656
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672
  ]

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 "@."
673 674


675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698
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
699
    | a::b -> a,b
700 701 702 703
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
704
  match cmd with
705 706 707 708 709 710
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
Clément Fumex's avatar
Clément Fumex committed
711 712 713 714 715 716 717 718 719
      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
720 721

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