use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 14:40:57 2011 +0200
@@ -11,15 +11,6 @@
   type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
-  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
-  datatype type_level =
-    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-
-  datatype type_system =
-    Many_Typed |
-    Preds of polymorphism * type_level |
-    Tags of polymorphism * type_level
-
   type atp_config =
     {exec : string * string,
      required_execs : (string * string) list,
@@ -29,15 +20,11 @@
      hypothesis_kind : formula_kind,
      formats : format list,
      best_slices : unit -> (real * (bool * int)) list,
-     best_type_systems : type_system list}
+     best_type_systems : string list}
 
   datatype e_weight_method =
     E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
 
-  val polymorphism_of_type_sys : type_system -> polymorphism
-  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
   (* for experimentation purposes -- do not use in production code *)
   val e_weight_method : e_weight_method Unsynchronized.ref
   val e_default_fun_weight : real Unsynchronized.ref
@@ -58,7 +45,7 @@
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (failure * string) list -> formula_kind -> format list -> (unit -> int)
-    -> type_system list -> string * atp_config
+    -> string list -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -75,35 +62,6 @@
 
 (* ATP configuration *)
 
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
-datatype type_level =
-  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-
-datatype type_system =
-  Many_Typed |
-  Preds of polymorphism * type_level |
-  Tags of polymorphism * type_level
-
-val mangled_preds = Preds (Mangled_Monomorphic, All_Types)
-val const_args = Preds (Polymorphic, Const_Arg_Types)
-
-fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
-  | polymorphism_of_type_sys (Preds (poly, _)) = poly
-  | polymorphism_of_type_sys (Tags (poly, _)) = poly
-
-fun level_of_type_sys Many_Typed = All_Types
-  | level_of_type_sys (Preds (_, level)) = level
-  | level_of_type_sys (Tags (_, level)) = level
-
-val is_type_level_virtually_sound =
-  member (op =) [All_Types, Nonmonotonic_Types]
-val is_type_sys_virtually_sound =
-  is_type_level_virtually_sound o level_of_type_sys
-
-fun is_type_level_fairly_sound level =
-  is_type_level_virtually_sound level orelse level = Finite_Types
-val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
-
 type atp_config =
   {exec : string * string,
    required_execs : (string * string) list,
@@ -113,7 +71,7 @@
    hypothesis_kind : formula_kind,
    formats : format list,
    best_slices : unit -> (real * (bool * int)) list,
-   best_type_systems : type_system list}
+   best_type_systems : string list}
 
 val known_perl_failures =
   [(CantConnect, "HTTP error"),
@@ -240,7 +198,7 @@
         (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
      else
        [(1.0, (true, 250 (* FUDGE *)))],
-   best_type_systems = [const_args, mangled_preds]}
+   best_type_systems = ["const_args", "mangled_preds"]}
 
 val e = (eN, e_config)
 
@@ -271,7 +229,7 @@
    best_slices =
      K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = [mangled_preds]}
+   best_type_systems = ["mangled_preds"]}
 
 val spass = (spassN, spass_config)
 
@@ -307,7 +265,7 @@
    best_slices =
      K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = [mangled_preds]}
+   best_type_systems = ["mangled_preds"]}
 
 val vampire = (vampireN, vampire_config)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 14:40:57 2011 +0200
@@ -46,7 +46,6 @@
 
 open ATP_Problem
 open ATP_Proof
-open ATP_Systems
 open Metis_Translate
 open Sledgehammer_Util
 open Sledgehammer_Filter

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 14:40:57 2011 +0200
@@ -10,7 +10,16 @@
 sig
   type 'a fo_term = 'a ATP_Problem.fo_term
   type 'a problem = 'a ATP_Problem.problem
-  type type_system = ATP_Systems.type_system
+
+  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+  datatype type_level =
+    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
+  datatype type_system =
+    Many_Typed |
+    Preds of polymorphism * type_level |
+    Tags of polymorphism * type_level
+
   type translated_formula
 
   val readable_names : bool Unsynchronized.ref
@@ -20,6 +29,11 @@
   val explicit_app_base : string
   val type_pred_base : string
   val tff_type_prefix : string
+  val type_sys_from_string : string -> type_system
+  val polymorphism_of_type_sys : type_system -> polymorphism
+  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 num_atp_type_args : theory -> type_system -> string -> int
   val unmangled_const : string -> string * string fo_term list
   val translate_atp_fact :
@@ -37,7 +51,6 @@
 struct
 
 open ATP_Problem
-open ATP_Systems
 open Metis_Translate
 open Sledgehammer_Util
 
@@ -72,6 +85,58 @@
 (* Freshness almost guaranteed! *)
 val sledgehammer_weak_prefix = "Sledgehammer:"
 
+datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype type_level =
+  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
+datatype type_system =
+  Many_Typed |
+  Preds of polymorphism * type_level |
+  Tags of polymorphism * type_level
+
+fun type_sys_from_string s =
+  (case try (unprefix "mangled_") s of
+     SOME s => (Mangled_Monomorphic, s)
+   | NONE =>
+     case try (unprefix "mono_") s of
+       SOME s => (Monomorphic, s)
+     | NONE => (Polymorphic, s))
+  ||> (fn s =>
+          case try (unsuffix " ?") s of
+            SOME s => (Nonmonotonic_Types, s)
+          | NONE =>
+            case try (unsuffix " !") s of
+              SOME s => (Finite_Types, s)
+            | NONE => (All_Types, s))
+  |> (fn (polymorphism, (level, core)) =>
+         case (core, (polymorphism, level)) of
+           ("many_typed", (Polymorphic (* naja *), All_Types)) =>
+           Many_Typed
+         | ("preds", extra) => Preds extra
+         | ("tags", extra) => Tags extra
+         | ("const_args", (_, All_Types (* naja *))) =>
+           Preds (polymorphism, Const_Arg_Types)
+         | ("erased", (Polymorphic, All_Types (* naja *))) =>
+           Preds (polymorphism, No_Types)
+         | _ => error ("Unknown type system: " ^ quote s ^ "."))
+
+fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
+  | polymorphism_of_type_sys (Preds (poly, _)) = poly
+  | polymorphism_of_type_sys (Tags (poly, _)) = poly
+
+fun level_of_type_sys Many_Typed = All_Types
+  | level_of_type_sys (Preds (_, level)) = level
+  | level_of_type_sys (Tags (_, level)) = level
+
+val is_type_level_virtually_sound =
+  member (op =) [All_Types, Nonmonotonic_Types]
+val is_type_sys_virtually_sound =
+  is_type_level_virtually_sound o level_of_type_sys
+
+fun is_type_level_fairly_sound level =
+  is_type_level_virtually_sound level orelse level = Finite_Types
+val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+
 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 02 14:40:57 2011 +0200
@@ -233,33 +233,10 @@
     val blocking = auto orelse debug orelse lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
-    val type_sys = lookup_string "type_sys"
     val type_sys =
-      (case try (unprefix "mangled_") type_sys of
-         SOME s => (Mangled_Monomorphic, s)
-       | NONE =>
-         case try (unprefix "mono_") type_sys of
-           SOME s => (Monomorphic, s)
-         | NONE => (Polymorphic, type_sys))
-      ||> (fn s => case try (unsuffix " ?") s of
-                     SOME s => (Nonmonotonic_Types, s)
-                   | NONE =>
-                     case try (unsuffix " !") s of
-                       SOME s => (Finite_Types, s)
-                     | NONE => (All_Types, s))
-      |> (fn (polymorphism, (level, core)) =>
-             case (core, (polymorphism, level)) of
-               ("many_typed", (Polymorphic (* naja *), All_Types)) =>
-               Dumb_Type_Sys Many_Typed
-             | ("preds", extra) => Dumb_Type_Sys (Preds extra)
-             | ("tags", extra) => Dumb_Type_Sys (Tags extra)
-             | ("const_args", (_, All_Types (* naja *))) =>
-               Dumb_Type_Sys (Preds (polymorphism, Const_Arg_Types))
-             | ("erased", (Polymorphic, All_Types (* naja *))) =>
-               Dumb_Type_Sys (Preds (polymorphism, No_Types))
-             | ("smart", (Polymorphic, All_Types) (* naja *)) =>
-               Smart_Type_Sys (lookup_bool "full_types")
-             | _ => error ("Unknown type system: " ^ quote type_sys ^ "."))
+      case lookup_string "type_sys" of
+        "smart" => Smart_Type_Sys (lookup_bool "full_types")
+      | s => Dumb_Type_Sys (type_sys_from_string s)
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
     val monomorphize_limit = lookup_int "monomorphize_limit"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 14:40:57 2011 +0200
@@ -352,7 +352,7 @@
     adjust_dumb_type_sys formats type_sys
   | determine_format_and_type_sys best_type_systems formats
                                   (Smart_Type_Sys full_types) =
-    best_type_systems @ fallback_best_type_systems
+    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
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 14:40:57 2011 +0200
@@ -23,7 +23,6 @@
 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
 struct
 
-open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Filter
 open Sledgehammer_ATP_Translate

--- a/src/HOL/ex/tptp_export.ML	Mon May 02 14:28:28 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 14:40:57 2011 +0200
@@ -98,9 +98,10 @@
              Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
              ((Thm.get_name_hint th, loc), th)))
     val type_sys =
-      ATP_Systems.Preds (ATP_Systems.Polymorphic,
-                         if full_types then ATP_Systems.All_Types
-                         else ATP_Systems.Const_Arg_Types)
+      Sledgehammer_ATP_Translate.Preds
+          (Sledgehammer_ATP_Translate.Polymorphic,
+           if full_types then Sledgehammer_ATP_Translate.All_Types
+           else Sledgehammer_ATP_Translate.Const_Arg_Types)
     val explicit_apply = false
     val (atp_problem, _, _, _, _) =
       Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys