--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 16 19:13:50 2014 +0200
@@ -295,7 +295,7 @@
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
fun str_of_meth l meth =
- string_of_proof_method meth ^ " " ^
+ string_of_proof_method [] meth ^ " " ^
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
fun comment_of l = map (str_of_meth l) #> commas
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri May 16 19:13:50 2014 +0200
@@ -248,18 +248,13 @@
|> maybe_quote),
ctxt |> Variable.auto_fixes term)
- fun with_facts none _ [] [] = none
- | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
-
- val using_facts = with_facts "" (enclose "using " " ")
-
- fun maybe_paren s = s |> String.isSubstring " " s ? enclose "(" ")"
- fun by_facts meth ls ss =
- "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss
+ fun using_facts [] [] = ""
+ | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
fun is_direct_method (Metis_Method _) = true
| is_direct_method Meson_Method = true
| is_direct_method SMT2_Method = true
+ | is_direct_method Simp_Method = true
| is_direct_method _ = false
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
@@ -269,7 +264,7 @@
fun of_method ls ss meth =
let val direct = is_direct_method meth in
using_facts ls (if direct then [] else ss) ^
- by_facts (string_of_proof_method meth) [] (if direct then ss else [])
+ "by " ^ string_of_proof_method (if direct then ss else []) meth
end
fun of_free (s, T) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri May 16 19:13:50 2014 +0200
@@ -33,7 +33,7 @@
type one_line_params =
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
- val string_of_proof_method : proof_method -> string
+ val string_of_proof_method : string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
tactic
val string_of_play_outcome : play_outcome -> string
@@ -72,23 +72,30 @@
type one_line_params =
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
-fun string_of_proof_method meth =
- (case meth of
- Metis_Method (NONE, NONE) => "metis"
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
- | Meson_Method => "meson"
- | SMT2_Method => "smt2"
- | SATx_Method => "satx"
- | Blast_Method => "blast"
- | Simp_Method => "simp"
- | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
- | Auto_Method => "auto"
- | Fastforce_Method => "fastforce"
- | Force_Method => "force"
- | Linarith_Method => "linarith"
- | Presburger_Method => "presburger"
- | Algebra_Method => "algebra")
+fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
+
+fun string_of_proof_method ss meth =
+ let
+ val meth_s =
+ (case meth of
+ Metis_Method (NONE, NONE) => "metis"
+ | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ | Meson_Method => "meson"
+ | SMT2_Method => "smt2"
+ | SATx_Method => "satx"
+ | Blast_Method => "blast"
+ | Simp_Method => if null ss then "simp" else "simp add:"
+ | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Linarith_Method => "linarith"
+ | Presburger_Method => "presburger"
+ | Algebra_Method => "algebra")
+ in
+ maybe_paren (space_implode " " (meth_s :: ss))
+ end
fun tac_of_proof_method ctxt debug (local_facts, global_facts) meth =
Method.insert_tac local_facts THEN'
@@ -98,12 +105,12 @@
(lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
| Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
| SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts
+ | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
| _ =>
Method.insert_tac global_facts THEN'
(case meth of
SATx_Method => SAT.satx_tac ctxt
| Blast_Method => blast_tac ctxt
- | Simp_Method => Simplifier.asm_full_simp_tac ctxt
| Simp_Size_Method =>
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
| Auto_Method => K (Clasimp.auto_tac ctxt)
@@ -128,27 +135,14 @@
| play_outcome_ord (_, Play_Timed_Out _) = GREATER
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
-(* FIXME: Various bugs, esp. with "unfolding"
-fun unusing_chained_facts _ 0 = ""
- | unusing_chained_facts used_chaineds num_chained =
- if length used_chaineds = num_chained then ""
- else if null used_chaineds then "(* using no facts *) "
- else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
-*)
-
fun apply_on_subgoal _ 1 = "by "
| apply_on_subgoal 1 _ = "apply "
| apply_on_subgoal i n =
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
-fun command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
(* FIXME *)
-fun proof_method_command meth i n used_chaineds num_chained ss =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
+fun proof_method_command meth i n _(*used_chaineds*) _(*num_chained*) ss =
+ apply_on_subgoal i n ^ string_of_proof_method ss meth
fun try_command_line banner play command =
let val s = string_of_play_outcome play in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri May 16 19:13:50 2014 +0200
@@ -230,7 +230,7 @@
let
val _ =
if verbose then
- Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
+ Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^
"\" for " ^ string_of_time timeout ^ "...")
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:13:50 2014 +0200
@@ -221,6 +221,8 @@
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
+
fun weight_facts facts =
let val num_facts = length facts in
map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
@@ -245,8 +247,8 @@
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 thy rewrite_rules prem_ids conjecture_id
- fact_ids z3_proof
+ val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
+ prem_ids conjecture_id fact_ids z3_proof
val isar_params =
K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
minimize <> SOME false, atp_proof, goal)