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