--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Dec 16 20:14:04 2010 +0000
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Dec 16 20:14:21 2010 +0000
@@ -552,11 +552,14 @@
\opfalse{verbose}{quiet}
Specifies whether the \textbf{sledgehammer} command should explain what it does.
+This option is implicitly disabled for automatic runs.
\opfalse{debug}{no\_debug}
Specifies whether Sledgehammer should display additional debugging information
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
-enables \textit{verbose} behind the scenes.
+enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
+behind the scenes. The \textit{debug} option is implicitly disabled for
+automatic runs.
\nopagebreak
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 16 20:14:21 2010 +0000
@@ -346,7 +346,6 @@
fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
- val thy = ProofContext.theory_of ctxt
val i = 1
fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
| change_dir NONE = I
@@ -537,9 +536,6 @@
val reconstructor = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
- val ctxt = Proof.context_of pre
- val (prover_name, _) = get_prover ctxt args
- val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
val trivial =
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 16 20:14:21 2010 +0000
@@ -100,11 +100,12 @@
| string_for_failure prover NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail prover
| string_for_failure prover MalformedInput =
- "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
- \developers."
+ "The " ^ prover ^ " problem is malformed. Please report this to the \
+ \Isabelle developers."
| string_for_failure prover MalformedOutput =
"The " ^ prover ^ " output is malformed."
- | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
+ | string_for_failure prover Interrupted =
+ "The " ^ prover ^ " was interrupted."
| string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
| string_for_failure prover InternalError =
"An internal " ^ prover ^ " error occurred."
@@ -216,9 +217,9 @@
fun parse_term x =
(scan_general_id
- -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
- --| $$ ")") []
- --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
+ -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
+ --| $$ ")") []
+ --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
>> ATerm) x
and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
@@ -253,6 +254,8 @@
Scan.optional ($$ "," |-- parse_annotation false
--| Scan.option ($$ "," |-- parse_annotations false)) []
+val vampire_unknown_fact = "unknown"
+
(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
val parse_tstp_line =
@@ -263,7 +266,8 @@
let
val (name, deps) =
case deps of
- ["file", _, s] => ((num, SOME s), [])
+ ["file", _, s] =>
+ ((num, if s = vampire_unknown_fact then NONE else SOME s), [])
| _ => ((num, NONE), deps)
in
case role of
@@ -281,13 +285,16 @@
(**** PARSING OF VAMPIRE OUTPUT ****)
val parse_vampire_braced_stuff =
- $$ "{" -- scan_general_id -- $$ "}"
- -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
+ $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
+val parse_vampire_parenthesized_detritus =
+ $$ "(" |-- parse_vampire_detritus --| $$ ")"
(* Syntax: <num>. <formula> <annotation> *)
val parse_vampire_line =
scan_general_id --| $$ "." -- parse_formula
- --| Scan.option parse_vampire_braced_stuff -- parse_annotation true
+ --| Scan.option parse_vampire_braced_stuff
+ --| Scan.option parse_vampire_parenthesized_detritus
+ -- parse_annotation true
>> (fn ((num, phi), deps) =>
Inference ((num, NONE), phi, map (rpair NONE) deps))
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Dec 16 20:14:21 2010 +0000
@@ -153,8 +153,9 @@
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
arguments = fn complete => fn timeout =>
- ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
- " --thanks Andrei --input_file")
+ (* This would work too but it's less tested: "--proof tptp " ^ *)
+ "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+ " --thanks \"Andrei and Krystof\" --input_file"
|> not complete ? prefix "--sos on ",
has_incomplete_mode = true,
proof_delims =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper Thu Dec 16 20:14:21 2010 +0000
@@ -0,0 +1,45 @@
+#!/usr/bin/env perl
+#
+# Author: Jasmin Blanchette, TU Muenchen
+#
+# Invoke Z3 with error detection and correction.
+# To use this wrapper, set
+#
+# Z3_REAL_SOLVER=/path-to-z3/z3
+# Z3_SOLVER=$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/z3_wrapper
+#
+# in your "~/.isabelle/etc/settings" file.
+
+my $in_file = @ARGV[$ARGV - 1];
+my $out_file = "/tmp/foo"; # FIXME
+my $err_file = "/tmp/bar"; # FIXME
+
+$ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set";
+
+RUN:
+my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file";
+
+if ($code == 0) {
+ open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\"";
+ my @out_lines = <OUT_FILE>;
+ close(OUT_FILE);
+ print @out_lines;
+} else {
+ open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\"";
+ my @err_lines = <ERR_FILE>;
+ close(ERR_FILE);
+ foreach (@err_lines) {
+ if (m/[lL]ine ([0-9]+)/) {
+ open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\"";
+ my @in_lines = <IN_FILE>;
+ close(IN_FILE);
+ delete $in_lines[$1 - 1];
+ open(IN_FILE, ">$in_file") || die "Cannot open file \"$in_file\"";
+ print IN_FILE join ("", @in_lines);
+ close(IN_FILE);
+ goto RUN;
+ }
+ }
+ print STDERR @err_lines;
+ exit $code;
+}
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Thu Dec 16 20:14:21 2010 +0000
@@ -76,12 +76,13 @@
(* search for necessary substitutions *)
-fun new_substitutions thy grounds (n, T) subst =
+fun new_substitutions thy limit grounds (n, T) subst =
if not (typ_has_tvars T) then [subst]
else
Symtab.lookup_list grounds n
|> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
|> cons subst
+ |> take limit (* limit the breadth of the search as well as the width *)
fun apply_subst grounds consts subst =
let
@@ -97,11 +98,11 @@
end
in fold_map apply_const consts #>> pair subst end
-fun specialize thy all_grounds new_grounds scs =
+fun specialize thy limit all_grounds new_grounds scs =
let
fun spec (subst, consts) next_grounds =
[subst]
- |> fold (maps o new_substitutions thy new_grounds) consts
+ |> fold (maps o new_substitutions thy limit new_grounds) consts
|> rpair next_grounds
|-> fold_map (apply_subst all_grounds consts)
in
@@ -115,7 +116,7 @@
let
val thy = ProofContext.theory_of ctxt
val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
- val spec = specialize thy all_grounds' new_grounds
+ val spec = specialize thy limit all_grounds' new_grounds
val (scss', new_grounds') = fold_map spec scss Symtab.empty
in
if Symtab.is_empty new_grounds' then scss'
--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 20:14:21 2010 +0000
@@ -202,7 +202,12 @@
fun expf t i T ts =
let val Ts = U.dest_funT i T |> fst |> drop (length ts)
- in Term.list_comb (t, ts) |> fold_rev eta Ts end
+ in
+ Term.list_comb (t, ts)
+ |> Term.incr_boundvars (length Ts)
+ |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
+ |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
+ end
fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
| expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
@@ -249,16 +254,18 @@
val T = Term.fastype_of1 (Us @ Ts, t)
val lev = length Us
val bs = sort int_ord (Term.add_loose_bnos (t, lev, []))
- val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs
+ val bss = map_index (fn (i, j) => (j + lev, i + lev)) bs
val norm = perhaps (AList.lookup (op =) bss)
val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t
val Ts' = map (nth Ts) bs
fun mk_abs U u = Abs (Name.uu, U, u)
val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t')
+
+ fun app f = Term.list_comb (f, map Bound bs)
in
(case Termtab.lookup defs abs_rhs of
- SOME (f, _) => (Term.list_comb (f, map Bound bs), cx)
+ SOME (f, _) => (app f, cx)
| NONE =>
let
val (n, ctxt') =
@@ -270,7 +277,7 @@
|> fold_rev (mk_bapp o snd) bss
|> fold_rev mk_bapp (0 upto (length Us - 1))
val def = mk_def (Us @ Ts') T lhs t'
- in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
+ in (app f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
end
fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
@@ -356,7 +363,7 @@
| (u as Bound i, ts) =>
appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i)
| (Abs (n, T, u), ts) =>
- let val env' = (get_arities 0 u [] :: arities, T :: Ts)
+ let val env' = (get_arities 0 u [0] :: arities, T :: Ts)
in traverses env (Abs (n, T, traverse env' u)) ts end
| (u, ts) => traverses env u ts)
and traverses env t ts = Term.list_comb (t, map (traverse env) ts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Dec 16 20:14:21 2010 +0000
@@ -144,6 +144,8 @@
"\nTo minimize the number of lemmas, try this: " ^
Markup.markup Markup.sendback command ^ "."
+val vampire_fact_prefix = "f" (* grrr... *)
+
fun resolve_fact fact_names ((_, SOME s)) =
(case strip_prefix_and_unascii fact_prefix s of
SOME s' => (case find_first_in_list_vector fact_names s' of
@@ -151,7 +153,7 @@
| NONE => [])
| NONE => [])
| resolve_fact fact_names (num, NONE) =
- case Int.fromString num of
+ case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
SOME j =>
if j > 0 andalso j <= Vector.length fact_names then
Vector.sub (fact_names, j - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Dec 16 20:14:21 2010 +0000
@@ -220,28 +220,13 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
- it leaves metaequalities over "prop"s alone. *)
-val atomize_term =
- let
- fun aux (@{const Trueprop} $ t1) = t1
- | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
- HOLogic.all_const T $ Abs (s, T, aux t')
- | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
- | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
- HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
- | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
- HOLogic.eq_const T $ t1 $ t2
- | aux _ = raise Fail "aux"
- in perhaps (try aux) end
-
(* making fact and conjecture formulas *)
fun make_formula ctxt eq_as_iff presimp name kind t =
let
val thy = ProofContext.theory_of ctxt
val t = t |> Envir.beta_eta_contract
|> transform_elim_term
- |> atomize_term
+ |> Object_Logic.atomize_term thy
val need_trueprop = (fastype_of t = HOLogic.boolT)
val t = t |> need_trueprop ? HOLogic.mk_Trueprop
|> extensionalize_term
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Dec 16 20:14:21 2010 +0000
@@ -53,8 +53,7 @@
val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
-(* experimental features *)
-val term_patterns = false
+(* experimental feature *)
val respect_no_atp = true
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
@@ -126,6 +125,75 @@
|> snd
end
+(* This is a terrible hack. Free variables are sometimes code as "M__" when they
+ are displayed as "M" and we want to avoid clashes with these. But sometimes
+ it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
+ free variables. In the worse case scenario, where the fact won't be resolved
+ correctly, the user can fix it manually, e.g., by naming the fact in
+ question. Ideally we would need nothing of it, but backticks just don't work
+ with schematic variables. *)
+fun all_prefixes_of s =
+ map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
+fun close_form t =
+ (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
+ |> fold (fn ((s, i), T) => fn (t', taken) =>
+ let val s' = Name.variant taken s in
+ ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
+ else Term.all) T
+ $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
+ s' :: taken)
+ end)
+ (Term.add_vars t [] |> sort_wrt (fst o fst))
+ |> fst
+
+fun string_for_term ctxt t =
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) (Syntax.string_of_term ctxt) t
+ |> String.translate (fn c => if Char.isPrint c then str c else "")
+ |> simplify_spaces
+
+(** Structural induction rules **)
+
+fun struct_induct_rule_on th =
+ 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
+ exists (exists_subterm (curry (op aconv) p)) prems andalso
+ not (exists (exists_subterm (curry (op aconv) a)) prems) then
+ SOME (p_name, ind_T)
+ else
+ NONE
+ | _ => NONE
+
+fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), (multi, th))
+ ind_x =
+ let
+ fun varify_noninducts (t as Free (s, T)) =
+ if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
+ | varify_noninducts t = t
+ val p_inst =
+ concl_prop |> map_aterms varify_noninducts |> close_form
+ |> lambda (Free ind_x)
+ |> string_for_term ctxt
+ in
+ ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
+ (multi, th |> read_instantiate ctxt [((p_name, 0), p_inst)]))
+ end
+
+fun type_match thy (T1, T2) =
+ (Sign.typ_match thy (T2, T1) Vartab.empty; true)
+ handle Type.TYPE_MATCH => false
+
+fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) =
+ case struct_induct_rule_on th of
+ SOME (p_name, ind_T) =>
+ let val thy = ProofContext.theory_of ctxt in
+ stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
+ |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
+ end
+ | NONE => [ax]
+
(***************************************************************)
(* Relevance Filtering *)
(***************************************************************)
@@ -171,21 +239,13 @@
| pattern_for_type (TFree (s, _)) = PApp (s, [])
| pattern_for_type (TVar _) = PVar
-fun pterm thy t =
- case strip_comb t of
- (Const x, ts) => PApp (pconst thy true x ts)
- | (Free x, ts) => PApp (pconst thy false x ts)
- | (Var _, []) => PVar
- | _ => PApp ("?", []) (* equivalence class of higher-order constructs *)
(* Pairs a constant with the list of its type instantiations. *)
-and ptype thy const x ts =
+fun ptype thy const x =
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
- else []) @
- (if term_patterns then map (pterm thy) ts else [])
-and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
-and rich_ptype thy const (s, T) ts =
- PType (order_of_type T, ptype thy const (s, T) ts)
-and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
+ else [])
+fun rich_ptype thy const (s, T) =
+ PType (order_of_type T, ptype thy const (s, T))
+fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
fun string_for_hyper_pconst (s, ps) =
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
@@ -202,11 +262,12 @@
let
val flip = Option.map not
(* We include free variables, as well as constants, to handle locales. For
- each quantifiers that must necessarily be skolemized by the ATP, we
- introduce a fresh constant to simulate the effect of Skolemization. *)
+ each quantifiers that must necessarily be skolemized by the automatic
+ prover, we introduce a fresh constant to simulate the effect of
+ Skolemization. *)
fun do_const const x ts =
(not (is_built_in_const x ts)
- ? add_pconst_to_table also_skolems (rich_pconst thy const x ts))
+ ? add_pconst_to_table also_skolems (rich_pconst thy const x))
#> fold do_term ts
and do_term t =
case strip_comb t of
@@ -266,17 +327,16 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun theory_const_prop_of ({theory_const_rel_weight,
- theory_const_irrel_weight, ...} : relevance_fudge)
- th =
+fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
+ : relevance_fudge) thy_name t =
if exists (curry (op <) 0.0) [theory_const_rel_weight,
theory_const_irrel_weight] then
- let
- val name = Context.theory_name (theory_of_thm th)
- val t = Const (name ^ theory_const_suffix, @{typ bool})
- in t $ prop_of th end
+ Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
else
- prop_of th
+ t
+
+fun theory_const_prop_of fudge th =
+ theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
(**** Constant / Type Frequencies ****)
@@ -300,7 +360,7 @@
let
fun do_const const (s, T) ts =
(* Two-dimensional table update. Constant maps to types maps to count. *)
- PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
+ PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
|> Symtab.map_default (s, PType_Tab.empty)
#> fold do_term ts
and do_term t =
@@ -454,7 +514,6 @@
fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
|> is_none
-
fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
(fudge as {threshold_divisor, ridiculous_threshold, ...})
({add, del, ...} : relevance_override) facts goal_ts =
@@ -574,9 +633,9 @@
(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
- ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy",
- "case_cong", "weak_case_cong"]
+ ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
+ "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
+ "weak_case_cong"]
|> map (prefix ".")
val max_lambda_nesting = 3
@@ -709,26 +768,6 @@
val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
-fun all_prefixes_of s =
- map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
-
-(* This is a terrible hack. Free variables are sometimes code as "M__" when they
- are displayed as "M" and we want to avoid clashes with these. But sometimes
- it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
- free variables. In the worse case scenario, where the fact won't be resolved
- correctly, the user can fix it manually, e.g., by naming the fact in
- question. Ideally we would need nothing of it, but backticks just don't work
- with schematic variables. *)
-fun close_form t =
- (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
- |> fold (fn ((s, i), T) => fn (t', taken) =>
- let val s' = Name.variant taken s in
- (Term.all T $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
- s' :: taken)
- end)
- (Term.add_vars t [] |> sort_wrt (fst o fst))
- |> fst
-
fun all_facts ctxt reserved no_dangerous_types
({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
add_ths chained_ths =
@@ -765,12 +804,8 @@
else
let
val multi = length ths > 1
- fun backquotify th =
- "`" ^ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ()))
- (Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`"
- |> String.translate (fn c => if Char.isPrint c then str c else "")
- |> simplify_spaces
+ val backquotify =
+ enclose "`" "`" o string_for_term ctxt o close_form o prop_of
fun check_thms a =
case try (ProofContext.get_thms ctxt) a of
NONE => false
@@ -820,24 +855,29 @@
List.partition (fst o snd) #> op @ #> map (apsnd snd)
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
-(***************************************************************)
-(* ATP invocation methods setup *)
-(***************************************************************)
+fun external_frees t =
+ [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
fun relevant_facts ctxt no_dangerous_types (threshold0, threshold1)
max_relevant is_built_in_const fudge
(override as {add, only, ...}) chained_ths hyp_ts concl_t =
let
+ val thy = ProofContext.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
val add_ths = Attrib.eval_thms ctxt add
val reserved = reserved_isar_keyword_table ()
+ val ind_stmt =
+ Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
+ |> Object_Logic.atomize_term thy
+ val ind_stmt_xs = external_frees ind_stmt
val facts =
(if only then
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o fact_from_ref ctxt reserved chained_ths) add
else
all_facts ctxt reserved no_dangerous_types fudge add_ths chained_ths)
+ |> maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt (respect_no_atp andalso not only)
|> uniquify
in
@@ -849,8 +889,9 @@
max_relevant = 0 then
[]
else
- relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
- fudge override facts (concl_t :: hyp_ts))
+ ((concl_t |> theory_constify fudge (Context.theory_name thy)) :: hyp_ts)
+ |> relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+ fudge override facts)
|> map (apfst (apfst (fn f => f ())))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 16 20:14:21 2010 +0000
@@ -75,10 +75,10 @@
type raw_param = string * string list
val default_default_params =
- [("blocking", "false"),
- ("debug", "false"),
+ [("debug", "false"),
("verbose", "false"),
("overlord", "false"),
+ ("blocking", "false"),
("type_sys", "smart"),
("explicit_apply", "false"),
("relevance_thresholds", "0.45 0.85"),
@@ -91,10 +91,10 @@
("atps", "provers"), (* FIXME: legacy *)
("atp", "provers")] (* FIXME: legacy *)
val negated_alias_params =
- [("non_blocking", "blocking"),
- ("no_debug", "debug"),
+ [("no_debug", "debug"),
("quiet", "verbose"),
("no_overlord", "overlord"),
+ ("non_blocking", "blocking"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
("no_isar_proof", "isar_proof")]
@@ -219,10 +219,10 @@
case lookup name of
SOME "smart" => NONE
| _ => SOME (lookup_int name)
- val blocking = auto orelse lookup_bool "blocking"
val debug = not auto andalso lookup_bool "debug"
val verbose = debug orelse (not auto andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
+ val blocking = auto orelse debug orelse lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> auto ? single o hd
val type_sys =
@@ -244,7 +244,7 @@
val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
val expect = lookup_string "expect"
in
- {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
+ {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 16 20:14:21 2010 +0000
@@ -54,7 +54,7 @@
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
val params =
- {blocking = true, debug = debug, verbose = false, overlord = overlord,
+ {debug = debug, verbose = false, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 16 20:14:21 2010 +0000
@@ -16,10 +16,10 @@
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
type params =
- {blocking: bool,
- debug: bool,
+ {debug: bool,
verbose: bool,
overlord: bool,
+ blocking: bool,
provers: string list,
type_sys: type_system,
explicit_apply: bool,
@@ -214,10 +214,10 @@
(** problems, results, ATPs, etc. **)
type params =
- {blocking: bool,
- debug: bool,
+ {debug: bool,
verbose: bool,
overlord: bool,
+ blocking: bool,
provers: string list,
type_sys: type_system,
explicit_apply: bool,
@@ -442,6 +442,8 @@
[(139, Crashed)]
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
+val internal_error_prefix = "Internal error: "
+
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
@@ -449,7 +451,9 @@
SOME failure => failure
| NONE => UnknownError)
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
- | failure_from_smt_failure _ = UnknownError
+ | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
+ if String.isPrefix internal_error_prefix msg then InternalError
+ else UnknownError
(* FUDGE *)
val smt_max_iter = Unsynchronized.ref 8
@@ -483,12 +487,15 @@
()
val birth = Timer.checkRealTimer timer
val _ =
- if debug then
- Output.urgent_message "Invoking SMT solver..."
- else
- ()
- val {outcome, used_facts, ...} =
+ if debug then Output.urgent_message "Invoking SMT solver..." else ()
+ val (outcome, used_facts) =
SMT_Solver.smt_filter remote iter_timeout state facts i
+ |> (fn {outcome, used_facts, ...} => (outcome, used_facts))
+ handle exn => if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (internal_error_prefix ^ ML_Compiler.exn_message exn
+ |> SMT_Failure.Other_Failure |> SOME, [])
val death = Timer.checkRealTimer timer
val _ =
if verbose andalso is_some outcome then
@@ -515,7 +522,7 @@
();
true (* kind of *))
| SOME SMT_Failure.Out_Of_Memory => true
- | SOME _ => true
+ | SOME (SMT_Failure.Other_Failure _) => true
val timeout = Time.- (timeout, Timer.checkRealTimer timer)
in
if too_many_facts_perhaps andalso iter_num < !smt_max_iter andalso
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 16 20:14:04 2010 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 16 20:14:21 2010 +0000
@@ -26,7 +26,7 @@
open Sledgehammer_Provers
open Sledgehammer_Minimize
-fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
+fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
n goal =
quote name ^
(if verbose then
@@ -41,7 +41,7 @@
val implicit_minimization_threshold = 50
-fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
+fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
auto minimize_command only
{state, goal, subgoal, subgoal_count, facts} name =
let
@@ -118,7 +118,7 @@
(* FUDGE *)
val auto_max_relevant_divisor = 2
-fun run_sledgehammer (params as {blocking, debug, provers, type_sys,
+fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
relevance_thresholds, max_relevant, ...})
auto i (relevance_override as {only, ...}) minimize_command
state =