# HG changeset patch # User blanchet # Date 1400260430 -7200 # Node ID 132142089ea65678236c0c4c884cba47d9ef1ac9 # Parent 51d4189d95cf357b47f2b34c72abcc7f2af6c3a9 use 'simp add:' syntax in Sledgehammer rather than 'using' diff -r 51d4189d95cf -r 132142089ea6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 51d4189d95cf -r 132142089ea6 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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) = diff -r 51d4189d95cf -r 132142089ea6 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r 51d4189d95cf -r 132142089ea6 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 () diff -r 51d4189d95cf -r 132142089ea6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- 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)