src/HOL/Tools/ATP/atp_translate.ML
changeset 44496 c1884789ff80
parent 44495 4c2242c8a96c
child 44499 8870232a87ad
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 13:55:52 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 19:02:47 2011 +0200
     1.3 @@ -35,6 +35,8 @@
     1.4      Guards of polymorphism * type_level * type_uniformity |
     1.5      Tags of polymorphism * type_level * type_uniformity
     1.6  
     1.7 +  val type_tag_idempotence : bool Config.T
     1.8 +  val type_tag_arguments : bool Config.T
     1.9    val no_lambdasN : string
    1.10    val concealedN : string
    1.11    val liftingN : string
    1.12 @@ -114,6 +116,11 @@
    1.13  
    1.14  type name = string * string
    1.15  
    1.16 +val type_tag_idempotence =
    1.17 +  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
    1.18 +val type_tag_arguments =
    1.19 +  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
    1.20 +
    1.21  val no_lambdasN = "no_lambdas"
    1.22  val concealedN = "concealed"
    1.23  val liftingN = "lifting"
    1.24 @@ -1257,7 +1264,7 @@
    1.25    ([tptp_equal, tptp_old_equal]
    1.26     |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
    1.27  
    1.28 -fun sym_table_for_facts ctxt format explicit_apply facts =
    1.29 +fun sym_table_for_facts ctxt explicit_apply facts =
    1.30    ((false, []), Symtab.empty)
    1.31    |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
    1.32    |> fold Symtab.update default_sym_tab_entries
    1.33 @@ -1998,7 +2005,8 @@
    1.34        end
    1.35    in
    1.36      [] |> not pred_sym ? add_formula_for_res
    1.37 -       |> fold add_formula_for_arg (ary - 1 downto 0)
    1.38 +       |> Config.get ctxt type_tag_arguments
    1.39 +          ? fold add_formula_for_arg (ary - 1 downto 0)
    1.40    end
    1.41  
    1.42  fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
    1.43 @@ -2060,11 +2068,12 @@
    1.44                 syms []
    1.45    in mono_lines @ decl_lines end
    1.46  
    1.47 -fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
    1.48 +fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
    1.49 +    Config.get ctxt type_tag_idempotence andalso
    1.50      poly <> Mangled_Monomorphic andalso
    1.51      ((level = All_Types andalso uniformity = Nonuniform) orelse
    1.52       is_type_level_monotonicity_based level)
    1.53 -  | needs_type_tag_idempotence _ = false
    1.54 +  | needs_type_tag_idempotence _ _ = false
    1.55  
    1.56  fun offset_of_heading_in_problem _ [] j = j
    1.57    | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
    1.58 @@ -2116,12 +2125,12 @@
    1.59      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
    1.60        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
    1.61                           hyp_ts concl_t facts
    1.62 -    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt format explicit_apply
    1.63 +    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
    1.64      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
    1.65      val repair = repair_fact ctxt format type_enc sym_tab
    1.66      val (conjs, facts) = (conjs, facts) |> pairself (map repair)
    1.67      val repaired_sym_tab =
    1.68 -      conjs @ facts |> sym_table_for_facts ctxt format (SOME false)
    1.69 +      conjs @ facts |> sym_table_for_facts ctxt (SOME false)
    1.70      val helpers =
    1.71        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    1.72                         |> map repair
    1.73 @@ -2134,7 +2143,7 @@
    1.74        0 upto length helpers - 1 ~~ helpers
    1.75        |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
    1.76                                      type_enc)
    1.77 -      |> (if needs_type_tag_idempotence type_enc then
    1.78 +      |> (if needs_type_tag_idempotence ctxt type_enc then
    1.79              cons (type_tag_idempotence_fact type_enc)
    1.80            else
    1.81              I)