tweaking polymorphic TFF and THF output
authorblanchet
Wed Sep 07 13:50:17 2011 +0200 (2011-09-07)
changeset 44786815afb08c079
parent 44785 f4975fa4a2f8
child 44787 3c0741556e19
tweaking polymorphic TFF and THF output
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 13:50:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -403,11 +403,11 @@
     1.4     prem_kind = Hypothesis,
     1.5     best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
     1.6  
     1.7 -val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
     1.8 +val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
     1.9  val pff_config = dummy_config pff_format "poly_simple"
    1.10  val pff = (pffN, pff_config)
    1.11  
    1.12 -val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
    1.13 +val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
    1.14  val phf_config = dummy_config phf_format "poly_simple_higher"
    1.15  val phf = (phfN, phf_config)
    1.16  
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     2.3 @@ -1361,21 +1361,21 @@
     2.4    K (add_iterm_syms_to_table ctxt explicit_apply)
     2.5    |> formula_fold NONE |> fact_lift
     2.6  
     2.7 -val default_sym_tab_entries : (string * sym_info) list =
     2.8 -  (prefixed_predicator_name,
     2.9 -   {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
    2.10 -       (* FIXME: needed? *) ::
    2.11 +fun default_sym_tab_entries type_enc =
    2.12    (make_fixed_const NONE @{const_name undefined},
    2.13 -   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
    2.14 +                   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
    2.15    ([tptp_false, tptp_true]
    2.16     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
    2.17    ([tptp_equal, tptp_old_equal]
    2.18     |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
    2.19 +  |> not (is_type_enc_higher_order type_enc)
    2.20 +     ? cons (prefixed_predicator_name,
    2.21 +             {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
    2.22  
    2.23 -fun sym_table_for_facts ctxt explicit_apply facts =
    2.24 +fun sym_table_for_facts ctxt type_enc explicit_apply facts =
    2.25    ((false, []), Symtab.empty)
    2.26    |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
    2.27 -  |> fold Symtab.update default_sym_tab_entries
    2.28 +  |> fold Symtab.update (default_sym_tab_entries type_enc)
    2.29  
    2.30  fun min_ary_of sym_tab s =
    2.31    case Symtab.lookup sym_tab s of
    2.32 @@ -1873,8 +1873,8 @@
    2.33         ? (fold (add_fact_syms true) conjs
    2.34            #> fold (add_fact_syms false) facts
    2.35            #> (case type_enc of
    2.36 -                Simple_Types (_, poly, _) =>
    2.37 -                if poly = Polymorphic then add_TYPE_const () else I
    2.38 +                Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
    2.39 +              | Simple_Types _ => I
    2.40                | _ => fold add_undefined_const (var_types ())))
    2.41    end
    2.42  
    2.43 @@ -2205,11 +2205,13 @@
    2.44      val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
    2.45        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
    2.46                           hyp_ts concl_t facts
    2.47 -    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
    2.48 +    val sym_tab =
    2.49 +      conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
    2.50      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
    2.51      val firstorderize = firstorderize_fact thy format type_enc sym_tab
    2.52      val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
    2.53 -    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
    2.54 +    val sym_tab =
    2.55 +      conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
    2.56      val helpers =
    2.57        sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    2.58                |> map firstorderize