# HG changeset patch # User desharna # Date 1605194323 -3600 # Node ID 7b7227d9ae5e5024ec2d69ecd8c00803808b02d6 # Parent f5507622baa9fa007486c9d876eb5a671400afcc# Parent 20587c17cb20c0edf39989a7108477a225a9cb00 Merged diff -r f5507622baa9 -r 7b7227d9ae5e src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Nov 12 14:49:02 2020 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Nov 12 16:18:43 2020 +0100 @@ -47,6 +47,8 @@ \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} +\hyphenation{Isa-belle super-posi-tion zipper-posi-tion} + \begin{document} %%% TYPESETTING @@ -129,15 +131,15 @@ \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} -\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak -in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremail{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak +google.\allowbreak com}} To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is imported---this is rarely a problem in practice since it is part of -\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's -\texttt{src/HOL/Metis\_Examples} directory. -Comments and bug reports concerning Sledgehammer or this manual should be -directed to the author at \authoremail. +\textit{Main}. Examples of Sledgehammer use can be found in the +\texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports +concerning Sledgehammer or this manual should be directed to the author at +\authoremail. \section{Installation} @@ -219,7 +221,7 @@ (\texttt{libwww-perl}) installed. If you must use a proxy server to access the Internet, set the \texttt{http\_proxy} environment variable to the proxy, either in the environment in which Isabelle is launched or in your -\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few +\texttt{\$ISABELLE\_HOME\_USER/etc/\allowbreak settings} file. Here are a few examples: \prew @@ -360,16 +362,16 @@ \begin{enum} \item[\labelitemi] -The traditional relevance filter, called \emph{MePo} -(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact -(lemma, theorem, definition, or axiom) based upon how many constants that fact -shares with the conjecture. This process iterates to include facts relevant to -those just accepted. The constants are weighted to give unusual ones greater -significance. MePo copes best when the conjecture contains some unusual -constants; if all the constants are common, it is unable to discriminate among -the hundreds of facts that are picked up. The filter is also memoryless: It has -no information about how many times a particular fact has been used in a proof, -and it cannot learn. +The traditional relevance filter, \emph{MePo} +(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available +fact (lemma, theorem, definition, or axiom) based upon how many constants that +fact shares with the conjecture. This process iterates to include facts +relevant to those just accepted. The constants are weighted to give unusual +ones greater significance. MePo copes best when the conjecture contains some +unusual constants; if all the constants are common, it is unable to +discriminate among the hundreds of facts that are picked up. The filter is also +memoryless: It has no information about how many times a particular fact has +been used in a proof, and it cannot learn. \item[\labelitemi] An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for @@ -438,32 +440,7 @@ strongly encouraged to report this to the author at \authoremail. -\point{How can I tell whether a suggested proof is sound?} - -Earlier versions of Sledgehammer often suggested unsound proofs---either proofs -of nontheorems or simply proofs that rely on type-unsound inferences. This -is a thing of the past, unless you explicitly specify an unsound encoding -using \textit{type\_enc} (\S\ref{problem-encoding}). -% -Officially, the only form of ``unsoundness'' that lurks in the sound -encodings is related to missing characteristic theorems of datatypes. For -example, - -\prew -\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ -\textbf{sledgehammer} () -\postw - -suggests an argumentless \textit{metis} call that fails. However, the conjecture -does actually hold, and the \textit{metis} call can be repaired by adding -\textit{list.distinct}. -% -We hope to address this problem in a future version of Isabelle. In the -meantime, you can avoid it by passing the \textit{strict} option -(\S\ref{problem-encoding}). - - -\point{What are the \textit{full\_types}, \textit{no\_types}, and +\point{What are the \textit{full\_types}, \textit{no\_types}, and \\ \textit{mono\_tags} arguments to Metis?} The \textit{metis}~(\textit{full\_types}) proof method @@ -499,7 +476,7 @@ \textit{full\_types} option to \textit{metis} directly. -\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments +\point{And what are the \textit{lifting} and \textit{hide\_lams} \\ arguments to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate @@ -516,12 +493,7 @@ Sledgehammer includes a minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps -reconstruction, while also removing superfluous clutter from the proof scripts. - -In earlier versions of Sledgehammer, generated proofs were systematically -accompanied by a suggestion to invoke the minimization tool. This step is now -performed by default but can be disabled using the \textit{minimize} option -(\S\ref{mode-of-operation}). +reconstruction, while decluttering the proof scripts. \point{A strange error occurred---what should I do?} @@ -541,9 +513,9 @@ \point{Why are there so many options?} -Sledgehammer's philosophy should work out of the box, without user guidance. -Many of the options are meant to be used mostly by the Sledgehammer developers -for experiments. Of course, feel free to try them out if you are so inclined. +Sledgehammer's philosophy is that it should work out of the box, without user +guidance. Most of the options are meant to be used by the Sledgehammer +developers for experiments. \section{Command Syntax} @@ -825,11 +797,11 @@ \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition \cite{cruanes-2014} is a higher-order superposition prover developed by Simon -Cruanes and colleagues. To use Zipperposition, set the environment variable -\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the -\texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the -version number (e.g., ``2.0.1''). Sledgehammer has been tested with version -2.0.1. +Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the +environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that +contains the \texttt{zipperposition} executable and +\texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). +Sledgehammer has been tested with version 2.0.1. \end{enum} \end{sloppy} @@ -1098,10 +1070,10 @@ \item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); -\textit{mono\_args} (unsound):} \\ +\textit{mono\_args} \\ (unsound):} \\ Similar to \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and -\textit{raw\_mono\_args}, respectively but types are mangled in constant names +\textit{raw\_mono\_\allowbreak args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate $\const{g}(\tau, t)$ becomes a unary predicate $\const{g\_}\tau(t)$, and the binary function @@ -1112,14 +1084,23 @@ first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. -\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits -native higher-order types if the prover supports the TH0 syntax; otherwise, -falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is -monomorphized. +\item[\labelitemi] \textbf{\textit{mono\_native\_fool} (sound):} Exploits native +first-order types, including Booleans, if the prover supports the TFX0, TFX1, +TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_native}. The problem +is monomorphized. -\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native -first-order polymorphic types if the prover supports the TF1 or TH1 syntax; -otherwise, falls back on \textit{mono\_native}. +\item[\labelitemi] \textbf{\textit{mono\_native\_higher}, +\textit{mono\_native\_higher\_fool} \\ (sound):} Exploits native higher-order +types, including Booleans if ending with ``\textit{\_fool}'', if the prover +supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or +\textit{mono\_native\_fool}. The problem is monomorphized. + +\item[\labelitemi] \textbf{\textit{poly\_native}, \textit{poly\_native\_fool}, +\textit{poly\_native\_higher}, \\ \textit{poly\_native\_higher\_fool} (sound):} +Exploits native first-order polymorphic types if the prover supports the TF1, +TFX1, or TH1 syntax; otherwise, falls back on \textit{mono\_native}, +\textit{mono\_native\_fool}, \textit{mono\_native\_higher}, or +\textit{mono\_native\_higher\_fool}. \item[\labelitemi] \textbf{% @@ -1327,8 +1308,7 @@ \end{verbatim} This command specifies Sledgehammer as the action, using E as the prover with a -timeout of 10 seconds. The results are written to the file -\texttt{output/Huffman.log}. +timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Benchmarking Another Tool} @@ -1337,7 +1317,7 @@ \end{verbatim} This command specifies the \textbf{try0} command as the action, with a timeout -of 10 seconds. The results are written to the file \texttt{output/Huffman.log}. +of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Generating TPTP Files} diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/ATP.thy --- a/src/HOL/ATP.thy Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/ATP.thy Thu Nov 12 16:18:43 2020 +0100 @@ -137,4 +137,18 @@ ML_file \Tools/ATP/atp_problem_generate.ML\ ML_file \Tools/ATP/atp_proof_reconstruct.ML\ +ML \ +open ATP_Problem_Generate +val _ = @{print} (type_enc_of_string Strict "mono_native") +val _ = @{print} (type_enc_of_string Strict "mono_native_fool") +val _ = @{print} (type_enc_of_string Strict "poly_native") +val _ = @{print} (type_enc_of_string Strict "poly_native_fool") +val _ = @{print} (type_enc_of_string Strict "mono_native?") +val _ = @{print} (type_enc_of_string Strict "mono_native_fool?") +val _ = @{print} (type_enc_of_string Strict "erased") +(* val _ = @{print} (type_enc_of_string Strict "erased_fool") *) +val _ = @{print} (type_enc_of_string Strict "poly_guards") +(* val _ = @{print} (type_enc_of_string Strict "poly_guards_fool") *) +\ + end diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Nov 12 16:18:43 2020 +0100 @@ -33,4 +33,20 @@ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ +lemma "\ P" + sledgehammer [e, dont_slice, timeout = 1, type_enc = "mono_native_fool"] () + oops + +lemma "P (x \ f False) = P (f False \ x)" + sledgehammer [prover = dummy_tfx, overlord] () + oops + +lemma "P (y \ f False) = P (f False \ y)" + sledgehammer [e, overlord, type_enc = "mono_native_fool"] () + oops + +lemma "P (f True) \ P (f (x = x))" + sledgehammer [e, dont_slice, timeout = 1, type_enc = "mono_native_fool", dont_preplay] () + oops + end diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 12 16:18:43 2020 +0100 @@ -31,15 +31,16 @@ gen_prec : bool, gen_simp : bool} + datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic - datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice + datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | CNF_UEQ | FOF | - TFF of polymorphism | - THF of polymorphism * thf_choice | + TFF of fool * polymorphism | + THF of fool * polymorphism * thf_choice | DFG of polymorphism datatype atp_formula_role = @@ -188,15 +189,16 @@ gen_prec : bool, gen_simp : bool} +datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic -datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice +datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | CNF_UEQ | FOF | - TFF of polymorphism | - THF of polymorphism * thf_choice | + TFF of fool * polymorphism | + THF of fool * polymorphism * thf_choice | DFG of polymorphism datatype atp_formula_role = @@ -915,9 +917,6 @@ end in add 1 |> apsnd SOME end) -fun avoid_clash_with_alt_ergo_type_vars s = - if is_tptp_variable s then s else s ^ "_" - fun avoid_clash_with_dfg_keywords s = let val n = String.size s in if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse @@ -936,8 +935,7 @@ if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE val avoid_clash = (case format of - TFF Polymorphic => avoid_clash_with_alt_ergo_type_vars - | DFG _ => avoid_clash_with_dfg_keywords + DFG _ => avoid_clash_with_dfg_keywords | _ => I) val nice_name = nice_name avoid_clash diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 12 16:18:43 2020 +0100 @@ -153,7 +153,7 @@ No_Types datatype type_enc = - Native of order * polymorphism * type_level | + Native of order * fool * polymorphism * type_level | Guards of polymorphism * type_level | Tags of polymorphism * type_level @@ -162,13 +162,12 @@ fun is_type_enc_native (Native _) = true | is_type_enc_native _ = false -fun is_type_enc_full_higher_order (Native (Higher_Order THF_Predicate_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 +fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true + | is_type_enc_fool _ = false +fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true | is_type_enc_higher_order _ = false -fun polymorphism_of_type_enc (Native (_, poly, _)) = poly +fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly | polymorphism_of_type_enc (Guards (poly, _)) = poly | polymorphism_of_type_enc (Tags (poly, _)) = poly @@ -181,7 +180,7 @@ fun is_type_enc_mangling type_enc = polymorphism_of_type_enc type_enc = Mangled_Monomorphic -fun level_of_type_enc (Native (_, _, level)) = level +fun level_of_type_enc (Native (_, _, _, level)) = level | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level @@ -381,7 +380,7 @@ fun default c = const_prefix ^ lookup_const c in fun make_fixed_const _ \<^const_name>\HOL.eq\ = tptp_old_equal - | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c = + | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c = if c = choice_const then tptp_choice else default c | make_fixed_const _ c = default c end @@ -600,102 +599,125 @@ fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE fun type_enc_of_string strictness s = - (case try (unprefix "tc_") s of - SOME s => (SOME Type_Class_Polymorphic, s) - | NONE => - (case try (unprefix "poly_") s of - SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s) - | NONE => - (case try (unprefix "ml_poly_") s of - SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s) + let + val (poly, s) = + (case try (unprefix "tc_") s of + SOME s => (SOME Type_Class_Polymorphic, s) | NONE => - (case try (unprefix "raw_mono_") s of - SOME s => (SOME Raw_Monomorphic, s) + (case try (unprefix "poly_") s of + SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s) | NONE => - (case try (unprefix "mono_") s of - SOME s => (SOME Mangled_Monomorphic, s) - | NONE => (NONE, s)))))) - ||> (fn s => - (case try_unsuffixes queries s of - SOME s => - (case try_unsuffixes queries s of - SOME s => (Nonmono_Types (strictness, Non_Uniform), s) - | NONE => (Nonmono_Types (strictness, Uniform), s)) - | NONE => - (case try_unsuffixes ats s of - SOME s => (Undercover_Types, s) - | NONE => (All_Types, s)))) - |> (fn (poly, (level, core)) => - (case (core, (poly, level)) of - ("native", (SOME poly, _)) => + (case try (unprefix "ml_poly_") s of + SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s) + | NONE => + (case try (unprefix "raw_mono_") s of + SOME s => (SOME Raw_Monomorphic, s) + | NONE => + (case try (unprefix "mono_") s of + SOME s => (SOME Mangled_Monomorphic, s) + | NONE => (NONE, s)))))) + + val (level, s) = + case try_unsuffixes queries s of + SOME s => + (case try_unsuffixes queries s of + SOME s => (Nonmono_Types (strictness, Non_Uniform), s) + | NONE => (Nonmono_Types (strictness, Uniform), s)) + | NONE => + (case try_unsuffixes ats s of + SOME s => (Undercover_Types, s) + | NONE => (All_Types, s)) + + fun native_of_string s = + let + val (fool, core) = + (case try (unsuffix "_fool") s of + SOME s => (With_FOOL, s) + | NONE => (Without_FOOL, s)) + in + (case (core, poly) of + ("native", SOME poly) => (case (poly, level) of (Mangled_Monomorphic, _) => - if is_type_level_uniform level then Native (First_Order, Mangled_Monomorphic, level) - else raise Same.SAME + if is_type_level_uniform level then + Native (First_Order, fool, Mangled_Monomorphic, level) + else + raise Same.SAME | (Raw_Monomorphic, _) => raise Same.SAME - | (poly, All_Types) => Native (First_Order, poly, All_Types)) - | ("native_higher", (SOME poly, _)) => + | (poly, All_Types) => Native (First_Order, fool, poly, All_Types)) + | ("native_higher", SOME poly) => (case (poly, level) of (_, Nonmono_Types _) => raise Same.SAME | (_, Undercover_Types) => raise Same.SAME | (Mangled_Monomorphic, _) => if is_type_level_uniform level then - Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, level) + Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level) else raise Same.SAME | (poly as Raw_Polymorphic _, All_Types) => - Native (Higher_Order THF_With_Choice, poly, All_Types) - | _ => raise Same.SAME) - | ("guards", (SOME poly, _)) => - if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse - poly = Type_Class_Polymorphic then - raise Same.SAME - else - Guards (poly, level) - | ("tags", (SOME poly, _)) => - if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse - poly = Type_Class_Polymorphic then - raise Same.SAME - else - Tags (poly, level) - | ("args", (SOME poly, All_Types (* naja *))) => - if poly = Type_Class_Polymorphic then raise Same.SAME - else Guards (poly, Const_Types Without_Ctr_Optim) - | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) => - if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then - raise Same.SAME - else - Guards (poly, Const_Types With_Ctr_Optim) - | ("erased", (NONE, All_Types (* naja *))) => - Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) - | _ => raise Same.SAME)) + Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types) + | _ => raise Same.SAME)) + end + + fun nonnative_of_string core = + (case (core, poly, level) of + ("guards", SOME poly, _) => + if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse + poly = Type_Class_Polymorphic then + raise Same.SAME + else + Guards (poly, level) + | ("tags", SOME poly, _) => + if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse + poly = Type_Class_Polymorphic then + raise Same.SAME + else + Tags (poly, level) + | ("args", SOME poly, All_Types (* naja *)) => + if poly = Type_Class_Polymorphic then raise Same.SAME + else Guards (poly, Const_Types Without_Ctr_Optim) + | ("args", SOME poly, Nonmono_Types (_, Uniform) (* naja *)) => + if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then + raise Same.SAME + else + Guards (poly, Const_Types With_Ctr_Optim) + | ("erased", NONE, All_Types (* naja *)) => + Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) + | _ => raise Same.SAME) + in + if String.isPrefix "native" s then + native_of_string s + else + nonnative_of_string s + end handle Same.SAME => error ("Unknown type encoding: " ^ quote s) -fun min_hologic THF_Predicate_Free _ = THF_Predicate_Free - | min_hologic _ THF_Predicate_Free = THF_Predicate_Free - | min_hologic THF_Without_Choice _ = THF_Without_Choice +fun 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 adjust_fool Without_FOOL _ = Without_FOOL + | adjust_fool _ fool = fool + fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars | no_type_classes poly = poly -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)) = - Native (First_Order, poly, level) - | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) = - Native (First_Order, Mangled_Monomorphic, level) - | adjust_type_enc (TFF _) (Native (_, poly, level)) = - Native (First_Order, no_type_classes poly, level) - | adjust_type_enc format (Native (_, poly, level)) = +fun adjust_type_enc (THF (fool, Polymorphic, hologic)) (Native (order, fool', poly, level)) = + Native (adjust_hologic hologic order, adjust_fool fool fool', no_type_classes poly, level) + | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', _, level)) = + Native (adjust_hologic hologic order, adjust_fool fool fool', Mangled_Monomorphic, level) + | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', _, level)) = + Native (First_Order, adjust_fool fool fool', Mangled_Monomorphic, level) + | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) = + Native (First_Order, Without_FOOL, poly, level) + | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) = + Native (First_Order, Without_FOOL, Mangled_Monomorphic, level) + | adjust_type_enc (TFF (fool, _)) (Native (_, fool', poly, level)) = + Native (First_Order, adjust_fool fool fool', no_type_classes poly, level) + | adjust_type_enc format (Native (_, _, poly, level)) = adjust_type_enc format (Guards (no_type_classes poly, level)) | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = (if is_type_enc_sound type_enc then Tags else Guards) stuff @@ -838,8 +860,8 @@ T_args else (case type_enc of - Native (_, Raw_Polymorphic _, _) => T_args - | Native (_, Type_Class_Polymorphic, _) => T_args + Native (_, _, Raw_Polymorphic _, _) => T_args + | Native (_, _, Type_Class_Polymorphic, _) => T_args | _ => let fun gen_type_args _ _ [] = [] @@ -889,7 +911,8 @@ 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 + else if s = \<^type_name>\bool\ andalso + (is_type_enc_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) @@ -934,17 +957,11 @@ 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_full_higher_order type_enc then to_ho - else if is_type_enc_higher_order type_enc then to_lfho + if is_type_enc_higher_order type_enc then to_ho else to_fo ary end @@ -974,7 +991,7 @@ val tm_args = tm_args @ (case type_enc of - Native (_, Raw_Polymorphic Without_Phantom_Type_Vars, _) => + Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) => [ATerm ((TYPE_name, ty_args), [])] | _ => []) in AAtom (ATerm ((cl, ty_args), tm_args)) end @@ -1078,8 +1095,7 @@ fun introduce_proxies_in_iterm type_enc = let fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, []) - | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) - _ = + | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ = (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser limitation. This works in conjuction with special code in "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever @@ -1093,38 +1109,49 @@ fun intro top_level args (IApp (tm1, tm2)) = IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2) | intro top_level args (IConst (name as (s, _), T, T_args)) = + (* is_type_enc_fool *) (case proxify_const s of SOME proxy_base => - 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, []) - | (false, "c_Not") => IConst (`I tptp_not, T, []) - | (false, "c_conj") => IConst (`I tptp_and, T, []) - | (false, "c_disj") => IConst (`I tptp_or, T, []) - | (false, "c_implies") => IConst (`I tptp_implies, T, []) - | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args - | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args - | (false, s) => - if is_tptp_equal s then - if length args = 2 then - IConst (`I tptp_equal, T, []) + let + val argc = length args + val plain_const = IConst (name, T, []) + fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) + fun if_card_matches card x = if card = argc then x else plain_const + val is_fool = is_type_enc_fool type_enc + in + if top_level orelse is_fool orelse is_type_enc_higher_order type_enc then + (case (top_level, s) of + (_, "c_False") => IConst (`I tptp_false, T, []) + | (_, "c_True") => IConst (`I tptp_true, T, []) + | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, [])) + | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, [])) + | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, [])) + | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, [])) + | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args) + | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args) + | (false, s) => + if is_tptp_equal s then + if argc = 2 then + IConst (`I tptp_equal, T, []) + else if is_fool then + proxy_const () + else + (* Eta-expand partially applied THF equality, because the + LEO-II and Satallax parsers complain about not being able to + infer the type of "=". *) + let val i_T = domain_type T in + IAbs ((`I "Y", i_T), + IAbs ((`I "Z", i_T), + IApp (IApp (IConst (`I tptp_equal, T, []), + IConst (`I "Y", i_T, [])), + IConst (`I "Z", i_T, [])))) + end else - (* Eta-expand partially applied THF equality, because the - LEO-II and Satallax parsers complain about not being able to - infer the type of "=". *) - let val i_T = domain_type T in - IAbs ((`I "Y", i_T), - IAbs ((`I "Z", i_T), - IApp (IApp (IConst (`I tptp_equal, T, []), - IConst (`I "Y", i_T, [])), - IConst (`I "Z", i_T, [])))) - end - else - IConst (name, T, []) - | _ => IConst (name, T, [])) - else - IConst (proxy_base |>> prefix const_prefix, T, T_args) + plain_const + | _ => plain_const) + else + IConst (proxy_base |>> prefix const_prefix, T, T_args) + end | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args else IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) @@ -1251,7 +1278,7 @@ |> transform_elim_prop |> Object_Logic.atomize_term ctxt val need_trueprop = (fastype_of t = \<^typ>\bool\) - val is_ho = is_type_enc_full_higher_order type_enc + val is_ho = is_type_enc_higher_order type_enc in t |> need_trueprop ? HOLogic.mk_Trueprop |> (if is_ho then unextensionalize_def @@ -1264,7 +1291,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_full_higher_order format) + | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format) | should_use_iff_for_eq _ _ = true fun make_formula ctxt format type_enc iff_for_eq name stature role t = @@ -1397,7 +1424,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_full_higher_order type_enc) + |> not (is_type_enc_fool type_enc orelse is_type_enc_higher_order type_enc) ? cons (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) @@ -1596,8 +1623,9 @@ 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) - #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators) + (not (is_type_enc_higher_order type_enc) ? + (introduce_app_ops #> + not (is_type_enc_fool type_enc) ? introduce_predicators)) #> filter_type_args_in_iterm thy ctrss type_enc in update_iformula (formula_map do_iterm) end @@ -1679,10 +1707,10 @@ |> class_membs_of_types type_enc add_sorts_on_tvar |> map (class_atom type_enc))) #> (case type_enc of - Native (_, Type_Class_Polymorphic, _) => + Native (_, _, Type_Class_Polymorphic, _) => mk_atyquant AForall (map (fn TVar (z as (_, S)) => (AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts) - | Native (_, Raw_Polymorphic _, _) => + | Native (_, _, Raw_Polymorphic _, _) => mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts) | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))) @@ -2101,7 +2129,7 @@ fun decl_lines_of_classes type_enc = (case type_enc of - Native (_, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms) + Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms) | _ => K []) fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) = @@ -2161,7 +2189,7 @@ ? (fold (fold add_fact_syms) [conjs, facts] #> fold add_iterm_syms extra_tms #> (case type_enc of - Native (_, Raw_Polymorphic phantoms, _) => + Native (_, _, Raw_Polymorphic phantoms, _) => phantoms = Without_Phantom_Type_Vars ? add_TYPE_const () | Native _ => I | _ => fold add_undefined_const (var_types ()))) diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Nov 12 16:18:43 2020 +0100 @@ -58,6 +58,7 @@ val z3_tptpN : string val zipperpositionN : string val remote_prefix : string + val dummy_tfxN : string val agsyhol_core_rule : string val spass_input_rule : string @@ -120,6 +121,7 @@ val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" +val dummy_tfxN = "dummy_tfx" val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) val spass_input_rule = "Inp" diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Tools/ATP/scripts/dummy_atp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/scripts/dummy_atp Thu Nov 12 16:18:43 2020 +0100 @@ -0,0 +1,3 @@ +#!/bin/sh + +echo "SZS status Unknown" diff -r f5507622baa9 -r 7b7227d9ae5e src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 12 14:49:02 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Nov 12 16:18:43 2020 +0100 @@ -173,7 +173,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -195,7 +195,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -293,10 +293,12 @@ best_slices = fn ctxt => let val heuristic = Config.get ctxt e_selection_heuristic - val ehoh = string_ord (getenv "E_VERSION", "2.3") <> LESS + val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS val (format, enc) = - if ehoh then (THF (Monomorphic, THF_Predicate_Free), "mono_native_higher") - else (TFF Monomorphic, "mono_native") + if modern then + (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool") + else + (TFF (Without_FOOL, Monomorphic), "mono_native") in (* FUDGE *) if heuristic = e_smartN then @@ -355,7 +357,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -376,7 +378,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), THF (Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -399,7 +401,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -504,9 +506,9 @@ prem_role = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (((500, meshN), TFF Monomorphic, "mono_native", combs_or_liftingN, false), sosN)), - (0.333, (((150, meshN), TFF Monomorphic, "poly_tags??", combs_or_liftingN, false), sosN)), - (0.334, (((50, meshN), TFF Monomorphic, "mono_native", combs_or_liftingN, false), no_sosN))] + [(0.333, (((500, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), sosN)), + (0.333, (((150, meshN), TFF (Without_FOOL, Monomorphic), "poly_tags??", combs_or_liftingN, false), sosN)), + (0.334, (((50, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), no_sosN))] |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -525,10 +527,10 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (((250, meshN), TFF Monomorphic, "mono_native", combsN, false), "")), - (0.25, (((125, mepoN), TFF Monomorphic, "mono_native", combsN, false), "")), - (0.125, (((62, mashN), TFF Monomorphic, "mono_native", combsN, false), "")), - (0.125, (((31, meshN), TFF Monomorphic, "mono_native", combsN, false), ""))], + K [(0.5, (((250, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), + (0.25, (((125, mepoN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), + (0.125, (((62, mashN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), + (0.125, (((31, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -551,9 +553,9 @@ prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) - [(0.333, (((128, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), - (0.333, (((32, "meshN"), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)), - (0.334, (((512, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], + [(0.333, (((128, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), + (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)), + (0.334, (((512, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -636,29 +638,50 @@ val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] - (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] - (K (((250, ""), TFF Polymorphic, "poly_native", keep_lamsN, false), "") (* FUDGE *)) + (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] - (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *)) + (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] - (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) + (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] - (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["THF-4.4"] - (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) + (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.0"] - (K (((512, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + + +(* Dummy prover *) + +fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = + {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]), + arguments = K (K (K (K (K (K ""))))), + proof_delims = [], + known_failures = known_szs_status_failures, + prem_role = prem_role, + best_slices = + K [(1.0, (((200, ""), format, type_enc, + if is_format_higher_order format then keep_lamsN + else combsN, uncurried_aliases), ""))], + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + +val dummy_tfx_format = TFF (With_FOOL, Polymorphic) + +val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false +val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config) (* Setup *) @@ -696,7 +719,7 @@ val atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, - remote_vampire, remote_waldmeister, remote_zipperposition] + remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx] val _ = Theory.setup (fold add_atp atps)