# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID 06afb3070af675da86796c2ec3d47db2ad29d773
# Parent  c9b0968484fb4164fa8d7c7f8cbf081f2f611567
renamed "shallow" to "thin" and make it the default

diff -r c9b0968484fb -r 06afb3070af6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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,12 +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_thinness = Thin | Fat
 
   datatype type_system =
     Simple_Types of type_level |
-    Preds of polymorphism * type_level * type_depth |
-    Tags of polymorphism * type_level * type_depth
+    Preds of polymorphism * type_level * type_thinness |
+    Tags of polymorphism * type_level * type_thinness
 
   type translated_formula
 
@@ -90,12 +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_thinness = Thin | Fat
 
 datatype type_system =
   Simple_Types of type_level |
-  Preds of polymorphism * type_level * type_depth |
-  Tags of polymorphism * type_level * type_depth
+  Preds of polymorphism * type_level * type_thinness |
+  Tags of polymorphism * type_level * type_thinness
 
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
@@ -119,27 +119,29 @@
               SOME s => (Finite_Types, s)
             | NONE => (All_Types, s))
   ||> 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 *))) =>
+                case try (unsuffix "_fat") s of
+                  SOME s => (Fat, s)
+                | NONE => (Thin, s))
+  |> (fn (poly, (level, (thinness, core))) =>
+         case (core, (poly, level, thinness)) of
+           ("simple_types", (NONE, level, Thin (* naja *))) =>
            Simple_Types level
-         | ("preds", (SOME Polymorphic, level, depth)) =>
-           if level = All_Types then Preds (Polymorphic, level, depth)
+         | ("preds", (SOME Polymorphic, level, thinness)) =>
+           if level = All_Types then Preds (Polymorphic, level, thinness)
            else raise Same.SAME
-         | ("preds", (SOME poly, level, depth)) => Preds (poly, level, depth)
-         | ("tags", (SOME Polymorphic, level, depth)) =>
+         | ("preds", (SOME poly, level, thinness)) =>
+           Preds (poly, level, thinness)
+         | ("tags", (SOME Polymorphic, level, thinness)) =>
            if level = All_Types orelse level = Finite_Types then
-             Tags (Polymorphic, level, depth)
+             Tags (Polymorphic, level, thinness)
            else
              raise Same.SAME
-         | ("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)
+         | ("tags", (SOME poly, level, thinness)) =>
+           Tags (poly, level, thinness)
+         | ("args", (SOME poly, All_Types (* naja *), Thin)) =>
+           Preds (poly, Const_Arg_Types, Thin)
+         | ("erased", (NONE, All_Types (* naja *), Thin)) =>
+           Preds (Polymorphic, No_Types, Thin)
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
@@ -151,9 +153,9 @@
   | level_of_type_sys (Preds (_, level, _)) = level
   | level_of_type_sys (Tags (_, level, _)) = level
 
-fun depth_of_type_sys (Simple_Types _) = Deep
-  | depth_of_type_sys (Preds (_, _, depth)) = depth
-  | depth_of_type_sys (Tags (_, _, depth)) = depth
+fun thinness_of_type_sys (Simple_Types _) = Fat
+  | thinness_of_type_sys (Preds (_, _, thinness)) = thinness
+  | thinness_of_type_sys (Tags (_, _, thinness)) = thinness
 
 fun is_type_level_virtually_sound level =
   level = All_Types orelse level = Nonmonotonic_Types
@@ -200,8 +202,8 @@
   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 (_, _, Shallow) => false
-    | Tags (_, All_Types, Deep) => true
+      Tags (_, _, Thin) => false
+    | Tags (_, All_Types, Fat) => true
     | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
            member (op =) boring_consts s))
 
@@ -213,7 +215,7 @@
 
 fun should_drop_arg_type_args type_sys =
   level_of_type_sys type_sys = All_Types andalso
-  depth_of_type_sys type_sys = Deep
+  thinness_of_type_sys type_sys = Fat
 
 fun general_type_arg_policy type_sys =
   if level_of_type_sys type_sys = No_Types then
@@ -497,19 +499,19 @@
     exists (curry Type.raw_instance T) nonmono_Ts
   | should_encode_type _ _ _ _ = false
 
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, depth)) T =
-    (case depth of
-       Deep => should_encode_type ctxt nonmono_Ts level T
-     | Shallow => error "Not implemented yet.")
+fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, thinness)) T =
+    (case thinness of
+       Thin => should_encode_type ctxt nonmono_Ts level T (* FIXME *)
+     | Fat => should_encode_type ctxt nonmono_Ts level T)
   | should_predicate_on_type _ _ _ _ = false
 
 datatype tag_site = Top_Level | Eq_Arg | Elsewhere
 
 fun should_tag_with_type _ _ _ Top_Level _ _ = false
-  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, depth)) site u T =
-    (case depth of
-       Deep => should_encode_type ctxt nonmono_Ts level T
-     | Shallow =>
+  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, thinness)) site u T =
+    (case thinness of
+       Fat => should_encode_type ctxt nonmono_Ts level T
+     | Thin =>
        case (site, u) of
          (Eq_Arg, CombVar _) =>
          let
@@ -977,7 +979,7 @@
   let val level = level_of_type_sys type_sys in
     (level = Nonmonotonic_Types orelse
      (case type_sys of
-        Tags (poly, _, Shallow) => poly <> Polymorphic
+        Tags (poly, _, Thin) => poly <> Polymorphic
       | _ => false))
     ? (fold (add_fact_nonmonotonic_types ctxt level) facts
        (* in case helper "True_or_False" is included *)
@@ -1100,10 +1102,10 @@
       |-> map2 (formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts
                                                type_sys n s)
     end
-  | Tags (_, _, depth) =>
-    (case depth of
-       Deep => []
-     | Shallow =>
+  | Tags (_, _, thinness) =>
+    (case thinness of
+       Fat => []
+     | Thin =>
        let val n = length decls in
          (0 upto n - 1 ~~ decls)
          |> maps (formula_lines_for_tag_sym_decl ctxt nonmono_Ts type_sys n s)
@@ -1132,7 +1134,7 @@
 fun decl_line_for_tff_type (s, s') =
   Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
 
-fun should_add_ti_ti_helper (Tags (Polymorphic, level, Deep)) =
+fun should_add_ti_ti_helper (Tags (Polymorphic, level, Fat)) =
     level = Nonmonotonic_Types orelse level = Finite_Types
   | should_add_ti_ti_helper _ = false
 
diff -r c9b0968484fb -r 06afb3070af6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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, Deep),
-   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Deep)]
+  [Preds (Polymorphic, Const_Arg_Types, Thin),
+   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Thin)]
 
 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, Deep))
+    else (Fof, Preds (Mangled_Monomorphic, level, Fat))
   | 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
diff -r c9b0968484fb -r 06afb3070af6 src/HOL/ex/tptp_export.ML
--- 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
@@ -101,7 +101,7 @@
           (Sledgehammer_ATP_Translate.Polymorphic,
            if full_types then Sledgehammer_ATP_Translate.All_Types
            else Sledgehammer_ATP_Translate.Const_Arg_Types,
-           Sledgehammer_ATP_Translate.Deep)
+           Sledgehammer_ATP_Translate.Fat)
     val explicit_apply = false
     val (atp_problem, _, _, _, _, _) =
       Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom