--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu May 22 04:12:06 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu May 22 05:23:50 2014 +0200
@@ -84,8 +84,8 @@
Term.map_abs_vars (perhaps (try Name.dest_skolem))
#> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
-fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids
- proof =
+fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id
+ fact_helper_ids proof =
let
val thy = Proof_Context.theory_of ctxt
@@ -108,12 +108,12 @@
(case rule of
Z3_New_Proof.Asserted =>
let
- val ss = the_list (AList.lookup (op =) fact_ids id)
+ val ss = the_list (AList.lookup (op =) fact_helper_ids id)
val name0 = (sid ^ "a", ss)
val (role0, concl0) =
(case ss of
- [s] => (Axiom, the (AList.lookup (op =) fact_ts s))
+ [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
| _ =>
if id = conjecture_id then
(Conjecture, concl_t)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 04:12:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 05:23:50 2014 +0200
@@ -129,8 +129,7 @@
? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
print_used_facts used_facts used_from
| _ => ())
- |> spy
- ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
+ |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
@@ -143,13 +142,12 @@
really_go ()
else
(really_go ()
- handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
- | exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (unknownN, fn () => "Internal error:\n" ^
- Runtime.exn_message exn ^ "\n"))
+ handle
+ ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
+ | exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
@@ -175,9 +173,7 @@
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
val outcome =
- if outcome_code = someN orelse mode = Normal then
- quote name ^ ": " ^ message ()
- else ""
+ if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
val _ =
if outcome <> "" andalso is_some output_result then
the output_result outcome
@@ -274,9 +270,8 @@
if mode = Auto_Try then
(unknownN, state)
|> fold (fn prover => fn accum as (outcome_code, _) =>
- if outcome_code = someN then accum
- else launch problem prover)
- provers
+ if outcome_code = someN then accum else launch problem prover)
+ provers
else
provers
|> (if blocking then Par_List.map else map) (launch problem #> fst)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 04:12:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 05:23:50 2014 +0200
@@ -73,16 +73,11 @@
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 = Conjecture orelse role = Negated_Conjecture then
- line :: lines
- else if is_True_prop t then
- map (replace_dependencies_in_line (name, [])) lines
- else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
- line :: lines
- else if role = Axiom then
- lines (* axioms (facts) need no proof lines *)
- else
- map (replace_dependencies_in_line (name, [])) lines
+ if role = Conjecture orelse role = Negated_Conjecture then line :: lines
+ else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
+ else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
+ else if role = Axiom then lines (* axioms (facts) need no proof lines *)
+ else map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines
fun add_lines_pass2 res _ [] = rev res
@@ -364,7 +359,9 @@
SOME s => s
| NONE =>
if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
- in one_line_proof ^ isar_proof end
+ in
+ one_line_proof ^ isar_proof
+ end
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 04:12:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 05:23:50 2014 +0200
@@ -63,8 +63,8 @@
message_tail : string}
type prover =
- params -> ((string * string list) list -> string -> minimize_command)
- -> prover_problem -> prover_result
+ params -> ((string * string list) list -> string -> minimize_command) -> prover_problem ->
+ prover_result
val SledgehammerN : string
val str_of_mode : mode -> string
@@ -76,8 +76,7 @@
val is_atp : theory -> string -> bool
val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
val is_fact_chained : (('a * stature) * 'b) -> bool
- val filter_used_facts :
- bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
+ val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
@@ -294,8 +293,7 @@
sort_strings (SMT2_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Supported provers: " ^
- commas (local_provers @ remote_provers) ^ ".")
+ Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
end
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 04:12:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 05:23:50 2014 +0200
@@ -242,15 +242,22 @@
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
- val fact_ids =
- map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
- map (fn (id, ((name, _), _)) => (id, name)) fact_ids
- val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
- (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id
- fact_ids z3_proof
- val isar_params =
- K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
+ fun isar_params () =
+ let
+ val fact_helper_ts =
+ map (fn (_, th) => (short_thm_name ctxt th, prop_of th)) helper_ids @
+ map (fn ((s, _), th) => (s, prop_of th)) used_named_facts
+ val fact_helper_ids =
+ map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
+ map (fn (id, ((name, _), _)) => (id, name)) fact_ids
+
+ val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts
+ concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids z3_proof
+ in
+ (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
minimize <> SOME false, atp_proof, goal)
+ end
+
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command thy params minimize_command name preplay, subgoal,