Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

why3shell.ml 22.5 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
open Why3
Sylvain Dailler's avatar
Sylvain Dailler committed
114
open Session_user_interface
115 116
open Format

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

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

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

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

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

139 140
(* -- declare provers -- *)

141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
(* 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))

156
(* -- init controller -- *)
157

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

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

163
let () = C.set_max_tasks (Whyconf.running_provers_max main)
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 190 191
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
192

193
let sort_pair (x,_) (y,_) = String.compare x y
194

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

205 206
open Controller_itp
open Session_itp
207

208 209
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
210

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

216
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
217

218
let ctxt = Stack.create ()
219 220 221 222 223

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

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

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

let zipper_up () =
268 269
  if not (Stack.is_empty zipper.ctxt) then begin
    zipper.cursor <- Stack.pop zipper.ctxt;
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 298 299
    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

300 301 302
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)

303 304 305 306 307
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 ())

308
let prev_node () = zipper_left () || zipper_up ()
309

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

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

329 330
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)

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

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

343 344 345 346
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

let print_proof_attempt fmt pa =
Clément Fumex's avatar
Clément Fumex committed
347
  fprintf fmt "%a tl=%d %a obsolete=%a"
348 349 350
          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
351
          pp_print_bool pa.proof_obsolete
352 353 354 355

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

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

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

let print_theory s fmt th : unit =
392
  if Controller_itp.th_proved cont th then
Clément Fumex's avatar
Clément Fumex committed
393
    fprintf fmt "P";
Clément Fumex's avatar
Clément Fumex committed
394 395 396
  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)
397

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

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
407 408 409
  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;;
410 411 412 413

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

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

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
let test_schedule_proof_attempt fmt (args: string list) =
450
  (* temporary : get the first goal *)
451
  let id = nearest_goal () in
452
  let callback _panid status =
453
    match status with
454
    | Done _prover_result -> (display_session fmt []; test_print_goal fmt [];
455 456 457 458 459 460 461 462 463
                              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
464 465 466 467
      let default_limit = Call_provers.{limit_time = Whyconf.timelimit main;
                                        limit_mem = Whyconf.memlimit main;
                                        limit_steps = 0} in
      name, default_limit
468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484
  | [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@."*)
485

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

(*******)

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
530 531

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

MARCHE Claude's avatar
MARCHE Claude committed
539 540 541
let run_strategy _fmt args =
  match args with
  | [s] ->
542 543 544
     let l = Session_user_interface.strategies
            cont.Controller_itp.controller_env config
     in
MARCHE Claude's avatar
MARCHE Claude committed
545 546 547 548 549 550 551 552 553
     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
MARCHE Claude's avatar
MARCHE Claude committed
554 555 556
          let callback_pa _panid _st = () in
          let callback_tr _tr = () in
          C.run_strategy_on_goal cont id st ~callback_pa ~callback_tr ~callback
MARCHE Claude's avatar
MARCHE Claude committed
557 558 559 560
       | _ -> printf "Strategy '%s' not found@." s
     end
  | _ -> printf "Please give the strategy shortcut as argument@."

Sylvain Dailler's avatar
Sylvain Dailler committed
561
(*******)
MARCHE Claude's avatar
MARCHE Claude committed
562 563


564 565 566 567 568 569 570 571 572
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

Sylvain Dailler's avatar
Sylvain Dailler committed
573
let test_print_id _fmt args =
574 575
  let id = nearest_goal () in
  let task = get_task cont.controller_session id in
576
  Format.printf "%s@." (print_id cont task args)
Sylvain Dailler's avatar
Sylvain Dailler committed
577

Sylvain Dailler's avatar
Sylvain Dailler committed
578
let test_search_id _fmt args =
Sylvain Dailler's avatar
Sylvain Dailler committed
579 580
  let id = nearest_goal () in
  let task = get_task cont.controller_session id in
581
  Format.printf "%s@." (search_id cont task args)
Sylvain Dailler's avatar
Sylvain Dailler committed
582

583
(****)
584

585 586
let commands =
  [
587
    "k", "list known identifiers", print_known_map;
588 589
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
MARCHE Claude's avatar
MARCHE Claude committed
590
    "list-strategies", "list available strategies", list_strategies;
Sylvain Dailler's avatar
Sylvain Dailler committed
591
    "a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
MARCHE Claude's avatar
MARCHE Claude committed
592
    "t", "<transname> <args>: behave like 'a' but add function to display into the callback", test_transform_and_display;
593 594
    "pr", "print the session in raw form", dump_session_raw;
    "p", "print the session", display_session;
MARCHE Claude's avatar
MARCHE Claude committed
595 596
    "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;
597
    "print", "<s> print the declaration where s was defined", test_print_id;
Sylvain Dailler's avatar
Sylvain Dailler committed
598
    "search", "<s> print some declarations where s appear", test_search_id;
MARCHE Claude's avatar
MARCHE Claude committed
599
    "g", "prints the current goal", test_print_goal;
600
    "r", "reload the session (test only)", test_reload;
601
    "rp", "replay", test_replay;
Clément Fumex's avatar
Clément Fumex committed
602
    "s", "save the current session", test_save_session;
MARCHE Claude's avatar
MARCHE Claude committed
603 604 605 606 607 608
    "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);
609
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
610 611 612 613 614 615 616 617 618 619
    "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);
620 621 622
    "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
623
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639
  ]

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 "@."
640 641


642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665
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
666
    | a::b -> a,b
667 668 669 670
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
671
  match cmd with
672 673 674 675 676 677
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
Clément Fumex's avatar
Clément Fumex committed
678 679 680 681 682 683 684 685 686
      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
687 688

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