1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 05 10:47:33 2011 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 05 12:40:48 2011 +0200
1.3 @@ -570,17 +570,6 @@
1.4 "Code_Numeral.code_numeral"] s orelse
1.5 (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
1.6
1.7 -(* TODO: use "Term_Subst.instantiateT" instead? *)
1.8 -fun instantiate_type thy T1 T1' T2 =
1.9 - Same.commit (Envir.subst_type_same
1.10 - (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
1.11 - handle Type.TYPE_MATCH =>
1.12 - raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
1.13 -fun varify_and_instantiate_type ctxt T1 T1' T2 =
1.14 - let val thy = Proof_Context.theory_of ctxt in
1.15 - instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
1.16 - end
1.17 -
1.18 fun repair_constr_type ctxt body_T' T =
1.19 varify_and_instantiate_type ctxt (body_type T) body_T' T
1.20
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 05 10:47:33 2011 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 05 12:40:48 2011 +0200
2.3 @@ -64,11 +64,13 @@
2.4 val typ_of_dtyp :
2.5 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
2.6 -> typ
2.7 + val varify_type : Proof.context -> typ -> typ
2.8 + val instantiate_type : theory -> typ -> typ -> typ -> typ
2.9 + val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
2.10 val is_of_class_const : theory -> string * typ -> bool
2.11 val get_class_def : theory -> string -> (string * term) option
2.12 val monomorphic_term : Type.tyenv -> term -> term
2.13 val specialize_type : theory -> string * typ -> term -> term
2.14 - val varify_type : Proof.context -> typ -> typ
2.15 val eta_expand : typ list -> term -> int -> term
2.16 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
2.17 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
2.18 @@ -264,15 +266,13 @@
2.19 val simple_string_of_typ = Refute.string_of_typ
2.20 val is_real_constr = Refute.is_IDT_constructor
2.21 val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
2.22 +val varify_type = Sledgehammer_Util.varify_type
2.23 +val instantiate_type = Sledgehammer_Util.instantiate_type
2.24 +val varify_and_instantiate_type = Sledgehammer_Util.varify_and_instantiate_type
2.25 val is_of_class_const = Refute.is_const_of_class
2.26 val get_class_def = Refute.get_classdef
2.27 val monomorphic_term = Sledgehammer_Util.monomorphic_term
2.28 val specialize_type = Sledgehammer_Util.specialize_type
2.29 -
2.30 -fun varify_type ctxt T =
2.31 - Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
2.32 - |> snd |> the_single |> dest_Const |> snd
2.33 -
2.34 val eta_expand = Sledgehammer_Util.eta_expand
2.35
2.36 fun time_limit NONE = I
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 05 10:47:33 2011 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 05 12:40:48 2011 +0200
3.3 @@ -495,13 +495,13 @@
3.4 | (k1, k2) =>
3.5 if k1 >= max orelse k2 >= max then max
3.6 else Int.min (max, Integer.pow k2 k1))
3.7 - | @{typ int} => 0
3.8 | @{typ bool} => 2 (* optimization *)
3.9 - | Type _ =>
3.10 + | @{typ nat} => 0 (* optimization *)
3.11 + | @{typ int} => 0 (* optimization *)
3.12 + | Type (s, _) =>
3.13 let val thy = Proof_Context.theory_of ctxt in
3.14 case datatype_constrs thy T of
3.15 - [] => default_card
3.16 - | constrs =>
3.17 + constrs as _ :: _ =>
3.18 let
3.19 val constr_cards =
3.20 map (Integer.prod o map (aux (T :: avoid)) o binder_types
3.21 @@ -510,6 +510,21 @@
3.22 if exists (curry (op =) 0) constr_cards then 0
3.23 else Int.min (max, Integer.sum constr_cards)
3.24 end
3.25 + | [] =>
3.26 + case Typedef.get_info ctxt s of
3.27 + ({abs_type, rep_type, ...}, _) :: _ =>
3.28 + (* We cheat here by assuming that typedef types are infinite if
3.29 + their underlying type is infinite. This is unsound in general
3.30 + but it's hard to think of a realistic example where this would
3.31 + not be the case. *)
3.32 + (case varify_and_instantiate_type ctxt
3.33 + (Logic.varifyT_global abs_type) T
3.34 + (Logic.varifyT_global rep_type)
3.35 + |> aux avoid of
3.36 + 0 => 0
3.37 + | 1 => 1
3.38 + | _ => default_card)
3.39 + | [] => default_card
3.40 end
3.41 | _ => default_card)
3.42 in Int.min (max, aux [] T) end
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 05 10:47:33 2011 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 05 12:40:48 2011 +0200
4.3 @@ -18,6 +18,9 @@
4.4 val typ_of_dtyp :
4.5 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
4.6 -> typ
4.7 + val varify_type : Proof.context -> typ -> typ
4.8 + val instantiate_type : theory -> typ -> typ -> typ -> typ
4.9 + val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
4.10 val monomorphic_term : Type.tyenv -> term -> term
4.11 val eta_expand : typ list -> term -> int -> term
4.12 val transform_elim_term : term -> term
4.13 @@ -92,6 +95,21 @@
4.14 Type (s, map (typ_of_dtyp descr typ_assoc) ds)
4.15 end
4.16
4.17 +fun varify_type ctxt T =
4.18 + Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
4.19 + |> snd |> the_single |> dest_Const |> snd
4.20 +
4.21 +(* TODO: use "Term_Subst.instantiateT" instead? *)
4.22 +fun instantiate_type thy T1 T1' T2 =
4.23 + Same.commit (Envir.subst_type_same
4.24 + (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
4.25 + handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
4.26 +
4.27 +fun varify_and_instantiate_type ctxt T1 T1' T2 =
4.28 + let val thy = Proof_Context.theory_of ctxt in
4.29 + instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
4.30 + end
4.31 +
4.32 fun monomorphic_term subst t =
4.33 map_types (map_type_tvar (fn v =>
4.34 case Type.lookup subst v of