--- a/NEWS Mon Feb 03 19:50:16 2014 +0100
+++ b/NEWS Mon Feb 03 19:50:38 2014 +0100
@@ -115,6 +115,8 @@
* Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
* Sledgehammer:
+ - New option:
+ smt_proofs
- Renamed options:
isar_compress ~> compress_isar
isar_try0 ~> try0_isar
--- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 19:50:38 2014 +0100
@@ -1103,7 +1103,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
\keyw{simps\_of\_case} command provided by the theory
-\verb|~~/src/HOL/Library/Simps_Case_Conv|.
+\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
*}
simps_of_case at_simps: at.simps
--- a/src/Doc/Datatypes/document/root.tex Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Doc/Datatypes/document/root.tex Mon Feb 03 19:50:38 2014 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper]{article} % fleqn
+\usepackage[T1]{fontenc}
\usepackage{cite}
\usepackage{enumitem}
\usepackage{footmisc}
@@ -17,6 +18,8 @@
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\newbox\boxA
\setbox\boxA=\hbox{\ }
\parindent=4\wd\boxA
@@ -52,6 +55,9 @@
Dmitriy Traytel \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
\hbox{}}
+
+\urlstyle{tt}
+
\begin{document}
\maketitle
--- a/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 03 19:50:38 2014 +0100
@@ -2640,9 +2640,11 @@
\item @{command (HOL) "code_identifier"} associates a a series of symbols
(constants, type constructors, classes, class relations, instances,
module names) with target-specific hints how these symbols shall be named.
- \emph{Warning:} These hints are still subject to name disambiguation.
+ These hints gain precedence over names for symbols with no hints at all.
+ Conflicting hints are subject to name disambiguation.
@{command (HOL) "code_modulename"} is a legacy variant for
- @{command (HOL) "code_identifier"} on module names. It is at the discretion
+ @{command (HOL) "code_identifier"} on module names.
+ \emph{Warning:} It is at the discretion
of the user to ensure that name prefixes of identifiers in compound
statements like type classes or datatypes are still the same.
--- a/src/Doc/Nitpick/document/root.tex Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex Mon Feb 03 19:50:38 2014 +0100
@@ -40,6 +40,8 @@
\urlstyle{tt}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\begin{document}
%%% TYPESETTING
@@ -127,7 +129,7 @@
To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
imported---this is rarely a problem in practice since it is part of
\textit{Main}. The examples presented in this manual can be found
-in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
+in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory.
The known bugs and limitations at the time of writing are listed in
\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either
the tool or the manual should be directed to the author at \authoremail.
--- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:50:38 2014 +0100
@@ -42,6 +42,8 @@
\urlstyle{tt}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\begin{document}
%%% TYPESETTING
@@ -115,7 +117,7 @@
The result of a successful proof search is some source text that usually (but
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
-proof relies on the general-purpose \textit{metis} proof method, which
+proof typically relies on the general-purpose \textit{metis} proof method, which
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
the kernel. Thus its results are correct by construction.
@@ -294,7 +296,7 @@
Waldmeister is run only for unit equational problems, where the goal's
conclusion is a (universally quantified) equation.
-For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
+For each successful prover, Sledgehammer gives a one-line \textit{metis} or
\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
@@ -306,7 +308,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt} one-liners.
+readable and also faster than the \textit{metis} or \textit{smt} one-line proofs.
This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -357,7 +359,7 @@
if that helps.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, in addition to one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-line \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress\_isar} (\S\ref{output-format}).
@@ -461,9 +463,8 @@
\begin{enum}
\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
-obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
-Since the steps are fairly small, \textit{metis} is more likely to be able to
-replay them.
+obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis}
+and the other Isabelle proof methods are more likely to be able to replay them.
\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
It is usually stronger, but you need to either have Z3 available to replay the
@@ -523,8 +524,8 @@
versions of Metis. It is somewhat slower than \textit{metis}, but the proof
search is fully typed, and it also includes more powerful rules such as the
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
-higher-order places (e.g., in set comprehensions). The method kicks in
-automatically as a fallback when \textit{metis} fails, and it is sometimes
+higher-order places (e.g., in set comprehensions). The method is automatically
+tried as a fallback when \textit{metis} fails, and it is sometimes
generated by Sledgehammer instead of \textit{metis} if the proof obviously
requires type information or if \textit{metis} failed when Sledgehammer
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
@@ -1067,9 +1068,9 @@
\opdefault{max\_facts}{smart\_int}{smart}
Specifies the maximum number of facts that may be returned by the relevance
-filter. If the option is set to \textit{smart}, it is set to a value that was
-empirically found to be appropriate for the prover. Typical values range between
-50 and 1000.
+filter. If the option is set to \textit{smart} (the default), it effectively
+takes a value that was empirically found to be appropriate for the prover.
+Typical values range between 50 and 1000.
For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
@@ -1093,9 +1094,9 @@
Specifies the maximum number of monomorphic instances to generate beyond
\textit{max\_facts}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 100.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover. For
+most provers, this value is 100.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1104,9 +1105,9 @@
Specifies the maximum number of iterations for the monomorphization fixpoint
construction. The higher this limit is, the more monomorphic instances are
potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it is set to a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 3.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover.
+For most provers, this value is 3.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1296,12 +1297,11 @@
\textit{overlord} (\S\ref{mode-of-operation}).}
\opsmart{isar\_proofs}{no\_isar\_proofs}
-Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. The construction of Isar proof is still experimental and
-may sometimes fail; however, when they succeed they are usually faster and more
-intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
-(the default), Isar proofs are only generated when no working one-liner
-\textit{metis} proof is available.
+Specifies whether Isar proofs should be output in addition to one-line proofs.
+The construction of Isar proof is still experimental and may sometimes fail;
+however, when they succeed they are usually faster and more intelligible than
+one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are only generated when no working one-line proof is available.
\opdefault{compress\_isar}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
@@ -1313,9 +1313,14 @@
\optrue{try0\_isar}{dont\_try0\_isar}
Specifies whether standard proof methods such as \textit{auto} and
-\textit{blast} should be tried as alternatives to \textit{metis} and
-\textit{smt} in Isar proofs. The collection of methods is roughly the same as
-for the \textbf{try0} command.
+\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
+The collection of methods is roughly the same as for the \textbf{try0} command.
+
+\opsmart{smt\_proofs}{no\_smt\_proofs}
+Specifies whether the \textit{smt} proof method should be tried as an
+alternative to \textit{metis}. If the option is set to \textit{smart} (the
+default), the \textit{smt} method is used for one-line proofs but not in Isar
+proofs.
\end{enum}
\subsection{Authentication}
@@ -1351,10 +1356,10 @@
searching for a proof. This excludes problem preparation and is a soft limit.
\opdefault{preplay\_timeout}{float}{\upshape 2}
-Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
-should spend trying to ``preplay'' the found proof. If this option is set to 0,
-no preplaying takes place, and no timing information is displayed next to the
-suggested \textit{metis} calls.
+Specifies the maximum number of seconds that \textit{metis} or other proof
+methods should spend trying to ``preplay'' the found proof. If this option
+is set to 0, no preplaying takes place, and no timing information is displayed
+next to the suggested proof method calls.
\nopagebreak
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 19:50:38 2014 +0100
@@ -19,7 +19,7 @@
(*refers to minimization attempted by Mirabelle*)
val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*)
-val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
+val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
@@ -43,8 +43,7 @@
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun reconstructor_tag reconstructor id =
- "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
+fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
val separator = "-----"
@@ -130,16 +129,16 @@
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
nontriv_success, proofs, time, timeout, lemmas, posns)
-datatype reconstructor_mode =
+datatype proof_method_mode =
Unminimized | Minimized | UnminimizedFT | MinimizedFT
datatype data = Data of {
sh: sh_data,
min: min_data,
- re_u: re_data, (* reconstructor with unminimized set of lemmas *)
- re_m: re_data, (* reconstructor with minimized set of lemmas *)
- re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
- re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
+ re_u: re_data, (* proof method with unminimized set of lemmas *)
+ re_m: re_data, (* proof method with minimized set of lemmas *)
+ re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *)
+ re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *)
mini: bool (* with minimization *)
}
@@ -218,39 +217,39 @@
fun inc_min_ab_ratios r = map_min_data
(fn (succs, ab_ratios) => (succs, ab_ratios+r))
-val inc_reconstructor_calls = map_re_data
+val inc_proof_method_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_success = map_re_data
+val inc_proof_method_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_nontriv_calls = map_re_data
+val inc_proof_method_nontriv_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_nontriv_success = map_re_data
+val inc_proof_method_nontriv_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_proofs = map_re_data
+val inc_proof_method_proofs = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
-fun inc_reconstructor_time m t = map_re_data
+fun inc_proof_method_time m t = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
-val inc_reconstructor_timeout = map_re_data
+val inc_proof_method_timeout = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
-fun inc_reconstructor_lemmas m n = map_re_data
+fun inc_proof_method_lemmas m n = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
-fun inc_reconstructor_posns m pos = map_re_data
+fun inc_proof_method_posns m pos = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
@@ -292,19 +291,19 @@
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
re_nontriv_success, re_proofs, re_time, re_timeout,
(lemmas, lems_sos, lems_max), re_posns) =
- (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
- log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
+ (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls);
+ log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^
" (proof: " ^ str re_proofs ^ ")");
- log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
+ log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout);
log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
- log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
- log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
+ log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls);
+ log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^
" (proof: " ^ str re_proofs ^ ")");
- log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
- log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
- log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
- log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
- log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
+ log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas);
+ log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos);
+ log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max);
+ log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time));
+ log ("Average time for successful " ^ tag ^ "proof method calls: " ^
str3 (avg_time re_time re_success));
if tag=""
then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
@@ -325,7 +324,7 @@
fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
fun log_re tag m =
log_re_data log tag sh_calls (tuple_of_re_data m)
- fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+ fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
(log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
in
if sh_calls > 0
@@ -334,14 +333,14 @@
log_sh_data log (tuple_of_sh_data sh);
log "";
if not mini
- then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
+ then log_proof_method ("", re_u) ("fully-typed ", re_uft)
else
app_if re_u (fn () =>
- (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
+ (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
log "";
app_if re_m (fn () =>
(log_min_data log (tuple_of_min_data min); log "";
- log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
+ log_proof_method ("", re_m) ("fully-typed ", re_mft))))))
else ()
end
@@ -385,8 +384,8 @@
andalso not (String.isSubstring "may fail" s)
(* Fragile hack *)
-fun reconstructor_from_msg args msg =
- (case AList.lookup (op =) args reconstructorK of
+fun proof_method_from_msg args msg =
+ (case AList.lookup (op =) args proof_methodK of
SOME name => name
| NONE =>
if exists good_line (split_lines msg) then
@@ -460,8 +459,8 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Prover.plain_metis,
- Sledgehammer_Reconstructor.Play_Failed),
+ preplay = Lazy.value (Sledgehammer_Proof_Methods.Metis_Method (NONE, NONE),
+ Sledgehammer_Proof_Methods.Play_Failed),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
: Sledgehammer_Prover.prover_result,
@@ -501,7 +500,7 @@
in
-fun run_sledgehammer trivial args reconstructor named_thms id
+fun run_sledgehammer trivial args proof_method named_thms id
({pre=st, log, pos, ...}: Mirabelle.run_args) =
let
val thy = Proof.theory_of st
@@ -557,7 +556,7 @@
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
change_data id (inc_sh_time_prover time_prover);
- reconstructor := reconstructor_from_msg args msg;
+ proof_method := proof_method_from_msg args msg;
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -572,7 +571,7 @@
end
-fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
+fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
let
val thy = Proof.theory_of st
val {goal, ...} = Proof.goal st
@@ -614,7 +613,7 @@
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
- else (reconstructor := reconstructor_from_msg args msg;
+ else (meth := proof_method_from_msg args msg;
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
@@ -629,10 +628,10 @@
("slice", "false"),
("timeout", timeout |> Time.toSeconds |> string_of_int)]
-fun run_reconstructor trivial full m name reconstructor named_thms id
+fun run_proof_method trivial full m name meth named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
- fun do_reconstructor named_thms ctxt =
+ fun do_method named_thms ctxt =
let
val ref_of_str =
suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
@@ -646,56 +645,56 @@
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
(override_params prover type_enc (my_timeout time_slice)) fact_override
in
- if !reconstructor = "sledgehammer_tac" then
+ if !meth = "sledgehammer_tac" then
sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
ORELSE' SMT_Solver.smt_tac ctxt thms
- else if !reconstructor = "smt" then
+ else if !meth = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full then
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
- else if String.isPrefix "metis (" (!reconstructor) then
+ else if String.isPrefix "metis (" (!meth) then
let
val (type_encs, lam_trans) =
- !reconstructor
+ !meth
|> Outer_Syntax.scan Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
- else if !reconstructor = "metis" then
+ else if !meth = "metis" then
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
else
K all_tac
end
- fun apply_reconstructor named_thms =
- Mirabelle.can_apply timeout (do_reconstructor named_thms) st
+ fun apply_method named_thms =
+ Mirabelle.can_apply timeout (do_method named_thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
- | with_time (true, t) = (change_data id (inc_reconstructor_success m);
+ | with_time (true, t) = (change_data id (inc_proof_method_success m);
if trivial then ()
- else change_data id (inc_reconstructor_nontriv_success m);
- change_data id (inc_reconstructor_lemmas m (length named_thms));
- change_data id (inc_reconstructor_time m t);
- change_data id (inc_reconstructor_posns m (pos, trivial));
- if name = "proof" then change_data id (inc_reconstructor_proofs m) else ();
+ else change_data id (inc_proof_method_nontriv_success m);
+ change_data id (inc_proof_method_lemmas m (length named_thms));
+ change_data id (inc_proof_method_time m t);
+ change_data id (inc_proof_method_posns m (pos, trivial));
+ if name = "proof" then change_data id (inc_proof_method_proofs m) else ();
"succeeded (" ^ string_of_int t ^ ")")
- fun timed_reconstructor named_thms =
- (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
- handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false))
+ fun timed_method named_thms =
+ (with_time (Mirabelle.cpu_time apply_method named_thms), true)
+ handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
val _ = log separator
- val _ = change_data id (inc_reconstructor_calls m)
- val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m)
+ val _ = change_data id (inc_proof_method_calls m)
+ val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m)
in
named_thms
- |> timed_reconstructor
- |>> log o prefix (reconstructor_tag reconstructor id)
+ |> timed_method
+ |>> log o prefix (proof_method_tag meth id)
|> snd
end
@@ -717,7 +716,7 @@
if !num_sledgehammer_calls > max_calls then ()
else
let
- val reconstructor = Unsynchronized.ref ""
+ val meth = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
@@ -728,33 +727,28 @@
Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
else false
- fun apply_reconstructor m1 m2 =
+ fun apply_method m1 m2 =
if metis_ft
then
- if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st)
+ if not (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false m1 name meth (these (!named_thms))) id st)
then
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial true m2 name reconstructor
- (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ())
else ()
else
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
in
change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
- named_thms) id st;
+ Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
if is_some (!named_thms)
then
- (apply_reconstructor Unminimized UnminimizedFT;
+ (apply_method Unminimized UnminimizedFT;
if minimize andalso not (null (these (!named_thms)))
then
- (Mirabelle.catch minimize_tag
- (run_minimize args reconstructor named_thms) id st;
- apply_reconstructor Minimized MinimizedFT)
+ (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st;
+ apply_method Minimized MinimizedFT)
else ())
else ()
end
--- a/src/HOL/Sledgehammer.thy Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Feb 03 19:50:38 2014 +0100
@@ -17,7 +17,7 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 19:50:38 2014 +0100
@@ -28,9 +28,9 @@
val partial_type_encs : string list
val default_metis_lam_trans : string
- val metis_call : string -> string -> string
val forall_of : term -> term -> term
val exists_of : term -> term -> term
+ val type_enc_aliases : (string * string list) list
val unalias_type_enc : string -> string list
val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
(string, string atp_type) atp_term -> term
@@ -84,17 +84,6 @@
val default_metis_lam_trans = combsN
-fun metis_call type_enc lam_trans =
- let
- val type_enc =
- (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
- [alias] => alias
- | _ => type_enc)
- val opts =
- [] |> type_enc <> partial_typesN ? cons type_enc
- |> lam_trans <> default_metis_lam_trans ? cons lam_trans
- in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-
fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
| term_name' _ = ""
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 19:50:38 2014 +0100
@@ -129,6 +129,17 @@
| ord => ord
in {weight = weight, precedence = precedence} end
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
+ [alias] => alias
+ | _ => type_enc)
+ val opts =
+ [] |> type_enc <> partial_typesN ? cons type_enc
+ |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+
exception METIS_UNPROVABLE of unit
(* Main function to start Metis proof and reconstruction *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 19:50:38 2014 +0100
@@ -10,7 +10,7 @@
sig
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type minimize_command = Sledgehammer_Proof_Methods.minimize_command
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
@@ -33,6 +33,7 @@
open ATP_Problem_Generate
open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_Minimize
@@ -49,13 +50,11 @@
NONE
|> fold (fn candidate =>
fn accum as SOME _ => accum
- | NONE => if member (op =) codes candidate then SOME candidate
- else NONE)
- ordered_outcome_codes
+ | NONE => if member (op =) codes candidate then SOME candidate else NONE)
+ ordered_outcome_codes
|> the_default unknownN
-fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
- n goal =
+fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
(quote name,
(if verbose then
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
@@ -211,88 +210,91 @@
fun string_of_factss factss =
if forall (null o snd) factss then
"Found no relevant facts."
- else case factss of
- [(_, facts)] => string_of_facts facts
- | _ =>
- factss
- |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
- |> space_implode "\n\n"
+ else
+ (case factss of
+ [(_, facts)] => string_of_facts facts
+ | _ =>
+ factss
+ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
+ |> space_implode "\n\n")
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
output_result i (fact_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
- else case subgoal_count state of
- 0 =>
+ else
+ (case subgoal_count state of
+ 0 =>
((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
- | n =>
- let
- val _ = Proof.assert_backward state
- val print =
- if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
- val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug)
- val ctxt = Proof.context_of state
- val {facts = chained, goal, ...} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
- val ho_atp = exists (is_ho_atp ctxt) provers
- val reserved = reserved_isar_keyword_table ()
- val css = clasimpset_rule_table_of ctxt
- val all_facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
- concl_t
- val _ = () |> not blocking ? kill_provers
- val _ = case find_first (not o is_prover_supported ctxt) provers of
- SOME name => error ("No such prover: " ^ name ^ ".")
- | NONE => ()
- val _ = print "Sledgehammering..."
- val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
+ | n =>
+ let
+ val _ = Proof.assert_backward state
+ val print =
+ if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
+ val state = state |> Proof.map_context (silence_proof_methods debug)
+ val ctxt = Proof.context_of state
+ val {facts = chained, goal, ...} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
+ val ho_atp = exists (is_ho_atp ctxt) provers
+ val reserved = reserved_isar_keyword_table ()
+ val css = clasimpset_rule_table_of ctxt
+ val all_facts =
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+ concl_t
+ val _ = () |> not blocking ? kill_provers
+ val _ =
+ (case find_first (not o is_prover_supported ctxt) provers of
+ SOME name => error ("No such prover: " ^ name ^ ".")
+ | NONE => ())
+ val _ = print "Sledgehammering..."
+ val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
- val spying_str_of_factss =
- commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
+ val spying_str_of_factss =
+ commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
- fun get_factss provers =
- let
- val max_max_facts =
- case max_facts of
- SOME n => n
- | NONE =>
- 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
- |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
- val _ = spying spy (fn () => (state, i, "All",
- "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
- in
- all_facts
- |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
- |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
- |> spy ? tap (fn factss => spying spy (fn () =>
- (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
- end
+ fun get_factss provers =
+ let
+ val max_max_facts =
+ (case max_facts of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
+ |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
+ val _ = spying spy (fn () => (state, i, "All",
+ "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
+ in
+ all_facts
+ |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
+ |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
+ |> spy ? tap (fn factss => spying spy (fn () =>
+ (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+ end
- fun launch_provers state =
- let
- val factss = get_factss provers
- val problem =
- {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = factss}
- val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
- val launch = launch_prover params mode output_result minimize_command only learn
- in
- if mode = Auto_Try then
- (unknownN, state)
- |> fold (fn prover => fn accum as (outcome_code, _) =>
- if outcome_code = someN then accum
- else launch problem prover)
- provers
- else
- provers
- |> (if blocking then Par_List.map else map) (launch problem #> fst)
- |> max_outcome_code |> rpair state
- end
- in
- (if blocking then launch_provers state
- else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
- handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
- end
- |> `(fn (outcome_code, _) => outcome_code = someN)
+ fun launch_provers state =
+ let
+ val factss = get_factss provers
+ val problem =
+ {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
+ factss = factss}
+ val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
+ val launch = launch_prover params mode output_result minimize_command only learn
+ in
+ if mode = Auto_Try then
+ (unknownN, state)
+ |> fold (fn prover => fn accum as (outcome_code, _) =>
+ if outcome_code = someN then accum
+ else launch problem prover)
+ provers
+ else
+ provers
+ |> (if blocking then Par_List.map else map) (launch problem #> fst)
+ |> max_outcome_code |> rpair state
+ end
+ in
+ (if blocking then launch_provers state
+ else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
+ handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
+ end
+ |> `(fn (outcome_code, _) => outcome_code = someN))
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:50:38 2014 +0100
@@ -96,6 +96,7 @@
("isar_proofs", "smart"),
("compress_isar", "10"),
("try0_isar", "true"),
+ ("smt_proofs", "smart"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "2")]
@@ -117,7 +118,8 @@
("no_isar_proofs", "isar_proofs"),
("dont_slice", "slice"),
("dont_minimize", "minimize"),
- ("dont_try0_isar", "try0_isar")]
+ ("dont_try0_isar", "try0_isar"),
+ ("no_smt_proofs", "smt_proofs")]
val params_not_for_minimize =
["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -131,12 +133,12 @@
member (op =) property_dependent_params s orelse s = "expect"
fun is_prover_list ctxt s =
- case space_explode " " s of
+ (case space_explode " " s of
ss as _ :: _ => forall (is_prover_supported ctxt) ss
- | _ => false
+ | _ => false)
fun unalias_raw_param (name, value) =
- case AList.lookup (op =) alias_params name of
+ (case AList.lookup (op =) alias_params name of
SOME (name', []) => (name', value)
| SOME (param' as (name', _)) =>
if value <> ["false"] then
@@ -145,13 +147,14 @@
error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
\(cf. " ^ quote name' ^ ").")
| NONE =>
- case AList.lookup (op =) negated_alias_params name of
- SOME name' => (name', case value of
- ["false"] => ["true"]
- | ["true"] => ["false"]
- | [] => ["false"]
- | _ => value)
- | NONE => (name, value)
+ (case AList.lookup (op =) negated_alias_params name of
+ SOME name' => (name',
+ (case value of
+ ["false"] => ["true"]
+ | ["true"] => ["false"]
+ | [] => ["false"]
+ | _ => value))
+ | NONE => (name, value)))
val any_type_enc = type_enc_of_string Strict "erased"
@@ -266,9 +269,10 @@
val type_enc =
if mode = Auto_Try then
NONE
- else case lookup_string "type_enc" of
- "smart" => NONE
- | s => (type_enc_of_string Strict s; SOME s)
+ else
+ (case lookup_string "type_enc" of
+ "smart" => NONE
+ | s => (type_enc_of_string Strict s; SOME s))
val strict = mode = Auto_Try orelse lookup_bool "strict"
val lam_trans = lookup_option lookup_string "lam_trans"
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
@@ -284,6 +288,7 @@
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val compress_isar = Real.max (1.0, lookup_real "compress_isar")
val try0_isar = lookup_bool "try0_isar"
+ val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
val timeout = lookup_time "timeout"
@@ -295,8 +300,8 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params mode
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 19:50:38 2014 +0100
@@ -110,18 +110,18 @@
fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
| normT (TVar (z as (_, S))) =
(fn ((knownT, nT), accum) =>
- case find_index (equal z) knownT of
+ (case find_index (equal z) knownT of
~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
- | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
+ | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
| normT (T as TFree _) = pair T
fun norm (t $ u) = norm t ##>> norm u #>> op $
| norm (Const (s, T)) = normT T #>> curry Const s
| norm (Var (z as (_, T))) =
normT T
#> (fn (T, (accumT, (known, n))) =>
- case find_index (equal z) known of
+ (case find_index (equal z) known of
~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
- | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
+ | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))))
| norm (Abs (_, T, t)) =
norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
| norm (Bound j) = pair (Bound j)
@@ -138,11 +138,11 @@
Induction
else
let val t = normalize_vars t in
- case Termtab.lookup css t of
+ (case Termtab.lookup css t of
SOME status => status
| NONE =>
let val concl = Logic.strip_imp_concl t in
- case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
+ (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
SOME lrhss =>
let
val prems = Logic.strip_imp_prems t
@@ -150,8 +150,8 @@
in
Termtab.lookup css t' |> the_default General
end
- | NONE => General
- end
+ | NONE => General)
+ end)
end
end
@@ -165,15 +165,14 @@
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
|> implode
fun nth_name j =
- case xref of
+ (case xref of
Facts.Fact s => backquote s ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) =>
make_name reserved (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
make_name reserved true
- (nth (maps (explode_interval (length ths)) intervals) j) name ^
- bracket
+ (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
fun add_nth th (j, rest) =
let val name = nth_name j in
(j + 1, ((name, stature_of_thm false [] chained css name th), th)
@@ -364,9 +363,9 @@
corresponding low-level facts, so that MaSh can learn from the low-level
proofs. *)
fun un_class_ify s =
- case first_field "_class" s of
+ (case first_field "_class" s of
SOME (pref, suf) => [s, pref ^ suf]
- | NONE => [s]
+ | NONE => [s])
fun build_name_tables name_of facts =
let
@@ -388,7 +387,7 @@
|> Net.entries
fun struct_induct_rule_on th =
- case Logic.strip_horn (prop_of th) of
+ (case Logic.strip_horn (prop_of th) of
(prems, @{const Trueprop}
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
if not (is_TVar ind_T) andalso length prems > 1 andalso
@@ -397,7 +396,7 @@
SOME (p_name, ind_T)
else
NONE
- | _ => NONE
+ | _ => NONE)
val instantiate_induct_timeout = seconds 0.01
@@ -420,14 +419,15 @@
handle Type.TYPE_MATCH => false
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
- case struct_induct_rule_on th of
+ (case struct_induct_rule_on th of
SOME (p_name, ind_T) =>
let val thy = Proof_Context.theory_of ctxt in
- stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
- |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
- (instantiate_induct_rule ctxt stmt p_name ax)))
+ stmt_xs
+ |> filter (fn (_, T) => type_match thy (T, ind_T))
+ |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
+ (instantiate_induct_rule ctxt stmt p_name ax)))
end
- | NONE => [ax]
+ | NONE => [ax])
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
@@ -482,9 +482,9 @@
val n = length ths
val multi = n > 1
fun check_thms a =
- case try (Proof_Context.get_thms ctxt) a of
+ (case try (Proof_Context.get_thms ctxt) a of
NONE => false
- | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
+ | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
in
snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) =>
(j - 1,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:50:38 2014 +0100
@@ -11,16 +11,16 @@
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
type stature = ATP_Problem_Generate.stature
- type one_line_params = Sledgehammer_Reconstructor.one_line_params
+ type one_line_params = Sledgehammer_Proof_Methods.one_line_params
val trace : bool Config.T
type isar_params =
bool * (string option * string option) * Time.time * real * bool * bool
- * (term, string) atp_step list * thm
+ * (term, string) atp_step list * thm
- val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
- one_line_params -> string
+ val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
+ int -> one_line_params -> string
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -31,7 +31,7 @@
open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Compress
@@ -109,12 +109,13 @@
type isar_params =
bool * (string option * string option) * Time.time * real * bool * bool
- * (term, string) atp_step list * thm
+ * (term, string) atp_step list * thm
val arith_methods =
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
-val datatype_methods = [Simp_Method, Simp_Size_Method]
+val datatype_methods =
+ [Simp_Method, Simp_Size_Method]
val metislike_methods0 =
[Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
Fastforce_Method, Force_Method, Algebra_Method, Meson_Method,
@@ -122,9 +123,10 @@
val rewrite_methods =
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
Meson_Method]
-val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
+val skolem_methods =
+ [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
-fun isar_proof_text ctxt debug isar_proofs isar_params
+fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
fun isar_proof_of () =
@@ -134,7 +136,10 @@
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
- val massage_meths = not try0_isar ? single o hd
+ fun massage_meths (meths as meth :: _) =
+ if not try0_isar then [meth]
+ else if smt_proofs = SOME true then SMT_Method :: meths
+ else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
@@ -169,7 +174,7 @@
else ([], rewrite_methods))
||> massage_meths
in
- Prove ([], skos, l, t, [], ([], []), meths)
+ Prove ([], skos, l, t, [], ([], []), meths, "")
end)
val bot = atp_proof |> List.last |> #1
@@ -218,7 +223,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- (the_list predecessor, []), massage_meths metislike_methods))
+ (the_list predecessor, []), massage_meths metislike_methods, ""))
else
I)
|> rev
@@ -237,7 +242,7 @@
else metislike_methods)
|> massage_meths
- fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths)
+ fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
in
if is_clause_tainted c then
@@ -251,7 +256,7 @@
steps_of_rest (prove [] deps)
| _ => steps_of_rest (prove [] deps))
else
- steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths)
+ steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
else prove [] deps)
end
| isar_steps outer predecessor accum (Cases cases :: infs) =
@@ -264,7 +269,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- (the_list predecessor, []), massage_meths metislike_methods)
+ (the_list predecessor, []), massage_meths metislike_methods, "")
in
isar_steps outer (SOME l) (step :: accum) infs
end
@@ -284,9 +289,7 @@
|> postprocess_isar_proof_remove_unreferenced_steps I
|> relabel_isar_proof_canonically
- val ctxt = ctxt
- |> enrich_context_with_local_facts canonical_isar_proof
- |> silence_reconstructors debug
+ val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
@@ -296,7 +299,6 @@
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
-
fun str_of_meth l meth =
string_of_proof_method meth ^ " " ^
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
@@ -304,11 +306,17 @@
fun trace_isar_proof label proof =
if trace then
- tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
- "\n")
+ tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
+ string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n")
else
()
+ fun comment_of l (meth :: _) =
+ (case (verbose,
+ Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
+ (false, Played _) => ""
+ | (_, outcome) => string_of_play_outcome outcome)
+
val (play_outcome, isar_proof) =
canonical_isar_proof
|> tap (trace_isar_proof "Original")
@@ -319,11 +327,12 @@
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
|> `(preplay_outcome_of_isar_proof (!preplay_data))
+ ||> comment_isar_proof comment_of
||> chain_isar_proof
||> kill_useless_labels_in_isar_proof
- ||> relabel_isar_proof_finally
+ ||> relabel_isar_proof_nicely
in
- (case string_of_isar_proof (K (K "")) isar_proof of
+ (case string_of_isar_proof isar_proof of
"" =>
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
else ""
@@ -354,18 +363,18 @@
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
in one_line_proof ^ isar_proof end
-fun isar_proof_would_be_a_good_idea (reconstr, play) =
+fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
- Played _ => reconstr = SMT
+ Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
| Play_Timed_Out _ => true
| Play_Failed => true
| Not_Played => false)
-fun proof_text ctxt debug isar_proofs isar_params num_chained
+fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
- (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt debug isar_proofs isar_params
+ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
+ isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
else
one_line_proof_text num_chained) one_line_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 19:50:38 2014 +0100
@@ -41,12 +41,12 @@
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
fun fold_map_atypes f T s =
- case T of
+ (case T of
Type (name, Ts) =>
- let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
- (Type (name, Ts), s)
- end
- | _ => f T s
+ let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
+ (Type (name, Ts), s)
+ end
+ | _ => f T s)
val indexname_ord = Term_Ord.fast_indexname_ord
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 19:50:38 2014 +0100
@@ -19,7 +19,7 @@
struct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
@@ -32,7 +32,7 @@
| collect_steps [] accum = accum
| collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
and collect_step (Let _) x = x
- | collect_step (step as Prove (_, _, l, _, subproofs, _, _)) x =
+ | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
(case collect_subproofs subproofs x of
([], accu) => ([], accu)
| accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
@@ -55,16 +55,16 @@
| update_steps (step :: steps) updates = update_step step (update_steps steps updates)
and update_step step (steps, []) = (step :: steps, [])
| update_step (step as Let _) (steps, updates) = (step :: steps, updates)
- | update_step (Prove (qs, xs, l, t, subproofs, facts, meths))
- (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths') :: updates') =
- let
- val (subproofs, updates) =
- if l = l' then update_subproofs subproofs' updates'
- else update_subproofs subproofs updates
- in
- if l = l' then (Prove (qs', xs', l', t', subproofs, facts', meths') :: steps, updates)
- else (Prove (qs, xs, l, t, subproofs, facts, meths) :: steps, updates)
- end
+ | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
+ (steps,
+ updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
+ (if l = l' then
+ update_subproofs subproofs' updates'
+ |>> (fn subproofs' => Prove (qs', xs', l', t', subproofs', facts', meths', comment'))
+ else
+ update_subproofs subproofs updates
+ |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment)))
+ |>> (fn step => step :: steps)
and update_subproofs [] updates = ([], updates)
| update_subproofs steps [] = (steps, [])
| update_subproofs (proof :: subproofs) updates =
@@ -80,18 +80,30 @@
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
end
-fun try_merge (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1))
- (Prove (qs2, fix, l2, t, subproofs, (lfs2, gfs2), meths2)) =
- (case inter (op =) meths1 meths2 of
+fun merge_methods preplay_data (l1, meths1) (l2, meths2) =
+ let
+ fun is_method_hopeful l meth =
+ let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in
+ not (Lazy.is_finished outcome) orelse
+ (case Lazy.force outcome of Played _ => true | _ => false)
+ end
+ in
+ inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2)
+ end
+
+fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
+ (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
+ (case merge_methods preplay_data (l1, meths1) (l2, meths2) of
[] => NONE
| meths =>
let
val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, l2, t, subproofs, (lfs, gfs), meths))
+ SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
+ comment1 ^ comment2))
end)
- | try_merge _ _ = NONE
+ | try_merge _ _ _ = NONE
val compress_degree = 2
val merge_timeout_slack_time = seconds 0.005
@@ -117,9 +129,9 @@
val (get_successors, replace_successor) =
let
- fun add_refs (Let _) = I
- | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) =
- fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
+ fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) =
+ fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs
+ | add_refs _ = I
val tab =
Canonical_Label_Tab.empty
@@ -140,11 +152,11 @@
end
(* elimination of trivial, one-step subproofs *)
- fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
+ fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) comment subs nontriv_subs =
if null subs orelse not (compress_further ()) then
let
val subproofs = List.revAppend (nontriv_subs, subs)
- val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)
+ val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)
in
set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
step
@@ -154,7 +166,7 @@
(sub as Proof (_, assms, sub_steps)) :: subs =>
(let
(* trivial subproofs have exactly one "Prove" step *)
- val [Prove (_, [], l', _, [], (lfs', gfs'), meths')] = sub_steps
+ val [Prove (_, [], l', _, [], (lfs', gfs'), meths', _)] = sub_steps
(* only touch proofs that can be preplayed sucessfully *)
val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l'
@@ -163,8 +175,8 @@
val subs'' = subs @ nontriv_subs
val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
- val meths'' as _ :: _ = inter (op =) meths' meths
- val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
+ val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths)
+ val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment)
(* check if the modified step can be preplayed fast enough *)
val timeout = slackify_merge_timeout (Time.+ (time, time'))
@@ -172,20 +184,20 @@
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
+ elim_one_subproof time'' qs fix l t lfs'' gfs'' meths comment subs nontriv_subs
end
handle Bind =>
- elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
+ elim_one_subproof time qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
- fun elim_subproofs (step as Let _) = step
- | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) =
+ fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
if subproofs = [] then
step
else
(case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
- Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
+ Played time => elim_one_subproof time qs fix l t lfs gfs meths comment subproofs []
| _ => step)
+ | elim_subproofs step = step
fun compress_top_level steps =
let
@@ -198,8 +210,8 @@
val cand_ord = pairself cand_key #> compression_ord
- fun pop_next_cand [] = (NONE, [])
- | pop_next_cand (cands as (cand :: cands')) =
+ fun pop_next_candidate [] = (NONE, [])
+ | pop_next_candidate (cands as (cand :: cands')) =
let
val best as (i, _, _) =
fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
@@ -207,8 +219,8 @@
val candidates =
let
- fun add_cand (_, Let _) = I
- | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t)
+ fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t)
+ | add_cand _ = I
in
(steps
|> split_last |> fst (* keep last step *)
@@ -217,15 +229,16 @@
fun try_eliminate (i, l, _) labels steps =
let
- val ((cand as Prove (_, _, _, _, _, (lfs, _), _)) :: steps') = drop i steps
+ val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps
val succs = collect_successors steps' labels
(* only touch steps that can be preplayed successfully *)
val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
- val succs' = map (try_merge cand #> the) succs
+ val succs' = map (try_merge (!preplay_data) cand #> the) succs
+ (* FIXME: more generous! *)
val times0 = map ((fn Played time => time) o
forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels
val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
@@ -236,16 +249,16 @@
(* ensure none of the modified successors timed out *)
val times = map (fn (_, Played time) :: _ => time) meths_outcomess
- val (steps1, _ :: steps2) = chop i steps
+ val (steps_before, _ :: steps_after) = chop i steps
(* replace successors with their modified versions *)
- val steps2 = update_steps steps2 succs'
+ val steps_after = update_steps steps_after succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
succs' meths_outcomess;
map (replace_successor l labels) lfs;
(* removing the step would mess up the indices; replace with dummy step instead *)
- steps1 @ dummy_isar_step :: steps2
+ steps_before @ dummy_isar_step :: steps_after
end
handle Bind => steps
| Match => steps
@@ -255,7 +268,7 @@
if not (compress_further ()) then
steps
else
- (case pop_next_cand candidates of
+ (case pop_next_candidate candidates of
(NONE, _) => steps (* no more candidates for elimination *)
| (SOME (cand as (_, l, _)), candidates) =>
let val successors = get_successors l in
@@ -280,9 +293,9 @@
steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
|> compress_further () ? compress_top_level
and compress_sub_levels (step as Let _) = step
- | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+ | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
(* compress subproofs *)
- Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths)
+ Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
(* eliminate trivial subproofs *)
|> compress_further () ? elim_subproofs
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:50:38 2014 +0100
@@ -21,22 +21,25 @@
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
struct
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
-fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) =
- Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
+fun keep_fastest_method_of_isar_step preplay_data
+ (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
+ Prove (qs, xs, l, t, subproofs, facts,
+ meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
+ comment)
| keep_fastest_method_of_isar_step _ step = step
val slack = seconds 0.1
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
+ (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
@@ -75,7 +78,7 @@
else
(used, accu))
and process_used_step step = step |> postproc_step |> process_used_step_subproofs
- and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
+ and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
let
val (used, subproofs) =
map process_proof subproofs
@@ -83,7 +86,7 @@
|>> Ord_List.unions label_ord
|>> fold (Ord_List.insert label_ord) lfs
in
- (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
+ (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
end
in
snd o process_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:50:38 2014 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_ISAR_PREPLAY =
sig
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type proof_method = Sledgehammer_Isar_Proof.proof_method
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
@@ -36,7 +36,7 @@
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
@@ -52,9 +52,9 @@
fun enrich_with_proof (Proof (_, assms, isar_steps)) =
enrich_with_assms assms #> fold enrich_with_step isar_steps
- and enrich_with_step (Let _) = I
- | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
+ and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
enrich_with_fact l t #> fold enrich_with_proof subproofs
+ | enrich_with_step _ = I
in
enrich_with_proof proof ctxt
end
@@ -88,7 +88,7 @@
val concl =
(case try List.last steps of
- SOME (Prove (_, [], _, t, _, _, _)) => t
+ SOME (Prove (_, [], _, t, _, _, _, _)) => t
| _ => raise Fail "preplay error: malformed subproof")
val var_idx = maxidx_of_term concl + 1
@@ -100,29 +100,8 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac local_facts THEN'
- (case meth of
- Meson_Method => Meson.meson_tac ctxt global_facts
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
- (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
- (case meth of
- Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Arith_Method => Arith_Data.arith_tac ctxt
- | Blast_Method => blast_tac ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt
- | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
-
-(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
+(* may throw exceptions *)
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -131,10 +110,10 @@
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
- (* FIXME: generate fresh name *)
- val thesis = Free ("thesis_preplay", HOLogic.boolT)
+ val frees = map Free xs
+ val thesis =
+ Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
- val frees = map Free xs
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
@@ -143,18 +122,18 @@
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)
- val facts =
- resolve_fact_names ctxt fact_names
+ val assmsp =
+ resolve_fact_names ctxt facts
|>> append (map (thm_of_proof ctxt) subproofs)
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method ctxt facts meth))
+ HEADGOAL (tac_of_proof_method ctxt assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
in
- (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+ (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
play_outcome)
end
@@ -185,7 +164,7 @@
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
- (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 =
+ (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
@@ -228,8 +207,8 @@
#> get_best_method_outcome Lazy.force
#> fst
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
- Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
+ Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
| forced_outcome_of_step _ _ = Played Time.zeroTime
fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:50:38 2014 +0100
@@ -8,37 +8,25 @@
signature SLEDGEHAMMER_ISAR_PROOF =
sig
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+
type label = string * int
type facts = label list * string list (* local and global facts *)
datatype isar_qualifier = Show | Then
- datatype proof_method =
- Metis_Method of string option * string option |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Meson_Method |
- Algebra_Method
-
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list
+ * facts * proof_method list * string
val no_label : label
val label_ord : label * label -> order
val string_of_label : label -> string
- val string_of_proof_method : proof_method -> string
-
val steps_of_isar_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
@@ -53,13 +41,13 @@
val canonical_label_ord : (label * label) -> order
+ val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
val chain_isar_proof : isar_proof -> isar_proof
val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
val relabel_isar_proof_canonically : isar_proof -> isar_proof
- val relabel_isar_proof_finally : isar_proof -> isar_proof
+ val relabel_isar_proof_nicely : isar_proof -> isar_proof
- val string_of_isar_proof : Proof.context -> int -> int ->
- (label -> proof_method list -> string) -> isar_proof -> string
+ val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
end;
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -70,7 +58,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Annotate
type label = string * int
@@ -78,24 +66,12 @@
datatype isar_qualifier = Show | Then
-datatype proof_method =
- Metis_Method of string option * string option |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Meson_Method |
- Algebra_Method
-
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
- * facts * proof_method list
+ * facts * proof_method list * string
val no_label = ("", ~1)
@@ -103,33 +79,18 @@
fun string_of_label (s, num) = s ^ string_of_int num
-fun string_of_proof_method meth =
- (case meth of
- Metis_Method (NONE, NONE) => "metis"
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
- | Simp_Method => "simp"
- | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
- | Auto_Method => "auto"
- | Fastforce_Method => "fastforce"
- | Force_Method => "force"
- | Arith_Method => "arith"
- | Blast_Method => "blast"
- | Meson_Method => "meson"
- | Algebra_Method => "algebra")
-
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
-fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
+fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
| label_of_isar_step _ = NONE
-fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _)) = subs
+fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
| subproofs_of_isar_step _ = []
-fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts
+fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
| facts_of_isar_step _ = ([], [])
-fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
| proof_methods_of_isar_step _ = []
fun fold_isar_step f step =
@@ -140,8 +101,8 @@
let
fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
and map_step (step as Let _) = f step
- | map_step (Prove (qs, xs, l, t, subs, facts, meths)) =
- f (Prove (qs, xs, l, t, map map_proof subs, facts, meths))
+ | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+ f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
in map_proof end
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -153,12 +114,17 @@
type key = label
val ord = canonical_label_ord)
+fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
+ Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
+ | comment_isar_step _ step = step
+fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
+
fun chain_qs_lfs NONE lfs = ([], lfs)
| chain_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths)
+ Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
end
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
@@ -175,8 +141,8 @@
fun kill_label l = if member (op =) used_ls l then l else no_label
- fun kill_step (Prove (qs, xs, l, t, subs, facts, meths)) =
- Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths)
+ fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
| kill_step step = step
and kill_proof (Proof (fix, assms, steps)) =
Proof (fix, map (apfst kill_label) assms, map kill_step steps)
@@ -189,14 +155,15 @@
fun next_label l (next, subst) =
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
- fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+ fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
+ (accum as (_, subst)) =
let
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
val ((subs', l'), accum') = accum
|> fold_map relabel_proof subs
||>> next_label l
in
- (Prove (qs, fix, l', t, subs', (lfs', gfs), meths), accum')
+ (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
end
| relabel_step step accum = (step, accum)
and relabel_proof (Proof (fix, assms, steps)) =
@@ -210,7 +177,7 @@
val assume_prefix = "a"
val have_prefix = "f"
-val relabel_isar_proof_finally =
+val relabel_isar_proof_nicely =
let
fun next_label depth prefix l (accum as (next, subst)) =
if l = no_label then
@@ -220,13 +187,14 @@
(l', (next + 1, (l, l') :: subst))
end
- fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+ fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
+ (accum as (_, subst)) =
let
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
val (l', accum' as (next', subst')) = next_label depth have_prefix l accum
val subs' = map (relabel_proof subst' (depth + 1)) subs
in
- (Prove (qs, xs, l', t, subs', (lfs', gfs), meths), accum')
+ (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
end
| relabel_step _ step accum = (step, accum)
and relabel_proof subst depth (Proof (fix, assms, steps)) =
@@ -240,7 +208,7 @@
val indent_size = 2
-fun string_of_isar_proof ctxt i n comment_of proof =
+fun string_of_isar_proof ctxt i n proof =
let
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
@@ -291,6 +259,7 @@
fun is_direct_method (Metis_Method _) = true
| is_direct_method Meson_Method = true
+ | is_direct_method SMT_Method = true
| is_direct_method _ = false
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
@@ -336,7 +305,7 @@
and add_step ind (Let (t1, t2)) =
add_str (of_indent ind ^ "let ")
#> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
- | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _)) =
+ | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _, comment)) =
add_step_pre ind qs subs
#> (case xs of
[] => add_str (of_have qs (length subs) ^ " ")
@@ -345,9 +314,7 @@
#> add_term t
#> add_str (" " ^
of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
- (case comment_of l meths of
- "" => ""
- | comment => " (* " ^ comment ^ " *)") ^ "\n")
+ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
and add_steps ind = fold (add_step ind)
and of_proof ind ctxt (Proof (xs, assms, steps)) =
("", ctxt)
@@ -359,7 +326,7 @@
(* One-step Metis proofs are pointless; better use the one-liner directly. *)
(case proof of
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
- | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _)]) => ""
+ | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => ""
| _ =>
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 19:50:38 2014 +0100
@@ -178,9 +178,9 @@
fun run_on () =
(Isabelle_System.bash command
|> tap (fn _ =>
- case try File.read (Path.explode err_file) |> the_default "" of
+ (case try File.read (Path.explode err_file) |> the_default "" of
"" => trace_msg ctxt (K "Done")
- | s => warning ("MaSh error: " ^ elide_string 1000 s));
+ | s => warning ("MaSh error: " ^ elide_string 1000 s)));
read_suggs (fn () => try File.read_lines sugg_path |> these))
fun clean_up () =
if overlord then ()
@@ -243,17 +243,16 @@
(* The suggested weights don't make much sense. *)
fun extract_suggestion sugg =
- case space_explode "=" sugg of
+ (case space_explode "=" sugg of
[name, _ (* weight *)] =>
SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
| [name] => SOME (unencode_str name (* , 1.0 *))
- | _ => NONE
+ | _ => NONE)
fun extract_suggestions line =
- case space_explode ":" line of
- [goal, suggs] =>
- (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
- | _ => ("", [])
+ (case space_explode ":" line of
+ [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
+ | _ => ("", []))
structure MaSh =
struct
@@ -294,11 +293,10 @@
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
(trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
- run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs)
- (fn suggs =>
- case suggs () of
- [] => []
- | suggs => snd (extract_suggestions (List.last suggs)))
+ run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
+ (case suggs () of
+ [] => []
+ | suggs => snd (extract_suggestions (List.last suggs))))
handle List.Empty => [])
end;
@@ -362,48 +360,47 @@
exception FILE_VERSION_TOO_NEW of unit
fun extract_node line =
- case space_explode ":" line of
+ (case space_explode ":" line of
[head, parents] =>
(case space_explode " " head of
- [kind, name] =>
- SOME (unencode_str name, unencode_strs parents,
- try proof_kind_of_str kind |> the_default Isar_Proof)
- | _ => NONE)
- | _ => NONE
+ [kind, name] =>
+ SOME (unencode_str name, unencode_strs parents,
+ try proof_kind_of_str kind |> the_default Isar_Proof)
+ | _ => NONE)
+ | _ => NONE)
fun load_state _ _ (state as (true, _)) = state
| load_state ctxt overlord _ =
let val path = mash_state_file () in
(true,
- case try File.read_lines path of
+ (case try File.read_lines path of
SOME (version' :: node_lines) =>
let
fun add_edge_to name parent =
Graph.default_node (parent, Isar_Proof)
#> Graph.add_edge (parent, name)
fun add_node line =
- case extract_node line of
+ (case extract_node line of
NONE => I (* shouldn't happen *)
| SOME (name, parents, kind) =>
- update_access_graph_node (name, kind)
- #> fold (add_edge_to name) parents
+ update_access_graph_node (name, kind) #> fold (add_edge_to name) parents)
val (access_G, num_known_facts) =
- case string_ord (version', version) of
+ (case string_ord (version', version) of
EQUAL =>
(try_graph ctxt "loading state" Graph.empty (fn () =>
- fold add_node node_lines Graph.empty),
+ fold add_node node_lines Graph.empty),
length node_lines)
| LESS =>
(* can't parse old file *)
(MaSh.unlearn ctxt overlord; (Graph.empty, 0))
- | GREATER => raise FILE_VERSION_TOO_NEW ()
+ | GREATER => raise FILE_VERSION_TOO_NEW ())
in
trace_msg ctxt (fn () =>
"Loaded fact graph (" ^ graph_info access_G ^ ")");
{access_G = access_G, num_known_facts = num_known_facts,
dirty = SOME []}
end
- | _ => empty_state)
+ | _ => empty_state))
end
fun save_state _ (state as {dirty = SOME [], ...}) = state
@@ -415,10 +412,9 @@
fun append_entry (name, (kind, (parents, _))) =
cons (name, Graph.Keys.dest parents, kind)
val (banner, entries) =
- case dirty of
- SOME names =>
- (NONE, fold (append_entry o Graph.get_entry access_G) names [])
- | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
+ (case dirty of
+ SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
+ | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
in
write_file banner (entries, str_of_entry) (mash_state_file ());
trace_msg ctxt (fn () =>
@@ -471,11 +467,11 @@
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
(* There must be a better way to detect local facts. *)
- case try (unprefix local_prefix) hint of
+ (case try (unprefix local_prefix) hint of
SOME suf =>
- thy_name_of_thm th ^ Long_Name.separator ^ suf ^
- Long_Name.separator ^ elided_backquote_thm 50 th
- | NONE => hint
+ thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
+ elided_backquote_thm 50 th
+ | NONE => hint)
end
else
elided_backquote_thm 200 th
@@ -512,9 +508,9 @@
let
val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score)
in
- case find_index (curry fact_eq fact o fst) sels of
+ (case find_index (curry fact_eq fact o fst) sels of
~1 => if member fact_eq unks fact then NONE else SOME 0.0
- | rank => score_at rank
+ | rank => score_at rank)
end
fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
@@ -536,20 +532,21 @@
if Theory.eq_thy p then EQUAL else LESS
else if Theory.subthy (swap p) then
GREATER
- else case int_ord (pairself (length o Theory.ancestors_of) p) of
- EQUAL => string_ord (pairself Context.theory_name p)
- | order => order
+ else
+ (case int_ord (pairself (length o Theory.ancestors_of) p) of
+ EQUAL => string_ord (pairself Context.theory_name p)
+ | order => order)
fun crude_thm_ord p =
- case crude_theory_ord (pairself theory_of_thm p) of
+ (case crude_theory_ord (pairself theory_of_thm p) of
EQUAL =>
let val q = pairself nickname_of_thm p in
(* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
- case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
+ (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
EQUAL => string_ord q
- | ord => ord
+ | ord => ord)
end
- | ord => ord
+ | ord => ord)
val thm_less_eq = Theory.subthy o pairself theory_of_thm
fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
@@ -724,7 +721,7 @@
add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
fun add_term Ts = add_term_pats Ts term_max_depth
fun add_subterms Ts t =
- case strip_comb t of
+ (case strip_comb t of
(Const (s, T), args) =>
(not (is_widely_irrelevant_const s) ? add_term Ts t)
#> add_subtypes T
@@ -735,7 +732,7 @@
| Var (_, T) => add_subtypes T
| Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body
| _ => I)
- #> fold (add_subterms Ts) args
+ #> fold (add_subterms Ts) args)
in [] |> fold (add_subterms []) ts end
val term_max_depth = 2
@@ -805,7 +802,7 @@
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
auto_level facts name_tabs th =
- case isar_dependencies_of name_tabs th of
+ (case isar_dependencies_of name_tabs th of
[] => (false, [])
| isar_deps =>
let
@@ -819,9 +816,10 @@
fun add_isar_dep facts dep accum =
if exists (is_dep dep) accum then
accum
- else case find_first (is_dep dep) facts of
- SOME ((_, status), th) => accum @ [(("", status), th)]
- | NONE => accum (* shouldn't happen *)
+ else
+ (case find_first (is_dep dep) facts of
+ SOME ((_, status), th) => accum @ [(("", status), th)]
+ | NONE => accum (* shouldn't happen *))
val mepo_facts =
facts
|> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
@@ -838,7 +836,7 @@
|> Output.urgent_message
else
();
- case run_prover_for_mash ctxt params prover name facts goal of
+ (case run_prover_for_mash ctxt params prover name facts goal of
{outcome = NONE, used_facts, ...} =>
(if verbose andalso auto_level = 0 then
let val num_facts = length used_facts in
@@ -849,8 +847,8 @@
else
();
(true, map fst used_facts))
- | _ => (false, isar_deps)
- end
+ | _ => (false, isar_deps))
+ end)
(*** High-level communication with MaSh ***)
@@ -1140,9 +1138,9 @@
val access_G = access_G |> fold flop_wrt_access_graph flops
val num_known_facts = num_known_facts + length learns
val dirty =
- case (was_empty, dirty, relearns) of
+ (case (was_empty, dirty, relearns) of
(false, SOME names, []) => SOME (map #1 learns @ names)
- | _ => NONE
+ | _ => NONE)
in
MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
MaSh.relearn ctxt overlord save relearns;
@@ -1202,9 +1200,9 @@
let
val name = nickname_of_thm th
val (n, relearns, flops) =
- case deps_of status th of
+ (case deps_of status th of
SOME deps => (n + 1, (name, deps) :: relearns, flops)
- | NONE => (n, relearns, name :: flops)
+ | NONE => (n, relearns, name :: flops))
val (relearns, flops, next_commit) =
if Time.> (Timer.checkRealTimer timer, next_commit) then
(commit false [] relearns flops;
@@ -1325,7 +1323,7 @@
in
if length facts - num_known_facts
<= max_facts_to_learn_before_query then
- case length (filter_out is_in_access_G facts) of
+ (case length (filter_out is_in_access_G facts) of
0 => false
| num_facts_to_learn =>
if num_facts_to_learn <= max_facts_to_learn_before_query then
@@ -1333,21 +1331,21 @@
|> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
true)
else
- (maybe_launch_thread (); false)
+ (maybe_launch_thread (); false))
else
(maybe_launch_thread (); false)
end
else
false
val (save, effective_fact_filter) =
- case fact_filter of
+ (case fact_filter of
SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
| NONE =>
if is_mash_enabled () then
(maybe_learn (),
if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
else
- (false, mepoN)
+ (false, mepoN))
val unique_facts = drop_duplicate_facts facts
val add_ths = Attrib.eval_thms ctxt add
@@ -1373,11 +1371,11 @@
val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take
in
if save then MaSh.save ctxt overlord else ();
- case (fact_filter, mess) of
+ (case (fact_filter, mess) of
(NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
[(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
(mashN, mash |> map fst |> add_and_take)]
- | _ => [(effective_fact_filter, mesh)]
+ | _ => [(effective_fact_filter, mesh)])
end
fun kill_learners ctxt ({overlord, ...} : params) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 19:50:38 2014 +0100
@@ -171,7 +171,7 @@
(not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x))
#> fold (do_term false) ts
and do_term ext_arg t =
- case strip_comb t of
+ (case strip_comb t of
(Const x, ts) => do_const true x ts
| (Free x, ts) => do_const false x ts
| (Abs (_, T, t'), ts) =>
@@ -182,11 +182,11 @@
? add_pconst_to_table (pseudo_abs_name,
PType (order_of_type T + 1, [])))
#> fold (do_term false) (t' :: ts)
- | (_, ts) => fold (do_term false) ts
+ | (_, ts) => fold (do_term false) ts)
and do_term_or_formula ext_arg T =
if T = HOLogic.boolT then do_formula else do_term ext_arg
and do_formula t =
- case t of
+ (case t of
Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
| @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
@@ -212,7 +212,7 @@
do_formula (t1 $ Bound ~1) #> do_formula t'
| (t0 as Const (_, @{typ bool})) $ t1 =>
do_term false t0 #> do_formula t1 (* theory constant *)
- | _ => do_term false t
+ | _ => do_term false t)
in do_formula end
fun pconsts_in_fact thy t =
@@ -233,17 +233,16 @@
theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
fun pair_consts_fact thy fudge fact =
- case fact |> snd |> theory_const_prop_of fudge
- |> pconsts_in_fact thy of
+ (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
[] => NONE
- | consts => SOME ((fact, consts), NONE)
+ | consts => SOME ((fact, consts), NONE))
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
first by constant name and second by its list of type instantiations. For the
latter, we need a linear ordering on "pattern list". *)
fun patternT_ord p =
- case p of
+ (case p of
(Type (s, ps), Type (t, qs)) =>
(case fast_string_ord (s, t) of
EQUAL => dict_ord patternT_ord (ps, qs)
@@ -253,7 +252,7 @@
| (Type _, TVar _) => GREATER
| (Type _, TFree _) => LESS
| (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
- | (TFree _, _) => GREATER
+ | (TFree _, _) => GREATER)
fun ptype_ord (PType (m, ps), PType (n, qs)) =
(case dict_ord patternT_ord (ps, qs) of
EQUAL => int_ord (m, n)
@@ -269,11 +268,11 @@
|> Symtab.map_default (s, PType_Tab.empty)
#> fold do_term ts
and do_term t =
- case strip_comb t of
+ (case strip_comb t of
(Const x, ts) => do_const true x ts
| (Free x, ts) => do_const false x ts
| (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
- | (_, ts) => fold do_term ts
+ | (_, ts) => fold do_term ts)
in do_term o theory_const_prop_of fudge o snd end
fun pow_int _ 0 = 1.0
@@ -356,7 +355,7 @@
fun fact_weight fudge stature const_tab rel_const_tab chained_const_tab
fact_consts =
- case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
+ (case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
||> filter_out (pconst_hyper_mem swap rel_const_tab) of
([], _) => 0.0
| (rel, irrel) =>
@@ -373,7 +372,7 @@
o irrel_pconst_weight fudge const_tab chained_const_tab)
irrel
val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
+ in if Real.isFinite res then res else 0.0 end)
fun take_most_relevant ctxt max_facts remaining_max
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
@@ -411,15 +410,16 @@
let
fun aux _ _ NONE = NONE
| aux t args (SOME tab) =
- case t of
+ (case t of
t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
| Const (s, _) =>
(if is_widely_irrelevant_const s then
SOME tab
- else case Symtab.lookup tab s of
- NONE => SOME (Symtab.update (s, length args) tab)
- | SOME n => if n = length args then SOME tab else NONE)
- | _ => SOME tab
+ else
+ (case Symtab.lookup tab s of
+ NONE => SOME (Symtab.update (s, length args) tab)
+ | SOME n => if n = length args then SOME tab else NONE))
+ | _ => SOME tab)
in aux (prop_of th) [] end
(* FIXME: This is currently only useful for polymorphic type encodings. *)
@@ -507,11 +507,10 @@
:: hopeful) =
let
val weight =
- case cached_weight of
+ (case cached_weight of
SOME w => w
| NONE =>
- fact_weight fudge stature const_tab rel_const_tab
- chained_const_tab fact_consts
+ fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts)
in
if weight >= thres then
relevant ((ax, weight) :: candidates) rejects hopeful
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 03 19:50:38 2014 +0100
@@ -0,0 +1,201 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Reconstructors.
+*)
+
+signature SLEDGEHAMMER_PROOF_METHODS =
+sig
+ type stature = ATP_Problem_Generate.stature
+
+ datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
+
+ datatype play_outcome =
+ Played of Time.time |
+ Play_Timed_Out of Time.time |
+ Play_Failed |
+ Not_Played
+
+ type minimize_command = string list -> string
+ type one_line_params =
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+
+ val smtN : string
+
+ val string_of_proof_method : proof_method -> string
+ val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+ val string_of_play_outcome : play_outcome -> string
+ val play_outcome_ord : play_outcome * play_outcome -> order
+ val one_line_proof_text : int -> one_line_params -> string
+ val silence_proof_methods : bool -> Proof.context -> Proof.context
+end;
+
+structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
+struct
+
+open ATP_Util
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+
+datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
+
+datatype play_outcome =
+ Played of Time.time |
+ Play_Timed_Out of Time.time |
+ Play_Failed |
+ Not_Played
+
+type minimize_command = string list -> string
+type one_line_params =
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+
+val smtN = "smt"
+
+fun string_of_proof_method meth =
+ (case meth of
+ Metis_Method (NONE, NONE) => "metis"
+ | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ | Meson_Method => "meson"
+ | SMT_Method => "smt"
+ | Simp_Method => "simp"
+ | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Arith_Method => "arith"
+ | Blast_Method => "blast"
+ | Algebra_Method => "algebra")
+
+fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
+ Method.insert_tac local_facts THEN'
+ (case meth of
+ Metis_Method (type_enc_opt, lam_trans_opt) =>
+ Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
+ (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+ | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | Meson_Method => Meson.meson_tac ctxt global_facts
+ | _ =>
+ Method.insert_tac global_facts THEN'
+ (case meth of
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+ | Auto_Method => K (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Arith_Method => Arith_Data.arith_tac ctxt
+ | Blast_Method => blast_tac ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+
+fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
+ | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
+ | string_of_play_outcome Play_Failed = "failed"
+ | string_of_play_outcome _ = "unknown"
+
+fun play_outcome_ord (Played time1, Played time2) =
+ int_ord (pairself Time.toMilliseconds (time1, time2))
+ | play_outcome_ord (Played _, _) = LESS
+ | play_outcome_ord (_, Played _) = GREATER
+ | play_outcome_ord (Not_Played, Not_Played) = EQUAL
+ | play_outcome_ord (Not_Played, _) = LESS
+ | play_outcome_ord (_, Not_Played) = GREATER
+ | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
+ int_ord (pairself Time.toMilliseconds (time1, time2))
+ | play_outcome_ord (Play_Timed_Out _, _) = LESS
+ | play_outcome_ord (_, Play_Timed_Out _) = GREATER
+ | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
+
+(* FIXME: Various bugs, esp. with "unfolding"
+fun unusing_chained_facts _ 0 = ""
+ | unusing_chained_facts used_chaineds num_chained =
+ if length used_chaineds = num_chained then ""
+ else if null used_chaineds then "(* using no facts *) "
+ else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+*)
+
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
+fun command_call name [] =
+ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
+(* FIXME *)
+fun proof_method_command meth i n used_chaineds num_chained ss =
+ (* unusing_chained_facts used_chaineds num_chained ^ *)
+ apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
+
+fun try_command_line banner time command =
+ banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "."
+
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ (case minimize_command ss of
+ "" => ""
+ | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
+
+fun split_used_facts facts =
+ facts
+ |> List.partition (fn (_, (sc, _)) => sc = Chained)
+ |> pairself (sort_distinct (string_ord o pairself fst))
+
+fun one_line_proof_text num_chained
+ ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+
+ val (failed, ext_time) =
+ (case play of
+ Played time => (false, (SOME (false, time)))
+ | Play_Timed_Out time => (false, SOME (true, time))
+ | Play_Failed => (true, NONE)
+ | Not_Played => (false, NONE))
+
+ val try_line =
+ map fst extra
+ |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
+ |> (if failed then
+ enclose "One-line proof reconstruction failed: "
+ ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
+ else
+ try_command_line banner ext_time)
+ in
+ try_line ^ minimize_line minimize_command (map fst (extra @ chained))
+ end
+
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+ exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
+ Try0.silence_methods debug
+ #> Config.put SMT_Config.verbose debug
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:50:38 2014 +0100
@@ -12,9 +12,9 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
+ type minimize_command = Sledgehammer_Proof_Methods.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -38,6 +38,7 @@
isar_proofs : bool option,
compress_isar : real,
try0_isar : bool,
+ smt_proofs : bool option,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -57,8 +58,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -66,23 +67,22 @@
-> prover_problem -> prover_result
val SledgehammerN : string
- val plain_metis : reconstructor
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
- val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
- val is_reconstructor : string -> bool
+ val extract_proof_method : params -> proof_method -> string * (string * string list) list
+ val is_proof_method : string -> bool
val is_atp : theory -> string -> bool
- val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
+ val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
val is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
- Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
+ Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
val remotify_atp_if_not_installed : theory -> string -> string option
val isar_supported_prover_of : theory -> string -> string
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
- string -> reconstructor * play_outcome -> 'a
+ string -> proof_method * play_outcome -> 'a
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
Proof.context
@@ -102,7 +102,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -110,9 +110,8 @@
"Async_Manager". *)
val SledgehammerN = "Sledgehammer"
-val reconstructor_names = [metisN, smtN]
-val plain_metis = Metis (hd partial_type_encs, combsN)
-val is_reconstructor = member (op =) reconstructor_names
+val proof_method_names = [metisN, smtN]
+val is_proof_method = member (op =) proof_method_names
val is_atp = member (op =) o supported_atps
@@ -148,6 +147,7 @@
isar_proofs : bool option,
compress_isar : real,
try0_isar : bool,
+ smt_proofs : bool option,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -167,8 +167,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -183,29 +183,28 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
-fun bunch_of_reconstructors needs_full_types lam_trans =
- if needs_full_types then
- [Metis (full_type_enc, lam_trans false),
- Metis (really_full_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
- else
- [Metis (partial_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans false),
- Metis (no_typesN, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
+fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
+ [Metis_Method (SOME full_type_enc, NONE)] @
+ (if needs_full_types then
+ [Metis_Method (SOME full_type_enc, NONE),
+ Metis_Method (SOME really_full_type_enc, NONE),
+ Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
+ else
+ [Metis_Method (NONE, NONE),
+ Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
+ [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
+ (if smt_proofs then [SMT_Method] else [])
-fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
+fun extract_proof_method ({type_enc, lam_trans, ...} : params)
+ (Metis_Method (type_enc', lam_trans')) =
let
val override_params =
- (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
- else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
- (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
- else [("lam_trans", [lam_trans'])])
+ (if is_none type_enc' andalso is_none type_enc then []
+ else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
+ (if is_none lam_trans' andalso is_none lam_trans then []
+ else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
in (metisN, override_params) end
- | extract_reconstructor _ SMT = (smtN, [])
+ | extract_proof_method _ SMT_Method = (smtN, [])
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -216,49 +215,43 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
- | tac_of_reconstructor SMT = SMT_Solver.smt_tac
-
-fun timed_reconstructor reconstr debug timeout ths =
- timed_apply timeout (silence_reconstructors debug
- #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
+fun timed_proof_method meth timeout ths =
+ timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
let
- fun get_preferred reconstrs =
- if member (op =) reconstrs preferred then preferred
- else List.last reconstrs
+ fun get_preferred meths = if member (op =) meths preferred then preferred else meth
in
if timeout = Time.zeroTime then
- (get_preferred reconstrs, Not_Played)
+ (get_preferred meths, Not_Played)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
- fun play [] [] = (get_preferred reconstrs, Play_Failed)
+ fun play [] [] = (get_preferred meths, Play_Failed)
| play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
- | play timed_out (reconstr :: reconstrs) =
+ | play timed_out (meth :: meths) =
let
val _ =
if verbose then
- Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+ Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
"\" for " ^ string_of_time timeout ^ "...")
else
()
val timer = Timer.startRealTimer ()
in
- case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
- | _ => play timed_out reconstrs
+ (case timed_proof_method meth timeout ths state i of
+ SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
+ | _ => play timed_out meths)
end
- handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+ handle TimeLimit.TimeOut => play (meth :: timed_out) meths
in
- play [] reconstrs
+ play [] meths
end
end
@@ -275,9 +268,8 @@
val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
val (min_name, override_params) =
(case preplay of
- (reconstr, Played _) =>
- if isar_proofs = SOME true then (maybe_isar_name, [])
- else extract_reconstructor params reconstr
+ (meth, Played _) =>
+ if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
| _ => (maybe_isar_name, []))
in minimize_command override_params min_name end
@@ -293,7 +285,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- reconstructor_names @
+ proof_method_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:50:38 2014 +0100
@@ -31,7 +31,7 @@
open ATP_Proof_Reconstruct
open ATP_Systems
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar
open Sledgehammer_Prover
@@ -132,7 +132,7 @@
fun run_atp mode name
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
- try0_isar, slice, minimize, timeout, preplay_timeout, ...})
+ try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -346,18 +346,15 @@
let
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
- val reconstrs =
- bunch_of_reconstructors needs_full_types (fn desperate =>
- if desperate then
- if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN
- else
- default_metis_lam_trans)
+ val meths =
+ bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
+ (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
in
(used_facts,
Lazy.lazy (fn () =>
let val used_pairs = used_from |> filter_used_facts false used_facts in
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- (hd reconstrs) reconstrs
+ (hd meths) meths
end),
fn preplay =>
let
@@ -383,7 +380,7 @@
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
+ proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
end,
(if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
(if important_message <> "" then
@@ -392,7 +389,8 @@
""))
end
| SOME failure =>
- ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+ fn _ => string_of_atp_failure failure, ""))
in
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:50:38 2014 +0100
@@ -8,8 +8,8 @@
signature SLEDGEHAMMER_PROVER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
type prover = Sledgehammer_Prover.prover
@@ -23,11 +23,11 @@
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
- Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
+ Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
((string * stature) * thm list) list ->
((string * stature) * thm list) list option
- * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
- * string)
+ * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string)
+ * string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
@@ -44,35 +44,31 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT
-fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
- val reconstr =
- if name = metisN then
- Metis (type_enc |> the_default (hd partial_type_encs),
- lam_trans |> the_default default_metis_lam_trans)
- else if name = smtN then
- SMT
- else
- raise Fail ("unknown reconstructor: " ^ quote name)
+ val meth =
+ if name = metisN then Metis_Method (type_enc, lam_trans)
+ else if name = smtN then SMT_Method
+ else raise Fail ("unknown proof_method: " ^ quote name)
val used_facts = facts |> map fst
in
(case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
- state subgoal reconstr [reconstr] of
+ state subgoal meth [meth] of
play as (_, Played time) =>
{outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
preplay = Lazy.value play,
message =
fn play =>
let
- val (_, override_params) = extract_reconstructor params reconstr
+ val (_, override_params) = extract_proof_method params meth
val one_line_params =
(play, proof_banner mode name, used_facts, minimize_command override_params name,
subgoal, subgoal_count)
@@ -93,18 +89,18 @@
fun is_prover_supported ctxt =
let val thy = Proof_Context.theory_of ctxt in
- is_reconstructor orf is_atp thy orf is_smt_prover ctxt
+ is_proof_method orf is_atp thy orf is_smt_prover ctxt
end
fun is_prover_installed ctxt =
- is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+ is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
-val reconstructor_default_max_facts = 20
+val proof_method_default_max_facts = 20
fun default_max_facts_of_prover ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then
- reconstructor_default_max_facts
+ if is_proof_method name then
+ proof_method_default_max_facts
else if is_atp thy name then
fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
else (* is_smt_prover ctxt name *)
@@ -113,7 +109,7 @@
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then run_reconstructor mode name
+ if is_proof_method name then run_proof_method mode name
else if is_atp thy name then run_atp mode name
else if is_smt_prover ctxt name then run_smt_solver mode name
else error ("No such prover: " ^ name ^ ".")
@@ -134,7 +130,7 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
- preplay_timeout, ...} : params)
+ smt_proofs, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state goal facts =
let
val _ =
@@ -149,8 +145,8 @@
max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
- slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = ""}
+ smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)]}
@@ -286,20 +282,21 @@
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
\timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
| {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
- handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
+ handle ERROR msg =>
+ (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
end
-fun adjust_reconstructor_params override_params
+fun adjust_proof_method_params override_params
({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
- max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
- preplay_timeout, expect} : params) =
+ max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
+ timeout, preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
(case AList.lookup (op =) override_params name of
SOME [s] => SOME s
| _ => default_value)
- (* Only those options that reconstructors are interested in are considered here. *)
+ (* Only those options that proof_methods are interested in are considered here. *)
val type_enc = lookup_override "type_enc" type_enc
val lam_trans = lookup_override "lam_trans" lam_trans
in
@@ -308,8 +305,8 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
@@ -336,18 +333,18 @@
fun prover_fast_enough () = can_min_fast_enough run_time
in
(case Lazy.force preplay of
- (reconstr as Metis _, Played timeout) =>
+ (meth as Metis_Method _, Played timeout) =>
if isar_proofs = SOME true then
(* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
else if can_min_fast_enough timeout then
- (true, extract_reconstructor params reconstr
+ (true, extract_proof_method params meth
||> (fn override_params =>
- adjust_reconstructor_params override_params params))
+ adjust_proof_method_params override_params params))
else
(prover_fast_enough (), (name, params))
- | (SMT, Played timeout) =>
+ | (SMT_Method, Played timeout) =>
(* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (name, params))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:50:38 2014 +0100
@@ -38,7 +38,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
@@ -212,8 +212,8 @@
do_slice timeout 1 NONE Time.zeroTime
end
-fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
- ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
+ minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -233,9 +233,8 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
- (bunch_of_reconstructors false (fn desperate =>
- if desperate then liftingN else default_metis_lam_trans))),
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =
@@ -248,7 +247,8 @@
end,
if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
| SOME failure =>
- (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+ fn _ => string_of_atp_failure failure, ""))
in
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 19:50:16 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Reconstructors.
-*)
-
-signature SLEDGEHAMMER_RECONSTRUCTOR =
-sig
- type stature = ATP_Problem_Generate.stature
-
- datatype reconstructor =
- Metis of string * string |
- SMT
-
- datatype play_outcome =
- Played of Time.time |
- Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
-
- type minimize_command = string list -> string
- type one_line_params =
- (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
- val smtN : string
-
- val string_of_reconstructor : reconstructor -> string
- val string_of_play_outcome : play_outcome -> string
- val play_outcome_ord : play_outcome * play_outcome -> order
-
- val one_line_proof_text : int -> one_line_params -> string
- val silence_reconstructors : bool -> Proof.context -> Proof.context
-end;
-
-structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
-struct
-
-open ATP_Util
-open ATP_Problem_Generate
-open ATP_Proof_Reconstruct
-
-datatype reconstructor =
- Metis of string * string |
- SMT
-
-datatype play_outcome =
- Played of Time.time |
- Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
-
-type minimize_command = string list -> string
-type one_line_params =
- (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
-val smtN = "smt"
-
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
- | string_of_reconstructor SMT = smtN
-
-fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
- | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
- | string_of_play_outcome Play_Failed = "failed"
- | string_of_play_outcome _ = "unknown"
-
-fun play_outcome_ord (Played time1, Played time2) =
- int_ord (pairself Time.toMilliseconds (time1, time2))
- | play_outcome_ord (Played _, _) = LESS
- | play_outcome_ord (_, Played _) = GREATER
- | play_outcome_ord (Not_Played, Not_Played) = EQUAL
- | play_outcome_ord (Not_Played, _) = LESS
- | play_outcome_ord (_, Not_Played) = GREATER
- | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
- int_ord (pairself Time.toMilliseconds (time1, time2))
- | play_outcome_ord (Play_Timed_Out _, _) = LESS
- | play_outcome_ord (_, Play_Timed_Out _) = GREATER
- | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
-
-(* FIXME: Various bugs, esp. with "unfolding"
-fun unusing_chained_facts _ 0 = ""
- | unusing_chained_facts used_chaineds num_chained =
- if length used_chaineds = num_chained then ""
- else if null used_chaineds then "(* using no facts *) "
- else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
-*)
-
-fun apply_on_subgoal _ 1 = "by "
- | apply_on_subgoal 1 _ = "apply "
- | apply_on_subgoal i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
-
-fun command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
-fun reconstructor_command reconstr i n used_chaineds num_chained ss =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-fun try_command_line banner time command =
- banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "."
-
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- (case minimize_command ss of
- "" => ""
- | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
-
-fun split_used_facts facts =
- facts
- |> List.partition (fn (_, (sc, _)) => sc = Chained)
- |> pairself (sort_distinct (string_ord o pairself fst))
-
-fun one_line_proof_text num_chained
- ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
-
- val (failed, ext_time) =
- (case play of
- Played time => (false, (SOME (false, time)))
- | Play_Timed_Out time => (false, SOME (true, time))
- | Play_Failed => (true, NONE)
- | Not_Played => (false, NONE))
-
- val try_line =
- map fst extra
- |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
- |> (if failed then
- enclose "One-line proof reconstruction failed: "
- ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
- else
- try_command_line banner ext_time)
- in
- try_line ^ minimize_line minimize_command (map fst (extra @ chained))
- end
-
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
- bound exceeded" warnings and the like. *)
-fun silence_reconstructors debug =
- Try0.silence_methods debug
- #> Config.put SMT_Config.verbose debug
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 19:50:38 2014 +0100
@@ -69,10 +69,10 @@
| "" => SOME true
| _ => raise Option.Option)
handle Option.Option =>
- let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
- error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss) ^ ".")
- end
+ let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+ error ("Parameter " ^ quote name ^ " must be assigned " ^
+ space_implode " " (serial_commas "or" ss) ^ ".")
+ end
val has_junk =
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
@@ -80,8 +80,8 @@
fun parse_time name s =
let val secs = if has_junk s then NONE else Real.fromString s in
if is_none secs orelse Real.< (the secs, 0.0) then
- error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
- \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
+ error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
+ \(e.g., \"60\", \"0.5\") or \"none\".")
else
seconds (the secs)
end
--- a/src/Tools/Code/code_namespace.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML Mon Feb 03 19:50:38 2014 +0100
@@ -42,26 +42,42 @@
(** fundamental module name hierarchy **)
-fun lookup_identifier identifiers sym =
- Code_Symbol.lookup identifiers sym
- |> Option.map (split_last o Long_Name.explode);
+fun module_fragments' { identifiers, reserved } name =
+ case Code_Symbol.lookup_module_data identifiers name of
+ SOME (fragments, _) => fragments
+ | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name);
+
+fun module_fragments { module_name, identifiers, reserved } =
+ if module_name = ""
+ then module_fragments' { identifiers = identifiers, reserved = reserved }
+ else K (Long_Name.explode module_name);
-fun force_identifier ctxt fragments_tab force_module identifiers sym =
- case lookup_identifier identifiers sym of
- NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
+fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
+ let
+ val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
+ val module_fragments' = module_fragments
+ { module_name = module_name, identifiers = identifiers, reserved = reserved };
+ in
+ fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
+ module_names Symtab.empty
+ end;
+
+fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym =
+ case Code_Symbol.lookup identifiers sym of
+ NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym,
+ Code_Symbol.default_base sym)
| SOME prefix_name => if null force_module then prefix_name
else (force_module, snd prefix_name);
-fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
- let
- fun alias_fragments name = case module_identifiers name
- of SOME name' => Long_Name.explode name'
- | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
- val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
- in
- fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
- module_names Symtab.empty
- end;
+fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers;
+
+fun build_proto_program { empty, add_stmt, add_dep } program =
+ empty
+ |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
+ |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
+ Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
+
+fun prioritize has_priority = uncurry append o List.partition has_priority;
(** flat program structure **)
@@ -73,13 +89,12 @@
let
(* building module name hierarchy *)
- val module_identifiers = if module_name = ""
- then Code_Symbol.lookup_module_data identifiers
- else K (SOME module_name);
- val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
- module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
+ val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
+ module_name = module_name, identifiers = identifiers, reserved = reserved } program;
+ val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
+ force_module = Long_Name.explode module_name, identifiers = identifiers }
#>> Long_Name.implode;
+ val sym_priority = has_priority identifiers;
(* distribute statements over hierarchy *)
fun add_stmt sym stmt =
@@ -89,7 +104,7 @@
Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
#> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
end;
- fun add_dependency sym sym' =
+ fun add_dep sym sym' =
let
val (module_name, _) = prep_sym sym;
val (module_name', _) = prep_sym sym';
@@ -97,10 +112,8 @@
then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
end;
- val proto_program = Graph.empty
- |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
- |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
- Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
+ val proto_program = build_proto_program
+ { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
(* name declarations and statement modifications *)
fun declare sym (base, stmt) (gr, nsp) =
@@ -109,7 +122,8 @@
val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
in (gr', nsp') end;
fun declarations gr = (gr, empty_nsp)
- |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr)
+ |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
+ (prioritize sym_priority (Code_Symbol.Graph.keys gr))
|> fst
|> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
val flat_program = proto_program
@@ -165,12 +179,11 @@
let
(* building module name hierarchy *)
- val module_identifiers = if module_name = ""
- then Code_Symbol.lookup_module_data identifiers
- else K (SOME module_name);
- val fragments_tab = build_module_namespace ctxt { module_prefix = "",
- module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
+ val module_namespace = build_module_namespace ctxt { module_prefix = "",
+ module_name = module_name, identifiers = identifiers, reserved = reserved } program;
+ val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
+ force_module = Long_Name.explode module_name, identifiers = identifiers }
+ val sym_priority = has_priority identifiers;
(* building empty module hierarchy *)
val empty_module = (empty_data, Code_Symbol.Graph.empty);
@@ -184,9 +197,9 @@
#> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
val empty_program =
empty_module
- |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
+ |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace
|> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
- o lookup_identifier identifiers o fst) program;
+ o Code_Symbol.lookup identifiers o fst) program;
(* distribute statements over hierarchy *)
fun add_stmt sym stmt =
@@ -195,7 +208,7 @@
in
(map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
end;
- fun add_dependency sym sym' =
+ fun add_dep sym sym' =
let
val (name_fragments, _) = prep_sym sym;
val (name_fragments', _) = prep_sym sym';
@@ -211,17 +224,18 @@
^ " would result in module dependency cycle"))
else Code_Symbol.Graph.add_edge dep
in (map_module name_fragments_common o apsnd) add_edge end;
- val proto_program = empty_program
- |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
- |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
- Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
+ val proto_program = build_proto_program
+ { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program;
(* name declarations, data and statement modifications *)
fun make_declarations nsps (data, nodes) =
let
- val (module_fragments, stmt_syms) = List.partition
- (fn sym => case Code_Symbol.Graph.get_node nodes sym
- of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
+ val (module_fragments, stmt_syms) =
+ Code_Symbol.Graph.keys nodes
+ |> List.partition
+ (fn sym => case Code_Symbol.Graph.get_node nodes sym
+ of (_, Module _) => true | _ => false)
+ |> pairself (prioritize sym_priority)
fun declare namify sym (nsps, nodes) =
let
val (base, node) = Code_Symbol.Graph.get_node nodes sym;
--- a/src/Tools/Code/code_target.ML Mon Feb 03 19:50:16 2014 +0100
+++ b/src/Tools/Code/code_target.ML Mon Feb 03 19:50:38 2014 +0100
@@ -81,7 +81,8 @@
class * (string * 'c option) list, (class * class) * (string * 'd option) list,
(class * string) * (string * 'e option) list,
string * (string * 'f option) list) Code_Symbol.attr;
-type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
+type identifier_data = (string list * string, string list * string, string list * string, string list * string,
+ string list * string, string list * string) Code_Symbol.data;
type tyco_syntax = Code_Printer.tyco_syntax;
type raw_const_syntax = Code_Printer.raw_const_syntax;
@@ -144,7 +145,7 @@
val y' = Name.desymbolize false y;
in ys' @ [y'] end;
in if xs' = xs
- then s
+ then if is_module then (xs, "") else split_last xs
else error ("Invalid code name: " ^ quote s ^ "\n"
^ "better try " ^ quote (Long_Name.implode xs'))
end;
@@ -372,11 +373,12 @@
val width = the_default default_width some_width;
in (fn program => prepared_serializer program width, prepared_program) end;
-fun invoke_serializer thy target some_width module_name args program syms =
+fun invoke_serializer thy target some_width raw_module_name args program syms =
let
- val check = if module_name = "" then I else check_name true;
+ val module_name = if raw_module_name = "" then ""
+ else (check_name true raw_module_name; raw_module_name)
val (mounted_serializer, prepared_program) = mount_serializer thy
- target some_width (check module_name) args program syms;
+ target some_width module_name args program syms;
in mounted_serializer prepared_program end;
fun assert_module_name "" = error "Empty module name not allowed here"