Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

why3shell.ml 25 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 157 158

module C = Why3.Controller_itp.Make(Unix_scheduler)

159 160
let cont_init () =
  (* create controller *)
161
  if Queue.is_empty files then Why3.Whyconf.Args.exit_with_usage spec usage_str;
Clément Fumex's avatar
Clément Fumex committed
162 163 164 165 166 167 168 169 170 171 172 173
  let fname = Queue.peek files in
  (* extract project directory, and create it if needed *)
  let dir =
    if Filename.check_suffix fname ".why" ||
       Filename.check_suffix fname ".mlw"
    then begin
      let dir = Filename.chop_extension fname in
      if not (Sys.file_exists dir) then
        Unix.mkdir dir 0o777;
      dir
    end
    else Filename.dirname fname
174
  in
Clément Fumex's avatar
Clément Fumex committed
175
  (* we load the session *)
Clément Fumex's avatar
Clément Fumex committed
176 177
  let ses,use_shapes = Session_itp.load_session dir in
  eprintf "using shapes: %a@." pp_print_bool use_shapes;
Clément Fumex's avatar
Clément Fumex committed
178
  (* create the controller *)
179
  let c = Controller_itp.create_controller env ses in
Clément Fumex's avatar
Clément Fumex committed
180
  (* update the session *)
Clément Fumex's avatar
Clément Fumex committed
181
  C.reload_files c env ~use_shapes;
182
  (* add files to controller *)
183
  Queue.iter (fun fname -> C.add_file c fname) files;
184
  (* load provers drivers *)
185 186
  Whyconf.Mprover.iter
    (fun _ p ->
187 188 189 190 191 192 193 194 195 196 197
       try
         let d = Driver.load_driver env p.Whyconf.driver [] in
         Whyconf.Hprover.add c.Controller_itp.controller_provers p.Whyconf.prover (p,d)
       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
           Exn_printer.exn_printer e)
    provers;
  (* return the controller *)
  c
198

199 200 201
let cont = cont_init ()

(* --  -- *)
202

203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
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
228

229
let sort_pair (x,_) (y,_) = String.compare x y
230

231 232 233 234 235 236 237 238 239 240
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)

241 242
open Controller_itp
open Session_itp
243

244 245
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
246

247 248 249 250 251
type proof_hole =
    Th of theory list * theory * theory list |
    Pn of proofNodeID list * proofNodeID * proofNodeID list |
    Tn of transID list * transID * transID list

252
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
253

254
let ctxt = Stack.create ()
255 256 257 258 259

let zipper =
  let files =
    get_files cont.Controller_itp.controller_session
  in
260 261 262
  let file = ref None in
  Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
  let file = Opt.get !file in
263 264
  match file.file_theories with
  | th :: tail -> { cursor = (Th ([], th, tail)); ctxt }
265 266
  | _ -> assert false

267 268 269 270 271 272 273 274 275
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));
276
      while not (Stack.is_empty zipper.ctxt) do ignore (Stack.pop zipper.ctxt) done
277 278
  | _ -> assert false

279 280 281 282 283
let zipper_down () =
  match zipper.cursor with
  | Th (_,th,_) ->
    (match theory_goals th with
    | pn::l ->
284
      Stack.push zipper.cursor zipper.ctxt;
285 286 287 288 289 290
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)
  | Pn (_,pn,_) ->
    (match get_transformations cont.controller_session pn with
    | tn::l ->
291
      Stack.push zipper.cursor zipper.ctxt;
292 293 294 295 296 297
      zipper.cursor <- Tn ([],tn,l);
      true
    | _ -> false)
  | Tn (_,tn,_) ->
    (match get_sub_tasks cont.controller_session tn with
    | pn::l ->
298
      Stack.push zipper.cursor zipper.ctxt;
299 300 301 302 303
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)

let zipper_up () =
304 305
  if not (Stack.is_empty zipper.ctxt) then begin
    zipper.cursor <- Stack.pop zipper.ctxt;
306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
    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

336 337 338
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)

339 340 341 342 343
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 ())

344
let prev_node () = zipper_left () || zipper_up ()
345

346 347 348 349
(* This function try to reach a goal from the current position using
   the move function *)
let rec move_to_goal move =
  if move () then
350 351
    match zipper.cursor with
    | Pn (_,pn,_) -> Some pn
352
    | _  -> move_to_goal move
353 354 355
  else
    None

356
let move_to_goal_ret move =
357
  match
358
    (match move_to_goal move with
Sylvain Dailler's avatar
Sylvain Dailler committed
359
    | None -> Printf.printf "No more goal right; back to root@.";
360
	zipper_init(); move_to_goal next_node
361 362 363 364
    | Some id -> Some id) with
  | None -> failwith "After initialization there is no goal to go to@."
  | Some id -> id

365 366
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)

367 368
(* The cursor of the zipper is on a goal *)
let is_goal_cursor () =
369
  match zipper.cursor with
370 371 372 373 374
  | Pn (_, pn, _) -> Some pn
  | _ -> None

(* If on goal, do nothing else go to next_goal *)
let nearest_goal () =
375 376
  match is_goal_cursor () with
  | None -> move_to_goal_ret next_node
377
  | Some id -> id
378

379 380 381 382
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

let print_proof_attempt fmt pa =
Clément Fumex's avatar
Clément Fumex committed
383
  fprintf fmt "%a tl=%d %a obsolete=%a"
384 385 386
          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
387
          pp_print_bool pa.proof_obsolete
388 389 390 391

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
392
  | Trans id -> get_transf_name s id
393 394 395 396 397 398 399 400
  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
401
  if Controller_itp.pn_proved cont p then
402
    fprintf fmt "P";
403 404

  fprintf fmt
MARCHE Claude's avatar
MARCHE Claude committed
405
    "@[<hv 2>{ Goal=%s;@ parent=%s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@] }@]"
406 407 408 409 410 411
    (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
412
    fprintf fmt " **"
413 414

and print_trans_node s fmt id =
415 416
  let name = get_transf_name s id in
  let args = get_transf_args s id in
417
  let l = get_sub_tasks s id in
Clément Fumex's avatar
Clément Fumex committed
418
  let ll = get_detached_sub_tasks s id in
419
  let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
Clément Fumex's avatar
Clément Fumex committed
420 421
  if Controller_itp.tn_proved cont id then
    fprintf fmt "P";
Clément Fumex's avatar
Clément Fumex committed
422 423
  fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a];@ detached[%a] }@]" name
    (Pp.print_list Pp.semi pp_print_string) args parent
424
    (Pp.print_list Pp.semi (print_proof_node s)) l
Clément Fumex's avatar
Clément Fumex committed
425
    (Pp.print_list Pp.semi (print_proof_node s)) ll
426 427

let print_theory s fmt th : unit =
428
  if Controller_itp.th_proved cont th then
Clément Fumex's avatar
Clément Fumex committed
429
    fprintf fmt "P";
Clément Fumex's avatar
Clément Fumex committed
430 431 432
  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)
433

Clément Fumex's avatar
Clément Fumex committed
434 435
let print_file s fmt (file, thl, detached) =
  fprintf fmt "@[<hv 1> File %s;@ [%a];@ detached[%a]@]" file.file_name
436
    (Pp.print_list Pp.semi (print_theory s)) thl
Clément Fumex's avatar
Clément Fumex committed
437
    (Pp.print_list Pp.semi (print_theory s)) detached
438 439 440 441 442

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
443 444 445
  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;;
446 447 448 449

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

450 451
let display_session fmt _args =
  fprintf fmt "%a@." Controller_itp.print_session cont
452 453 454 455 456 457 458 459 460

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
461 462 463 464 465 466
let task_driver =
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver env d []

467 468 469 470 471 472
(* 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
473 474
          (*Pretty.print_task*)
          (Driver.print_task ~cntexample:false task_driver)
475 476 477 478 479 480 481
          task

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

482 483 484
(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)

485
let test_schedule_proof_attempt fmt (args: string list) =
486
  (* temporary : get the first goal *)
487 488 489
  let id = nearest_goal () in
  let callback status =
    match status with
490
    | Done _prover_result -> (display_session fmt []; test_print_goal fmt [];
491 492 493 494 495 496 497 498 499
                              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
500 501 502 503
      let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
                                        limit_mem = Whyconf.memlimit main;
                                        limit_steps = 0} in
      name, default_limit
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
  | [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@."*)
521

Sylvain Dailler's avatar
Sylvain Dailler committed
522
let apply_transform fmt args =
523
  match args with
Sylvain Dailler's avatar
Sylvain Dailler committed
524
    | tr :: tl ->
525 526 527 528 529
       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
530 531
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."
MARCHE Claude's avatar
MARCHE Claude committed
532 533 534

(*******)

Clément Fumex's avatar
Clément Fumex committed
535 536
let test_save_session _fmt _args =
  Session_itp.save_session cont.Controller_itp.controller_session
537 538 539

let test_reload fmt _args =
  fprintf fmt "Reloading... @?";
Clément Fumex's avatar
Clément Fumex committed
540 541
  (* use_shapes is true since session is in memory *)
  C.reload_files cont env ~use_shapes:true;
542
  zipper_init ();
543
  fprintf fmt "done @."
544

545 546 547 548 549 550
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
551 552 553 554 555 556 557 558
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
559
         | TSdone _tid -> (ignore (move_to_goal_ret next_node);
560
             display_session fmt []; test_print_goal fmt [])
Sylvain Dailler's avatar
Sylvain Dailler committed
561 562 563 564 565
         | _ -> ()
       in
       C.schedule_transformation cont id tr tl ~callback
    | _ -> printf "Error: Give the name of the transformation@."

MARCHE Claude's avatar
MARCHE Claude committed
566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598

(***************** 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
MARCHE Claude's avatar
MARCHE Claude committed
599
  let pp_strat fmt (n,s,desc,_) = fprintf fmt "%s (%s): %s" s n desc in
MARCHE Claude's avatar
MARCHE Claude committed
600 601 602
  printf "@[<hov 2>== Known strategies ==@\n%a@]@."
          (Pp.print_list Pp.newline pp_strat) l

MARCHE Claude's avatar
MARCHE Claude committed
603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620
let run_strategy _fmt args =
  match args with
  | [s] ->
     let l = strategies () in
     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
621
(*******)
MARCHE Claude's avatar
MARCHE Claude committed
622 623


624 625 626 627 628 629 630 631 632
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

633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655
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"
656

657
(****)
658

659 660
let commands =
  [
661
    "k", "list known identifiers", print_known_map;
662 663
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
MARCHE Claude's avatar
MARCHE Claude committed
664
    "list-strategies", "list available strategies", list_strategies;
Sylvain Dailler's avatar
Sylvain Dailler committed
665
    "a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
MARCHE Claude's avatar
MARCHE Claude committed
666
    "t", "<transname> <args>: behave like 'a' but add function to display into the callback", test_transform_and_display;
667 668
    "pr", "print the session in raw form", dump_session_raw;
    "p", "print the session", display_session;
MARCHE Claude's avatar
MARCHE Claude committed
669 670
    "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;
671
    "print", "<s> print the declaration where s was defined", test_print_id;
MARCHE Claude's avatar
MARCHE Claude committed
672
    "g", "prints the current goal", test_print_goal;
673
    "r", "reload the session (test only)", test_reload;
674
    "rp", "replay", test_replay;
Clément Fumex's avatar
Clément Fumex committed
675
    "s", "save the current session", test_save_session;
MARCHE Claude's avatar
MARCHE Claude committed
676 677 678 679 680 681
    "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);
682
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
683 684 685 686 687 688 689 690 691 692
    "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);
693 694 695
    "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
696
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712
  ]

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 "@."
713 714


715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738
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
739
    | a::b -> a,b
740 741 742 743
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
744
  match cmd with
745 746 747 748 749 750
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
Clément Fumex's avatar
Clément Fumex committed
751 752 753 754 755 756 757 758 759
      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
760 761

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