Commit 36373030 authored by Sylvain Dailler's avatar Sylvain Dailler

Added cases for exception in transformation and query.

I added an exception to TSfailed. Also changed the query exceptions.
parent 87585cc2
......@@ -561,6 +561,29 @@ let rec update_status_column_from cont iter =
| Some p -> update_status_column_from cont p
| 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 "Uncatched error"
(* Callback of a transformation *)
let callback_update_tree_transform cont status =
match status with
......@@ -575,6 +598,7 @@ let callback_update_tree_transform cont status =
(* Put the selection on the first goal *)
goals_view#selection#select_iter (Hpn.find pn_id_to_gtree first_goal)#iter
| [] -> ())
| TSfailed e -> match_transformation_exception e
| _ -> ()
let move_current_row_selection_up () =
......@@ -746,12 +770,6 @@ let on_selected_row r =
let index = goals_model#get ~row:r#iter ~column:index_column in
try
let session_element = Hint.find model_index index in
(*
let () = match session_element with
| IproofNode id -> Hpn.add pn_id_to_gtree id r (* TODO maybe not the good place to fill
this table *)
| _ -> () in
*)
current_selected_index := session_element;
match session_element with
| IproofNode id ->
......
......@@ -4,6 +4,8 @@
open Format
open Session_itp
exception Noprogress
(** State of a proof *)
type proof_attempt_status =
| Unedited (** editor not yet run for interactive proof *)
......@@ -27,13 +29,13 @@ let print_status fmt st =
| Uninstalled pr -> fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed
| TSscheduled | TSdone of transID | TSfailed of exn
let print_trans_status fmt st =
match st with
| TSscheduled -> fprintf fmt "TScheduled"
| TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSfailed -> fprintf fmt "TSfailed"
| TSfailed _e -> fprintf fmt "TSfailed"
type strategy_status = STSgoto of proofNodeID * int | STShalt
......@@ -373,9 +375,9 @@ let timeout_handler () =
try
build_prover_call c id pr limit callback
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
(*Format.eprintf
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
Exn_printer.exn_printer e;
Exn_printer.exn_printer e;*)
callback (InternalFailure e)
done
with Queue.Empty -> ()
......@@ -420,16 +422,16 @@ let schedule_transformation_r c id name args ~callback =
begin
match subtasks with
| [t'] when Task.task_equal t' task ->
callback TSfailed
callback (TSfailed Noprogress)
| _ ->
let tid = graft_transf c.controller_session id name args subtasks in
callback (TSdone tid)
end
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
(* Format.eprintf
"@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
name Exn_printer.exn_printer e;
callback TSfailed
name Exn_printer.exn_printer e; TODO *)
callback (TSfailed e)
end;
false
in
......@@ -445,7 +447,7 @@ let schedule_transformation c id name args ~callback =
| _ -> false
in
update_trans_node c tid has_subtasks
| TSfailed -> ()
| TSfailed _e -> ()
| _ -> ()); callback s in
schedule_transformation_r c id name args ~callback
......@@ -483,7 +485,7 @@ let run_strategy_on_goal c id strat ~callback_pa ~callback_tr ~callback =
let callback ntr =
callback_tr ntr;
match ntr with
| TSfailed -> (* transformation failed *)
| TSfailed _e -> (* transformation failed *)
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
S.idle ~prio:0 run_next
......
......@@ -11,6 +11,8 @@
open Session_itp
exception Noprogress
(** State of a proof *)
type proof_attempt_status =
| Unedited (** editor not yet run for interactive proof *)
......@@ -24,7 +26,7 @@ type proof_attempt_status =
val print_status : Format.formatter -> proof_attempt_status -> unit
type transformation_status = TSscheduled | TSdone of transID | TSfailed
type transformation_status = TSscheduled | TSdone of transID | TSfailed of exn
val print_trans_status : Format.formatter -> transformation_status -> unit
......
......@@ -199,7 +199,7 @@ let find_any_id nt s =
| Not_found -> (Stdlib.Mstr.find s nt.Theory.ns_ts).Ty.ts_name
(* The id you are trying to use is undefined *)
exception Undefined_id
exception Undefined_id of string
(* Bad number of arguments *)
exception Number_of_arguments
......@@ -207,7 +207,7 @@ let print_id s task =
let tables = Args_wrapper.build_name_tables task in
let km = tables.Args_wrapper.known_map in
let id = try find_any_id tables.Args_wrapper.namespace s with
| Not_found -> raise Undefined_id in
| Not_found -> raise (Undefined_id s) in
let d =
try Ident.Mid.find id km with
| Not_found -> raise Not_found (* Should not happen *)
......@@ -223,7 +223,7 @@ let search s task =
let tables = Args_wrapper.build_name_tables task in
let id_decl = tables.Args_wrapper.id_decl in
let id = try find_any_id tables.Args_wrapper.namespace s with
| Not_found -> raise Undefined_id in
| Not_found -> raise (Undefined_id s) in
let l =
try Ident.Mid.find id id_decl with
| Not_found -> raise Not_found (* Should not happen *)
......@@ -314,7 +314,10 @@ let interp cont id s =
| Qtask _, None -> Query "please select a goal first"
| Qtask f, Some id ->
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
Query (f cont task args)
let s = try Query (f cont task args) with
| Undefined_id s -> Query ("No existing id corresponding to " ^ s)
| Number_of_arguments -> Query "Bad number of arguments"
in s
with Not_found ->
try
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
......
......@@ -17,6 +17,15 @@ 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_theory_not_found of string
open Stdlib
......@@ -240,10 +249,6 @@ let parse_and_type ~as_fmla s task =
in
t
exception Arg_parse_error of string*string
exception Arg_expected of string
exception Arg_theory_not_found of string
let parse_int s =
try int_of_string s
with Failure _ -> raise (Arg_parse_error (s,"int expected"))
......
......@@ -2,6 +2,16 @@
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_theory_not_found of string
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
......
......@@ -10,10 +10,6 @@ open Reduction_engine
let debug_matching = Debug.register_info_flag "print_match"
~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
exception Arg_trans of string
exception Arg_trans_term of (string * Term.term option * Term.term option)
exception Arg_trans_type of (string * Ty.ty option * Ty.ty option)
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
let gen_ident = Ident.id_fresh
......@@ -54,7 +50,10 @@ let subst_quant c tq x : term =
(let new_t = t_subst_single hdv x te in
t_quant_close c tl tr new_t)
with
| Ty.TypeMismatch (ty1, ty2) -> raise (Arg_trans_type ("subst_quant", Some ty1, Some ty2)))
| 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))))
| [] -> failwith "subst_quant: Should not happen, please report")
(* Transform the term (exists v, f) into f[x/v] *)
......@@ -141,7 +140,6 @@ let intros f =
| _ -> (lp, lv, f) in
intros_aux [] Svs.empty f
exception Hyp_not_found
(* Apply:
1) takes the hypothesis and introduce parts of it to keep only the last element of
......@@ -156,7 +154,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
let g, task = Task.task_separate_goal task in
let g = term_decl g in
let d = find_hypothesis name task in
if d = None then raise Hyp_not_found;
if d = None then raise (Arg_hyp_not_found "apply");
let d = Opt.get d in
let t = term_decl d in
let (lp, lv, nt) = intros t in
......@@ -175,7 +173,9 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
(create_prsymbol (gen_ident "G")) ng)) nlp in
lt
else
raise (Arg_trans_term ("apply", Some inst_nt, Some g)))
raise (Arg_trans_term ("apply",
Some (Pp.string_of Pretty.print_term inst_nt),
Some (Pp.string_of Pretty.print_term g))))
(*(Format.printf
"Term %a and %a are not equal. Failure in matching @."
......@@ -237,8 +237,6 @@ let replace_subst lp lv f1 f2 t =
| Some subst ->
(List.map (t_subst subst) lp, t)
exception Bad_hypothesis of Term.term
let rewrite_in rev h h1 =
let found_eq =
(* Used to find the equality we are rewriting on *)
......@@ -250,13 +248,13 @@ 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 (Bad_hypothesis f)) in
| _ -> raise (Arg_bad_hypothesis ("rewrite", Some (Pp.string_of Pretty.print_term f)))) in
Some (lp, lv, t1, t2)
| _ -> acc) None in
(* Return instantiated premises and the hypothesis correctly rewritten *)
let lp_new found_eq =
match found_eq with
| None -> raise Hyp_not_found
| None -> raise (Arg_hyp_not_found "rewrite")
| Some (lp, lv, t1, t2) ->
fold (fun d acc ->
match d.d_node with
......@@ -295,7 +293,9 @@ let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
(* Replace occurences of t1 with t2 in h *)
let replace t1 t2 h =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace", Some t1, Some t2))
raise (Arg_trans_term ("replace",
Some (Pp.string_of Pretty.print_term t1),
Some (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
......@@ -307,7 +307,6 @@ let replace t1 t2 h =
| _ -> [d]) None in
Trans.par [g; ng]
let is_good_type t ty =
try (Term.t_ty_check t (Some ty); true) with
| _ -> false
......
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