--- 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)
--- 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 ())
--- 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
--- 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)
--- 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,
--- 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"
--- 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)
--- 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
--- 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) ^ " ")
--- 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))
--- 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)