# HG changeset patch # User blanchet # Date 1304592048 -7200 # Node ID 9bc5dc48f1a5b2f56fe73b66416c368188d119fb # Parent 7c7ca3fc7ce53fee147f25c4acd4528eeb200ab7 query typedefs as well for monotonicity diff -r 7c7ca3fc7ce5 -r 9bc5dc48f1a5 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 05 10:47:33 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 05 12:40:48 2011 +0200 @@ -570,17 +570,6 @@ "Code_Numeral.code_numeral"] s orelse (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) -(* TODO: use "Term_Subst.instantiateT" instead? *) -fun instantiate_type thy T1 T1' T2 = - Same.commit (Envir.subst_type_same - (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 - handle Type.TYPE_MATCH => - raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) -fun varify_and_instantiate_type ctxt T1 T1' T2 = - let val thy = Proof_Context.theory_of ctxt in - instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) - end - fun repair_constr_type ctxt body_T' T = varify_and_instantiate_type ctxt (body_type T) body_T' T diff -r 7c7ca3fc7ce5 -r 9bc5dc48f1a5 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 05 10:47:33 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 05 12:40:48 2011 +0200 @@ -64,11 +64,13 @@ val typ_of_dtyp : Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ + val varify_type : Proof.context -> typ -> typ + val instantiate_type : theory -> typ -> typ -> typ -> typ + val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ val is_of_class_const : theory -> string * typ -> bool val get_class_def : theory -> string -> (string * term) option val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> string * typ -> term -> term - val varify_type : Proof.context -> typ -> typ val eta_expand : typ list -> term -> int -> term val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic @@ -264,15 +266,13 @@ val simple_string_of_typ = Refute.string_of_typ val is_real_constr = Refute.is_IDT_constructor val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp +val varify_type = Sledgehammer_Util.varify_type +val instantiate_type = Sledgehammer_Util.instantiate_type +val varify_and_instantiate_type = Sledgehammer_Util.varify_and_instantiate_type val is_of_class_const = Refute.is_const_of_class val get_class_def = Refute.get_classdef val monomorphic_term = Sledgehammer_Util.monomorphic_term val specialize_type = Sledgehammer_Util.specialize_type - -fun varify_type ctxt T = - Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] - |> snd |> the_single |> dest_Const |> snd - val eta_expand = Sledgehammer_Util.eta_expand fun time_limit NONE = I diff -r 7c7ca3fc7ce5 -r 9bc5dc48f1a5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 05 10:47:33 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 05 12:40:48 2011 +0200 @@ -495,13 +495,13 @@ | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, Integer.pow k2 k1)) - | @{typ int} => 0 | @{typ bool} => 2 (* optimization *) - | Type _ => + | @{typ nat} => 0 (* optimization *) + | @{typ int} => 0 (* optimization *) + | Type (s, _) => let val thy = Proof_Context.theory_of ctxt in case datatype_constrs thy T of - [] => default_card - | constrs => + constrs as _ :: _ => let val constr_cards = map (Integer.prod o map (aux (T :: avoid)) o binder_types @@ -510,6 +510,21 @@ if exists (curry (op =) 0) constr_cards then 0 else Int.min (max, Integer.sum constr_cards) end + | [] => + case Typedef.get_info ctxt s of + ({abs_type, rep_type, ...}, _) :: _ => + (* We cheat here by assuming that typedef types are infinite if + their underlying type is infinite. This is unsound in general + but it's hard to think of a realistic example where this would + not be the case. *) + (case varify_and_instantiate_type ctxt + (Logic.varifyT_global abs_type) T + (Logic.varifyT_global rep_type) + |> aux avoid of + 0 => 0 + | 1 => 1 + | _ => default_card) + | [] => default_card end | _ => default_card) in Int.min (max, aux [] T) end diff -r 7c7ca3fc7ce5 -r 9bc5dc48f1a5 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 05 10:47:33 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 05 12:40:48 2011 +0200 @@ -18,6 +18,9 @@ val typ_of_dtyp : Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ + val varify_type : Proof.context -> typ -> typ + val instantiate_type : theory -> typ -> typ -> typ -> typ + val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term val transform_elim_term : term -> term @@ -92,6 +95,21 @@ Type (s, map (typ_of_dtyp descr typ_assoc) ds) end +fun varify_type ctxt T = + Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] + |> snd |> the_single |> dest_Const |> snd + +(* TODO: use "Term_Subst.instantiateT" instead? *) +fun instantiate_type thy T1 T1' T2 = + Same.commit (Envir.subst_type_same + (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 + handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) + +fun varify_and_instantiate_type ctxt T1 T1' T2 = + let val thy = Proof_Context.theory_of ctxt in + instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) + end + fun monomorphic_term subst t = map_types (map_type_tvar (fn v => case Type.lookup subst v of