--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200
@@ -140,15 +140,12 @@
|> (fn (poly, (level, (heaviness, core))) =>
case (core, (poly, level, heaviness)) of
("simple", (NONE, _, Light)) => Simple_Types level
- | ("preds", (SOME Polymorphic, _, _)) =>
- Preds (Polymorphic, level, heaviness)
| ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
| ("tags", (SOME Polymorphic, All_Types, _)) =>
Tags (Polymorphic, All_Types, heaviness)
- | ("tags", (SOME Polymorphic, Finite_Types, _)) =>
- (* The actual light encoding yields too many unsound proofs. *)
- Tags (Polymorphic, Finite_Types, Heavy)
- | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME
+ | ("tags", (SOME Polymorphic, _, _)) =>
+ (* The actual light encoding is very unsound. *)
+ Tags (Polymorphic, level, Heavy)
| ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
| ("args", (SOME poly, All_Types (* naja *), Light)) =>
Preds (poly, Const_Arg_Types, Light)
@@ -499,13 +496,19 @@
(** Finite and infinite type inference **)
+fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
+ | deep_freeze_atyp T = T
+val deep_freeze_type = map_atyps deep_freeze_atyp
+
+val type_instance = Sign.typ_instance o Proof_Context.theory_of
+
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Löwenheim-Skolem). *)
-fun should_encode_type _ (nonmono_Ts as _ :: _) _ T =
- exists (curry Type.raw_instance T) nonmono_Ts
+fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
+ exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
| should_encode_type _ _ All_Types _ = true
| should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
| should_encode_type _ _ _ _ = false
@@ -951,10 +954,10 @@
(** Symbol declarations **)
-fun insert_type get_T x xs =
+fun insert_type ctxt get_T x xs =
let val T = get_T x in
- if exists (curry Type.raw_instance T o get_T) xs then xs
- else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
+ if exists (curry (type_instance ctxt) T o get_T) xs then xs
+ else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
end
fun should_declare_sym type_sys pred_sym s =
@@ -965,7 +968,7 @@
| Tags (_, _, Light) => true
| _ => false) orelse not pred_sym)
-fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
let
fun add_combterm in_conj tm =
let val (head, args) = strip_combterm_comb tm in
@@ -974,8 +977,8 @@
let val pred_sym = is_pred_sym repaired_sym_tab s in
if should_declare_sym type_sys pred_sym s then
Symtab.map_default (s, [])
- (insert_type #3 (s', T_args, T, pred_sym, length args,
- in_conj))
+ (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
+ in_conj))
else
I
end
@@ -990,35 +993,37 @@
? (fold (add_fact true) conjs #> fold (add_fact false) facts)
end
+(* These types witness that the type classes they belong to allow infinite
+ models and hence that any types with these type classes is monotonic. *)
+val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}]
+
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
+fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
| add_combterm_nonmonotonic_types ctxt level _
(CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
tm2)) =
(exists is_var_or_bound_var [tm1, tm2] andalso
(case level of
- Nonmonotonic_Types => not (is_type_surely_infinite ctxt T)
+ Nonmonotonic_Types =>
+ not (is_type_surely_infinite ctxt known_infinite_types T)
| Finite_Types => is_type_surely_finite ctxt T
- | _ => true)) ? insert_type I T
+ | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
| add_combterm_nonmonotonic_types _ _ _ _ = I
fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
: translated_formula) =
formula_fold (SOME (kind <> Conjecture))
(add_combterm_nonmonotonic_types ctxt level) combformula
-fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
+fun nonmonotonic_types_for_facts ctxt type_sys facts =
let val level = level_of_type_sys type_sys in
- (case level of
- Nonmonotonic_Types => true
- | Finite_Types =>
- heaviness_of_type_sys type_sys = Light andalso
- polymorphism_of_type_sys type_sys <> Polymorphic
- | _ => false)
- ? (fold (add_fact_nonmonotonic_types ctxt level) facts
- (* We must add bool in case the helper "True_or_False" is added later.
- In addition, several places in the code rely on the list of
- nonmonotonic types not being empty. *)
- #> insert_type I @{typ bool})
+ if level = Nonmonotonic_Types orelse level = Finite_Types then
+ [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
+ (* We must add "bool" in case the helper "True_or_False" is added
+ later. In addition, several places in the code rely on the list of
+ nonmonotonic types not being empty. *)
+ |> insert_type ctxt I @{typ bool}
+ else
+ []
end
fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
@@ -1124,7 +1129,7 @@
case decls of
decl :: (decls' as _ :: _) =>
let val T = result_type_of_decl decl in
- if forall ((fn T' => Type.raw_instance (T', T))
+ if forall (curry (type_instance ctxt o swap) T
o result_type_of_decl) decls' then
[decl]
else
@@ -1198,8 +1203,7 @@
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
- val nonmono_Ts =
- [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
+ val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
@@ -1207,7 +1211,7 @@
repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts type_sys repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
val helper_lines =
map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200
@@ -22,7 +22,7 @@
val instantiate_type : theory -> typ -> typ -> typ -> typ
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
val is_type_surely_finite : Proof.context -> typ -> bool
- val is_type_surely_infinite : Proof.context -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_term : term -> term
@@ -122,79 +122,74 @@
| NONE => [])
| datatype_constrs _ _ = []
-(* Feel free to extend this list with any sorts that don't have finiteness
- axioms. *)
-val safe_sorts =
- @{sort type} @ @{sort "{default,zero,one,plus,minus,uminus,times,inverse}"} @
- @{sort "{abs,sgn,ord,equal,number}"}
-
(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt default_card T =
+fun tiny_card_of_type ctxt default_card assigns T =
let
+ val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
fun aux slack avoid T =
if member (op =) avoid T then
0
- else case T of
- Type (@{type_name fun}, [T1, T2]) =>
- (case (aux slack avoid T1, aux slack avoid T2) of
- (k, 1) => if slack andalso k = 0 then 0 else 1
- | (0, _) => 0
- | (_, 0) => 0
- | (k1, k2) =>
- if k1 >= max orelse k2 >= max then max
- else Int.min (max, Integer.pow k2 k1))
- | @{typ prop} => 2
- | @{typ bool} => 2 (* optimization *)
- | @{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
- constrs as _ :: _ =>
- let
- val constr_cards =
- map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
- o snd) constrs
- in
- 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. We are also slack with representation types:
- If a representation type has the form "sigma => tau", we
- consider it enough to check "sigma" for infiniteness. (Look for
- "slack" in this function.) *)
- (case varify_and_instantiate_type ctxt
- (Logic.varifyT_global abs_type) T
- (Logic.varifyT_global rep_type)
- |> aux true avoid of
- 0 => 0
- | 1 => 1
- | _ => default_card)
- | [] => default_card
- end
- (* Very slightly unsound: Type variables are assumed not to be
- constrained to cardinality 1. (In practice, the user would most
- likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
- (* Schematic type variables that contain only unproblematic sorts
- (with no finiteness axiom) can safely be considered infinite. *)
- | TVar (_, S) =>
- if default_card = 0 orelse subset (op =) (S, safe_sorts) then 0
- else default_card
+ else case AList.lookup (Sign.typ_instance thy o swap) assigns T of
+ SOME k => k
+ | NONE =>
+ case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ prop} => 2
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | @{typ int} => 0 (* optimization *)
+ | Type (s, _) =>
+ (case datatype_constrs thy T of
+ constrs as _ :: _ =>
+ let
+ val constr_cards =
+ map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+ o snd) constrs
+ in
+ 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. We are also slack with representation types:
+ If a representation type has the form "sigma => tau", we
+ consider it enough to check "sigma" for infiniteness. (Look
+ for "slack" in this function.) *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ | [] => default_card)
+ (* Very slightly unsound: Type variables are assumed not to be
+ constrained to cardinality 1. (In practice, the user would most
+ likely have used "unit" directly anyway.) *)
+ | TFree _ => if default_card = 1 then 2 else default_card
+ (* Schematic type variables that contain only unproblematic sorts
+ (with no finiteness axiom) can safely be considered infinite. *)
+ | TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
-fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0
+fun is_type_surely_infinite ctxt infinite_Ts T =
+ tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>