--- a/doc-src/Sledgehammer/sledgehammer.tex Mon May 30 16:10:12 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon May 30 16:15:37 2011 +0100
@@ -249,34 +249,27 @@
\slshape
Sledgehammer: ``\textit{e}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis last\_ConsL}) (46 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{vampire}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{spass}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps insert\_Nil}) (25 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
-\phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
+Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
\postw
Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
@@ -286,13 +279,11 @@
where the goal's conclusion is a (universally quantified) equation.
For each successful prover, Sledgehammer gives a one-liner proof that uses Metis
-or the \textit{smt} proof method. For Metis, timings are shown in parentheses,
-indicating how fast the call is. You can click the proof to insert it into the
-theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
-command if you want to look for a shorter (and probably faster) proof. But here
-the proof found by Vampire is both short and fast already.
+or the \textit{smt} proof method. For Metis, approximate timings are shown in
+parentheses, indicating how fast the call is. You can click the proof to insert
+it into the theory text.
-You can ask Sledgehammer for an Isar text proof by passing the
+In addition, you can ask Sledgehammer for an Isar text proof by passing the
\textit{isar\_proof} option (\S\ref{output-format}):
\prew
@@ -526,21 +517,27 @@
in a successful Metis proof, you can advantageously replace the \textit{metis}
call with \textit{metisFT}.
-\point{Should I minimize the number of lemmas?}
+\point{Are generated proofs minimal?}
-In general, minimization is a good idea, because proofs involving fewer lemmas
-tend to be shorter as well, and hence easier to re-find by Metis. But the
-opposite is sometimes the case. Keep an eye on the timing information displayed
-next to the suggested Metis calls.
+Automatic provers frequently use many more facts than are necessary.
+Sledgehammer inclues a minimization tool that takes a set of facts returned by a
+given prover and repeatedly calls the same prover or Metis with subsets of those
+axioms in order to find a minimal set. Reducing the number of axioms typically
+improves Metis's speed and success rate, while also removing superfluous clutter
+from the proof scripts.
-\point{Why does the minimizer sometimes starts on its own?}
+In earlier versions of Sledgehammer, generated proofs were accompanied by a
+suggestion to invoke the minimization tool. This step is now performed
+implicitly if it can be done in a reasonable amount of time (something that can
+be guessed from the number of facts in the original proof and the time it took
+to find it or replay it).
-There are two scenarios in which this can happen. First, some provers (notably
-CVC3, Satallax, and Yices) do not provide proofs or sometimes provide incomplete
-proofs. The minimizer is then invoked to find out which facts are actually
-needed from the (large) set of facts that was initinally given to the prover.
-Second, if a prover returns a proof with lots of facts, the minimizer is invoked
-automatically since Metis would be unlikely to re-find the proof.
+In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
+proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
+find out which facts are actually needed from the (large) set of facts that was
+initinally given to the prover. Finally, if a prover returns a proof with lots
+of facts, the minimizer is invoked automatically since Metis would be unlikely
+to re-find the proof.
\point{A strange error occurred---what should I do?}
@@ -666,7 +663,6 @@
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -750,6 +746,11 @@
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
for experimental purposes. It requires version 2.18 or above.
+
+\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
+the external provers, Metis itself can be used for proof search.
+
+\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
\end{enum}
In addition, the following remote provers are supported:
@@ -814,6 +815,9 @@
success rate to running the most effective of these for 120~seconds
\cite{boehme-nipkow-2010}.
+For the \textit{min} subcommand, the default prover is \textit{metis}. If
+several provers are set, the first one is used.
+
\opnodefault{prover}{string}
Alias for \textit{provers}.
@@ -861,13 +865,6 @@
\label{problem-encoding}
\begin{enum}
-\opfalse{explicit\_apply}{implicit\_apply}
-Specifies whether function application should be encoded as an explicit
-``apply'' operator in ATP problems. If the option is set to \textit{false}, each
-function will be directly applied to as many arguments as possible. Enabling
-this option can sometimes help discover higher-order proofs that otherwise would
-not be found.
-
\opfalse{full\_types}{partial\_types}
Specifies whether full type information is encoded in ATP problems. Enabling
this option prevents the discovery of type-incorrect proofs, but it can slow
@@ -969,6 +966,12 @@
\nopagebreak
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
+
+\opsmart{explicit\_apply}{implicit\_apply}
+Specifies whether function application should be encoded as an explicit
+``apply'' operator in ATP problems. If the option is set to \textit{false}, each
+function will be directly applied to as many arguments as possible. Disabling
+this option can sometimes prevent the discovery of higher-order proofs.
\end{enum}
\subsection{Relevance Filter}
@@ -983,11 +986,11 @@
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
are relevant and 1 only theorems that refer to previously seen constants.
-\opsmart{max\_relevant}{smart\_int}
+\opdefault{max\_relevant}{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. A typical value would be
-300.
+250.
\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
Specifies the maximum number of monomorphic instances to generate beyond
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 16:15:37 2011 +0100
@@ -397,9 +397,10 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
- ({outcome = SOME failure, message = "", used_facts = [],
- run_time_in_msecs = NONE}, ~1)
- val ({outcome, message, used_facts, run_time_in_msecs}
+ ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ preplay = K Sledgehammer_ATP_Reconstruct.Failed_to_Play,
+ message = K ""}, ~1)
+ val ({outcome, used_facts, run_time_in_msecs, preplay, message}
: Sledgehammer_Provers.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
@@ -415,14 +416,15 @@
subgoal_count = Sledgehammer_Util.subgoal_count st,
facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
smt_filter = NONE}
- in prover params (K "") problem end)) ()
+ in prover params (K (K "")) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time_in_msecs |> the_default ~1
+ val msg = message (preplay ())
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_prover, used_facts))
- | SOME _ => (message, SH_FAIL (time_isa, time_prover))
+ NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
+ | SOME _ => (msg, SH_FAIL (time_isa, time_prover))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -503,18 +505,20 @@
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
- val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt
+ val params = Sledgehammer_Isar.default_params ctxt
[("provers", prover_name),
("verbose", "true"),
("type_sys", type_sys),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
- (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)
+ true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
+ val (used_facts, (preplay, message)) = minimize st (these (!named_thms))
+ val msg = message (preplay ())
in
- case minimize st (these (!named_thms)) of
- (SOME named_thms', msg) =>
+ case used_facts of
+ SOME named_thms' =>
(change_data id inc_min_succs;
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
@@ -523,7 +527,7 @@
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
- | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
+ | NONE => log (minimize_tag id ^ "failed: " ^ msg)
end
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 30 16:15:37 2011 +0100
@@ -16,7 +16,7 @@
datatype failure =
Unprovable |
- IncompleteUnprovable |
+ GaveUp |
ProofMissing |
ProofIncomplete |
UnsoundProof of bool * string list |
@@ -73,7 +73,7 @@
datatype failure =
Unprovable |
- IncompleteUnprovable |
+ GaveUp |
ProofMissing |
ProofIncomplete |
UnsoundProof of bool * string list |
@@ -146,7 +146,7 @@
" "
fun string_for_failure Unprovable = "The problem is unprovable."
- | string_for_failure IncompleteUnprovable = "The prover gave up."
+ | string_for_failure GaveUp = "The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
| string_for_failure ProofIncomplete =
@@ -231,7 +231,7 @@
extract_known_failure known_failures output) of
(_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
| ("", SOME failure) =>
- ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable
+ ("", SOME (if failure = GaveUp andalso complete then Unprovable
else failure))
| ("", NONE) =>
("", SOME (if res_code = 0 andalso output = "" then ProofMissing
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 30 16:15:37 2011 +0100
@@ -117,18 +117,11 @@
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
)
-fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
+fun to_secs time = (Time.toMilliseconds time + 999) div 1000
(* E *)
-(* Give E an extra second to reconstruct the proof. Older versions even get two
- seconds, because the "eproof" script wrongly subtracted an entire second to
- account for the overhead of the script itself, which is in fact much
- lower. *)
-fun e_bonus () =
- if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
-
val tstp_proof_delims =
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
@@ -210,8 +203,7 @@
arguments = fn ctxt => fn slice => fn timeout => fn weights =>
"--tstp-in --tstp-out -l5 " ^
e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
- " -tAutoDev --silent --cpu-limit=" ^
- string_of_int (to_secs (e_bonus ()) timeout),
+ " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
proof_delims = tstp_proof_delims,
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
@@ -229,8 +221,8 @@
best_slices = fn ctxt =>
(* FUDGE *)
if effective_e_weight_method ctxt = e_slicesN then
- [(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *),
- (0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *),
+ [(0.333, (true, (100, ["mangled_preds_heavy"]))) (* sym_offset_weight *),
+ (0.333, (true, (800, ["poly_preds?"]))) (* auto *),
(0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
(* fun_weight *)]
else
@@ -251,12 +243,12 @@
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
arguments = fn ctxt => fn slice => fn timeout => fn _ =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
|> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
known_perl_failures @
- [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
+ [(GaveUp, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
@@ -286,7 +278,7 @@
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
arguments = fn ctxt => fn slice => fn timeout => fn _ =>
- "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+ "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
" --thanks \"Andrei and Krystof\" --input_file"
|> (slice < 2 orelse Config.get ctxt vampire_force_sos)
? prefix "--sos on ",
@@ -296,9 +288,9 @@
("% SZS output start Refutation", "% SZS output end Refutation"),
("% SZS output start Proof", "% SZS output end Proof")],
known_failures =
- [(Unprovable, "UNPROVABLE"),
- (IncompleteUnprovable, "CANNOT PROVE"),
- (IncompleteUnprovable, "SZS status GaveUp"),
+ [(GaveUp, "UNPROVABLE"),
+ (GaveUp, "CANNOT PROVE"),
+ (GaveUp, "SZS status GaveUp"),
(ProofIncomplete, "predicate_definition_introduction,[]"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
@@ -325,12 +317,12 @@
{exec = ("Z3_HOME", "z3"),
required_execs = [],
arguments = fn _ => fn _ => fn timeout => fn _ =>
- "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
+ "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
proof_delims = [],
known_failures =
[(Unprovable, "\nsat"),
- (IncompleteUnprovable, "\nunknown"),
- (IncompleteUnprovable, "SZS status Satisfiable"),
+ (GaveUp, "\nunknown"),
+ (GaveUp, "SZS status Satisfiable"),
(ProofMissing, "\nunsat"),
(ProofMissing, "SZS status Unsatisfiable")],
conj_sym_kind = Hypothesis,
@@ -382,16 +374,16 @@
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn _ => fn timeout => fn _ =>
- "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
^ " -s " ^ the_system system_name system_versions,
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @
[(Unprovable, "says Satisfiable"),
(Unprovable, "says CounterSatisfiable"),
+ (GaveUp, "says Unknown"),
+ (GaveUp, "says GaveUp"),
(ProofMissing, "says Theorem"),
(ProofMissing, "says Unsatisfiable"),
- (IncompleteUnprovable, "says Unknown"),
- (IncompleteUnprovable, "says GaveUp"),
(TimedOut, "says Timeout"),
(Inappropriate, "says Inappropriate")],
conj_sym_kind = conj_sym_kind,
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon May 30 16:15:37 2011 +0100
@@ -9,6 +9,9 @@
signature METIS_TACTICS =
sig
+ val metisN : string
+ val metisF_N : string
+ val metisFT_N : string
val trace : bool Config.T
val verbose : bool Config.T
val type_lits : bool Config.T
@@ -26,6 +29,14 @@
open Metis_Translate
open Metis_Reconstruct
+fun method_binding_for_mode HO = @{binding metis}
+ | method_binding_for_mode FO = @{binding metisF}
+ | method_binding_for_mode FT = @{binding metisFT}
+
+val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
+val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
+val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
+
val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -53,10 +64,6 @@
models = []}
val resolution_params = {active = active_params, waiting = waiting_params}
-fun method_binding_for_mode HO = @{binding metis}
- | method_binding_for_mode FO = @{binding metisF}
- | method_binding_for_mode FT = @{binding metisFT}
-
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
@@ -136,7 +143,8 @@
| mode :: _ =>
(verbose_warning ctxt
("Falling back on " ^
- quote (Binding.str_of (method_binding_for_mode mode)) ^ "...");
+ quote (Binding.qualified_name_of
+ (method_binding_for_mode mode)) ^ "...");
FOL_SOLVE fallback_modes ctxt cls ths0)
val neg_clausify =
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Mon May 30 16:15:37 2011 +0100
@@ -111,7 +111,9 @@
Synchronized.change_result global_state
(fn {manager, timeout_heap, active, canceling, messages, store} =>
messages
- |> List.partition (fn (urgent, _) => null active orelse urgent)
+ |> List.partition
+ (fn (urgent, _) =>
+ (null active andalso null canceling) orelse urgent)
||> (fn postponed_messages =>
make_state manager timeout_heap active canceling
postponed_messages store))
@@ -156,7 +158,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister (false, "Timed out.\n"));
+ |> List.app (unregister (false, "Timed out."));
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 16:15:37 2011 +0100
@@ -17,14 +17,14 @@
MetisFT |
SMT of string
- datatype preplay =
- Preplayed of reconstructor * Time.time |
+ datatype play =
+ Played of reconstructor * Time.time |
Trust_Playable of reconstructor * Time.time option|
- Failed_to_Preplay
+ Failed_to_Play
type minimize_command = string list -> string
type one_line_params =
- preplay * string * (string * locality) list * minimize_command * int * int
+ play * string * (string * locality) list * minimize_command * int * int
type isar_params =
bool * bool * int * type_system * string Symtab.table * int list list
* int * (string * locality) list vector * int Symtab.table * string proof
@@ -40,9 +40,10 @@
Proof.context -> type_system -> int list list -> int
-> (string * locality) list vector -> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
+ val reconstructor_name : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val isar_proof_text :
- Proof.context -> isar_params -> one_line_params -> string
+ Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
end;
@@ -62,14 +63,14 @@
MetisFT |
SMT of string
-datatype preplay =
- Preplayed of reconstructor * Time.time |
+datatype play =
+ Played of reconstructor * Time.time |
Trust_Playable of reconstructor * Time.time option |
- Failed_to_Preplay
+ Failed_to_Play
type minimize_command = string list -> string
type one_line_params =
- preplay * string * (string * locality) list * minimize_command * int * int
+ play * string * (string * locality) list * minimize_command * int * int
type isar_params =
bool * bool * int * type_system * string Symtab.table * int list list * int
* (string * locality) list vector * int Symtab.table * string proof * thm
@@ -288,7 +289,7 @@
val (chained, extra) = split_used_facts used_facts
val (reconstructor, ext_time) =
case preplay of
- Preplayed (reconstructor, time) =>
+ Played (reconstructor, time) =>
(SOME reconstructor, (SOME (false, time)))
| Trust_Playable (reconstructor, time) =>
(SOME reconstructor,
@@ -296,13 +297,13 @@
NONE => NONE
| SOME time =>
if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Preplay => (NONE, NONE)
+ | Failed_to_Play => (NONE, NONE)
val try_line =
case reconstructor of
SOME r => ([], map fst extra)
|> reconstructor_command r subgoal subgoal_count
|> try_command_line banner ext_time
- | NONE => "Proof reconstruction failed."
+ | NONE => "One-line proof reconstruction failed."
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
(** Hard-core proof reconstruction: structured Isar proofs **)
@@ -1044,11 +1045,13 @@
(if n <> 1 then "next" else "qed")
in do_proof end
-fun isar_proof_text ctxt
+fun isar_proof_text ctxt isar_proof_requested
(debug, full_types, isar_shrink_factor, type_sys, pool,
conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
+ val isar_shrink_factor =
+ (if isar_proof_requested then 1 else 2) * isar_shrink_factor
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
@@ -1064,20 +1067,31 @@
|> kill_useless_labels_in_proof
|> relabel_proof
|> string_for_proof ctxt full_types subgoal subgoal_count of
- "" => "\nNo structured proof available (proof too short)."
- | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
+ "" =>
+ if isar_proof_requested then
+ "\nNo structured proof available (proof too short)."
+ else
+ ""
+ | proof =>
+ "\n\n" ^ (if isar_proof_requested then "Structured proof"
+ else "Perhaps this will work") ^
+ ":\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
if debug then
isar_proof_for ()
else
- try isar_proof_for ()
- |> the_default "\nWarning: The Isar proof construction failed."
+ case try isar_proof_for () of
+ SOME s => s
+ | NONE => if isar_proof_requested then
+ "\nWarning: The Isar proof construction failed."
+ else
+ ""
in one_line_proof ^ isar_proof end
fun proof_text ctxt isar_proof isar_params
(one_line_params as (preplay, _, _, _, _, _)) =
- (if isar_proof orelse preplay = Failed_to_Preplay then
- isar_proof_text ctxt isar_params
+ (if isar_proof orelse preplay = Failed_to_Play then
+ isar_proof_text ctxt isar_proof isar_params
else
one_line_proof_text) one_line_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 30 16:15:37 2011 +0100
@@ -46,7 +46,7 @@
-> translated_formula option * ((string * locality) * thm)
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_system
- -> bool -> term list -> term
+ -> bool option -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
* (string * 'a) list vector * int list * int Symtab.table
@@ -199,6 +199,13 @@
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+val type_instance = Sign.typ_instance o Proof_Context.theory_of
+
+fun insert_type ctxt get_T x xs =
+ let val T = get_T x in
+ if exists (curry (type_instance ctxt) T o get_T) xs then xs
+ else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
+ end
(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
@@ -519,8 +526,6 @@
| deep_freeze_atyp T = T
val deep_freeze_type = map_atyps deep_freeze_atyp
-val type_instance = Sign.typ_instance o Proof_Context.theory_of
-
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
@@ -567,46 +572,91 @@
(** "hBOOL" and "hAPP" **)
type sym_info =
- {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
+ {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
-fun add_combterm_syms_to_table explicit_apply =
+fun add_combterm_syms_to_table ctxt explicit_apply =
let
- fun aux top_level tm =
+ fun consider_var_arity const_T var_T max_ary =
+ let
+ fun iter ary T =
+ if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
+ else iter (ary + 1) (range_type T)
+ in iter 0 const_T end
+ fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
let val (head, args) = strip_combterm_comb tm in
(case head of
CombConst ((s, _), T, _) =>
if String.isPrefix bound_var_prefix s then
- I
+ if explicit_apply = NONE andalso can dest_funT T then
+ let
+ fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
+ {pred_sym = pred_sym,
+ min_ary =
+ fold (fn T' => consider_var_arity T' T) types min_ary,
+ max_ary = max_ary, types = types}
+ val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
+ in
+ if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
+ else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
+ end
+ else
+ accum
else
- let val ary = length args in
- Symtab.map_default
- (s, {pred_sym = true,
- min_ary = if explicit_apply then 0 else ary,
- max_ary = 0, typ = SOME T})
- (fn {pred_sym, min_ary, max_ary, typ} =>
- {pred_sym = pred_sym andalso top_level,
- min_ary = Int.min (ary, min_ary),
- max_ary = Int.max (ary, max_ary),
- typ = if typ = SOME T then typ else NONE})
- end
- | _ => I)
- #> fold (aux false) args
+ let
+ val ary = length args
+ in
+ (ho_var_Ts,
+ case Symtab.lookup sym_tab s of
+ SOME {pred_sym, min_ary, max_ary, types} =>
+ let
+ val types' = types |> insert_type ctxt I T
+ val min_ary =
+ if is_some explicit_apply orelse
+ pointer_eq (types', types) then
+ min_ary
+ else
+ fold (consider_var_arity T) ho_var_Ts min_ary
+ in
+ Symtab.update (s, {pred_sym = pred_sym andalso top_level,
+ min_ary = Int.min (ary, min_ary),
+ max_ary = Int.max (ary, max_ary),
+ types = types'})
+ sym_tab
+ end
+ | NONE =>
+ let
+ val min_ary =
+ case explicit_apply of
+ SOME true => 0
+ | SOME false => ary
+ | NONE => fold (consider_var_arity T) ho_var_Ts ary
+ in
+ Symtab.update_new (s, {pred_sym = top_level,
+ min_ary = min_ary, max_ary = ary,
+ types = [T]})
+ sym_tab
+ end)
+ end
+ | _ => accum)
+ |> fold (add false) args
end
- in aux true end
-fun add_fact_syms_to_table explicit_apply =
- fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
+ in add true end
+fun add_fact_syms_to_table ctxt explicit_apply =
+ fact_lift (formula_fold NONE
+ (K (add_combterm_syms_to_table ctxt explicit_apply)))
val default_sym_table_entries : (string * sym_info) list =
- [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
- (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
+ [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
+ (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
(make_fixed_const predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
([tptp_false, tptp_true]
- |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
+ |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
-fun sym_table_for_facts explicit_apply facts =
- Symtab.empty |> fold Symtab.default default_sym_table_entries
- |> fold (add_fact_syms_to_table explicit_apply) facts
+fun sym_table_for_facts ctxt explicit_apply facts =
+ Symtab.empty
+ |> fold Symtab.default default_sym_table_entries
+ |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
fun min_arity_of sym_tab s =
case Symtab.lookup sym_tab s of
@@ -759,7 +809,7 @@
|> close_formula_universally, simp_info, NONE)
end
-fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -775,9 +825,9 @@
Mangled_Type_Args _ => true
| _ => false) andalso
not (null (Term.hidden_polymorphism t)))
- ? (case typ of
- SOME T => specialize_type thy (invert_const unmangled_s, T)
- | NONE => I)
+ ? (case types of
+ [T] => specialize_type thy (invert_const unmangled_s, T)
+ | _ => I)
end)
fun make_facts eq_as_iff =
map_filter (make_fact ctxt format type_sys false eq_as_iff false)
@@ -990,12 +1040,6 @@
(** Symbol declarations **)
-fun insert_type ctxt get_T x xs =
- let val T = get_T x in
- if exists (curry (type_instance ctxt) T o get_T) xs then xs
- else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
- end
-
fun should_declare_sym type_sys pred_sym s =
is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
(case type_sys of
@@ -1223,11 +1267,12 @@
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
- val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
+ val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
- val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
+ val repaired_sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
|> map repair
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 30 16:15:37 2011 +0100
@@ -676,7 +676,7 @@
((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
(accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
|> take max_relevant
- fun append_facts ths accepts =
+ fun append_to_facts accepts ths =
let val add = facts |> filter (member Thm.eq_thm_prop ths o snd) in
(accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
|> take (max_relevant - length add)) @
@@ -685,20 +685,22 @@
fun uses_const s t =
fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
false
- fun maybe_add_set_const (s, ths) accepts =
- accepts |> (if exists (uses_const s o prop_of o snd) accepts orelse
- exists (uses_const s) (concl_t :: hyp_ts) then
- append_facts ths
- else
- I)
+ fun add_set_const_thms accepts (s, ths) =
+ if exists (uses_const s o prop_of o snd) accepts orelse
+ exists (uses_const s) (concl_t :: hyp_ts) then
+ append ths
+ else
+ I
+ fun append_special_facts accepts =
+ [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+ |> fold (add_set_const_thms accepts) set_consts
+ |> append_to_facts accepts
+
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
|> iter 0 max_relevant threshold0 goal_const_tab []
|> not (null add_ths) ? prepend_facts add_ths
- |> (fn accepts =>
- accepts |> could_benefit_from_ext is_built_in_const accepts
- ? append_facts @{thms ext}
- |> fold maybe_add_set_const set_consts)
+ |> append_special_facts
|> tap (fn accepts => trace_msg ctxt (fn () =>
"Total relevant: " ^ string_of_int (length accepts)))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 16:15:37 2011 +0100
@@ -96,7 +96,7 @@
("max_relevant", "smart"),
("max_mono_iters", "3"),
("max_new_mono_instances", "400"),
- ("explicit_apply", "false"),
+ ("explicit_apply", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1"),
("slicing", "true"),
@@ -118,8 +118,8 @@
val params_for_minimize =
["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
- "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
- "preplay_timeout"]
+ "max_new_mono_instances", "explicit_apply", "isar_proof",
+ "isar_shrink_factor", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "full_types", "timeout"]
@@ -262,10 +262,10 @@
| _ => error ("Parameter " ^ quote name ^
"must be assigned a pair of floating-point \
\values (e.g., \"0.6 0.95\")")
- fun lookup_int_option name =
+ fun lookup_option lookup' name =
case lookup name of
SOME "smart" => NONE
- | _ => SOME (lookup_int name)
+ | _ => SOME (lookup' name)
val debug = mode <> Auto_Try andalso lookup_bool "debug"
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
@@ -281,10 +281,10 @@
"smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
| s => Dumb_Type_Sys (type_sys_from_string s)
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
- val max_relevant = lookup_int_option "max_relevant"
+ val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
val max_new_mono_instances = lookup_int "max_new_mono_instances"
- val explicit_apply = lookup_bool "explicit_apply"
+ val explicit_apply = lookup_option lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
@@ -309,17 +309,27 @@
(* Sledgehammer the given subgoal *)
+val default_minimize_prover = Metis_Tactics.metisN
+
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
fun minimize_command override_params i prover_name fact_names =
- sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^
- (override_params |> filter is_raw_param_relevant_for_minimize
- |> implode o map (prefix ", " o string_for_raw_param)) ^
- "] (" ^ space_implode " " fact_names ^ ")" ^
- (if i = 1 then "" else " " ^ string_of_int i)
+ let
+ val params =
+ override_params
+ |> filter is_raw_param_relevant_for_minimize
+ |> map string_for_raw_param
+ |> (if prover_name = default_minimize_prover then I else cons prover_name)
+ |> space_implode ", "
+ in
+ sledgehammerN ^ " " ^ minN ^
+ (if params = "" then "" else enclose " [" "]" params) ^
+ " (" ^ space_implode " " fact_names ^ ")" ^
+ (if i = 1 then "" else " " ^ string_of_int i)
+ end
fun hammer_away override_params subcommand opt_i relevance_override state =
let
@@ -335,7 +345,9 @@
|> K ()
end
else if subcommand = minN then
- run_minimize (get_params Minimize ctxt override_params)
+ run_minimize (get_params Minimize ctxt
+ (("provers", [default_minimize_prover]) ::
+ override_params))
(the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 16:15:37 2011 +0100
@@ -8,13 +8,15 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type locality = Sledgehammer_Filter.locality
+ type play = Sledgehammer_ATP_Reconstruct.play
type params = Sledgehammer_Provers.params
val binary_min_facts : int Config.T
val minimize_facts :
- string -> params -> bool option -> bool -> int -> int -> Proof.state
+ string -> params -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list option * string
+ -> ((string * locality) * thm list) list option
+ * ((unit -> play) * (play -> string))
val run_minimize :
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
end;
@@ -25,6 +27,7 @@
open ATP_Proof
open Sledgehammer_Util
open Sledgehammer_Filter
+open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
(* wrapper for calling external prover *)
@@ -42,26 +45,16 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_sys, isar_proof,
+ max_new_mono_instances, type_sys, explicit_apply, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
- explicit_apply_opt silent (prover : prover) timeout i n state facts =
+ silent (prover : prover) timeout i n state facts =
let
- val ctxt = Proof.context_of state
- val thy = Proof.theory_of state
val _ =
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
else "") ^ "...")
val {goal, ...} = Proof.goal state
- val explicit_apply =
- case explicit_apply_opt of
- SOME explicit_apply => explicit_apply
- | NONE =>
- let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
- not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
- end
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
@@ -75,13 +68,19 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
- val result as {outcome, used_facts, ...} = prover params (K "") problem
+ val result as {outcome, used_facts, run_time_in_msecs, ...} =
+ prover params (K (K "")) problem
in
print silent (fn () =>
case outcome of
SOME failure => string_for_failure failure
- | NONE => if length used_facts = length facts then "Found proof."
- else "Found proof with " ^ n_facts used_facts ^ ".");
+ | NONE => "Found proof" ^
+ (if length used_facts = length facts then ""
+ else " with " ^ n_facts used_facts) ^
+ (case run_time_in_msecs of
+ SOME ms =>
+ " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
+ | NONE => "") ^ ".");
result
end
@@ -145,16 +144,15 @@
part of the timeout. *)
val slack_msecs = 200
-fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
- silent i n state facts =
+fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
+ facts =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
val msecs = Time.toMilliseconds timeout
- val _ = print silent (fn () => "Sledgehammer minimize: " ^
+ val _ = print silent (fn () => "Sledgehammer minimizer: " ^
quote prover_name ^ ".")
- fun do_test timeout =
- test_facts params explicit_apply_opt silent prover timeout i n state
+ fun do_test timeout = test_facts params silent prover timeout i n state
val timer = Timer.startRealTimer ()
in
(case do_test timeout facts of
@@ -165,7 +163,7 @@
Int.min (msecs, Time.toMilliseconds time + slack_msecs)
|> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
- val (min_thms, {message, ...}) =
+ val (min_thms, {preplay, message, ...}) =
if length facts >= Config.get ctxt binary_min_facts then
binary_minimize (do_test new_timeout) facts
else
@@ -176,13 +174,16 @@
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
- in (SOME min_thms, message) end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\").")
- | {message, ...} => (NONE, "Prover error: " ^ message))
- handle ERROR msg => (NONE, "Error: " ^ msg)
+ in (SOME min_thms, (preplay, message)) end
+ | {outcome = SOME TimedOut, preplay, ...} =>
+ (NONE,
+ (preplay,
+ fn _ => "Timeout: You can increase the time limit using the \
+ \\"timeout\" option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ "\")."))
+ | {preplay, message, ...} =>
+ (NONE, (preplay, prefix "Prover error: " o message)))
+ handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg))
end
fun run_minimize (params as {provers, ...}) i refs state =
@@ -200,8 +201,9 @@
[] => error "No prover is set."
| prover :: _ =>
(kill_provers ();
- minimize_facts prover params NONE false i n state facts
- |> snd |> Output.urgent_message)
+ minimize_facts prover params false i n state facts
+ |> (fn (_, (preplay, message)) =>
+ Output.urgent_message (message (preplay ()))))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 16:15:37 2011 +0100
@@ -13,6 +13,7 @@
type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type translated_formula = Sledgehammer_ATP_Translate.translated_formula
type type_system = Sledgehammer_ATP_Translate.type_system
+ type play = Sledgehammer_ATP_Reconstruct.play
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
datatype mode = Auto_Try | Try | Normal | Minimize
@@ -32,7 +33,7 @@
max_relevant: int option,
max_mono_iters: int,
max_new_mono_instances: int,
- explicit_apply: bool,
+ explicit_apply: bool option,
isar_proof: bool,
isar_shrink_factor: int,
slicing: bool,
@@ -56,9 +57,11 @@
{outcome: failure option,
used_facts: (string * locality) list,
run_time_in_msecs: int option,
- message: string}
+ preplay: unit -> play,
+ message: play -> string}
- type prover = params -> minimize_command -> prover_problem -> prover_result
+ type prover =
+ params -> (string -> minimize_command) -> prover_problem -> prover_result
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -73,6 +76,8 @@
val smt_slice_min_secs : int Config.T
val das_tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
+ val is_metis_prover : string -> bool
+ val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
val is_unit_equational_atp : Proof.context -> string -> bool
val is_prover_supported : Proof.context -> string -> bool
@@ -123,6 +128,11 @@
"Async_Manager". *)
val das_tool = "Sledgehammer"
+val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
+
+val is_metis_prover = member (op =) metis_prover_names
+val is_atp = member (op =) o supported_atps
+
val select_smt_solver =
Context.proof_map o SMT_Config.select_solver
@@ -138,22 +148,34 @@
fun is_prover_supported ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
+ is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
end
fun is_prover_installed ctxt =
- is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+ is_metis_prover orf is_smt_prover ctxt orf
+ is_atp_installed (Proof_Context.theory_of ctxt)
-fun get_slices slicing slices =
- (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
+fun get_slices num_facts slicing slices =
+ (0 upto length slices - 1) ~~ slices
+ |> (if slicing andalso
+ exists (fn (_, (_, (max_facts, _))) => max_facts < num_facts)
+ slices then
+ I
+ else
+ List.last #> single)
+
+val metis_default_max_relevant = 20
fun default_max_relevant_for_prover ctxt slicing name =
let val thy = Proof_Context.theory_of ctxt in
- if is_smt_prover ctxt name then
+ if is_metis_prover name then
+ metis_default_max_relevant
+ else if is_atp thy name then
+ fold (Integer.max o fst o snd o snd o snd)
+ (get_slices 16384 (* large number *) slicing
+ (#best_slices (get_atp thy name) ctxt)) 0
+ else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
- else
- fold (Integer.max o fst o snd o snd o snd)
- (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
end
(* These are either simplified away by "Meson.presimplify" (most of the time) or
@@ -250,6 +272,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
+ metis_prover_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
@@ -279,7 +302,7 @@
max_relevant: int option,
max_mono_iters: int,
max_new_mono_instances: int,
- explicit_apply: bool,
+ explicit_apply: bool option,
isar_proof: bool,
isar_shrink_factor: int,
slicing: bool,
@@ -301,11 +324,13 @@
type prover_result =
{outcome: failure option,
- message: string,
used_facts: (string * locality) list,
- run_time_in_msecs: int option}
+ run_time_in_msecs: int option,
+ preplay: unit -> play,
+ message: play -> string}
-type prover = params -> minimize_command -> prover_problem -> prover_result
+type prover =
+ params -> (string -> minimize_command) -> prover_problem -> prover_result
(* configuration attributes *)
@@ -373,13 +398,11 @@
|> Exn.release
|> tap (after path)
-fun proof_banner mode blocking name =
+fun proof_banner mode name =
case mode of
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
- | Normal => if blocking then quote name ^ " found a proof"
- else "Try this"
- | Minimize => "Try this"
+ | _ => "Try this"
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -399,22 +422,21 @@
fun filter_used_facts used = filter (member (op =) used o fst)
-fun preplay_one_line_proof debug timeout ths state i reconstructors =
+fun play_one_line_proof debug timeout ths state i reconstructors =
let
- fun preplay [] [] = Failed_to_Preplay
- | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
- | preplay timed_out (reconstructor :: reconstructors) =
+ fun play [] [] = Failed_to_Play
+ | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+ | play timed_out (reconstructor :: reconstructors) =
let val timer = Timer.startRealTimer () in
case timed_reconstructor reconstructor debug timeout ths state i of
- SOME (SOME _) =>
- Preplayed (reconstructor, Timer.checkRealTimer timer)
- | _ => preplay timed_out reconstructors
+ SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
+ | _ => play timed_out reconstructors
end
handle TimeLimit.TimeOut =>
- preplay (reconstructor :: timed_out) reconstructors
+ play (reconstructor :: timed_out) reconstructors
in
if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
- else preplay [] reconstructors
+ else play [] reconstructors
end
@@ -504,14 +526,26 @@
| _ => type_sys)
| format => (format, type_sys))
-fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
+fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys
- | determine_format_and_type_sys best_type_systems formats
- (Smart_Type_Sys full_types) =
+ | choose_format_and_type_sys best_type_systems formats
+ (Smart_Type_Sys full_types) =
map type_sys_from_string best_type_systems @ fallback_best_type_systems
|> find_first (if full_types then is_type_sys_virtually_sound else K true)
|> the |> adjust_dumb_type_sys formats
+val metis_minimize_max_time = seconds 2.0
+
+fun choose_minimize_command minimize_command name preplay =
+ (case preplay of
+ Played (reconstructor, time) =>
+ if Time.<= (time, metis_minimize_max_time) then
+ reconstructor_name reconstructor
+ else
+ name
+ | _ => name)
+ |> minimize_command
+
fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
Config.put SMT_Config.verbose debug
#> Config.put SMT_Config.monomorph_full false
@@ -521,8 +555,8 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, blocking, type_sys, max_relevant,
- max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
+ ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
+ max_new_mono_instances, explicit_apply, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -565,7 +599,8 @@
let
(* If slicing is disabled, we expand the last slice to fill the
entire time available. *)
- val actual_slices = get_slices slicing (best_slices ctxt)
+ val actual_slices =
+ get_slices (length facts) slicing (best_slices ctxt)
val num_actual_slices = length actual_slices
fun monomorphize_facts facts =
let
@@ -593,8 +628,7 @@
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val (format, type_sys) =
- determine_format_and_type_sys best_type_systems formats
- type_sys
+ choose_format_and_type_sys best_type_systems formats type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> not fairly_sound
@@ -676,8 +710,7 @@
UnsoundProof (is_type_sys_virtually_sound type_sys,
facts |> sort string_ord))
| SOME Unprovable =>
- if null blacklist then outcome
- else SOME IncompleteUnprovable
+ if null blacklist then outcome else SOME GaveUp
| _ => outcome
in
((pool, conjecture_shape, facts_offset, fact_names,
@@ -748,49 +781,54 @@
extract_important_message output
else
""
- val (message, used_facts) =
+ val (used_facts, preplay, message) =
case outcome of
NONE =>
let
val used_facts =
used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
atp_proof
- val reconstructors =
- if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis]
- else [Metis, MetisFT]
- val used_ths =
- facts |> map untranslated_fact
- |> filter_used_facts used_facts
- |> map snd
- val preplay =
- preplay_one_line_proof debug preplay_timeout used_ths state subgoal
- reconstructors
- val full_types = uses_typed_helpers typed_helpers atp_proof
- val isar_params =
- (debug, full_types, isar_shrink_factor, type_sys, pool,
- conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
- goal)
- val one_line_params =
- (preplay, proof_banner mode blocking name, used_facts,
- minimize_command, subgoal, subgoal_count)
in
- (proof_text ctxt isar_proof isar_params one_line_params ^
- (if verbose then
- "\nATP real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
- else
- "") ^
- (if important_message <> "" then
- "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
- important_message
- else
- ""),
- used_facts)
+ (used_facts,
+ fn () =>
+ let
+ val used_ths =
+ facts |> map untranslated_fact |> filter_used_facts used_facts
+ |> map snd
+ in
+ play_one_line_proof debug preplay_timeout used_ths state subgoal
+ [Metis, MetisFT]
+ end,
+ fn preplay =>
+ let
+ val full_types = uses_typed_helpers typed_helpers atp_proof
+ val isar_params =
+ (debug, full_types, isar_shrink_factor, type_sys, pool,
+ conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
+ goal)
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
+ in
+ proof_text ctxt isar_proof isar_params one_line_params ^
+ (if verbose then
+ "\nATP real CPU time: " ^
+ string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+ else
+ "") ^
+ (if important_message <> "" then
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+ important_message
+ else
+ "")
+ end)
end
- | SOME failure => (string_for_failure failure, [])
+ | SOME failure =>
+ ([], K Failed_to_Play, fn _ => string_for_failure failure)
in
- {outcome = outcome, message = message, used_facts = used_facts,
- run_time_in_msecs = msecs}
+ {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
+ preplay = preplay, message = message}
end
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
@@ -814,7 +852,7 @@
remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
- if is_real_cex then Unprovable else IncompleteUnprovable
+ if is_real_cex then Unprovable else GaveUp
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt_failures code of
@@ -931,8 +969,7 @@
end
in do_slice timeout 1 NONE Time.zeroTime end
-fun run_smt_solver mode name
- (params as {debug, verbose, blocking, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
minimize_command
({state, subgoal, subgoal_count, facts, smt_filter, ...}
: prover_problem) =
@@ -945,44 +982,76 @@
smt_filter_loop ctxt name params state subgoal smt_filter facts
val (used_facts, used_ths) = used_facts |> ListPair.unzip
val outcome = outcome |> Option.map failure_from_smt_failure
- val message =
+ val (preplay, message) =
case outcome of
NONE =>
- let
- fun smt_settings () =
- if name = SMT_Solver.solver_name_of ctxt then ""
- else "smt_solver = " ^ maybe_quote name
- val preplay =
- case preplay_one_line_proof debug preplay_timeout used_ths state
- subgoal [Metis, MetisFT] of
- p as Preplayed _ => p
- | _ => Trust_Playable (SMT (smt_settings ()), NONE)
- val one_line_params =
- (preplay, proof_banner mode blocking name, used_facts,
- minimize_command, subgoal, subgoal_count)
- in
- one_line_proof_text one_line_params ^
- (if verbose then
- "\nSMT solver real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
- "."
- else
- "")
- end
- | SOME failure => string_for_failure failure
+ (fn () =>
+ let
+ fun smt_settings () =
+ if name = SMT_Solver.solver_name_of ctxt then ""
+ else "smt_solver = " ^ maybe_quote name
+ in
+ case play_one_line_proof debug preplay_timeout used_ths state
+ subgoal [Metis, MetisFT] of
+ p as Played _ => p
+ | _ => Trust_Playable (SMT (smt_settings ()), NONE)
+ end,
+ fn preplay =>
+ let
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
+ in
+ one_line_proof_text one_line_params ^
+ (if verbose then
+ "\nSMT solver real CPU time: " ^
+ string_from_time (Time.fromMilliseconds
+ (the run_time_in_msecs)) ^ "."
+ else
+ "")
+ end)
+ | SOME failure => (K Failed_to_Play, fn _ => string_for_failure failure)
in
{outcome = outcome, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, message = message}
+ run_time_in_msecs = run_time_in_msecs, preplay = preplay,
+ message = message}
+ end
+
+fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
+ ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
+ let
+ val reconstructor = if name = Metis_Tactics.metisN then Metis
+ else if name = Metis_Tactics.metisFT_N then MetisFT
+ else raise Fail ("unknown Metis version: " ^ quote name)
+ val (used_facts, used_ths) =
+ facts |> map untranslated_fact |> ListPair.unzip
+ in
+ case play_one_line_proof debug timeout used_ths state subgoal
+ [reconstructor] of
+ play as Played (_, time) =>
+ {outcome = NONE, used_facts = used_facts,
+ run_time_in_msecs = SOME (Time.toMilliseconds time),
+ preplay = K play,
+ message = fn play =>
+ let
+ val one_line_params =
+ (play, proof_banner mode name, used_facts,
+ minimize_command name, subgoal, subgoal_count)
+ in one_line_proof_text one_line_params end}
+ | play =>
+ let val failure = if play = Failed_to_Play then GaveUp else TimedOut in
+ {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ preplay = K play, message = fn _ => string_for_failure failure}
+ end
end
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
- if is_smt_prover ctxt name then
- run_smt_solver mode name
- else if member (op =) (supported_atps thy) name then
- run_atp mode name (get_atp thy name)
- else
- error ("No such prover: " ^ name ^ ".")
+ if is_metis_prover name then run_metis mode name
+ else if is_atp thy name then run_atp mode name (get_atp thy name)
+ else if is_smt_prover ctxt name then run_smt_solver mode name
+ else error ("No such prover: " ^ name ^ ".")
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 16:15:37 2011 +0100
@@ -19,6 +19,7 @@
val timeoutN : string
val unknownN : string
val auto_minimize_min_facts : int Config.T
+ val auto_minimize_max_seconds : real Config.T
val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -31,6 +32,7 @@
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_ATP_Translate
+open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
open Sledgehammer_Minimize
@@ -66,26 +68,50 @@
val auto_minimize_min_facts =
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
(fn generic => Config.get_generic generic binary_min_facts)
+val auto_minimize_max_seconds =
+ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
+ (K 5.0)
fun get_minimizing_prover ctxt mode name
- (params as {debug, verbose, explicit_apply, ...}) minimize_command
+ (params as {debug, verbose, ...}) minimize_command
(problem as {state, subgoal, subgoal_count, facts, ...}) =
get_prover ctxt mode name params minimize_command problem
- |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
+ |> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} =>
if is_some outcome then
result
else
let
- val (used_facts, message) =
- if length used_facts
- >= Config.get ctxt auto_minimize_min_facts then
- minimize_facts name params (SOME explicit_apply) (not verbose)
- subgoal subgoal_count state
+ val num_facts = length used_facts
+ fun can_minimize_fast_enough msecs =
+ 0.001 * Real.fromInt ((num_facts + 2) * msecs)
+ <= Config.get ctxt auto_minimize_max_seconds
+ val ((minimize, minimize_name), preplay) =
+ if mode = Normal then
+ if num_facts >= Config.get ctxt auto_minimize_min_facts then
+ ((true, name), preplay)
+ else
+ let val preplay = preplay () in
+ (case preplay of
+ Played (reconstructor, timeout) =>
+ (can_minimize_fast_enough (Time.toMilliseconds timeout),
+ reconstructor_name reconstructor)
+ | _ =>
+ case run_time_in_msecs of
+ SOME msecs => (can_minimize_fast_enough msecs, name)
+ | NONE => (false, name),
+ K preplay)
+ end
+ else
+ ((false, name), preplay)
+ val (used_facts, (preplay, message)) =
+ if minimize then
+ minimize_facts minimize_name params
+ (not verbose) subgoal subgoal_count state
(filter_used_facts used_facts
(map (apsnd single o untranslated_fact) facts))
|>> Option.map (map fst)
else
- (SOME used_facts, message)
+ (SOME used_facts, (preplay, message))
in
case used_facts of
SOME used_facts =>
@@ -103,12 +129,13 @@
else
();
{outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, message = message})
+ run_time_in_msecs = run_time_in_msecs, preplay = preplay,
+ message = message})
| NONE => result
end)
-fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
- expect, ...})
+fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
+ timeout, expect, ...})
mode minimize_command only
{state, goal, subgoal, subgoal_count, facts, smt_filter} name =
let
@@ -128,11 +155,11 @@
smt_filter = smt_filter}
fun really_go () =
problem
- |> get_minimizing_prover ctxt mode name params (minimize_command name)
- |> (fn {outcome, message, ...} =>
+ |> get_minimizing_prover ctxt mode name params minimize_command
+ |> (fn {outcome, preplay, message, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
- else someN, message))
+ else someN, message o preplay))
fun go () =
let
val (outcome_code, message) =
@@ -140,13 +167,13 @@
really_go ()
else
(really_go ()
- handle ERROR message => (unknownN, "Error: " ^ message ^ "\n")
+ handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
| exn =>
if Exn.is_interrupt exn then
reraise exn
else
- (unknownN, "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ (unknownN, fn () => "Internal error:\n" ^
+ ML_Compiler.exn_message exn ^ "\n"))
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
@@ -167,23 +194,26 @@
|> outcome_code = someN
? Proof.goal_message (fn () =>
[Pretty.str "",
- Pretty.mark Markup.hilite (Pretty.str message)]
+ Pretty.mark Markup.hilite (Pretty.str (message ()))]
|> Pretty.chunks))
end
else if blocking then
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
in
- (if outcome_code = someN then message
- else if mode = Normal then quote name ^ ": " ^ message
- else "")
+ (if outcome_code = someN orelse mode = Normal then
+ quote name ^ ": " ^ message ()
+ else
+ "")
|> Async_Manager.break_into_chunks
|> List.app Output.urgent_message;
(outcome_code, state)
end
else
(Async_Manager.launch das_tool birth_time death_time (desc ())
- (apfst (curry (op =) someN) o go);
+ ((fn (outcome_code, message) =>
+ (verbose orelse outcome_code = someN,
+ message ())) o go);
(unknownN, state))
end
--- a/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 16:15:37 2011 +0100
@@ -43,7 +43,7 @@
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
smt_filter = NONE}
in
- (case prover params (K "") problem of
+ (case prover params (K (K "")) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
--- a/src/HOL/ex/tptp_export.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/HOL/ex/tptp_export.ML Mon May 30 16:15:37 2011 +0100
@@ -103,7 +103,7 @@
facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
Sledgehammer_ATP_Translate.translate_atp_fact ctxt format
type_sys true ((Thm.get_name_hint th, loc), th)))
- val explicit_apply = false
+ val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format
ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []
--- a/src/Pure/Tools/find_theorems.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon May 30 16:15:37 2011 +0100
@@ -13,12 +13,32 @@
datatype theorem =
Internal of Facts.ref * thm | External of Facts.ref * term
+ type 'term query = {
+ goal: thm option,
+ limit: int option,
+ rem_dups: bool,
+ criteria: (bool * 'term criterion) list
+ }
+
val tac_limit: int Unsynchronized.ref
val limit: int Unsynchronized.ref
+
+ val read_criterion: Proof.context -> string criterion -> term criterion
+ val query_parser: (bool * string criterion) list parser
+
+ val xml_of_query: term query -> XML.tree
+ val query_of_xml: XML.tree -> term query
+ val xml_of_result: int option * theorem list -> XML.tree
+ val result_of_xml: XML.tree -> int option * theorem list
+
val find_theorems: Proof.context -> thm option -> int option -> bool ->
+ (bool * term criterion) list -> int option * (Facts.ref * thm) list
+ val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
- val filter_theorems: Proof.context -> theorem list -> thm option ->
- int option -> bool -> (bool * string criterion) list ->
+
+ val filter_theorems: Proof.context -> theorem list -> term query ->
+ int option * theorem list
+ val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
int option * theorem list
val pretty_theorem: Proof.context -> theorem -> Pretty.T
@@ -81,11 +101,98 @@
end;
+(** queries **)
+
+type 'term query = {
+ goal: thm option,
+ limit: int option,
+ rem_dups: bool,
+ criteria: (bool * 'term criterion) list
+};
+
+fun map_criteria f {goal, limit, rem_dups, criteria} =
+ {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
+
+fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
+ | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
+ | xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , [])
+ | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
+ | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
+ | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
+ | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
+ | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
+
+fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
+ | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
+ | criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff
+ | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
+ | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
+ | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
+ | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
+ | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
+ | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
+
+fun xml_of_query {goal=NONE, limit, rem_dups, criteria} =
+ let
+ val properties = []
+ |> (if rem_dups then cons ("rem_dups", "") else I)
+ |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
+ in
+ XML.Elem (("Query", properties), XML_Data.make_list
+ (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
+ end
+ | xml_of_query _ = raise Fail "cannot serialize goal";
+
+fun query_of_xml (XML.Elem (("Query", properties), body)) =
+ let
+ val rem_dups = Properties.defined properties "rem_dups";
+ val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
+ val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool
+ (criterion_of_xml o the_single)) body;
+ in
+ {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
+ end
+ | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
+
(** theorems, either internal or external (without proof) **)
datatype theorem =
Internal of Facts.ref * thm |
- External of Facts.ref * term;
+ External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
+
+fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) =
+ Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
+ | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
+ Position.markup pos o Markup.properties [("name", name)]
+ | fact_ref_markup fact_ref = raise Fail "bad fact ref"
+
+fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
+ | xml_of_theorem (External (fact_ref, prop)) =
+ XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop])
+
+fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
+ let
+ val name = the (Properties.get properties "name");
+ val pos = Position.of_properties properties;
+ val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
+ (Properties.get properties "index");
+ in
+ External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
+ end
+ | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
+
+fun xml_of_result (opt_found, theorems) =
+ let
+ val properties =
+ if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
+ in
+ XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
+ end;
+
+fun result_of_xml (XML.Elem (("Result", properties), body)) =
+ (Properties.get properties "found" |> Option.map Markup.parse_int,
+ XML_Data.dest_list (theorem_of_xml o the_single) body)
+ | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
| prop_of (External (_, prop)) = prop;
@@ -420,16 +527,10 @@
val limit = Unsynchronized.ref 40;
-fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
+fun filter_theorems ctxt theorems query =
let
- val assms =
- Proof_Context.get_fact ctxt (Facts.named "local.assms")
- handle ERROR _ => [];
- val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
- val opt_goal' = Option.map add_prems opt_goal;
-
- val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val filters = map (filter_criterion ctxt opt_goal') criteria;
+ val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query
+ val filters = map (filter_criterion ctxt opt_goal) criteria;
fun find_all theorems =
let
@@ -451,10 +552,25 @@
in find theorems end;
-fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
- filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
- rem_dups raw_criteria
- |> apsnd (map (fn Internal f => f));
+fun filter_theorems_cmd ctxt theorems raw_query =
+ filter_theorems ctxt theorems (map_criteria
+ (map (apsnd (read_criterion ctxt))) raw_query);
+
+fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
+ let
+ val assms =
+ Proof_Context.get_fact ctxt (Facts.named "local.assms")
+ handle ERROR _ => [];
+ val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
+ val opt_goal' = Option.map add_prems opt_goal;
+ in
+ filter ctxt (map Internal (all_facts_of ctxt))
+ {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria}
+ |> apsnd (map (fn Internal f => f))
+ end;
+
+val find_theorems = gen_find_theorems filter_theorems;
+val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
@@ -465,13 +581,13 @@
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
-fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val start = Timing.start ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
- opt_goal opt_limit rem_dups raw_criteria;
+ val (foundo, theorems) = find
+ {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
val returned = length theorems;
val tally_msg =
@@ -493,6 +609,8 @@
map (pretty_theorem ctxt) theorems)
end |> Pretty.chunks |> Pretty.writeln;
+fun print_theorems ctxt =
+ gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
(** command syntax **)
@@ -516,10 +634,12 @@
--| Parse.$$$ ")")) (NONE, true);
in
+val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+
val _ =
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
Keyword.diag
- (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
+ (options -- query_parser
>> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.no_timing o
Toplevel.keep (fn state =>
--- a/src/Tools/WWW_Find/IsaMakefile Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/IsaMakefile Mon May 30 16:15:37 2011 +0100
@@ -29,8 +29,9 @@
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
- http_status.ML http_util.ML mime.ML scgi_req.ML scgi_server.ML \
- socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
+ html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
+ scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
+ ROOT.ML
@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
--- a/src/Tools/WWW_Find/ROOT.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/ROOT.ML Mon May 30 16:15:37 2011 +0100
@@ -10,5 +10,7 @@
use "scgi_req.ML";
use "scgi_server.ML";
use "echo.ML";
- use "find_theorems.ML")
+ use "html_templates.ML";
+ use "find_theorems.ML";
+ use "yxml_find_theorems.ML")
else ()
--- a/src/Tools/WWW_Find/find_theorems.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/find_theorems.ML Mon May 30 16:15:37 2011 +0100
@@ -7,237 +7,56 @@
local
val default_limit = 20;
-val thy_names = sort string_ord (Thy_Info.get_names ());
-
-val find_theorems_url = "find_theorems";
-
-fun is_sorry thm =
- Thm.proof_of thm
- |> Proofterm.approximate_proof_body
- |> Proofterm.all_oracles_of
- |> exists (fn (x, _) => x = "Pure.skip_proof");
-
-local open Xhtml in
-fun find_theorems_form thy_name (query, limit, withdups) =
- let
- val query_input =
- input (id "query", {
- name = "query",
- itype = TextInput { value = query, maxlength = NONE }});
-
- val max_results = divele noid
- [
- label (noid, { for = "limit" }, "Max. results:"),
- input (id "limit",
- { name = "limit",
- itype = TextInput { value = SOME (string_of_int limit),
- maxlength = NONE }})
- ];
-
- val theories = divele noid
- [
- label (noid, { for = "theory" }, "Search in:"),
- select (id "theory", { name = "theory", value = SOME thy_name })
- thy_names
- ];
-
- val with_dups = divele noid
- [
- label (noid, { for = "withdups" }, "Allow duplicates:"),
- input (id "withdups",
- { name = "withdups",
- itype = Checkbox { checked = withdups, value = SOME "true" }})
- ];
-
- val help = divele (class "help")
- [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
- in
- form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
- [tag "fieldset" []
- [tag "legend" [] [text "find_theorems"],
- (add_script (OnKeyPress, "encodequery(this)")
- o add_script (OnChange, "encodequery(this)")
- o add_script (OnMouseUp, "encodequery(this)")) query_input,
- divele (class "settings") [ max_results, theories, with_dups, help ],
- divele (class "mainbuttons")
- [ reset_button (id "reset"), submit_button (id "submit") ]
- ]
- ]
- end;
-
-fun html_header thy_name args =
- html { lang = "en" } [
- head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
- [script (noid, { script_type="text/javascript",
- src="/find_theorems.js" })],
- add_script (OnLoad, "encodequery(document.getElementById('query'))")
- (body noid [
- h (noid, 1, "Theory " ^ thy_name),
- find_theorems_form thy_name args,
- divele noid []
- ])
- ];
-
-fun html_error msg = p ((class "error"), msg);
-
-val find_theorems_table =
- table (class "findtheorems")
- [
- thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
- tbody noid []
- ];
-
-fun show_criterion (b, c) =
- let
- fun prfx s = let
- val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
- in span (class c, v) end;
-
- fun prfxwith s = let
- val (c, v) =
- if b
- then ("criterion", "with " ^ s)
- else ("ncriterion", "without " ^ s);
- in span (class c, v) end;
- in
- (case c of
- Find_Theorems.Name name => prfx ("name: " ^ quote name)
- | Find_Theorems.Intro => prfx "intro"
- | Find_Theorems.IntroIff => prfx "introiff"
- | Find_Theorems.Elim => prfx "elim"
- | Find_Theorems.Dest => prfx "dest"
- | Find_Theorems.Solves => prfx "solves"
- | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
- | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
- end;
-
-fun find_theorems_summary (othmslen, thmslen, query, args) =
- let
- val args =
- (case othmslen of
- NONE => args
- | SOME l => Symtab.update ("limit", string_of_int l) args)
- val qargs = HttpUtil.make_query_string args;
-
- val num_found_text =
- (case othmslen of
- NONE => text (string_of_int thmslen)
- | SOME l =>
- a { href = find_theorems_url ^
- (if qargs = "" then "" else "?" ^ qargs),
- text = string_of_int l })
- val found = [text "found ", num_found_text, text " theorems"] : tag list;
- val displayed =
- if is_some othmslen
- then " (" ^ string_of_int thmslen ^ " displayed)"
- else "";
- fun show_search c = tr [ td' noid [show_criterion c] ];
- in
- table (class "findtheoremsquery")
- (* [ tr [ th (noid, "searched for:") ] ]
- @ map show_search query @ *)
- [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
- end
-
-fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
-
-fun html_thm ctxt (n, (thmref, thm)) =
- let
- val output_thm =
- Output.output o Pretty.string_of_margin 100 o
- Display.pretty_thm (Config.put show_question_marks false ctxt);
- in
- tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
- [
- tag' "td" (class "name")
- [span' (sorry_class thm)
- [raw_text (Facts.string_of_ref thmref)]
- ],
- tag' "td" (class "thm") [pre noid (output_thm thm)]
- ]
- end;
-
-end;
-
-val criterion =
- Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
- Parse.reserved "intro" >> K Find_Theorems.Intro ||
- Parse.reserved "elim" >> K Find_Theorems.Elim ||
- Parse.reserved "dest" >> K Find_Theorems.Dest ||
- Parse.reserved "solves" >> K Find_Theorems.Solves ||
- Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
- Parse.term >> Find_Theorems.Pattern;
-
-val parse_query =
- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
+val all_thy_names = sort string_ord (Thy_Info.get_names ());
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
-fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
- content, send) =
+fun find_theorems arg_data send =
let
- val arg_data =
- (case request_method of
- ScgiReq.Get => query_string
- | ScgiReq.Post =>
- content
- |> Byte.bytesToString
- |> HttpUtil.parse_query_string
- | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
-
val args = Symtab.lookup arg_data;
- val query = the_default "" (args "query");
+ val query_str = the_default "" (args "query");
fun get_query () =
- query
- |> (fn s => s ^ ";")
+ (query_str ^ ";")
|> Outer_Syntax.scan Position.start
|> filter Token.is_proper
- |> Scan.error parse_query
+ |> Scan.error Find_Theorems.query_parser
|> fst;
- val limit =
- args "limit"
- |> Option.mapPartial Int.fromString
- |> the_default default_limit;
- val thy_name =
- args "theory"
- |> the_default "Main";
+ val limit = case args "limit" of
+ NONE => default_limit
+ | SOME str => the_default default_limit (Int.fromString str);
+ val thy_name = the_default "Main" (args "theory");
val with_dups = is_some (args "with_dups");
+
+ val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
- fun do_find () =
+ fun do_find query =
let
- val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
- val query = get_query ();
- val (othmslen, thms) = apsnd rev
- (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
- val thmslen = length thms;
- fun thm_row args = Xhtml.write send (html_thm ctxt args);
+ val (othmslen, thms) =
+ Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
+ ||> rev;
in
Xhtml.write send
- (find_theorems_summary (othmslen, thmslen, query, arg_data));
+ (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
if null thms then ()
- else (Xhtml.write_open send find_theorems_table;
- HTML_Unicode.print_mode (app_index thm_row) thms;
- Xhtml.write_close send find_theorems_table)
+ else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
+ HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
end;
-
- val header = (html_header thy_name (args "query", limit, with_dups));
in
send Xhtml.doctype_xhtml1_0_strict;
- Xhtml.write_open send header;
- if query = "" then ()
- else
- do_find ()
- handle
- ERROR msg => Xhtml.write send (html_error msg)
- | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e)); (* FIXME avoid handle e *)
- Xhtml.write_close send header
+ Xhtml.write_enclosed send
+ (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
+ (fn send =>
+ if query_str = "" then ()
+ else
+ do_find (get_query ())
+ handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
end;
in
val () = Printer.show_question_marks_default := false;
-val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/html_templates.ML Mon May 30 16:15:37 2011 +0100
@@ -0,0 +1,163 @@
+(* Title: Tools/WWW_Find/html_templates.ML
+ Author: Timothy Bourke, NICTA
+
+HTML Templates for find theorems server.
+*)
+
+signature HTML_TEMPLATES =
+sig
+ val find_theorems_form: string -> (string option * int * bool * string list) -> Xhtml.tag
+
+ val header: string -> (string option * int * bool * string list) -> Xhtml.tag
+ val error: string -> Xhtml.tag
+ val find_theorems_table: Xhtml.tag
+
+ val find_theorems_summary: int option * int * string Symtab.table -> Xhtml.tag
+ val html_thm: Proof.context -> (int * (Facts.ref * thm)) -> Xhtml.tag
+end
+
+
+structure HTML_Templates: HTML_TEMPLATES =
+struct
+
+open Xhtml;
+
+fun find_theorems_form thy_name (query, limit, withdups, all_thy_names) =
+ let
+ val query_input =
+ input (id "query", {
+ name = "query",
+ itype = TextInput { value = query, maxlength = NONE }});
+
+ val max_results = divele noid
+ [
+ label (noid, { for = "limit" }, "Max. results:"),
+ input (id "limit",
+ { name = "limit",
+ itype = TextInput { value = SOME (string_of_int limit),
+ maxlength = NONE }})
+ ];
+
+ val theories = divele noid
+ [
+ label (noid, { for = "theory" }, "Search in:"),
+ select (id "theory", { name = "theory", value = SOME thy_name })
+ all_thy_names
+ ];
+
+ val with_dups = divele noid
+ [
+ label (noid, { for = "withdups" }, "Allow duplicates:"),
+ input (id "withdups",
+ { name = "withdups",
+ itype = Checkbox { checked = withdups, value = SOME "true" }})
+ ];
+
+ val help = divele (class "help")
+ [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
+ in
+ form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
+ [tag "fieldset" []
+ [tag "legend" [] [text "find_theorems"],
+ (add_script (OnKeyPress, "encodequery(this)")
+ o add_script (OnChange, "encodequery(this)")
+ o add_script (OnMouseUp, "encodequery(this)")) query_input,
+ divele (class "settings") [ max_results, theories, with_dups, help ],
+ divele (class "mainbuttons")
+ [ reset_button (id "reset"), submit_button (id "submit") ]
+ ]
+ ]
+ end;
+
+fun header thy_name args =
+ html { lang = "en" } [
+ head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
+ [script (noid, { script_type="text/javascript",
+ src="/find_theorems.js" })],
+ add_script (OnLoad, "encodequery(document.getElementById('query'))")
+ (body noid [
+ h (noid, 1, "Theory " ^ thy_name),
+ find_theorems_form thy_name args,
+ divele noid []
+ ])
+ ];
+
+fun error msg = p ((class "error"), msg);
+
+val find_theorems_table =
+ table (class "findtheorems")
+ [
+ thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
+ tbody noid []
+ ];
+
+fun show_criterion (b, c) =
+ let
+ fun prfx s = let
+ val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
+ in span (class c, v) end;
+ in
+ (case c of
+ Find_Theorems.Name name => prfx ("name: " ^ quote name)
+ | Find_Theorems.Intro => prfx "intro"
+ | Find_Theorems.IntroIff => prfx "introiff"
+ | Find_Theorems.Elim => prfx "elim"
+ | Find_Theorems.Dest => prfx "dest"
+ | Find_Theorems.Solves => prfx "solves"
+ | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
+ | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
+ end;
+
+fun find_theorems_summary (othmslen, thmslen, args) =
+ let
+ val args =
+ (case othmslen of
+ NONE => args
+ | SOME l => Symtab.update ("limit", string_of_int l) args)
+ val qargs = HttpUtil.make_query_string args;
+
+ val num_found_text =
+ (case othmslen of
+ NONE => text (string_of_int thmslen)
+ | SOME l =>
+ a { href = "find_theorems" ^
+ (if qargs = "" then "" else "?" ^ qargs),
+ text = string_of_int l })
+ val found = [text "found ", num_found_text, text " theorems"] : tag list;
+ val displayed =
+ if is_some othmslen
+ then " (" ^ string_of_int thmslen ^ " displayed)"
+ else "";
+ in
+ table (class "findtheoremsquery")
+ [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
+ end
+
+(*FIXME!?!*)
+fun is_sorry thm =
+ Thm.proof_of thm
+ |> Proofterm.approximate_proof_body
+ |> Proofterm.all_oracles_of
+ |> exists (fn (x, _) => x = "Pure.skip_proof");
+
+fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
+
+fun html_thm ctxt (n, (thmref, thm)) =
+ let
+ val output_thm =
+ Output.output o Pretty.string_of_margin 100 o
+ Display.pretty_thm (Config.put show_question_marks false ctxt);
+ in
+ tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
+ [
+ tag' "td" (class "name")
+ [span' (sorry_class thm)
+ [raw_text (Facts.string_of_ref thmref)]
+ ],
+ tag' "td" (class "thm") [pre noid (output_thm thm)]
+ ]
+ end;
+
+end;
+
+
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind Mon May 30 16:15:37 2011 +0100
@@ -124,7 +124,7 @@
WWWPORT=`sed -e 's/[ ]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
SCGIPORT=`sed -e 's/[ ]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
-MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
+MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
case "$COMMAND" in
start)
--- a/src/Tools/WWW_Find/scgi_server.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/scgi_server.ML Mon May 30 16:15:37 2011 +0100
@@ -11,6 +11,8 @@
val register : (string * Mime.t option * handler) -> unit
val server : string -> int -> unit
val server' : int -> string -> int -> unit (* keeps trying for port *)
+ val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
+ val raw_post_handler : (string -> string) -> handler
end;
structure ScgiServer : SCGI_SERVER =
@@ -121,5 +123,19 @@
server' (countdown - 1) server_prefix port);
end;
+fun simple_handler h (ScgiReq.Req {request_method, query_string, ...}, content, send) =
+ h (case request_method of
+ ScgiReq.Get => query_string
+ | ScgiReq.Post =>
+ content
+ |> Byte.bytesToString
+ |> HttpUtil.parse_query_string
+ | ScgiReq.Head => raise Fail "Cannot handle Head requests.")
+ send;
+
+fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
+ send (h (Byte.bytesToString content))
+ | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
+
end;
--- a/src/Tools/WWW_Find/xhtml.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/WWW_Find/xhtml.ML Mon May 30 16:15:37 2011 +0100
@@ -31,8 +31,7 @@
val show: tag -> string list
val write: (string -> unit) -> tag -> unit
- val write_open: (string -> unit) -> tag -> unit
- val write_close: (string -> unit) -> tag -> unit
+ val write_enclosed: (string -> unit) -> tag -> ((string -> unit) -> unit) -> unit
val html: { lang : string } -> tag list -> tag
val head: { title : string, stylesheet_href : string } -> tag list -> tag
@@ -243,6 +242,9 @@
in f x; close nm; pr_text text end);
in f end;
+fun write_enclosed pr template content =
+ (write_open pr template; content pr; write_close pr template)
+
fun html { lang } tags = Tag ("html",
[("xmlns", "http://www.w3.org/1999/xhtml"),
("xml:lang", lang)],
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/yxml_find_theorems.ML Mon May 30 16:15:37 2011 +0100
@@ -0,0 +1,47 @@
+(* Title: src/Pure/Tools/yxml_find_theorems.ML
+ Author: Sree Harsha Totakura, TUM
+ Lars Noschinski, TUM
+ Alexander Krauss, TUM
+
+Simple find theorems web service with yxml interface for programmatic
+invocation.
+*)
+
+signature YXML_FIND_THEOREMS =
+sig
+ val init: unit -> unit
+end
+
+
+structure YXML_Find_Theorems : YXML_FIND_THEOREMS =
+struct
+
+val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *)
+
+fun yxml_find_theorems theorem_list yxml_query =
+ let
+ val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory);
+ in
+ Find_Theorems.query_of_xml (YXML.parse yxml_query)
+ |> Find_Theorems.filter_theorems ctxt theorem_list
+ ||> rev o (filter (fn Find_Theorems.External x => true | _ => false))
+ |> Find_Theorems.xml_of_result |> YXML.string_of
+ end;
+
+fun visible_facts facts =
+ Facts.dest_static [] facts
+ |> filter_out (Facts.is_concealed facts o #1);
+
+fun init () =
+ let
+ val all_facts =
+ maps Facts.selections
+ (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory)))
+ |> map (Find_Theorems.External o apsnd prop_of);
+ in
+ ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*),
+ ScgiServer.raw_post_handler (yxml_find_theorems all_facts))
+ end;
+
+end;
+
--- a/src/Tools/try.ML Mon May 30 16:10:12 2011 +0100
+++ b/src/Tools/try.ML Mon May 30 16:15:37 2011 +0100
@@ -54,7 +54,8 @@
(* configuration *)
-val tool_ord = prod_ord int_ord string_ord o pairself (swap o apsnd #1)
+fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
+ prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
structure Data = Theory_Data
(