first step towards polymorphic TFF + changed defaults for Vampire

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:04:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:34 2011 +0200
@@ -19,14 +19,15 @@
 
   datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
-  datatype tff_flavor = Implicit | Explicit
-  datatype thf_flavor = Without_Choice | With_Choice
+  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
+  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+  datatype thf_flavor = THF_Without_Choice | THF_With_Choice
   datatype format =
     CNF |
     CNF_UEQ |
     FOF |
-    TFF of tff_flavor |
-    THF of thf_flavor
+    TFF of tff_polymorphism * tff_explicitness |
+    THF0 of thf_flavor
 
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
@@ -119,15 +120,16 @@
 
 datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
-datatype tff_flavor = Implicit | Explicit
-datatype thf_flavor = Without_Choice | With_Choice
+datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
+datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+datatype thf_flavor = THF_Without_Choice | THF_With_Choice
 
 datatype format =
   CNF |
   CNF_UEQ |
   FOF |
-  TFF of tff_flavor |
-  THF of thf_flavor
+  TFF of tff_polymorphism * tff_explicitness |
+  THF0 of thf_flavor
 
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
@@ -211,10 +213,10 @@
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)
 
-fun is_format_thf (THF _) = true
+fun is_format_thf (THF0 _) = true
   | is_format_thf _ = false
 fun is_format_typed (TFF _) = true
-  | is_format_typed (THF _) = true
+  | is_format_typed (THF0 _) = true
   | is_format_typed _ = false
 
 fun string_for_kind Axiom = "axiom"
@@ -228,7 +230,7 @@
     raise Fail "unexpected higher-order type in first-order format"
   | strip_tff_type (AType s) = ([], s)
 
-fun string_for_type (THF _) ty =
+fun string_for_type (THF0 _) ty =
     let
       fun aux _ (AType s) = s
         | aux rhs (AFun (ty1, ty2)) =
@@ -270,7 +272,7 @@
       |> is_format_thf format ? enclose "(" ")"
     else
       (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
-             s = tptp_choice andalso format = THF With_Choice, ts) of
+             s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
          (true, _, [AAbs ((s', ty), tm)]) =>
          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
             possible, to work around LEO-II 1.2.8 parser limitation. *)
@@ -291,7 +293,7 @@
            else
              s ^ "(" ^ commas ss ^ ")"
          end)
-  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
+  | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
     "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
     string_for_term format tm ^ ")"
   | string_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -324,7 +326,7 @@
   | string_for_format CNF_UEQ = tptp_cnf
   | string_for_format FOF = tptp_fof
   | string_for_format (TFF _) = tptp_tff
-  | string_for_format (THF _) = tptp_thf
+  | string_for_format (THF0 _) = tptp_thf
 
 fun string_for_problem_line format (Decl (ident, sym, ty)) =
     string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:04:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:34 2011 +0200
@@ -241,8 +241,8 @@
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
-      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
+     [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
+      (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -262,7 +262,8 @@
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
-     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
+     K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
+     (* FUDGE *)}
 
 val satallax = (satallaxN, satallax_config)
 
@@ -309,6 +310,8 @@
 fun is_old_vampire_version () =
   string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
 
+val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
@@ -340,9 +343,9 @@
          (0.333, (false, (500, FOF, "mono_tags?", sosN))),
          (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
       else
-        [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
-         (0.333, (false, (500, TFF Implicit, "simple", sosN))),
-         (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
+        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
+         (0.333, (false, (500, vampire_tff, "simple", sosN))),
+         (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -351,6 +354,8 @@
 
 (* Z3 with TPTP syntax *)
 
+val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+
 val z3_tptp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
@@ -368,10 +373,10 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
-        (0.25, (false, (125, FOF, "mono_guards?", ""))),
-        (0.125, (false, (62, TFF Implicit, "simple", ""))),
-        (0.125, (false, (31, TFF Implicit, "simple", "")))]}
+     K [(0.5, (false, (250, z3_tff, "simple", ""))),
+        (0.25, (false, (125, z3_tff, "simple", ""))),
+        (0.125, (false, (62, z3_tff, "simple", ""))),
+        (0.125, (false, (31, z3_tff, "simple", "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
@@ -381,7 +386,8 @@
 val systems = Synchronized.var "atp_systems" ([] : string list)
 
 fun get_systems () =
-  case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
+  case Isabelle_System.bash_output
+           "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     (output, 0) => split_lines output
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
@@ -449,31 +455,32 @@
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice config)
 
+val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
+
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
                (K (750, FOF, "mono_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
+               (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
+               (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
-               (K (250, TFF Implicit, "simple") (* FUDGE *))
+               (K (250, FOF, "mono_guards?") (* FUDGE *))
 val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"]
-                       (K (250, TFF Implicit, "simple") (* FUDGE *))
+  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             (K (100, TFF Explicit, "simple") (* FUDGE *))
+             (K (100, dumb_tff, "simple") (* FUDGE *))
 val remote_e_tofof =
-  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
+  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
+             Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:04:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:34 2011 +0200
@@ -320,7 +320,7 @@
   fun default c = const_prefix ^ lookup_const c
 in
   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
-    | make_fixed_const (SOME (THF With_Choice)) c =
+    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
         if c = choice_const then tptp_choice else default c
     | make_fixed_const _ c = default c
 end
@@ -625,7 +625,7 @@
   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   | is_type_level_monotonicity_based _ = false
 
-fun adjust_type_enc (THF _) type_enc = type_enc
+fun adjust_type_enc (THF0 _) type_enc = type_enc
   | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
     Simple_Types (First_Order, level)
   | adjust_type_enc format (Simple_Types (_, level)) =
@@ -889,16 +889,17 @@
                if is_tptp_equal s andalso length args = 2 then
                  IConst (`I tptp_equal, T, [])
                else
-                 (* Use a proxy even for partially applied THF equality, because
-                    the LEO-II and Satallax parsers complain about not being
-                    able to infer the type of "=". *)
+                 (* Use a proxy even for partially applied THF0 equality,
+                    because the LEO-II and Satallax parsers complain about not
+                    being able to infer the type of "=". *)
                  IConst (proxy_base |>> prefix const_prefix, T, T_args)
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)
           | NONE => if s = tptp_choice then
                       tweak_ho_quant tptp_choice T args
-                    else IConst (name, T, T_args))
+                    else
+                      IConst (name, T, T_args))
       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
       | intro _ _ tm = tm
   in intro true [] end
@@ -2177,12 +2178,10 @@
       |> (case format of
             CNF => ensure_cnf_problem
           | CNF_UEQ => filter_cnf_ueq_problem
-          | _ => I)
-      |> (if is_format_typed format andalso format <> TFF Implicit then
-            declare_undeclared_syms_in_atp_problem type_decl_prefix
-                                                   implicit_declsN
-          else
-            I)
+          | FOF => I
+          | TFF (_, TFF_Implicit) => I
+          | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
+                                                        implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names
     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
     val typed_helpers =