Commit 2462a9c0 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Registered exception_printers.

parent fe3fc009
......@@ -673,27 +673,7 @@ let rec update_status_column_from_iter cont iter =
| None -> ()
let match_transformation_exception (e: exn) =
match e with
| Args_wrapper.Arg_parse_error (s1, s2) ->
message_zone#buffer#set_text ("Argument parsing error:" ^ s2 ^ "\n" ^ s1)
| Args_wrapper.Arg_expected (s) ->
message_zone#buffer#set_text ("Argument expected of type: " ^ s)
| Args_wrapper.Arg_theory_not_found (s) ->
message_zone#buffer#set_text ("Theory not found:" ^ s)
| Args_wrapper.Arg_trans (s) ->
message_zone#buffer#set_text ("Error in transformation function: " ^ s)
| Args_wrapper.Arg_trans_term (s, Some s1, Some s2) ->
message_zone#buffer#set_text ("Error in transformation " ^ s ^
" during unification of following two terms:\n" ^
s1 ^ "\n" ^ s2)
| Controller_itp.Noprogress ->
message_zone#buffer#set_text ("The transformation made no progress")
| Args_wrapper.Arg_trans_type (s, Some s1, Some s2) ->
message_zone#buffer#set_text ("Error in transformation function:" ^ s ^
". These types should be equal:\n" ^ s1 ^ "\n" ^ s2)
| Args_wrapper.Arg_hyp_not_found s ->
message_zone#buffer#set_text ("Hypothesis not found during execution of " ^ s)
| _ -> message_zone#buffer#set_text (Pp.sprintf "Uncatched error: %a" Exn_printer.exn_printer e)
message_zone#buffer#set_text (Pp.sprintf "%a" Exn_printer.exn_printer e)
let move_current_row_selection_up () =
let current_view = List.hd (goals_view#selection#get_selected_rows) in
......
......@@ -6,6 +6,12 @@ open Session_itp
exception Noprogress
let () = Exn_printer.register
(fun fmt e ->
match e with
| Noprogress -> Format.fprintf fmt "The transformation made no progress.\n"
| _ -> raise e)
(** State of a proof *)
type proof_attempt_status =
| Unedited (** editor not yet run for interactive proof *)
......
......@@ -17,15 +17,23 @@ let fresh_printer =
*)
fun () -> create_ident_printer bl (* ~sanitizer:isanitize *)
exception Arg_trans of string
exception Arg_trans_term of (string * string option * string option)
exception Arg_trans_type of (string * string option * string option)
exception Arg_hyp_not_found of string
exception Arg_bad_hypothesis of (string * string option)
exception Arg_parse_error of string*string
exception Arg_expected of string
exception Arg_parse_error of string * string
exception Arg_expected of string * string
exception Arg_theory_not_found of string
exception Arg_expected_none of string
let () = Exn_printer.register
(fun fmt e ->
match e with
| Arg_parse_error (s1, s2) ->
Format.fprintf fmt "Argument parsing error: %s \n %s" s2 s1
| Arg_expected (ty, s) ->
Format.fprintf fmt "Argument expected of type: %s\n Argument given: %s" ty s
| Arg_theory_not_found s ->
Format.fprintf fmt "Theory not found %s" s
| Arg_expected_none s ->
Format.fprintf fmt "Argument expected of type %s. None were given." s
| _ -> raise e)
open Stdlib
......@@ -379,7 +387,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Tstring t' ->
let arg = Some s' in
wrap_to_store t' (f arg) tail env task
| _ -> assert false
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
| Topt (_, t'), _ ->
wrap_to_store (trans_typ_tail t') (f None) l env task
......@@ -387,7 +395,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f true) tail env task
| Toptbool (_, t'), _ ->
wrap_to_store t' (f false) l env task
| _, _ -> raise (Arg_expected (string_of_trans_typ t))
| _, [] -> raise (Arg_expected_none (string_of_trans_typ t))
let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
fun t f l env -> Trans.store (wrap_to_store t f l env)
......
......@@ -2,15 +2,10 @@
open Ident
open Task
exception Arg_trans of string
exception Arg_trans_term of (string * string option * string option)
exception Arg_trans_type of (string * string option * string option)
exception Arg_hyp_not_found of string
exception Arg_bad_hypothesis of (string * string option)
exception Arg_parse_error of string*string
exception Arg_expected of string
exception Arg_parse_error of string * string
exception Arg_expected of string * string
exception Arg_theory_not_found of string
exception Arg_expected_none of string
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
......
......@@ -7,6 +7,23 @@ open Task
open Args_wrapper
open Reduction_engine
exception Arg_trans of string
exception Arg_trans_term of (string * string * string)
exception Arg_trans_type of (string * string * string)
exception Arg_hyp_not_found of string
exception Arg_bad_hypothesis of (string * string)
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Arg_trans_type (s, s1, s2) ->
Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %s \n %s" s s1 s2
| Arg_trans_term (s, s1, s2) ->
Format.fprintf fmt "Error in transformation %s during unification of following two terms:\n %s \n %s" s s1 s2
| Arg_trans (s) -> Format.fprintf fmt "Error in transformation function: %s \n" s
| Arg_hyp_not_found (s) -> Format.fprintf fmt "Following hypothesis was not found: %s \n" s
| Arg_theory_not_found (s) -> Format.fprintf fmt "Theory not found: %s" s
| e -> raise e)
let debug_matching = Debug.register_info_flag "print_match"
~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
......@@ -52,8 +69,8 @@ let subst_quant c tq x : term =
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("subst_quant",
Some (Pp.string_of Pretty.print_ty ty1),
Some (Pp.string_of Pretty.print_ty ty2))))
Pp.string_of Pretty.print_ty ty1,
Pp.string_of Pretty.print_ty ty2)))
| [] -> failwith "subst_quant: Should not happen, please report")
(* Transform the term (exists v, f) into f[x/v] *)
......@@ -163,8 +180,8 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2
else ()); raise (Reduction_engine.NoMatch (Some (t1, t2)))
| Reduction_engine.NoMatch None -> raise (Reduction_engine.NoMatch None)
else ()); raise (Arg_trans_term ("apply", Pp.string_of Pretty.print_term t1, Pp.string_of Pretty.print_term t2))
| Reduction_engine.NoMatch None -> raise (Arg_trans ("apply"))
in
let inst_nt = t_subst subst nt in
if (Term.t_equal_nt_nl inst_nt g) then
......@@ -174,8 +191,8 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
lt
else
raise (Arg_trans_term ("apply",
Some (Pp.string_of Pretty.print_term inst_nt),
Some (Pp.string_of Pretty.print_term g))))
Pp.string_of Pretty.print_term inst_nt,
Pp.string_of Pretty.print_term g)))
(*(Format.printf
"Term %a and %a are not equal. Failure in matching @."
......@@ -248,7 +265,7 @@ let rewrite_in rev h h1 =
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Support to rewrite from the right *)
if rev then (t1, t2) else (t2, t1)
| _ -> raise (Arg_bad_hypothesis ("rewrite", Some (Pp.string_of Pretty.print_term f)))) in
| _ -> raise (Arg_bad_hypothesis ("rewrite", Pp.string_of Pretty.print_term f))) in
Some (lp, lv, t1, t2)
| _ -> acc) None in
(* Return instantiated premises and the hypothesis correctly rewritten *)
......@@ -294,8 +311,8 @@ let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
let replace t1 t2 h =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace",
Some (Pp.string_of Pretty.print_term t1),
Some (Pp.string_of Pretty.print_term t2)))
Pp.string_of Pretty.print_term t1,
Pp.string_of Pretty.print_term t2))
else
(* Create a new goal for equality of the two terms *)
let g = Decl.create_prop_decl Decl.Pgoal (create_prsymbol (gen_ident "G")) (t_app_infer ps_equ [t1; t2]) in
......@@ -393,8 +410,8 @@ let destruct pr : Task.task Trans.tlist =
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("destruct_exists",
Some (Pp.string_of Pretty.print_ty ty1),
Some (Pp.string_of Pretty.print_ty ty2))))
Pp.string_of Pretty.print_ty ty1,
Pp.string_of Pretty.print_ty ty2)))
| [] -> raise (Arg_trans ("destruct_exists"))
end
| _ -> raise (Arg_trans ("destruct"))
......
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