# HG changeset patch
# User blanchet
# Date 1314291767 -7200
# Node ID c1884789ff80ea595bc1ea7efe897adf6d997031
# Parent  4c2242c8a96c8f2abb91b7df0a7b46562b9f1dc7
added config options to control two aspects of the translation, for evaluation purposes

diff -r 4c2242c8a96c -r c1884789ff80 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 13:55:52 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 19:02:47 2011 +0200
@@ -35,6 +35,8 @@
     Guards of polymorphism * type_level * type_uniformity |
     Tags of polymorphism * type_level * type_uniformity
 
+  val type_tag_idempotence : bool Config.T
+  val type_tag_arguments : bool Config.T
   val no_lambdasN : string
   val concealedN : string
   val liftingN : string
@@ -114,6 +116,11 @@
 
 type name = string * string
 
+val type_tag_idempotence =
+  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
+val type_tag_arguments =
+  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
+
 val no_lambdasN = "no_lambdas"
 val concealedN = "concealed"
 val liftingN = "lifting"
@@ -1257,7 +1264,7 @@
   ([tptp_equal, tptp_old_equal]
    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
 
-fun sym_table_for_facts ctxt format explicit_apply facts =
+fun sym_table_for_facts ctxt explicit_apply facts =
   ((false, []), Symtab.empty)
   |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
   |> fold Symtab.update default_sym_tab_entries
@@ -1998,7 +2005,8 @@
       end
   in
     [] |> not pred_sym ? add_formula_for_res
-       |> fold add_formula_for_arg (ary - 1 downto 0)
+       |> Config.get ctxt type_tag_arguments
+          ? fold add_formula_for_arg (ary - 1 downto 0)
   end
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
@@ -2060,11 +2068,12 @@
                syms []
   in mono_lines @ decl_lines end
 
-fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
+fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
+    Config.get ctxt type_tag_idempotence andalso
     poly <> Mangled_Monomorphic andalso
     ((level = All_Types andalso uniformity = Nonuniform) orelse
      is_type_level_monotonicity_based level)
-  | needs_type_tag_idempotence _ = false
+  | needs_type_tag_idempotence _ _ = false
 
 fun offset_of_heading_in_problem _ [] j = j
   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -2116,12 +2125,12 @@
     val (fact_names, (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 format explicit_apply
+    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val repair = repair_fact ctxt format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
     val repaired_sym_tab =
-      conjs @ facts |> sym_table_for_facts ctxt format (SOME false)
+      conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
                        |> map repair
@@ -2134,7 +2143,7 @@
       0 upto length helpers - 1 ~~ helpers
       |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
                                     type_enc)
-      |> (if needs_type_tag_idempotence type_enc then
+      |> (if needs_type_tag_idempotence ctxt type_enc then
             cons (type_tag_idempotence_fact type_enc)
           else
             I)