# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 1d46d85cd78bfa6f3bb08cbda07208181d257fda
# Parent  49347c6354b53dcbdca3fb8c30d781f9988d3d1c
make "prepare_atp_problem" more robust w.r.t. choice of type system

diff -r 49347c6354b5 -r 1d46d85cd78b src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -103,6 +103,7 @@
   val level_of_type_sys : type_system -> type_level
   val is_type_sys_virtually_sound : type_system -> bool
   val is_type_sys_fairly_sound : type_system -> bool
+  val choose_format : format list -> type_system -> format * type_system
   val raw_type_literals_for_types : typ list -> type_literal list
   val unmangled_const : string -> string * string fo_term list
   val translate_atp_fact :
@@ -568,6 +569,20 @@
 fun is_setting_higher_order THF (Simple_Types _) = true
   | is_setting_higher_order _ _ = false
 
+fun choose_format formats (Simple_Types level) =
+    if member (op =) formats THF then (THF, Simple_Types level)
+    else if member (op =) formats TFF then (TFF, Simple_Types level)
+    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavy))
+  | choose_format formats type_sys =
+    (case hd formats of
+       CNF_UEQ =>
+       (CNF_UEQ, case type_sys of
+                   Preds stuff =>
+                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
+                       stuff
+                 | _ => type_sys)
+     | format => (format, type_sys))
+
 type translated_formula =
   {name: string,
    locality: locality,
@@ -1756,6 +1771,7 @@
                         explicit_apply readable_names preproc hyp_ts concl_t
                         facts =
   let
+    val (format, type_sys) = choose_format [format] type_sys
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
                          facts
diff -r 49347c6354b5 -r 1d46d85cd78b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 31 16:38:36 2011 +0200
@@ -514,30 +514,13 @@
 val fallback_best_type_systems =
   [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
 
-fun adjust_dumb_type_sys formats (Simple_Types level) =
-    if member (op =) formats THF then
-      (THF, Simple_Types level)
-    else if member (op =) formats TFF then
-      (TFF, Simple_Types level)
-    else
-      adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
-  | adjust_dumb_type_sys formats type_sys =
-    (case hd formats of
-       CNF_UEQ =>
-       (CNF_UEQ, case type_sys of
-                   Preds stuff =>
-                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
-                       stuff
-                 | _ => type_sys)
-     | format => (format, type_sys))
-
 fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
-    adjust_dumb_type_sys formats type_sys
+    choose_format formats type_sys
   | choose_format_and_type_sys best_type_systems formats
                                (Smart_Type_Sys full_types) =
     map type_sys_from_string best_type_systems @ fallback_best_type_systems
     |> find_first (if full_types then is_type_sys_virtually_sound else K true)
-    |> the |> adjust_dumb_type_sys formats
+    |> the |> choose_format formats
 
 val metis_minimize_max_time = seconds 2.0