--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 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 (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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 16:50:14 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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 18 16:50:14 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/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 16:50:14 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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 16:50:14 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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 16:50:14 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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 16:50:14 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
@@ -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 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 18 16:50:14 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)