# HG changeset patch # User desharna # Date 1605795097 -3600 # Node ID f8d25850173b7f6d51d64045c8b43b6ad12fcafc # Parent 5f7d86b28ffb2062f96bbb6f44d25ea8a6bc0477 reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585 diff -r 5f7d86b28ffb -r f8d25850173b src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 19 14:46:49 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 19 15:11:37 2020 +0100 @@ -33,7 +33,7 @@ datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic - datatype thf_flavor = THF_Without_Choice | THF_With_Choice + datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | @@ -191,7 +191,7 @@ datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic -datatype thf_flavor = THF_Without_Choice | THF_With_Choice +datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | diff -r 5f7d86b28ffb -r f8d25850173b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 19 14:46:49 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 19 15:11:37 2020 +0100 @@ -162,6 +162,9 @@ fun is_type_enc_native (Native _) = true | is_type_enc_native _ = false +fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Bool_Free, _, _, _)) = false + | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true + | is_type_enc_full_higher_order _ = false fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true | is_type_enc_fool _ = false fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true @@ -692,7 +695,9 @@ end handle Same.SAME => error ("Unknown type encoding: " ^ quote s) -fun min_hologic THF_Without_Choice _ = THF_Without_Choice +fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free + | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free + | min_hologic THF_Without_Choice _ = THF_Without_Choice | min_hologic _ THF_Without_Choice = THF_Without_Choice | min_hologic _ _ = THF_With_Choice @@ -912,7 +917,7 @@ ((if s = \<^type_name>\fun\ andalso is_type_enc_higher_order type_enc then `I tptp_fun_type else if s = \<^type_name>\bool\ andalso - (is_type_enc_higher_order type_enc orelse is_type_enc_fool type_enc) then + (is_type_enc_full_higher_order type_enc orelse is_type_enc_fool type_enc) then `I tptp_bool_type else `make_fixed_type_const s, []), map term Ts) @@ -957,11 +962,17 @@ fun to_ho (ty as AType (((s, _), _), tys)) = if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty | to_ho _ = raise Fail "unexpected type" + fun to_lfho (ty as AType (((s, _), _), tys)) = + if s = tptp_fun_type then to_afun to_ho to_lfho tys + else if pred_sym then bool_atype + else to_atype ty + | to_lfho _ = raise Fail "unexpected type" fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys | to_fo _ _ = raise Fail "unexpected type" in - if is_type_enc_higher_order type_enc then to_ho + if is_type_enc_full_higher_order type_enc then to_ho + else if is_type_enc_higher_order type_enc then to_lfho else to_fo ary end @@ -1118,7 +1129,7 @@ val is_fool = is_type_enc_fool type_enc fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const in - if top_level orelse is_fool orelse is_type_enc_higher_order type_enc then + if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then (case (top_level, s) of (_, "c_False") => IConst (`I tptp_false, T, []) | (_, "c_True") => IConst (`I tptp_true, T, []) @@ -1277,7 +1288,7 @@ |> transform_elim_prop |> Object_Logic.atomize_term ctxt val need_trueprop = (fastype_of t = \<^typ>\bool\) - val is_ho = is_type_enc_higher_order type_enc + val is_ho = is_type_enc_full_higher_order type_enc in t |> need_trueprop ? HOLogic.mk_Trueprop |> (if is_ho then unextensionalize_def @@ -1290,7 +1301,7 @@ (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical reasons. *) fun should_use_iff_for_eq CNF _ = false - | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format) + | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format) | should_use_iff_for_eq _ _ = true fun make_formula ctxt format type_enc iff_for_eq name stature role t = @@ -1423,7 +1434,7 @@ |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @ ([tptp_equal, tptp_old_equal] |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false})) - |> not (is_type_enc_fool type_enc orelse is_type_enc_higher_order type_enc) + |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc) ? cons (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) @@ -1621,10 +1632,12 @@ (IConst ((s, _), _, _), _) => if is_pred_sym sym_tab s then tm else predicatify completish tm | _ => predicatify completish tm) + val is_ho = is_type_enc_higher_order type_enc + val is_full_ho = is_type_enc_full_higher_order type_enc + val is_fool = is_type_enc_fool type_enc val do_iterm = - (not (is_type_enc_higher_order type_enc) ? - (introduce_app_ops #> - not (is_type_enc_fool type_enc) ? introduce_predicators)) + (not is_ho ? introduce_app_ops) + #> (not (is_full_ho orelse is_fool) ? introduce_predicators) #> filter_type_args_in_iterm thy ctrss type_enc in update_iformula (formula_map do_iterm) end @@ -2622,7 +2635,7 @@ else Sufficient_App_Op_And_Predicator val lam_trans = - if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN + if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN else lam_trans val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts diff -r 5f7d86b28ffb -r f8d25850173b src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 19 14:46:49 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 19 15:11:37 2020 +0100 @@ -296,7 +296,7 @@ val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS val (format, enc) = if modern then - (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher") + (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher") else (TFF (Without_FOOL, Monomorphic), "mono_native") in