added syntax for "shallow" encodings

--- 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
@@ -16,11 +16,12 @@
   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   datatype type_level =
     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+  datatype type_depth = Deep | Shallow
 
   datatype type_system =
     Simple_Types of type_level |
-    Preds of polymorphism * type_level |
-    Tags of polymorphism * type_level
+    Preds of polymorphism * type_level * type_depth |
+    Tags of polymorphism * type_level * type_depth
 
   type translated_formula
 
@@ -89,11 +90,12 @@
 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
 datatype type_level =
   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+datatype type_depth = Deep | Shallow
 
 datatype type_system =
   Simple_Types of type_level |
-  Preds of polymorphism * type_level |
-  Tags of polymorphism * type_level
+  Preds of polymorphism * type_level * type_depth |
+  Tags of polymorphism * type_level * type_depth
 
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
@@ -116,33 +118,42 @@
             case try_unsuffixes ["!", "_bang"] s of
               SOME s => (Finite_Types, s)
             | NONE => (All_Types, s))
-  |> (fn (poly, (level, core)) =>
-         case (core, (poly, level)) of
-           ("simple_types", (NONE, level)) => Simple_Types level
-         | ("preds", (SOME Polymorphic, level)) =>
-           if level = All_Types then Preds (Polymorphic, level)
+  ||> apsnd (fn s =>
+                case try (unsuffix "_shallow") s of
+                  SOME s => (Shallow, s)
+                | NONE => (Deep, s))
+  |> (fn (poly, (level, (depth, core))) =>
+         case (core, (poly, level, depth)) of
+           ("simple_types", (NONE, level, Deep (* naja *))) =>
+           Simple_Types level
+         | ("preds", (SOME Polymorphic, level, depth)) =>
+           if level = All_Types then Preds (Polymorphic, level, depth)
            else raise Same.SAME
-         | ("preds", (SOME poly, level)) => Preds (poly, level)
-         | ("tags", (SOME Polymorphic, level)) =>
+         | ("preds", (SOME poly, level, depth)) => Preds (poly, level, depth)
+         | ("tags", (SOME Polymorphic, level, depth)) =>
            if level = All_Types orelse level = Finite_Types then
-             Tags (Polymorphic, level)
+             Tags (Polymorphic, level, depth)
            else
              raise Same.SAME
-         | ("tags", (SOME poly, level)) => Tags (poly, level)
-         | ("args", (SOME poly, All_Types (* naja *))) =>
-           Preds (poly, Const_Arg_Types)
-         | ("erased", (NONE, All_Types (* naja *))) =>
-           Preds (Polymorphic, No_Types)
+         | ("tags", (SOME poly, level, depth)) => Tags (poly, level, depth)
+         | ("args", (SOME poly, All_Types (* naja *), Deep (* naja *))) =>
+           Preds (poly, Const_Arg_Types, Shallow)
+         | ("erased", (NONE, All_Types (* naja *), Deep (* naja *))) =>
+           Preds (Polymorphic, No_Types, Shallow)
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
-  | polymorphism_of_type_sys (Preds (poly, _)) = poly
-  | polymorphism_of_type_sys (Tags (poly, _)) = poly
+  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
+  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
 
 fun level_of_type_sys (Simple_Types level) = level
-  | level_of_type_sys (Preds (_, level)) = level
-  | level_of_type_sys (Tags (_, level)) = level
+  | level_of_type_sys (Preds (_, level, _)) = level
+  | level_of_type_sys (Tags (_, level, _)) = level
+
+fun depth_of_type_sys (Simple_Types _) = Shallow
+  | depth_of_type_sys (Preds (_, _, depth)) = depth
+  | depth_of_type_sys (Tags (_, _, depth)) = depth
 
 fun is_type_level_virtually_sound level =
   level = All_Types orelse level = Nonmonotonic_Types
@@ -192,7 +203,7 @@
   s <> type_pred_base andalso s <> type_tag_name andalso
   (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
    (case type_sys of
-      Tags (_, All_Types) => true
+      Tags (_, All_Types, _) => true
     | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
            member (op =) boring_consts s))
 
@@ -486,11 +497,11 @@
     exists (curry Type.raw_instance T) nonmono_Ts
   | should_encode_type _ _ _ _ = false
 
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
+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 =
+fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level, _)) T =
     should_encode_type ctxt nonmono_Ts level T
   | should_tag_with_type _ _ _ _ = false
 
@@ -1082,7 +1093,7 @@
                                              type_sys)
                       (0 upto length helpers - 1 ~~ helpers)
                   |> (case type_sys of
-                        Tags (Polymorphic, level) =>
+                        Tags (Polymorphic, level, _) =>
                         is_type_level_partial level
                         ? cons (ti_ti_helper_fact ())
                       | _ => I)),

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
@@ -404,12 +404,12 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Polymorphic, Const_Arg_Types),
-   Preds (Mangled_Monomorphic, Nonmonotonic_Types)]
+  [Preds (Polymorphic, Const_Arg_Types, Deep),
+   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Deep)]
 
 fun adjust_dumb_type_sys formats (Simple_Types level) =
     if member (op =) formats Tff then (Tff, Simple_Types level)
-    else (Fof, Preds (Mangled_Monomorphic, level))
+    else (Fof, Preds (Mangled_Monomorphic, level, Deep))
   | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     adjust_dumb_type_sys formats type_sys

--- a/src/HOL/ex/tptp_export.ML	Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Tue May 17 15:11:36 2011 +0200
@@ -93,15 +93,15 @@
     val _ = File.write path ""
     val facts0 = facts_of thy
     val facts =
-      facts0
-      |> map_filter (try (fn ((_, loc), (_, th)) =>
-             Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
-             ((Thm.get_name_hint th, loc), th)))
+      facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
+                    Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
+                    ((Thm.get_name_hint th, loc), th)))
     val type_sys =
       Sledgehammer_ATP_Translate.Preds
           (Sledgehammer_ATP_Translate.Polymorphic,
            if full_types then Sledgehammer_ATP_Translate.All_Types
-           else Sledgehammer_ATP_Translate.Const_Arg_Types)
+           else Sledgehammer_ATP_Translate.Const_Arg_Types,
+           Sledgehammer_ATP_Translate.Deep)
     val explicit_apply = false
     val (atp_problem, _, _, _, _, _) =
       Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom