# HG changeset patch # User blanchet # Date 1304542033 -7200 # Node ID 562046fd8e0c55cd19f6ddde3143685b0665f80d # Parent 281cc069282c85e03378ff4b60534295f08a9641 added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types) diff -r 281cc069282c -r 562046fd8e0c src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 04 19:47:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed May 04 22:47:13 2011 +0200 @@ -210,7 +210,7 @@ (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)] else [(1.0, (true, 250 (* FUDGE *)))], - best_type_systems = ["const_args", "mangled_preds"]} + best_type_systems = ["args", "mangled_preds"]} val e = (eN, e_config) diff -r 281cc069282c -r 562046fd8e0c src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 19:47:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 22:47:13 2011 +0200 @@ -17,7 +17,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Many_Typed | + Many_Typed of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -96,7 +96,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Many_Typed | + Many_Typed of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -116,21 +116,20 @@ | NONE => (All_Types, s)) |> (fn (polymorphism, (level, core)) => case (core, (polymorphism, level)) of - ("many_typed", (Polymorphic (* naja *), All_Types)) => - Many_Typed + ("many_typed", (Polymorphic (* naja *), level)) => Many_Typed level | ("preds", extra) => Preds extra | ("tags", extra) => Tags extra - | ("const_args", (_, All_Types (* naja *))) => + | ("args", (_, All_Types (* naja *))) => Preds (polymorphism, Const_Arg_Types) | ("erased", (Polymorphic, All_Types (* naja *))) => Preds (polymorphism, No_Types) | _ => error ("Unknown type system: " ^ quote s ^ ".")) -fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic +fun polymorphism_of_type_sys (Many_Typed _) = Mangled_Monomorphic | polymorphism_of_type_sys (Preds (poly, _)) = poly | polymorphism_of_type_sys (Tags (poly, _)) = poly -fun level_of_type_sys Many_Typed = All_Types +fun level_of_type_sys (Many_Typed level) = level | level_of_type_sys (Preds (_, level)) = level | level_of_type_sys (Tags (_, level)) = level @@ -453,6 +452,83 @@ (0 upto last) ts end +(** Finite and infinite type inference **) + +(* 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 datatype_constrs thy (T as Type (s, Ts)) = + (case Datatype.get_info thy s of + SOME {index, descr, ...} => + let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in + map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) + constrs + end + | NONE => []) + | datatype_constrs _ _ = [] + +(* 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 = + let + val max = 2 (* 1 would be too small for the "fun" case *) + fun aux avoid T = + (if member (op =) avoid T then + 0 + else case T of + Type (@{type_name fun}, [T1, T2]) => + (case (aux avoid T1, aux avoid T2) of + (_, 1) => 1 + | (0, _) => 0 + | (_, 0) => 0 + | (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 _ => + let val thy = Proof_Context.theory_of ctxt in + case datatype_constrs thy T of + [] => default_card + | constrs => + let + val constr_cards = + map (Integer.prod o map (aux (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 + end + | _ => default_card) + in Int.min (max, aux [] 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 should_encode_type _ _ All_Types _ = true + | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T + | should_encode_type _ nonmono_Ts Nonmonotonic_Types T = + exists (curry Type.raw_instance T) nonmono_Ts + | should_encode_type _ _ _ _ = false + +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T = + should_encode_type ctxt nonmono_Ts level T + | should_predicate_on_type _ _ _ _ = false + +fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T = + should_encode_type ctxt nonmono_Ts level T + | should_tag_with_type _ _ _ _ = false + +val homo_infinite_T = @{typ ind} (* any infinite type *) + +fun homogenized_type ctxt nonmono_Ts level T = + if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T + (** "hBOOL" and "hAPP" **) type sym_info = @@ -554,29 +630,43 @@ | (head, args) => list_explicit_app head (map aux args) in aux end -fun impose_type_arg_policy_in_combterm type_sys = +fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = let fun aux (CombApp tmp) = CombApp (pairself aux tmp) | aux (CombConst (name as (s, _), T, T_args)) = - (case strip_prefix_and_unascii const_prefix s of - NONE => (name, T_args) - | SOME s'' => - let val s'' = invert_const s'' in - case type_arg_policy type_sys s'' of - No_Type_Args => (name, []) - | Explicit_Type_Args => (name, T_args) - | Mangled_Type_Args => (mangled_const_name T_args name, []) - end) - |> (fn (name, T_args) => CombConst (name, T, T_args)) + let + val level = level_of_type_sys type_sys + val (T, T_args) = + (* avoid needless identical homogenized versions of "hAPP" *) + if s = const_prefix ^ explicit_app_base then + T_args |> map (homogenized_type ctxt nonmono_Ts level) + |> (fn Ts => let val T = hd Ts --> nth Ts 1 in + (T --> T, Ts) + end) + else + (T, T_args) + in + (case strip_prefix_and_unascii const_prefix s of + NONE => (name, T_args) + | SOME s'' => + let val s'' = invert_const s'' in + case type_arg_policy type_sys s'' of + No_Type_Args => (name, []) + | Explicit_Type_Args => (name, T_args) + | Mangled_Type_Args => (mangled_const_name T_args name, []) + end) + |> (fn (name, T_args) => CombConst (name, T, T_args)) + end | aux tm = tm in aux end -fun repair_combterm type_sys sym_tab = +fun repair_combterm ctxt nonmono_Ts type_sys sym_tab = introduce_explicit_apps_in_combterm sym_tab #> introduce_predicators_in_combterm sym_tab - #> impose_type_arg_policy_in_combterm type_sys -fun repair_fact type_sys sym_tab = - update_combformula (formula_map (repair_combterm type_sys sym_tab)) + #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys +fun repair_fact ctxt nonmono_Ts type_sys sym_tab = + update_combformula (formula_map + (repair_combterm ctxt nonmono_Ts type_sys sym_tab)) (** Helper facts **) @@ -660,83 +750,17 @@ fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot -(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are - considered dangerous because their "exhaust" properties can easily lead to - unsound ATP proofs. The checks below are an (unsound) approximation of - finiteness. *) - -fun datatype_constrs thy (T as Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME {index, descr, ...} => - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in - map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) - constrs - end - | NONE => []) - | datatype_constrs _ _ = [] - -(* 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 = - let - val max = 2 (* 1 would be too small for the "fun" case *) - fun aux avoid T = - (if member (op =) avoid T then - 0 - else case T of - Type (@{type_name fun}, [T1, T2]) => - (case (aux avoid T1, aux avoid T2) of - (_, 1) => 1 - | (0, _) => 0 - | (_, 0) => 0 - | (k1, k2) => - if k1 >= max orelse k2 >= max then max - else Int.min (max, Integer.pow k2 k1)) - | Type _ => - (case datatype_constrs (Proof_Context.theory_of ctxt) T of - [] => default_card - | constrs => - let - val constr_cards = - map (Integer.prod o map (aux (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) - | _ => default_card) - in Int.min (max, aux [] 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 should_encode_type _ _ All_Types _ = true - | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T - | should_encode_type _ nonmono_Ts Nonmonotonic_Types T = - exists (curry Type.raw_instance T) nonmono_Ts - | should_encode_type _ _ _ _ = false - -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T = - should_encode_type ctxt nonmono_Ts level T - | should_predicate_on_type _ _ _ _ = false - -fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T = - should_encode_type ctxt nonmono_Ts level T - | should_tag_with_type _ _ _ _ = false - -fun type_pred_combatom type_sys T tm = +fun type_pred_combatom ctxt nonmono_Ts type_sys T tm = CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), tm) - |> impose_type_arg_policy_in_combterm type_sys + |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |> AAtom fun formula_from_combformula ctxt nonmono_Ts type_sys = let fun tag_with_type type_sys T tm = CombConst (`make_fixed_const type_tag_name, T --> T, [T]) - |> impose_type_arg_policy_in_combterm type_sys + |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |> do_term true |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) and do_term top_level u = @@ -758,10 +782,13 @@ I) end val do_bound_type = - if type_sys = Many_Typed then SOME o mangled_type_name else K NONE + case type_sys of + Many_Typed level => + SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level + | _ => K NONE fun do_out_of_bound_type (s, T) = if should_predicate_on_type ctxt nonmono_Ts type_sys T then - type_pred_combatom type_sys T (CombVar (s, T)) + type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T)) |> do_formula |> SOME else NONE @@ -859,7 +886,7 @@ fun should_declare_sym type_sys pred_sym s = not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso not (String.isPrefix "$" s) andalso - (type_sys = Many_Typed orelse not pred_sym) + ((case type_sys of Many_Typed _ => true | _ => false) orelse not pred_sym) fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab = let @@ -891,7 +918,6 @@ ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab) facts - (* FIXME: use CombVar not CombConst for bound variables? *) fun is_var_or_bound_var (CombConst ((s, _), _, _)) = String.isPrefix bound_var_prefix s @@ -911,7 +937,8 @@ combformula fun add_nonmonotonic_types_for_facts ctxt type_sys facts = level_of_type_sys type_sys = Nonmonotonic_Types - ? fold (add_fact_nonmonotonic_types ctxt) facts + ? (insert_type I @{typ bool} (* in case helper "True_or_False" is included *) + #> fold (add_fact_nonmonotonic_types ctxt) facts) fun n_ary_strip_type 0 T = ([], T) | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) = @@ -920,7 +947,7 @@ fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd -fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) = +fun decl_line_for_sym s (s', _, T, pred_sym, ary) = let val (arg_Ts, res_T) = n_ary_strip_type ary T in Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts, if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) @@ -944,7 +971,7 @@ (if n > 1 then "_" ^ string_of_int j else ""), Axiom, CombConst ((s, s'), T, T_args) |> fold (curry (CombApp o swap)) bound_tms - |> type_pred_combatom type_sys res_T + |> type_pred_combatom ctxt nonmono_Ts type_sys res_T |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_from_combformula ctxt nonmono_Ts type_sys |> close_formula_universally, @@ -952,9 +979,9 @@ end fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) = - if type_sys = Many_Typed then - map (decl_line_for_sym_decl s) decls - else + case type_sys of + Many_Typed _ => map (decl_line_for_sym s) decls + | _ => let val decls = case decls of @@ -1017,15 +1044,13 @@ val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply - val (conjs, facts) = - (conjs, facts) |> pairself (map (repair_fact type_sys sym_tab)) + val nonmono_Ts = + [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs] + 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 val helpers = - helper_facts_for_sym_table ctxt type_sys repaired_sym_tab - |> map (repair_fact type_sys sym_tab) - val nonmono_Ts = - [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) - [facts, conjs, helpers] + repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair val sym_decl_lines = conjs @ facts |> sym_decl_table_for_facts type_sys repaired_sym_tab @@ -1051,11 +1076,11 @@ (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] val problem = problem - |> (if type_sys = Many_Typed then + |> (case type_sys of + Many_Typed _ => cons (type_declsN, map decl_line_for_tff_type (tff_types_in_problem problem)) - else - I) + | _ => I) val (problem, pool) = problem |> nice_atp_problem (Config.get ctxt readable_names) in diff -r 281cc069282c -r 562046fd8e0c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 04 19:47:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 04 22:47:13 2011 +0200 @@ -346,14 +346,14 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Polymorphic, Const_Arg_Types), Many_Typed] + [Preds (Polymorphic, Const_Arg_Types), Many_Typed All_Types] -fun adjust_dumb_type_sys formats Many_Typed = - if member (op =) formats Tff then (Tff, Many_Typed) - else (Fof, Preds (Mangled_Monomorphic, All_Types)) +fun adjust_dumb_type_sys formats (Many_Typed level) = + if member (op =) formats Tff then (Tff, Many_Typed level) + else (Fof, Preds (Mangled_Monomorphic, level)) | adjust_dumb_type_sys formats type_sys = if member (op =) formats Fof then (Fof, type_sys) - else (Tff, Many_Typed) + else (Tff, Many_Typed (level_of_type_sys type_sys)) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats