Commit 5f75a67d authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

slight change to how sk and fk are used

parent 69bdaee1
......@@ -114,9 +114,6 @@ let unary_string state rule (l_index : string) =
(parse_int_list l_index (Formula.length state.c_proof.goal)))
exception Proof_done
exception Proof_failed
let binary_aux state rule l_prem r_prem sk sk' fk =
let binary_build proof rule l_prem r_prem =
......@@ -138,13 +135,8 @@ let binary_aux state rule l_prem r_prem sk sk' fk =
let l_state = { state with c_proof = l_proof }
and r_state = new_state state.param r_proof in
try
let state' = sk l_state fk in
state'.error_message ();
assert false
with
| Proof_done -> sk' r_state fk
| Proof_failed -> fk ()
ignore(sk l_state fk);
sk' r_state fk
let binding_aux state y =
......@@ -605,7 +597,7 @@ let simplify ?collect:(c=false) state =
(* pre_treatment state : Apply a pre treatment to the current formula. To be
called once per new goal. *)
let pre_treatment state =
let pre_treatment state sk fk =
let auto_ift_if_root state =
if state.c_proof.back_track = Root then
......@@ -625,9 +617,9 @@ let pre_treatment state =
if bool_res then
let _ = state.c_proof.premises <- PAxiom CCA in
raise Proof_done
state
else
state)
sk state fk)
(*****************)
......@@ -1476,11 +1468,8 @@ add_c_action
state.c_proof.goal <- { state.c_proof.goal with env = env' };
binary_aux state rule l_prem r_prem sk
(fun state' fk' ->
let state'' = pre_treatment state' in
sk state'' fk')
fk
binary_aux state rule l_prem r_prem
sk (fun state' _ -> pre_treatment state' sk fk) fk
| l, Some _ ->
let error_message =
......@@ -1637,7 +1626,7 @@ add_c_action
default_exn_handler
(fun y state sk fk ->
raise Proof_done
state
);;
......@@ -1654,17 +1643,17 @@ add_c_action
(fun y state sk fk -> fk () );;
let try_cca state =
let try_cca state sk fk =
let (state,bool_res) =
apply_unitary_and_set_feedback ~print:true CCA state in
if bool_res then
begin
state.c_proof.premises <- PAxiom CCA;
raise Proof_done
state
end
else
state;;
sk state fk;;
add_c_action
"cca2"
......@@ -1691,10 +1680,10 @@ add_c_action
simplify state in
if y = "guard" then
tact_andthen auto_guard (tact_wrap try_cca) sk fk state
tact_andthen auto_guard try_cca sk fk state
else
(tact_wrap try_cca) state sk fk
try_cca state sk fk
);;
......@@ -1745,6 +1734,8 @@ let rec exec_cmd_list l state sk fk = match l with
(exec_cmd_list tail)
sk fk c
exception Proof_failed
let rec interactive_loop state sk fk =
let state' = simplify state
......@@ -1766,9 +1757,10 @@ let rec interactive_loop state sk fk =
(* We insert a back_track point here. *)
exec_cmd_list input_commands state''
(fun state fk' ->
interactive_loop state sk fk')
(fun () -> interactive_loop state sk fk)
(fun n_state _ ->
interactive_loop n_state
sk (fun () -> interactive_loop state sk fk))
fk
let rec interactive_proof state_list = match state_list with
......@@ -1778,16 +1770,19 @@ let rec interactive_proof state_list = match state_list with
let init_state =
apply_unitary_and_set_feedback ~print:true CCA state
|> fst
|> new_screen
|> pre_treatment in
|> new_screen in
let final_sk (_,b) _ =
let final_sk _ _ =
assert false in
let rec bad_backtrack () =
interactive_loop init_state final_sk bad_backtrack in
ignore(interactive_loop init_state final_sk bad_backtrack)
ignore(tact_andthen
pre_treatment
interactive_loop
final_sk bad_backtrack
init_state);
interactive_proof tail
with
| Proof_done -> interactive_proof tail
| Proof_failed -> Printf.printf "Incorrect proof.\n%!"; raise Proof_failed
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