--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200
@@ -203,9 +203,11 @@
Mangled_Type_Args of bool |
No_Type_Args
-fun should_drop_arg_type_args type_sys =
- level_of_type_sys type_sys = All_Types andalso
- thinness_of_type_sys type_sys = Fat
+fun should_drop_arg_type_args (Simple_Types _) =
+ false (* since TFF doesn't support overloading *)
+ | should_drop_arg_type_args type_sys =
+ level_of_type_sys type_sys = All_Types andalso
+ thinness_of_type_sys type_sys = Fat
fun general_type_arg_policy type_sys =
if level_of_type_sys type_sys = No_Types then
@@ -444,8 +446,7 @@
|> perhaps (try (HOLogic.dest_Trueprop))
|> introduce_combinators_in_term ctxt kind
|> kind <> Axiom ? freeze_term
- val (combformula, atomic_types) =
- combformula_from_prop thy eq_as_iff t []
+ val (combformula, atomic_types) = combformula_from_prop thy eq_as_iff t []
in
{name = name, locality = loc, kind = kind, combformula = combformula,
atomic_types = atomic_types}
@@ -482,10 +483,10 @@
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 _ _ All_Types _ = true
+fun should_encode_type _ (nonmono_Ts as _ :: _) _ T =
+ exists (curry Type.raw_instance 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 _ 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, thinness))
@@ -494,6 +495,11 @@
should_encode_type ctxt nonmono_Ts level T
| should_predicate_on_type _ _ _ _ _ = false
+fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+ String.isPrefix bound_var_prefix s
+ | is_var_or_bound_var (CombVar _) = true
+ | is_var_or_bound_var _ = false
+
datatype tag_site = Top_Level | Eq_Arg | Elsewhere
fun should_tag_with_type _ _ _ Top_Level _ _ = false
@@ -501,13 +507,8 @@
(case thinness of
Fat => should_encode_type ctxt nonmono_Ts level T
| Thin =>
- case (site, u) of
- (Eq_Arg, CombVar _) =>
- let
- (* This trick ensures that "If" helpers are not unduely tagged, while
- "True_or_False" is correctly tagged. *)
- val level' = if null nonmono_Ts then level else Nonmonotonic_Types
- in should_encode_type ctxt nonmono_Ts level' T end
+ case (site, is_var_or_bound_var u) of
+ (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
| _ => false)
| should_tag_with_type _ _ _ _ _ _ = false
@@ -656,10 +657,12 @@
val (T, T_args) =
(* Aggressively merge most "hAPPs" if the type system is unsound
anyway, by distinguishing overloads only on the homogenized
- result type. *)
+ result type. Don't do it for thin type systems, though, since it
+ leads to too many unsound proofs. *)
if s = const_prefix ^ explicit_app_base andalso
length T_args = 2 andalso
- not (is_type_sys_virtually_sound type_sys) then
+ not (is_type_sys_virtually_sound type_sys) andalso
+ thinness_of_type_sys type_sys = Fat then
T_args |> map (homogenized_type ctxt nonmono_Ts level)
|> (fn Ts => let val T = hd Ts --> nth Ts 1 in
(T --> T, tl Ts)
@@ -965,11 +968,6 @@
? (fold (add_fact true) conjs #> fold (add_fact false) facts)
end
-fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
- String.isPrefix bound_var_prefix s
- | is_var_or_bound_var (CombVar _) = true
- | is_var_or_bound_var _ = false
-
(* 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
@@ -988,17 +986,19 @@
(add_combterm_nonmonotonic_types ctxt level) combformula
fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
let val level = level_of_type_sys type_sys in
- (level = Nonmonotonic_Types orelse
- (case type_sys of
- Tags (poly, _, Thin) => poly <> Polymorphic
- | _ => false))
+ (case level of
+ Nonmonotonic_Types => true
+ | Finite_Types =>
+ thinness_of_type_sys type_sys = Thin andalso
+ polymorphism_of_type_sys type_sys <> Polymorphic
+ | _ => false)
? (fold (add_fact_nonmonotonic_types ctxt level) facts
- (* in case helper "True_or_False" is included *)
+ (* 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})
end
-fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
-
fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
let
val translate_type =
@@ -1056,10 +1056,7 @@
else AAtom (ATerm (`I "equal", tms)))
|> bound_atomic_types type_sys atomic_Ts
|> close_formula_universally
- val should_encode =
- should_encode_type ctxt nonmono_Ts
- (if polymorphism_of_type_sys type_sys = Polymorphic then All_Types
- else Nonmonotonic_Types)
+ val should_encode = should_encode_type ctxt nonmono_Ts All_Types
val tag_with = tag_with_type ctxt nonmono_Ts type_sys
val add_formula_for_res =
if should_encode res_T then
@@ -1087,6 +1084,8 @@
|> fold add_formula_for_arg (ary - 1 downto 0)
end
+fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
+
fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
(s, decls) =
case type_sys of