Commit a4ce60da authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Tried to make something usable for PG.

parent a723970c
(* TODO *)
let proof_general = true
module Unix_scheduler = struct
......@@ -45,7 +47,7 @@ module Unix_scheduler = struct
(* buffer for storing character read on stdin *)
let buf = Bytes.create 256
let show_prompt = ref true
let show_prompt = ref 0
let prompt = ref "> "
(* [main_loop interp] starts the scheduler. On idle, standard input is
......@@ -54,12 +56,13 @@ module Unix_scheduler = struct
let main_loop interp =
try
while true do
if !show_prompt then begin
Format.printf "%s@?" !prompt;
show_prompt := false;
end;
show_prompt := !show_prompt + 1;
if !show_prompt = 2 then begin
Format.printf "%s@?" !prompt;
show_prompt := 0;
end;
(* attempt to run the first timeout handler *)
let time = Unix.gettimeofday () in
(let time = Unix.gettimeofday () in
match !timeout_handler with
| (ms,t,f) :: rem when t <= time ->
timeout_handler := rem;
......@@ -89,9 +92,9 @@ module Unix_scheduler = struct
| [_] ->
let n = Unix.read Unix.stdin buf 0 256 in
interp (Bytes.sub_string buf 0 (n-1));
show_prompt := true
show_prompt := 0
| [] -> () (* nothing read *)
| _ -> assert false
| _ -> assert false);
done
with Exit -> ()
......@@ -490,7 +493,7 @@ let test_transform_and_display fmt args =
Controller_itp.print_trans_status status;
match status with
| TSdone _tid -> (ignore (move_to_goal_ret next_node);
test_print_goal fmt [])
dump_session_raw fmt []; test_print_goal fmt [])
| _ -> ()
in
C.schedule_transformation cont id tr tl ~callback
......@@ -649,5 +652,5 @@ let interp chout fmt s =
let () =
printf "Welcome to Why3 shell. Type '?' for help.@.";
let chout = open_out "why3shell.out" in
let fmt = formatter_of_out_channel chout in
let fmt = if proof_general then formatter_of_out_channel stdout else formatter_of_out_channel chout in
Unix_scheduler.main_loop (interp chout fmt)
b introduce_premises
(* print goal with premisses introduced *)
b cut "exists x: int. x = x"
(* print goal with h in context *)
b exists "5"
(* print new goal G1 with (x = (2 * 5)) *)
b case "exists x. exists y. x + y = y - x"
(* print the goal with the hypothesis in context *)
pg
(* return to context with positive exists *)
b cut "exists x. exists y. x + y = 0"
ng
(* Have to prove h1 with 2 exists *)
b exists "4"
(* Instantiate x1 *)
b cut "forall x. forall y. x + y = 0"
(* print with h2 in context *)
b instantiate "h2" "4"
(* create h21 which is correct *)
b exists "3"
(* instantiate y in the goal *)
b cut "forall y. true -> 4 + y = 0"
(* generate h3 *)
b apply h2
(* apply h2 to the goal and generate the new goal*)
gu
(* go back to the 4 + 3 = 0 goal *)
b cut "forall y. y = 5 -> 4 + y = 0"
(* new hypothesis to apply *)
b apply h3
(* apply hypothesis and generate the goal 3 = 5 which is correct. *)
b remove h2
(* remove correct hypothesis h2 *)
b remove CompatOrderMult
(* Success *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment