# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID f6ba908b8b27025350c838dd2ee4e249049df4fe
# Parent  9e3e4563645937e51d81c972413e7471d3fa55ab
generate typing for "hBOOL" in "Many_Typed" mode + tuning

diff -r 9e3e45636459 -r f6ba908b8b27 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -334,10 +334,12 @@
   let
     fun aux opt_T extra_us u =
       case u of
-        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
-      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
-      | ATerm (a, us) =>
-        if a = type_tag_name then
+        ATerm (a, us) =>
+        if a = boolify_name then
+          aux (SOME @{typ bool}) [] (hd us)
+        else if a = explicit_app_name then
+          aux opt_T (nth us 1 :: extra_us) (hd us)
+        else if a = type_tag_name then
           case us of
             [typ_u, term_u] =>
             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
diff -r 9e3e45636459 -r f6ba908b8b27 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -21,6 +21,8 @@
 
   val fact_prefix : string
   val conjecture_prefix : string
+  val boolify_name : string
+  val explicit_app_name : string
   val is_type_system_sound : type_system -> bool
   val type_system_types_dangerous_types : type_system -> bool
   val num_atp_type_args : theory -> type_system -> string -> int
@@ -50,6 +52,8 @@
 val arity_clause_prefix = "arity_"
 val tfree_prefix = "tfree_"
 
+val boolify_name = "hBOOL"
+val explicit_app_name = "hAPP"
 val is_base = "is"
 val type_prefix = "ty_"
 
@@ -628,14 +632,16 @@
 fun consider_problem_syms problem =
   fold (fold consider_problem_line_syms o snd) problem
 
-(* needed for helper facts if the problem otherwise does not involve equality *)
-val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false})
+(* The "equal" entry is needed for helper facts if the problem otherwise does
+   not involve equality. *)
+val default_entries =
+  [("equal", {min_arity = 2, max_arity = 2, fun_sym = false})]
 
 fun sym_table_for_problem explicit_apply problem =
   if explicit_apply then
     NONE
   else
-    SOME (Symtab.empty |> Symtab.default equal_entry
+    SOME (Symtab.empty |> fold Symtab.default default_entries
                        |> consider_problem_syms problem)
 
 fun min_arity_of thy type_sys NONE s =
@@ -658,13 +664,13 @@
 
 fun list_hAPP_rev _ t1 [] = t1
   | list_hAPP_rev NONE t1 (t2 :: ts2) =
-    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+    ATerm (`I explicit_app_name, [list_hAPP_rev NONE t1 ts2, t2])
   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
     case full_type_of t2 of
       SOME ty2 =>
       let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
                            [ty2, ty]) in
-        ATerm (`I "hAPP",
+        ATerm (`I explicit_app_name,
                [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
       end
     | NONE => list_hAPP_rev NONE t1 (t2 :: ts2)
@@ -683,7 +689,7 @@
         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   in aux NONE end
 
-fun boolify t = ATerm (`I "hBOOL", [t])
+fun boolify t = ATerm (`I boolify_name, [t])
 
 (* True if the constant ever appears outside of the top-level position in
    literals, or if it appears with different arities (e.g., because of different
@@ -786,6 +792,12 @@
 fun type_decl_lines_for_const ctxt type_sys sym_tab (s, xs) =
   map (type_decl_line_for_const_entry ctxt type_sys sym_tab s) xs
 
+fun add_extra_type_decl_lines Many_Typed =
+    cons (Type_Decl (type_decl_prefix ^ boolify_name, `I boolify_name,
+                     [mangled_combtyp (combtyp_from_typ @{typ bool})],
+                     `I tff_bool_type))
+  | add_extra_type_decl_lines _ = I
+
 val factsN = "Relevant facts"
 val class_relsN = "Class relationships"
 val aritiesN = "Arity declarations"
@@ -826,6 +838,7 @@
     val type_decl_lines =
       Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys sym_tab)
                       const_tab []
+      |> add_extra_type_decl_lines type_sys
     val helper_lines =
       helper_facts
       |>> map (pair 0