--- 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
--- 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
--- 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
--- 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