# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID 358769224d94b73760f9a4d370df6ca77145b232
# Parent  9adf6b3965b3633d3aa15c2e7cb6a8dd0bc90f0a
renamed thin to light, fat to heavy

diff -r 9adf6b3965b3 -r 358769224d94 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_thinness = Thin | Fat
+  datatype type_heaviness = Heavy | Light
 
   datatype type_system =
     Simple_Types of type_level |
-    Preds of polymorphism * type_level * type_thinness |
-    Tags of polymorphism * type_level * type_thinness
+    Preds of polymorphism * type_level * type_heaviness |
+    Tags of polymorphism * type_level * type_heaviness
 
   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_thinness = Thin | Fat
+datatype type_heaviness = Heavy | Light
 
 datatype type_system =
   Simple_Types of type_level |
-  Preds of polymorphism * type_level * type_thinness |
-  Tags of polymorphism * type_level * type_thinness
+  Preds of polymorphism * type_level * type_heaviness |
+  Tags of polymorphism * type_level * type_heaviness
 
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
@@ -119,29 +119,33 @@
               SOME s => (Finite_Types, s)
             | NONE => (All_Types, s))
   ||> apsnd (fn s =>
-                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, thinness)) =>
-           if level = All_Types then Preds (Polymorphic, level, thinness)
-           else raise Same.SAME
-         | ("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, thinness)
+                case try (unsuffix "_heavy") s of
+                  SOME s => (SOME Heavy, s)
+                | NONE =>
+                  case try (unsuffix "_light") s of
+                    SOME s => (SOME Light, s)
+                  | NONE => (NONE, s))
+  |> (fn (poly, (level, (heaviness, core))) =>
+         case (core, (poly, level, heaviness)) of
+           ("simple_types", (NONE, level, NONE)) => Simple_Types level
+         | ("preds", (SOME Polymorphic, level, _)) =>
+           if level = All_Types then
+             Preds (Polymorphic, level, heaviness |> the_default Light)
            else
              raise Same.SAME
-         | ("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)
+         | ("preds", (SOME poly, level, _)) =>
+           Preds (poly, level, heaviness |> the_default Light)
+         | ("tags", (SOME Polymorphic, level, _)) =>
+           if level = All_Types orelse level = Finite_Types then
+             Tags (Polymorphic, level, heaviness |> the_default Light)
+           else
+             raise Same.SAME
+         | ("tags", (SOME poly, level, _)) =>
+           Tags (poly, level, heaviness |> the_default Light)
+         | ("args", (SOME poly, All_Types (* naja *), NONE)) =>
+           Preds (poly, Const_Arg_Types, Light)
+         | ("erased", (NONE, All_Types (* naja *), NONE)) =>
+           Preds (Polymorphic, No_Types, Light)
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
@@ -153,9 +157,9 @@
   | level_of_type_sys (Preds (_, level, _)) = level
   | level_of_type_sys (Tags (_, level, _)) = level
 
-fun thinness_of_type_sys (Simple_Types _) = Fat
-  | thinness_of_type_sys (Preds (_, _, thinness)) = thinness
-  | thinness_of_type_sys (Tags (_, _, thinness)) = thinness
+fun heaviness_of_type_sys (Simple_Types _) = Heavy
+  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
+  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
 
 fun is_type_level_virtually_sound level =
   level = All_Types orelse level = Nonmonotonic_Types
@@ -207,7 +211,7 @@
     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
+    heaviness_of_type_sys type_sys = Heavy
 
 fun general_type_arg_policy type_sys =
   if level_of_type_sys type_sys = No_Types then
@@ -489,9 +493,9 @@
   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
   | should_encode_type _ _ _ _ = false
 
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, thinness))
+fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
                              should_predicate_on_var T =
-     (thinness = Fat orelse should_predicate_on_var ()) andalso
+     (heaviness = Heavy orelse should_predicate_on_var ()) andalso
      should_encode_type ctxt nonmono_Ts level T
   | should_predicate_on_type _ _ _ _ _ = false
 
@@ -503,10 +507,10 @@
 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, thinness)) site u T =
-    (case thinness of
-       Fat => should_encode_type ctxt nonmono_Ts level T
-     | Thin =>
+  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
+    (case heaviness of
+       Heavy => should_encode_type ctxt nonmono_Ts level T
+     | Light =>
        case (site, is_var_or_bound_var u) of
          (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
        | _ => false)
@@ -657,12 +661,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. Don't do it for thin type systems, though, since it
-               leads to too many unsound proofs. *)
+               result type. Don't do it for lightweight 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) andalso
-               thinness_of_type_sys type_sys = Fat then
+               heaviness_of_type_sys type_sys = Heavy 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)
@@ -940,7 +944,7 @@
   not (String.isPrefix tptp_special_prefix s) andalso
   ((case type_sys of
       Simple_Types _ => true
-    | Tags (_, _, Thin) => true
+    | Tags (_, _, Light) => true
     | _ => false) orelse not pred_sym)
 
 fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
@@ -989,7 +993,7 @@
     (case level of
        Nonmonotonic_Types => true
      | Finite_Types =>
-       thinness_of_type_sys type_sys = Thin andalso
+       heaviness_of_type_sys type_sys = Light andalso
        polymorphism_of_type_sys type_sys <> Polymorphic
      | _ => false)
     ? (fold (add_fact_nonmonotonic_types ctxt level) facts
@@ -1113,10 +1117,10 @@
       |-> map2 (formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts
                                                type_sys n s)
     end
-  | Tags (_, _, thinness) =>
-    (case thinness of
-       Fat => []
-     | Thin =>
+  | Tags (_, _, heaviness) =>
+    (case heaviness of
+       Heavy => []
+     | Light =>
        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)
@@ -1145,7 +1149,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, Fat)) =
+fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
     level = Nonmonotonic_Types orelse level = Finite_Types
   | should_add_ti_ti_helper _ = false
 
diff -r 9adf6b3965b3 -r 358769224d94 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, Thin),
-   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Thin)]
+  [Preds (Polymorphic, Const_Arg_Types, Light),
+   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
 
 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, Fat))
+    else (Fof, Preds (Mangled_Monomorphic, level, Heavy))
   | 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 9adf6b3965b3 -r 358769224d94 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.Fat)
+           Sledgehammer_ATP_Translate.Heavy)
     val explicit_apply = false
     val (atp_problem, _, _, _, _, _) =
       Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom