# HG changeset patch
# User blanchet
# Date 1315396217 -7200
# Node ID 815afb08c079dabdd0e611b6699fc825d56acf78
# Parent  f4975fa4a2f8bcc7c484e48575ebe7346aafdb4a
tweaking polymorphic TFF and THF output

diff -r f4975fa4a2f8 -r 815afb08c079 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -403,11 +403,11 @@
    prem_kind = Hypothesis,
    best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
 
-val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
+val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
 val pff_config = dummy_config pff_format "poly_simple"
 val pff = (pffN, pff_config)
 
-val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
+val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
 val phf_config = dummy_config phf_format "poly_simple_higher"
 val phf = (phfN, phf_config)
 
diff -r f4975fa4a2f8 -r 815afb08c079 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -1361,21 +1361,21 @@
   K (add_iterm_syms_to_table ctxt explicit_apply)
   |> formula_fold NONE |> fact_lift
 
-val default_sym_tab_entries : (string * sym_info) list =
-  (prefixed_predicator_name,
-   {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
-       (* FIXME: needed? *) ::
+fun default_sym_tab_entries type_enc =
   (make_fixed_const NONE @{const_name undefined},
-   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
+                   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
   ([tptp_false, tptp_true]
    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
   ([tptp_equal, tptp_old_equal]
    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
+  |> not (is_type_enc_higher_order type_enc)
+     ? cons (prefixed_predicator_name,
+             {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
 
-fun sym_table_for_facts ctxt explicit_apply facts =
+fun sym_table_for_facts ctxt type_enc explicit_apply facts =
   ((false, []), Symtab.empty)
   |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
-  |> fold Symtab.update default_sym_tab_entries
+  |> fold Symtab.update (default_sym_tab_entries type_enc)
 
 fun min_ary_of sym_tab s =
   case Symtab.lookup sym_tab s of
@@ -1873,8 +1873,8 @@
        ? (fold (add_fact_syms true) conjs
           #> fold (add_fact_syms false) facts
           #> (case type_enc of
-                Simple_Types (_, poly, _) =>
-                if poly = Polymorphic then add_TYPE_const () else I
+                Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
+              | Simple_Types _ => I
               | _ => fold add_undefined_const (var_types ())))
   end
 
@@ -2205,11 +2205,13 @@
     val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                          hyp_ts concl_t facts
-    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
+    val sym_tab =
+      conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val firstorderize = firstorderize_fact thy format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
-    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
+    val sym_tab =
+      conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
     val helpers =
       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
               |> map firstorderize