# HG changeset patch # User kuncar # Date 1333660974 -7200 # Node ID 075d22b3a32f0e9825d6ab46b56275ecd4d829db # Parent 96e920e0d09a63ea4b333ceabda05883fdee4473 detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr diff -r 96e920e0d09a -r 075d22b3a32f src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 05 22:00:27 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Apr 05 23:22:54 2012 +0200 @@ -6,6 +6,8 @@ signature LIFTING_DEF = sig + exception FORCE_RTY of typ * term + val add_lift_def: (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory @@ -26,6 +28,8 @@ fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm +exception FORCE_RTY of typ * term + fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) | get_body_types (U, V) = (U, V) @@ -38,6 +42,7 @@ val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs val rty_schematic = fastype_of rhs_schematic val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty + handle Type.TYPE_MATCH => raise FORCE_RTY (rty, rhs) in Envir.subst_term_types match rhs_schematic end @@ -283,6 +288,46 @@ | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy end +fun quot_thm_err ctxt (rty, qty) pretty_msg = + let + val error_msg = cat_lines + ["Lifting failed for the following types:", + Pretty.string_of (Pretty.block + [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]), + Pretty.string_of (Pretty.block + [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]), + "", + (Pretty.string_of (Pretty.block + [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))] + in + error error_msg + end + +fun force_rty_err ctxt rty rhs = + let + 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 (fastype_of rhs)]), + "", + (Pretty.string_of (Pretty.block + [Pretty.str "Reason:", + Pretty.brk 2, + Pretty.str "The type of the term cannot be instancied to", + Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt rty), + Pretty.str "."]))] + in + error error_msg + end + +fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy = + (lift_def_cmd (raw_var, rhs_raw) lthy + handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg) + handle FORCE_RTY (rty, rhs) => force_rty_err lthy rty rhs + (* parser and command *) val liftdef_parser = ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2) @@ -291,7 +336,7 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} "definition for constants over the quotient type" - (liftdef_parser >> lift_def_cmd) + (liftdef_parser >> lift_def_cmd_with_err_handling) end; (* structure *) diff -r 96e920e0d09a -r 075d22b3a32f src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 05 22:00:27 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 05 23:22:54 2012 +0200 @@ -50,8 +50,35 @@ else lthy +fun quot_thm_sanity_check ctxt quot_thm = + let + val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt + val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed + val rty_tfreesT = Term.add_tfree_namesT rty [] + val qty_tfreesT = Term.add_tfree_namesT qty [] + val extra_rty_tfrees = + (case subtract (op =) qty_tfreesT rty_tfreesT of + [] => [] + | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:", + Pretty.brk 1] @ + ((Pretty.commas o map (Pretty.str o quote)) extras) @ + [Pretty.str "."])]) + val not_type_constr = + (case qty of + Type _ => [] + | _ => [Pretty.block [Pretty.str "The quotient type ", + Pretty.quote (Syntax.pretty_typ ctxt' qty), + Pretty.brk 1, + Pretty.str "is not a type constructor."]]) + val errs = extra_rty_tfrees @ not_type_constr + in + if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] + @ (map Pretty.string_of errs))) + end + fun setup_lifting_infr quot_thm equiv_thm lthy = let + val _ = quot_thm_sanity_check lthy quot_thm val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qtyp val quotients = { quot_thm = quot_thm } diff -r 96e920e0d09a -r 075d22b3a32f src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Apr 05 22:00:27 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Apr 05 23:22:54 2012 +0200 @@ -6,6 +6,8 @@ signature LIFTING_TERM = sig + exception QUOT_THM of typ * typ * Pretty.T + val prove_quot_theorem: Proof.context -> typ * typ -> thm val absrep_fun: Proof.context -> typ * typ -> term @@ -24,7 +26,10 @@ structure Lifting_Term: LIFTING_TERM = struct -exception LIFT_MATCH of string +(* generation of the Quotient theorem *) + +exception QUOT_THM_INTERNAL of Pretty.T +exception QUOT_THM of typ * typ * Pretty.T (* matches a type pattern with a type *) fun match ctxt err ty_pat ty = @@ -40,21 +45,24 @@ val ty_pat_str = Syntax.string_of_typ ctxt ty_pat val ty_str = Syntax.string_of_typ ctxt ty in - raise LIFT_MATCH (space_implode " " - ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) + raise QUOT_THM_INTERNAL (Pretty.block + [Pretty.str ("The quotient type " ^ quote ty_str), + Pretty.brk 1, + Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str), + Pretty.brk 1, + Pretty.str "don't match."]) end -(* generation of the Quotient theorem *) - -exception QUOT_THM of string - fun get_quot_thm ctxt s = let val thy = Proof_Context.theory_of ctxt in (case Lifting_Info.lookup_quotients ctxt s of SOME qdata => Thm.transfer thy (#quot_thm qdata) - | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found.")) + | NONE => raise QUOT_THM_INTERNAL (Pretty.block + [Pretty.str ("No quotient type " ^ quote s), + Pretty.brk 1, + Pretty.str "found."])) end fun get_rel_quot_thm ctxt s = @@ -63,7 +71,10 @@ in (case Lifting_Info.lookup_quotmaps ctxt s of SOME map_data => Thm.transfer thy (#quot_thm map_data) - | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")")) + | NONE => raise QUOT_THM_INTERNAL (Pretty.block + [Pretty.str ("No relator for the type " ^ quote s), + Pretty.brk 1, + Pretty.str "found."])) end fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) @@ -106,8 +117,19 @@ (domain_type abs_type, range_type abs_type) end +fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name = + if provided_rty_name <> rty_of_qty_name then + raise QUOT_THM_INTERNAL (Pretty.block + [Pretty.str ("The type " ^ quote provided_rty_name), + Pretty.brk 1, + Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"), + Pretty.brk 1, + Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")]) + else + () + fun prove_quot_theorem' ctxt (rty, qty) = - case (rty, qty) of + (case (rty, qty) of (Type (s, tys), Type (s', tys')) => if s = s' then @@ -123,7 +145,8 @@ else let val quot_thm = get_quot_thm ctxt s' - val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm + val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm + val _ = check_raw_types (s, rs) s' val qtyenv = match ctxt equiv_match_err qty_pat qty val rtys' = map (Envir.subst_type qtyenv) rtys val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys') @@ -138,7 +161,8 @@ [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} end end - | _ => @{thm identity_quotient} + | _ => @{thm identity_quotient}) + handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg) fun force_qty_type thy qty quot_thm = let