# HG changeset patch # User paulson # Date 1292530461 0 # Node ID ebeb9424c54b10faa009131eb45b4fd2af895d16 # Parent ee24717e3fe39e490fb82a2d2a00e072e7b808a5# Parent 8a341cf54a85d127fc76754cb6fe15416af41921 merged diff -r 8a341cf54a85 -r ebeb9424c54b doc-src/Sledgehammer/sledgehammer.tex --- 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}).} diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 = diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/ATP/atp_proof.ML --- 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)\(, , \). The 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: . *) 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)) diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/ATP/atp_systems.ML --- 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 = diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/SMT/lib/scripts/z3_wrapper --- /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 = ; + close(OUT_FILE); + print @out_lines; +} else { + open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\""; + my @err_lines = ; + 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 = ; + 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; +} diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/SMT/smt_monomorph.ML --- 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' diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/SMT/smt_translate.ML --- 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) diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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) diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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, diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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, diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 = diff -r 8a341cf54a85 -r ebeb9424c54b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML