Commit 69bdaee1 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

bug fix: errors in complexe actions were not properly handled (the error was...

bug fix: errors in complexe actions were not properly handled (the error was added to the state, but the function returned instead of called the success continuation)
parent eb496c39
Pipeline #1664 passed with stage
in 1 minute and 31 seconds
......@@ -139,7 +139,8 @@ let binary_aux state rule l_prem r_prem sk sk' fk =
and r_state = new_state state.param r_proof in
try
let _ = sk l_state fk in
let state' = sk l_state fk in
state'.error_message ();
assert false
with
| Proof_done -> sk' r_state fk
......@@ -181,8 +182,9 @@ let new_screen state =
(* Print errors *)
print_separator state.param.shell_mode;
Printf.printf "\n%!";
state.error_message ();
Printf.printf "\n";
let state' = err_reset state in
if state'.l_error_ref <> [] then
......@@ -198,10 +200,6 @@ let new_screen state =
if state'.param.shell_mode then
begin
let (_,h) = ANSITerminal.size () in
let (_,y) = ANSITerminal.pos_cursor () in
if (y + 1) >= h then
Printf.printf "\n";
Printf.printf "%!";
ANSITerminal.set_cursor 1 h
......@@ -1077,7 +1075,7 @@ type s_action =
short_description : Format.formatter -> unit -> unit;
description : Format.formatter -> unit -> unit;
exn_handler :
(state -> state) -> state -> state;
exn -> state -> state;
handler : string -> state -> state }
(* Complexe action type
......@@ -1087,6 +1085,8 @@ type c_action =
{ name : string;
short_description : Format.formatter -> unit -> unit;
description : Format.formatter -> unit -> unit;
exn_handler :
exn -> state -> state;
handler : string -> (state,state,state) t }
type action = S of s_action | C of c_action
......@@ -1161,8 +1161,7 @@ let pr_side ppf s =
(**********************)
(* This is the default exception handler for actions. *)
let default_exn_handler = fun excpt_throwing_fun state ->
try excpt_throwing_fun state with
let default_exn_handler = fun e state -> match e with
| Bad_argument ->
add_error_fun rule_short_help state
| Term_badly_formed s ->
......@@ -1173,7 +1172,6 @@ let default_exn_handler = fun excpt_throwing_fun state ->
add_error (Printf.sprintf "Negative index: %d" i) state
| e -> raise e
let add_s_action name short_descr descr exn_handler handler =
action_list :=
(S { name = name;
......@@ -1183,11 +1181,12 @@ let add_s_action name short_descr descr exn_handler handler =
handler = handler })
:: !action_list;;
let add_c_action name short_descr descr handler =
let add_c_action name short_descr descr exn_handler handler =
action_list :=
(C { name = name;
short_description = short_descr;
description = descr;
exn_handler = exn_handler;
handler = handler })
:: !action_list;;
......@@ -1428,30 +1427,23 @@ add_c_action
than term %a"
pr_pos "i")
default_exn_handler
(fun y state sk fk ->
try Scanf.sscanf y "%d"
(fun index ->
match Formula.nth state.c_proof.goal index with
| B _ -> raise Bad_argument
Scanf.sscanf y "%d"
(fun index ->
match Formula.nth state.c_proof.goal index with
| B _ -> raise Bad_argument
| T (u, u') ->
begin match u.content, u'.content with
| If (b,_,_), If (b',_,_) ->
let rule = (CS (b,b')) in
let (l_prem, r_prem) = cs_apply rule state.c_proof.goal in
| T (u, u') ->
begin match u.content, u'.content with
| If (b,_,_), If (b',_,_) ->
let rule = (CS (b,b')) in
let (l_prem, r_prem) = cs_apply rule state.c_proof.goal in
binary_aux state rule l_prem r_prem sk sk fk
binary_aux state rule l_prem r_prem sk sk fk
| _ -> raise Bad_argument end)
with
| Bad_argument ->
add_error_fun rule_short_help state
| Term_badly_formed s ->
add_error (Printf.sprintf "This term is badly formed: \"%s\"" s) state
| F_out_of_bound i ->
add_error (Printf.sprintf "Index out of bound: %d" i) state
| F_bad_argument i ->
add_error (Printf.sprintf "Negative index: %d" i) state
| _ -> raise Bad_argument end)
);;
......@@ -1470,42 +1462,41 @@ add_c_action
pr_side "side"
pr_term "b" pr_term "false")
default_exn_handler
(fun y state sk fk ->
try Scanf.sscanf y "%s %s@!"
(fun side_string b_string ->
match parse_b_terms state b_string,
string_to_side side_string with
| [b], Some side ->
let rule = Cond_fresh (side,b) in
let (l_prem, r_prem, env') =
cond_fresh_apply rule state.c_proof.goal in
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
| l, Some _ ->
let error_message =
Printf.sprintf
"Wanted to parse 1 boolean terms and got %d"
(List.length l) in
raise (Term_badly_formed error_message)
| _, None ->
let error_message =
Printf.sprintf
"You need to precise at what side the rule should be \
applied ('left' or 'right') " in
raise (Term_badly_formed error_message))
with
| Term_badly_formed s ->
add_error (Printf.sprintf "This term is badly formed: \"%s\"" s) state
Scanf.sscanf y "%s %s@!"
(fun side_string b_string ->
match parse_b_terms state b_string,
string_to_side side_string with
| [b], Some side ->
let rule = Cond_fresh (side,b) in
let (l_prem, r_prem, env') =
cond_fresh_apply rule state.c_proof.goal in
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
| l, Some _ ->
let error_message =
Printf.sprintf
"Wanted to parse 1 boolean terms and got %d"
(List.length l) in
raise (Term_badly_formed error_message)
| _, None ->
let error_message =
Printf.sprintf
"You need to precise at what side the rule should be \
applied ('left' or 'right') " in
raise (Term_badly_formed error_message))
);;
......@@ -1643,6 +1634,8 @@ add_c_action
(fun ppf () -> Fmt.pf ppf "admit")
default_exn_handler
(fun y state sk fk ->
raise Proof_done
);;
......@@ -1656,6 +1649,8 @@ add_c_action
(fun ppf () -> Fmt.pf ppf "back track")
default_exn_handler
(fun y state sk fk -> fk () );;
......@@ -1669,7 +1664,7 @@ let try_cca state =
raise Proof_done
end
else
add_error "Cannot apply the CCA2 axiom" state;;
state;;
add_c_action
"cca2"
......@@ -1678,6 +1673,8 @@ add_c_action
(fun ppf () -> Fmt.pf ppf "applies the cca2 axiom")
default_exn_handler
(fun y state sk fk ->
let state =
if y = "extend" then
......@@ -1716,10 +1713,14 @@ let exec_cmd state command sk fk =
match get_action name with
| S action ->
tact_wrap
(action.exn_handler (action.handler args))
(fun state ->
try action.handler args state with
| e -> action.exn_handler e state)
state sk fk
| C action -> action.handler args state sk fk
| C action ->
try action.handler args state sk fk with
| e -> sk (action.exn_handler e state) fk
with
| Not_found ->
......@@ -1746,26 +1747,25 @@ let rec exec_cmd_list l state sk fk = match l with
let rec interactive_loop state sk fk =
let state = simplify state
let state' = simplify state
|> new_screen in
Printf.printf "> %!";
let input_string =
if state.param.shell_mode then
get_user_input state
if state'.param.shell_mode then
get_user_input state'
else
try input_line state.param.input_channel with
try input_line state'.param.input_channel with
| End_of_file -> raise Proof_failed in
let (state,input_commands) =
try (state, parse_input input_string) with
let (state'',input_commands) =
try (state', parse_input input_string) with
| Term_badly_formed s ->
( add_error
(Printf.sprintf "This term is badly formed: %s" s) state,
( add_error (Printf.sprintf "This term is badly formed: %s" s) state',
[] ) in
(* We insert a back_track point here. *)
exec_cmd_list input_commands state
exec_cmd_list input_commands state''
(fun state fk' ->
interactive_loop state sk fk')
(fun () -> interactive_loop state sk fk)
......
......@@ -46,14 +46,14 @@ let new_state param proof =
let add_error err_msg state =
{ state with error_message = (fun () ->
state.error_message ();
Printf.printf "\n%s" err_msg) }
Printf.printf "%s\n" err_msg) }
(* Add a new error printing function. *)
let add_error_fun (err_fun : unit -> unit) state =
{ state with error_message = (fun () ->
state.error_message ();
Printf.printf "\n";
err_fun ()) }
err_fun ();
Printf.printf "\n") }
let err_reset state =
{ state with error_message = (fun () -> ()) }
......
(* First trace *)
obiwan;
cca2 guard;
cca2 guard;
fab 4;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
......
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