# HG changeset patch # User kuncar # Date 1430567886 -7200 # Node ID 8657416869269e8e02f014852c768826fcaa1df5 # Parent 3cab6f891c2faa07bf0e5f6f48dbf9af27fa2446 handle error messages also in after_qed diff -r 3cab6f891c2f -r 865741686926 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat May 02 13:58:06 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat May 02 13:58:06 2015 +0200 @@ -734,6 +734,28 @@ error error_msg end +fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) = + let + val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt + val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw + val error_msg = cat_lines + ["Lifting failed for the following term:", + Pretty.string_of (Pretty.block + [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]), + Pretty.string_of (Pretty.block + [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]), + "", + (Pretty.string_of (Pretty.block + [Pretty.str "Reason:", + Pretty.brk 2, + Pretty.str "The type of the term cannot be instantiated to", + Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt rty_forced), + Pretty.str "."]))] + in + error error_msg + end + fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy = let val config = evaluate_params params @@ -761,33 +783,15 @@ end in (SOME readable_rsp_tm_tnames, after_qed') - end + end + fun after_qed_with_err_handling thmss ctxt = (after_qed thmss ctxt + handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg) + handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => + check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw); in - Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy + Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] lthy end -fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) = - let - val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt - val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw - val error_msg = cat_lines - ["Lifting failed for the following term:", - Pretty.string_of (Pretty.block - [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]), - Pretty.string_of (Pretty.block - [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]), - "", - (Pretty.string_of (Pretty.block - [Pretty.str "Reason:", - Pretty.brk 2, - Pretty.str "The type of the term cannot be instantiated to", - Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt rty_forced), - Pretty.str "."]))] - in - error error_msg - end - fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy = (lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)