# HG changeset patch # User blanchet # Date 1527002102 -7200 # Node ID c45067867860307d0cceaf1577d30e13b5f795e4 # Parent 949d938047400aab6cae55c6f91d9d383bcdd6db added lambda-free HO output for Ehoh (higher-order E prototype) diff -r 949d93804740 -r c45067867860 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue May 22 11:08:37 2018 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Tue May 22 17:15:02 2018 +0200 @@ -768,6 +768,10 @@ Be aware that E-Par is experimental software. It has been known to generate zombie processes. Use at your own risks. +\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of +E that supports a $\lambda$-free fragment of higher-order logic. Use at your +own risks. + \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the diff -r 949d93804740 -r c45067867860 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 22 11:08:37 2018 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 22 17:15:02 2018 +0200 @@ -32,7 +32,7 @@ gen_simp : bool} datatype polymorphism = Monomorphic | Polymorphic - datatype thf_choice = THF_Without_Choice | THF_With_Choice + datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | @@ -188,7 +188,7 @@ gen_simp : bool} datatype polymorphism = Monomorphic | Polymorphic -datatype thf_choice = THF_Without_Choice | THF_With_Choice +datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | diff -r 949d93804740 -r c45067867860 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 11:08:37 2018 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 17:15:02 2018 +0200 @@ -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_Free, _, _)) = false + | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true + | is_type_enc_full_higher_order _ = false fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true | is_type_enc_higher_order _ = false @@ -668,17 +671,22 @@ | _ => raise Same.SAME)) handle Same.SAME => error ("Unknown type encoding: " ^ quote s) -fun adjust_order THF_Without_Choice (Higher_Order _) = - Higher_Order THF_Without_Choice - | adjust_order _ type_enc = type_enc +fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free + | min_hologic _ THF_Lambda_Free = THF_Lambda_Free + | min_hologic THF_Without_Choice _ = THF_Without_Choice + | min_hologic _ THF_Without_Choice = THF_Without_Choice + | min_hologic _ _ = THF_With_Choice + +fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic') + | adjust_hologic _ type_enc = type_enc fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars | no_type_classes poly = poly -fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) = - Native (adjust_order choice order, no_type_classes poly, level) - | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) = - Native (adjust_order choice order, Mangled_Monomorphic, level) +fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) = + Native (adjust_hologic hologic order, no_type_classes poly, level) + | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) = + Native (adjust_hologic hologic order, Mangled_Monomorphic, level) | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) = @@ -881,14 +889,15 @@ fun raw_atp_type_of_typ type_enc = let fun term (Type (s, Ts)) = - AType ((case (is_type_enc_higher_order type_enc, s) of - (true, @{type_name bool}) => `I tptp_bool_type - | (true, @{type_name fun}) => `I tptp_fun_type - | _ => - if s = fused_infinite_type_name andalso is_type_enc_native type_enc then - `I tptp_individual_type - else - `make_fixed_type_const s, []), map term Ts) + AType + ((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_full_higher_order type_enc then + `I tptp_bool_type + else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then + `I tptp_individual_type + else + `make_fixed_type_const s, []), map term Ts) | term (TFree (s, _)) = AType ((`make_tfree s, []), []) | term (TVar z) = AType ((tvar_name z, []), []) in term end @@ -927,13 +936,22 @@ if is_type_enc_polymorphic type_enc then to_poly_atype else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) + 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" - 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" - in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end + in + 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 fun native_atp_type_of_typ type_enc pred_sym ary = native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc @@ -1082,7 +1100,7 @@ | intro top_level args (IConst (name as (s, _), T, T_args)) = (case proxify_const s of SOME proxy_base => - if top_level orelse is_type_enc_higher_order type_enc then + if top_level 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, []) @@ -1238,7 +1256,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 @@ -1251,7 +1269,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 = @@ -1393,7 +1411,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_higher_order type_enc) + |> not (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}) @@ -1592,7 +1610,8 @@ if is_pred_sym sym_tab s then tm else predicatify completish tm | _ => predicatify completish tm) val do_iterm = - not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators) + (not (is_type_enc_higher_order type_enc) ? introduce_app_ops) + #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators) #> filter_type_args_in_iterm thy ctrss type_enc in update_iformula (formula_map do_iterm) end @@ -2595,7 +2614,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 949d93804740 -r c45067867860 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 22 11:08:37 2018 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 22 17:15:02 2018 +0200 @@ -54,6 +54,7 @@ val e_parN : string val e_sineN : string val e_tofofN : string + val ehohN : string val iproverN : string val iprover_eqN : string val leo2N : string @@ -124,6 +125,7 @@ val e_parN = "e_par" val e_sineN = "e_sine" val e_tofofN = "e_tofof" +val ehohN = "ehoh" val iproverN = "iprover" val iprover_eqN = "iprover_eq" val leo2N = "leo2" diff -r 949d93804740 -r c45067867860 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 11:08:37 2018 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 17:15:02 2018 +0200 @@ -353,6 +353,32 @@ val e_par = (e_parN, fn () => e_par_config) +(* Ehoh *) + +val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free) + +val ehoh_config : atp_config = + {exec = fn _ => (["E_HOME"], ["eprover"]), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^ + string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name, + proof_delims = + [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ + tstp_proof_delims, + known_failures = + [(TimedOut, "Failure: Resource limit exceeded (time)"), + (TimedOut, "time limit exceeded")] @ + known_szs_status_failures, + prem_role = Conjecture, + best_slices = + (* FUDGE *) + K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))], + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + +val ehoh = (ehohN, fn () => ehoh_config) + + (* iProver *) val iprover_config : atp_config = @@ -792,10 +818,11 @@ end val atps = - [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire, - z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine, - remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax, - remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new] + [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass, + vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, + remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, + remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister, + remote_waldmeister_new] val _ = Theory.setup (fold add_atp atps)