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


module Unix_scheduler = struct

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

MARCHE Claude's avatar
MARCHE Claude committed
9 10
    (* [insert_idle_handler p f] inserts [f] as a new function to call
       on idle, with priority [p] *)
MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14 15 16 17 18 19
    let insert_idle_handler p f =
      let rec aux l =
        match l with
          | [] -> [p,f]
          | (p1,_) as hd :: rem ->
             if p > p1 then (p,f) :: l else hd :: aux rem
      in
      idle_handler := aux !idle_handler

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

MARCHE Claude's avatar
MARCHE Claude committed
24 25
    (* [insert_timeout_handler ms t f] inserts [f] as a new function to call
       on timeout, with time step of [ms] and first call time as [t] *)
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29 30 31 32 33 34
    let insert_timeout_handler ms t f =
      let rec aux l =
        match l with
          | [] -> [ms,t,f]
          | (_,t1,_) as hd :: rem ->
             if t < t1 then (ms,t,f) :: l else hd :: aux rem
      in
      timeout_handler := aux !timeout_handler

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
51 52 53
     (* [main_loop interp] starts the scheduler. On idle, standard input is
        read.  When a complete line is read from stdin, it is passed
        as a string to the function [interp] *)
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
     let main_loop interp =
       try
         while true do
57 58 59 60
           if !show_prompt then begin
               Format.printf "%s@?" !prompt;
               show_prompt := false;
             end;
MARCHE Claude's avatar
MARCHE Claude committed
61 62 63
           (* attempt to run the first timeout handler *)
           let time = Unix.gettimeofday () in
           match !timeout_handler with
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
           | (ms,t,f) :: rem when t <= time ->
              timeout_handler := rem;
              let b = f () in
              let time = Unix.gettimeofday () in
              if b then insert_timeout_handler ms (ms +. time) f
           | _ ->
              (* time is not yet passed *)
              (* attempt to run the first idle handler *)
              match !idle_handler with
              | (p,f) :: rem ->
                 idle_handler := rem;
                 let b = f () in
                 if b then insert_idle_handler p f
              | [] ->
                 (* no idle handler *)
                 (* check stdin for a some delay *)
                 let delay =
                   match !timeout_handler with
                   | [] -> 0.125
                   (* 1/8 second by default *)
                   | (_,t,_) :: _ -> t -. time
                   (* or the time left until the next timeout otherwise *)
                 in
                 let a,_,_ = Unix.select [Unix.stdin] [] [] delay in
                 match a with
89 90 91 92
                 | [_] ->
                    let n = Unix.read Unix.stdin buf 0 256 in
                    interp (Bytes.sub_string buf 0 (n-1));
                    show_prompt := true
MARCHE Claude's avatar
MARCHE Claude committed
93 94
                 | [] -> () (* nothing read *)
                 | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98 99 100 101
         done
       with Exit -> ()

end



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

106 107 108
open Why3
open Format

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

let spec = Arg.align [
]

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

118 119

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

122 123 124 125 126 127 128 129
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)

130 131 132 133

module C = Why3.Controller_itp.Make(Unix_scheduler)

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

149
(* loading the drivers *)
150 151 152
let () =
  Whyconf.Mprover.iter
    (fun _ p ->
153 154
      try
        let d = Driver.load_driver env p.Whyconf.driver [] in
155
        Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
156 157 158 159
      with e ->
        let p = p.Whyconf.prover in
        eprintf "Failed to load driver for %s %s: %a@."
          p.Whyconf.prover_name p.Whyconf.prover_version
160
          Exn_printer.exn_printer e)
161 162 163 164 165 166 167 168 169 170 171 172 173
    provers

(* One prover named Alt-Ergo in the config file *)
let alt_ergo =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
  (** all provers that have the name "Alt-Ergo" *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
    eprintf "Prover Alt-Ergo not installed or not configured@.";
    exit 0
  end else
    snd (Whyconf.Mprover.choose provers)

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

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

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

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

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

212 213
open Controller_itp
open Session_itp
214 215
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
216 217 218 219 220 221 222 223 224 225 226 227 228
type proof_hole =
    Th of theory list * theory * theory list |
    Pn of proofNodeID list * proofNodeID * proofNodeID list |
    Tn of transID list * transID * transID list

type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Queue.t }

let ctxt = Queue.create ()

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

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


249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 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 298 299 300 301 302 303 304 305
let zipper_down () =
  match zipper.cursor with
  | Th (_,th,_) ->
    (match theory_goals th with
    | pn::l ->
      Queue.add zipper.cursor zipper.ctxt;
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)
  | Pn (_,pn,_) ->
    (match get_transformations cont.controller_session pn with
    | tn::l ->
      Queue.add zipper.cursor zipper.ctxt;
      zipper.cursor <- Tn ([],tn,l);
      true
    | _ -> false)
  | Tn (_,tn,_) ->
    (match get_sub_tasks cont.controller_session tn with
    | pn::l ->
      Queue.add zipper.cursor zipper.ctxt;
      zipper.cursor <- Pn ([],pn,l);
      true
    | _ -> false)

let zipper_up () =
  if not (Queue.is_empty zipper.ctxt) then begin
    zipper.cursor <- Queue.pop zipper.ctxt;
    true
  end else
    false

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

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

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

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

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

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

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

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

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

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

349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

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

let rec print_proof_node s (fmt: Format.formatter) p =
  let parent = match get_proof_parent s p with
  | Theory t -> (theory_name t).Ident.id_string
  | Trans id -> get_transformation_name s id
  in
  let current_goal =
    match is_goal_cursor () with
    | Some pn -> pn = p
    | _ -> false
  in
  if current_goal then
    fprintf fmt "**";

  fprintf fmt
    "@[<hv 2> Goal %s;@ parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
    (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
    fprintf fmt "**"

and print_trans_node s fmt id =
  let name = get_transformation_name s id in
  let l = get_sub_tasks s id in
  let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
  fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent
    (Pp.print_list Pp.semi (print_proof_node s)) l

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

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

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

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

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


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

let print_position_p s cursor fmt _ = print_position s cursor fmt

(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)

418 419
let test_schedule_proof_attempt fmt _args =
  (* temporary : get the first goal *)
420
  let id = nearest_goal () in
421 422 423 424
  let callback status =
    fprintf fmt "status: %a@."
            Controller_itp.print_status status
  in
MARCHE Claude's avatar
MARCHE Claude committed
425
  let limit = Call_provers.{empty_limit with limit_time = 2} in
426 427 428 429
  C.schedule_proof_attempt
    cont id alt_ergo.Whyconf.prover
    ~limit ~callback

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
let apply_transform_no_args fmt args =
  match args with
    | [s] ->
       let id = nearest_goal () in
       let callback status =
         fprintf fmt "transformation status: %a@."
                 Controller_itp.print_trans_status status
       in
       begin
         try
           C.schedule_transformation cont id s [] ~callback
         with
           e when not (Debug.test_flag Debug.stack_trace) ->
           printf "Error: %a@." Exn_printer.exn_printer e
       end
    | _ -> printf "Error: exactly one argument expected@."
446

447 448 449 450 451 452 453
let test_transformation_with_args fmt args =
  (* temporary : apply duplicate on the first goal *)
  let id = nearest_goal () in
  let callback status =
    fprintf fmt "transformation status: %a@."
            Controller_itp.print_trans_status status
  in
454
  C.schedule_transformation cont id "duplicate" args ~callback
455

MARCHE Claude's avatar
MARCHE Claude committed
456 457 458
(* Do not use this. TODO
   Claude: indeed type_fmla and type_term should never be used like this
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
459 460 461 462
let typing_terms t th =
  try (Typing.type_fmla th (fun _ -> None) t) with
  | _ -> Typing.type_term th (fun _ -> None) t

463
(*
464 465 466 467
let parse_transformation_arg args : Term.term option =
  (* temporary : parses the term *)
  match args with
  | [s] ->
MARCHE Claude's avatar
itp  
MARCHE Claude committed
468
     printf "parsing string '%s'@." s;
469 470 471 472 473 474 475 476
     begin try
         let lb = Lexing.from_string s in
         let t = Lexer.parse_term lb in
         printf "parsing OK@.";
         let env = cont.controller_env in
         let th = Theory.create_theory (Ident.id_fresh "dummy") in
         let int_theory = Env.read_theory env ["int"] "Int" in
         let th = Theory.use_export th int_theory in
Sylvain Dailler's avatar
Sylvain Dailler committed
477
         let t = typing_terms t th in
478 479 480 481 482 483 484
         let _ = printf "typing OK: %a@." Pretty.print_term t in
         Some t
       with e ->
         let _ = printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e in
         None
     end
  | _ -> let _ = printf "term argument expected@." in None
485
 *)
486

487

488
(*
489 490 491 492 493 494 495 496 497 498 499 500 501
let parse_transformation_string args : string option =
  (* temporary : parses a string *)
  match args with
  | [s] ->
     let s =
       let l = String.length s in
       if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
         String.sub s 1 (l - 2)
       else s
     in
     printf "parsing string \"%s\"@." s;
     Some s
  | _ -> let _ = printf "term argument expected@." in None
502
 *)
503

Sylvain Dailler's avatar
Sylvain Dailler committed
504 505
let test_simple_apply fmt args =
  (* temporary : parses a string *)
506
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531
  match args with
  | [s';s] ->
     let s =
       let l = String.length s in
       if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
         String.sub s 1 (l - 2)
       else s
     in
     let s' =
       let l = String.length s' in
       if l >= 2 && s'.[0] = '"' && s'.[l - 1] = '"' then
         String.sub s' 1 (l - 2)
       else s'
     in
     printf "parsing string \"%s\"@." s;
     begin try
       let lb = Lexing.from_string s in
       let t = Lexer.parse_term lb in
       printf "parsing OK@.";
       let env = cont.controller_env in
       let th = Theory.create_theory (Ident.id_fresh "dummy") in
       let int_theory = Env.read_theory env ["int"] "Int" in
       let th = Theory.use_export th int_theory in
       let t = typing_terms t th in
       let _ = printf "typing OK: %a@." Pretty.print_term t in
532 533
 *)
     let id = nearest_goal () in
Sylvain Dailler's avatar
Sylvain Dailler committed
534 535 536 537
     let callback status =
       fprintf fmt "transformation status: %a@."
         Controller_itp.print_trans_status status
     in
538 539
     C.schedule_transformation cont id "simple_apply" args ~callback
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
540 541 542 543 544
     with e ->
       let _ = printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e in
       ()
     end
  | _ -> let _ = printf "term argument expected@." in ()
545
 *)
546

547
let test_apply_with_string_args fmt args =
548
(*
549 550 551
  match (parse_transformation_string args) with
  | None -> ()
  | Some s ->
552
 *)
553 554 555 556 557
      let id = nearest_goal () in
      let callback status =
        fprintf fmt "transformation status: %a@."
          Controller_itp.print_trans_status status
      in
558
      C.schedule_transformation cont id "apply" args ~callback
559

560
let test_remove_with_string_args fmt args =
561
(*
562 563 564
  match (parse_transformation_string args) with
  | None -> ()
  | Some s ->
565
 *)
566 567 568 569 570
      let id = nearest_goal () in
      let callback status =
        fprintf fmt "transformation status: %a@."
          Controller_itp.print_trans_status status
      in
571
      C.schedule_transformation cont id "remove" args ~callback
572

MARCHE Claude's avatar
MARCHE Claude committed
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 599 600 601 602 603 604 605 606 607 608 609 610 611

(*** term argument parsed in the context of the task ***)

let type_ptree ~as_fmla t task =
  let used_ths = Task.used_theories task in
  let used_symbs = Task.used_symbols used_ths in
  let local_decls = Task.local_decls task used_symbs in
  (* rebuild a theory_uc *)
  let th_uc = Theory.create_theory (Ident.id_fresh "dummy") in
  let th_uc =
    Ident.Mid.fold
      (fun _id th acc -> Theory.use_export acc th)
      used_ths th_uc
  in
  let th_uc =
    List.fold_left
      (fun acc d -> Theory.add_decl ~warn:false acc d)
      th_uc local_decls
  in
  if as_fmla
  then Typing.type_fmla th_uc (fun _ -> None) t
  else Typing.type_term th_uc (fun _ -> None) t

let parse_arg_only s task =
  let lb = Lexing.from_string s in
  let t =
    (* try *)
      Lexer.parse_term lb
    (* with _ -> failwith "parsing error" *)
  in
  let t =
    (* try *)
      type_ptree ~as_fmla:false t task
    (* with *)
  in
  eprintf "transformation parse_arg_only succeeds: %a@." Pretty.print_term t;
  [task]

let () = Trans.(register_transform_with_args
612
           "parse_arg_only" Args_wrapper.(wrap (Tstring Ttrans) parse_arg_only)
MARCHE Claude's avatar
MARCHE Claude committed
613 614 615
           ~desc:"Just parse and type the string argument")

let test_transformation_with_string_parsed_later fmt args =
616
(*
MARCHE Claude's avatar
MARCHE Claude committed
617 618
  match args with
    | [s] ->
619
 *)
MARCHE Claude's avatar
MARCHE Claude committed
620 621 622 623 624
       let id = nearest_goal () in
       let callback status =
         fprintf fmt "transformation status: %a@."
                 Controller_itp.print_trans_status status
       in
625 626
       C.schedule_transformation cont id "parse_arg_only" args ~callback
(*
627
    | _ ->  printf "string argument expected@."
628
 *)
MARCHE Claude's avatar
MARCHE Claude committed
629 630 631 632 633


(*******)


634
(* Only parses arguments and print debugging information *)
635
(*
636 637
let test_transformation_with_term_arg _fmt args =
  let _ = parse_transformation_arg args in ()
638
 *)
639 640

let test_case_with_term_args fmt args =
641
(*
642 643 644
  match (parse_transformation_arg args) with
  | None -> ()
  | Some t ->
645
 *)
646 647 648 649 650
  let id = nearest_goal () in
  let callback status =
    fprintf fmt "transformation status: %a@."
            Controller_itp.print_trans_status status
  in
651
  C.schedule_transformation cont id "case" args ~callback
652

Sylvain Dailler's avatar
Sylvain Dailler committed
653 654 655 656 657 658 659 660 661 662 663

(* TODO rewrite this. Only for testing *)
let test_transformation_one_arg_term fmt args =
  match args with
  | [] -> printf "Give the name of the transformation@."
  | tr :: tl ->
      let id = nearest_goal () in
      let callback status =
        fprintf fmt "transformation %s status: %a@."
          tr Controller_itp.print_trans_status status
      in
664
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
665 666 667
      match (parse_transformation_arg tl) with
      | None -> ()
      | Some t ->
668 669 670
 *)
          C.schedule_transformation cont id tr tl ~callback

Sylvain Dailler's avatar
Sylvain Dailler committed
671

672 673 674 675 676
let task_driver =
  let d = Filename.concat (Whyconf.datadir main)
                          (Filename.concat "drivers" "why3_itp.drv")
  in
  Driver.load_driver env d []
677

678
(* Print current goal or nearest next goal if we are not on a goal *)
679 680
let test_print_goal fmt _args =
  (* temporary : get the first goal *)
681
  let id = nearest_goal () in
682
  let task = Session_itp.get_task cont.Controller_itp.controller_session id in
683
  fprintf fmt "@[====================== Task =====================@\n%a@]@."
684 685 686 687 688 689 690 691 692
    (Driver.print_task ~cntexample:false task_driver) task

let test_save_session _fmt args =
  match args with
  | file :: _ ->
    Session_itp.save_session (file ^ ".xml") cont.Controller_itp.controller_session;
    printf "session saved@."
  | [] ->
    printf "missing session file name@."
693 694 695 696 697

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

699 700 701 702 703 704
let commands =
  [
    "list-provers", "list available provers", list_provers;
    "list-transforms", "list available transformations", list_transforms;
    (* temporary *)
    "i", "run a simple test of Unix_scheduler.idle", test_idle;
705
(*
706
    "a", "run a simple test of Unix_scheduler.timeout", test_timeout;
707 708
 *)
    "a", "<transname>: apply the transformation <transname> with no argument", apply_transform_no_args;
709
    "p", "print the session in raw form", dump_session_raw;
710
    "t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
711
    "c", "case on next goal", test_case_with_term_args;
712
    "g", "prints the first goal", test_print_goal;
713
    "r", "reload the session (test only)", test_reload;
714
    "rem", "test remove transformation. Take one string argument", test_remove_with_string_args;
715
    "app", "test apply transformation. Take one string argument", test_apply_with_string_args;
716
    "s", "[s my_session] save the current session in my_session.xml", test_save_session;
717
(*
718
    "tr", "test schedule_transformation with split_goal on the current or next right goal (or on the top goal if there is none", test_transformation;
719
 *)
Sylvain Dailler's avatar
Sylvain Dailler committed
720
    "ttr", "takes 2 arguments. Name of the transformation (with one term argument) and a term" , test_transformation_one_arg_term;
721
    "tra", "test duplicate transformation", test_transformation_with_args;
722 723 724 725 726 727
    "ng", "get to the next goal", move_to_goal_ret_p next_node;
    "pg", "get to the prev goal", move_to_goal_ret_p prev_node;
    "gu", "get to the goal up",  move_to_goal_ret_p zipper_up;
    "gd", "get to the goal up",  move_to_goal_ret_p zipper_down;
    "gr", "get to the goal up",  move_to_goal_ret_p zipper_right;
    "gl", "get to the goal up",  move_to_goal_ret_p zipper_left;
728
    "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
MARCHE Claude's avatar
MARCHE Claude committed
729
    "tt", "test a transformation having a term as argument", test_transformation_with_string_parsed_later;
730 731 732
    "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
733 734
    "zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()));
    "sa", "test simple_apply", test_simple_apply
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
  ]

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 "@."
751 752


753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
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
777
    | a::b -> a,b
778 779 780 781
    | [] -> "",[]

let interp chout fmt s =
  let cmd,args = split_args s in
782
  match cmd with
783 784 785 786 787 788 789 790 791 792
    | "?" -> help ()
    | "q" ->
       fprintf fmt "Shell exited@.";
       close_out chout;
       exit 0
    | _ ->
       try
         let f = Stdlib.Hstr.find commands_table cmd in
         f fmt args
       with Not_found ->
793
         printf "unknown command '%s'@." cmd
794

MARCHE Claude's avatar
MARCHE Claude committed
795 796

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