# HG changeset patch # User panny # Date 1387385328 -3600 # Node ID f0fd945692bbdf9066f8f19ef698e9a7a080573e # Parent df6350c8f61a02f23581f3924e9c8ed5a9527d9b# Parent c05ed63333023e87e84340eab77cd4b59d6b0b22 merge diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 18 17:48:48 2013 +0100 @@ -261,9 +261,9 @@ (*Escaping of special characters. Alphanumeric characters are left unchanged. - The character _ goes to __ + The character _ goes to __. Characters in the range ASCII space to / go to _A to _P, respectively. - Other characters go to _nnn where nnn is the decimal ASCII code.*) + Other characters go to _nnn where nnn is the decimal ASCII code. *) val upper_a_minus_space = Char.ord #"A" - Char.ord #" " fun ascii_of_char c = @@ -571,19 +571,17 @@ else (s, T) |> Sign.const_typargs thy -(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. - Also accumulates sort infomation. *) +(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort + infomation. *) fun iterm_of_term thy type_enc bs (P $ Q) = let val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end | iterm_of_term thy type_enc _ (Const (c, T)) = - (IConst (`(make_fixed_const (SOME type_enc)) c, T, - robust_const_type_args thy (c, T)), + (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)), atomic_types_of T) - | iterm_of_term _ _ _ (Free (s, T)) = - (IConst (`make_fixed_var s, T, []), atomic_types_of T) + | iterm_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T) | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let @@ -600,7 +598,9 @@ val s = vary s val name = `make_bound_var s val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t - in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end + in + (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) + end (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *) val queries = ["?", "_query"] @@ -836,8 +836,8 @@ atomic_types : typ list} fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) = - {name = name, stature = stature, role = role, iformula = f iformula, - atomic_types = atomic_types} : ifact + {name = name, stature = stature, role = role, iformula = f iformula, atomic_types = atomic_types} + : ifact fun ifact_lift f ({iformula, ...} : ifact) = f iformula @@ -1007,9 +1007,7 @@ map (fn cl => class_atom type_enc (cl, T)) cls fun class_membs_of_types type_enc add_sorts_on_typ Ts = - [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso - level_of_type_enc type_enc <> No_Types) - ? fold add_sorts_on_typ Ts + [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c)) @@ -1780,22 +1778,22 @@ |> map (apsnd (map (apsnd zero_var_indexes))) fun bound_tvars type_enc sorts Ts = - case filter is_TVar Ts of + (case filter is_TVar Ts of [] => I | Ts => - (sorts ? mk_ahorn (Ts |> class_membs_of_types type_enc add_sorts_on_tvar - |> map (class_atom type_enc))) + ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic) + ? mk_ahorn (Ts + |> class_membs_of_types type_enc add_sorts_on_tvar + |> map (class_atom type_enc))) #> (case type_enc of - Native (_, poly, _) => - mk_atyquant AForall - (map (fn TVar (z as (_, S)) => - (AType (tvar_name z, []), - if poly = Type_Class_Polymorphic then - map (`make_class) (normalize_classes S) - else - [])) Ts) - | _ => - mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)) + Native (_, poly, _) => + mk_atyquant AForall (map (fn TVar (z as (_, S)) => + (AType (tvar_name z, []), + if poly = Type_Class_Polymorphic then + map (`make_class) (normalize_classes S) + else + [])) Ts) + | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))) fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) @@ -2218,8 +2216,7 @@ fun lines_of_free_types type_enc (facts : ifact list) = if is_type_enc_polymorphic type_enc then let - val type_classes = - (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic) + val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic) fun line j (cl, T) = if type_classes then Class_Memb (class_memb_prefix ^ string_of_int j, [], @@ -2230,7 +2227,9 @@ val membs = fold (union (op =)) (map #atomic_types facts) [] |> class_membs_of_types type_enc add_sorts_on_tfree - in map2 line (0 upto length membs - 1) membs end + in + map2 line (0 upto length membs - 1) membs + end else [] @@ -2403,8 +2402,7 @@ fun line_of_tags_mono_type ctxt mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in - Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), - Axiom, + Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, NONE, isabelle_info non_rec_defN helper_rank) diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 17:48:48 2013 +0100 @@ -220,15 +220,18 @@ val skip_term = let fun skip _ accum [] = (accum, []) - | skip 0 accum (ss as "," :: _) = (accum, ss) - | skip 0 accum (ss as ")" :: _) = (accum, ss) - | skip 0 accum (ss as "]" :: _) = (accum, ss) - | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum (s :: ss) = skip n (s :: accum) ss - in skip 0 [] #>> (rev #> implode) end + | skip n accum (ss as s :: ss') = + if s = "," andalso n = 0 then + (accum, ss) + else if member (op =) [")", "]", ">", "}"] s then + if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' + else if member (op =) ["(", "[", "<", "{"] s then + skip (n + 1) (s :: accum) ss' + else + skip n (s :: accum) ss' + in + skip 0 [] #>> (rev #> implode) + end datatype source = File_Source of string * string option | @@ -261,21 +264,17 @@ || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) || skip_term >> K dummy_inference) x -fun list_app (f, args) = - fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f +fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f (* We currently ignore TFF and THF types. *) -fun parse_type_stuff x = - Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x +fun parse_type_stuff x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x and parse_arg x = ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff || scan_general_id --| parse_type_stuff -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> (ATerm o apfst (rpair []))) x -and parse_term x = - (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x -and parse_terms x = - (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x +and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x +and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal @@ -311,9 +310,7 @@ and parse_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal - >> (fn ((q, ts), phi) => - (* We ignore TFF and THF types for now. *) - AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x + >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) @@ -351,9 +348,9 @@ c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst - (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) = + (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse - (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2) + (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false @@ -361,11 +358,13 @@ if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE -fun find_formula_in_problem problem phi = - problem |> maps snd |> map_filter (matching_formula_line_identifier phi) - |> try (single o hd) |> the_default [] +fun find_formula_in_problem phi = + maps snd + #> map_filter (matching_formula_line_identifier phi) + #> try (single o hd) + #> the_default [] -fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms)) +fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom @@ -392,7 +391,7 @@ (case deps of File_Source (_, SOME s) => (if s = waldmeister_conjecture_name then - (case find_formula_in_problem problem (mk_anot phi) of + (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => @@ -404,16 +403,14 @@ phi), "", []) | File_Source _ => - (((num, phi |> find_formula_in_problem problem |> map fst), - phi), "", []) + (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)) - fun mk_step () = - (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) + fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) in (case role_of_tptp_string role of Definition => (case phi of - AAtom (ATerm (("equal", []), _)) => + AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 17:48:48 2013 +0100 @@ -536,8 +536,8 @@ | add_sko _ = I (* union-find would be faster *) - fun add_cycle _ [] = I - | add_cycle name ss = + fun add_cycle [] = I + | add_cycle ss = fold (fn s => Graph.default_node (s, ())) ss #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss]) @@ -545,11 +545,7 @@ val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps) - - val groups = - Graph.empty - |> fold (fn (skos, (name, _, _, _, _)) => add_cycle name skos) skoss_input_steps - |> Graph.strong_conn + val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty) fun step_name_of_group skos = (implode skos, []) fun in_group group = member (op =) group o hd @@ -582,7 +578,7 @@ fun factify_atp_proof fact_names hyp_ts concl_t atp_proof = let - fun factify_step ((num, ss), role, t, rule, deps) = + fun factify_step ((num, ss), _, t, rule, deps) = let val (ss', role', t') = (case resolve_conjecture ss of diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 18 17:48:48 2013 +0100 @@ -68,7 +68,6 @@ val atom_eq = is_equal o Atom.ord val clause_ord = dict_ord Atom.ord -val clause_eq = is_equal o clause_ord fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp) fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Dec 18 17:48:48 2013 +0100 @@ -658,7 +658,7 @@ val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) val spass_pirate_format = DFG Polymorphic -val remote_spass_pirate_config = +val remote_spass_pirate_config : atp_config = {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => string_of_int (to_secs 1 timeout) ^ " " ^ file_name, diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/ATP/scripts/remote_spass_pirate --- a/src/HOL/Tools/ATP/scripts/remote_spass_pirate Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/ATP/scripts/remote_spass_pirate Wed Dec 18 17:48:48 2013 +0100 @@ -1,2 +1,2 @@ #!/usr/bin/env bash -curl -F file=@"$2" "http://91.228.53.68:8080/solve/pirate/"$1"s" +curl -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s" diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 17:48:48 2013 +0100 @@ -679,8 +679,8 @@ fun strs_of_type_arg (T as Type (s, _)) = massage_long_name s :: (if generalize_goal andalso in_goal then strs_of_sort (sort_of_type alg T) else []) - | strs_of_type_arg (TFree (s, S)) = strs_of_sort S - | strs_of_type_arg (TVar (s, S)) = strs_of_sort S + | strs_of_type_arg (TFree (_, S)) = strs_of_sort S + | strs_of_type_arg (TVar (_, S)) = strs_of_sort S val typargss = these (try (Sign.const_typargs thy) x) diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 17:48:48 2013 +0100 @@ -123,7 +123,7 @@ (* main function for preplaying Isar steps; may throw exceptions *) fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time | preplay_raw debug type_enc lam_trans ctxt timeout - (step as Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = + (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = let val goal = (case xs of diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 17:48:48 2013 +0100 @@ -238,7 +238,7 @@ #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = + | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = add_step_pre ind qs subproofs #> (case xs of [] => add_suffix (of_have qs (length subproofs) ^ " ") diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 17:48:48 2013 +0100 @@ -72,7 +72,7 @@ (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information. *) -fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines = +fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse @@ -94,7 +94,7 @@ fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) [] fun add_lines_pass3 res [] = rev res - | add_lines_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) = + | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) = if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse (* the last line must be kept *) null lines orelse @@ -200,7 +200,7 @@ [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method, Force_Method], [Meson_Method]] val rewrite_methodss = - [[Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]] + [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]] val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]] fun isar_proof_text ctxt isar_proofs @@ -208,7 +208,7 @@ atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt + val (params, _, concl_t) = strip_subgoal goal subgoal ctxt val (_, ctxt) = params |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) diff -r df6350c8f61a -r f0fd945692bb src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 18 14:50:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 18 17:48:48 2013 +0100 @@ -65,8 +65,7 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice, - timeout, expect, ...}) +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode output_result minimize_command only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let @@ -221,8 +220,8 @@ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) |> space_implode "\n\n" -fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...}) - mode output_result i (fact_override as {only, ...}) minimize_command state = +fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode + output_result i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." else case subgoal_count state of @@ -250,12 +249,10 @@ val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) - val (ueq_atps, full_provers) = List.partition (is_unit_equational_atp ctxt) provers - val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) - fun get_factss label is_appropriate_prop provers = + fun get_factss provers = let val max_max_facts = case max_facts of @@ -263,28 +260,19 @@ | NONE => 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) - val _ = spying spy (fn () => (state, i, label ^ "s", + val _ = spying spy (fn () => (state, i, "All", "Filtering " ^ string_of_int (length all_facts) ^ " facts")); in all_facts - |> (case is_appropriate_prop of - SOME is_app => filter (is_app o prop_of o snd) - | NONE => I) |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t - |> tap (fn factss => - if verbose then - label ^ plural_s (length provers) ^ ": " ^ - string_of_factss factss - |> print - else - ()) + |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) |> spy ? tap (fn factss => spying spy (fn () => - (state, i, label ^ "s", "Selected facts: " ^ spying_str_of_factss factss))) + (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) end - fun launch_provers state label is_appropriate_prop provers = + fun launch_provers state = let - val factss = get_factss label is_appropriate_prop provers + val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss} @@ -303,35 +291,11 @@ |> max_outcome_code |> rpair state end - fun maybe_launch_provers label is_appropriate_prop provers_to_launch accum = - if null provers_to_launch then - accum - else if is_some is_appropriate_prop andalso - not (the is_appropriate_prop concl_t) then - (if verbose orelse length provers_to_launch = length provers then - "Goal outside the scope of " ^ - space_implode " " (serial_commas "and" (map quote provers_to_launch)) ^ "." - |> Output.urgent_message - else - (); - accum) - else - launch_provers state label is_appropriate_prop provers_to_launch - - val launch_full_provers = maybe_launch_provers "ATP/SMT" NONE full_provers - val launch_ueq_atps = maybe_launch_provers "Unit-equational provers" (SOME is_unit_equality) ueq_atps - - fun launch_atps_and_smt_solvers p = - [launch_full_provers, launch_ueq_atps] - |> Par_List.map (fn f => fst (f p)) - handle ERROR msg => (print ("Error: " ^ msg); error msg) - fun maybe f (accum as (outcome_code, _)) = accum |> (mode = Normal orelse outcome_code <> someN) ? f in - (unknownN, state) - |> (if blocking then launch_full_provers - else (fn p => (Future.fork (tap (fn () => launch_full_provers p)); p))) + (if blocking then launch_provers state + else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) end |> `(fn (outcome_code, _) => outcome_code = someN)