# HG changeset patch # User blanchet # Date 1391437147 -3600 # Node ID e88ad20035f4bafa7ad75f54e83b85d756199e53 # Parent bd27ac6ad1c3343b3ddbe51017940a72584ef62b merged 'reconstructors' and 'proof methods' diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 15:19:07 2014 +0100 @@ -19,7 +19,7 @@ (*refers to minimization attempted by Mirabelle*) val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*) -val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) +val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) @@ -43,8 +43,7 @@ fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " -fun reconstructor_tag reconstructor id = - "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " +fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " val separator = "-----" @@ -130,16 +129,16 @@ proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) -datatype reconstructor_mode = +datatype proof_method_mode = Unminimized | Minimized | UnminimizedFT | MinimizedFT datatype data = Data of { sh: sh_data, min: min_data, - re_u: re_data, (* reconstructor with unminimized set of lemmas *) - re_m: re_data, (* reconstructor with minimized set of lemmas *) - re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *) - re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *) + re_u: re_data, (* proof method with unminimized set of lemmas *) + re_m: re_data, (* proof method with minimized set of lemmas *) + re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *) + re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *) mini: bool (* with minimization *) } @@ -218,39 +217,39 @@ fun inc_min_ab_ratios r = map_min_data (fn (succs, ab_ratios) => (succs, ab_ratios+r)) -val inc_reconstructor_calls = map_re_data +val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_success = map_re_data +val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_nontriv_calls = map_re_data +val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_nontriv_success = map_re_data +val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_proofs = map_re_data +val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) -fun inc_reconstructor_time m t = map_re_data +fun inc_proof_method_time m t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m -val inc_reconstructor_timeout = map_re_data +val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) -fun inc_reconstructor_lemmas m n = map_re_data +fun inc_proof_method_lemmas m n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m -fun inc_reconstructor_posns m pos = map_re_data +fun inc_proof_method_posns m pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m @@ -292,19 +291,19 @@ fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, re_nontriv_success, re_proofs, re_time, re_timeout, (lemmas, lems_sos, lems_max), re_posns) = - (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls); - log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^ + (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); + log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ " (proof: " ^ str re_proofs ^ ")"); - log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout); + log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); - log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls); - log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^ + log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); + log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ " (proof: " ^ str re_proofs ^ ")"); - log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas); - log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos); - log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max); - log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time)); - log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^ + log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); + log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); + log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); + log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); + log ("Average time for successful " ^ tag ^ "proof method calls: " ^ str3 (avg_time re_time re_success)); if tag="" then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) @@ -325,7 +324,7 @@ fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () fun log_re tag m = log_re_data log tag sh_calls (tuple_of_re_data m) - fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () => + fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () => (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2))) in if sh_calls > 0 @@ -334,14 +333,14 @@ log_sh_data log (tuple_of_sh_data sh); log ""; if not mini - then log_reconstructor ("", re_u) ("fully-typed ", re_uft) + then log_proof_method ("", re_u) ("fully-typed ", re_uft) else app_if re_u (fn () => - (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft); + (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft); log ""; app_if re_m (fn () => (log_min_data log (tuple_of_min_data min); log ""; - log_reconstructor ("", re_m) ("fully-typed ", re_mft)))))) + log_proof_method ("", re_m) ("fully-typed ", re_mft)))))) else () end @@ -385,8 +384,8 @@ andalso not (String.isSubstring "may fail" s) (* Fragile hack *) -fun reconstructor_from_msg args msg = - (case AList.lookup (op =) args reconstructorK of +fun proof_method_from_msg args msg = + (case AList.lookup (op =) args proof_methodK of SOME name => name | NONE => if exists good_line (split_lines msg) then @@ -460,7 +459,7 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, - preplay = Lazy.value (Sledgehammer_Prover.plain_metis, + preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE), Sledgehammer_Reconstructor.Play_Failed), message = K "", message_tail = ""}, ~1) val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} @@ -501,7 +500,7 @@ in -fun run_sledgehammer trivial args reconstructor named_thms id +fun run_sledgehammer trivial args proof_method named_thms id ({pre=st, log, pos, ...}: Mirabelle.run_args) = let val thy = Proof.theory_of st @@ -557,7 +556,7 @@ change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_prover time_prover); - reconstructor := reconstructor_from_msg args msg; + proof_method := proof_method_from_msg args msg; named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) @@ -572,7 +571,7 @@ end -fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = +fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = let val thy = Proof.theory_of st val {goal, ...} = Proof.goal st @@ -614,7 +613,7 @@ change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") - else (reconstructor := reconstructor_from_msg args msg; + else (meth := proof_method_from_msg args msg; named_thms := SOME named_thms'; log (minimize_tag id ^ "succeeded:\n" ^ msg)) ) @@ -629,10 +628,10 @@ ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] -fun run_reconstructor trivial full m name reconstructor named_thms id +fun run_proof_method trivial full m name meth named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let - fun do_reconstructor named_thms ctxt = + fun do_method named_thms ctxt = let val ref_of_str = suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm @@ -646,56 +645,56 @@ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override in - if !reconstructor = "sledgehammer_tac" then + if !meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Systems.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms - else if !reconstructor = "smt" then + else if !meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if String.isPrefix "metis (" (!reconstructor) then + else if String.isPrefix "metis (" (!meth) then let val (type_encs, lam_trans) = - !reconstructor + !meth |> Outer_Syntax.scan Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end - else if !reconstructor = "metis" then + else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else K all_tac end - fun apply_reconstructor named_thms = - Mirabelle.can_apply timeout (do_reconstructor named_thms) st + fun apply_method named_thms = + Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" - | with_time (true, t) = (change_data id (inc_reconstructor_success m); + | with_time (true, t) = (change_data id (inc_proof_method_success m); if trivial then () - else change_data id (inc_reconstructor_nontriv_success m); - change_data id (inc_reconstructor_lemmas m (length named_thms)); - change_data id (inc_reconstructor_time m t); - change_data id (inc_reconstructor_posns m (pos, trivial)); - if name = "proof" then change_data id (inc_reconstructor_proofs m) else (); + else change_data id (inc_proof_method_nontriv_success m); + change_data id (inc_proof_method_lemmas m (length named_thms)); + change_data id (inc_proof_method_time m t); + change_data id (inc_proof_method_posns m (pos, trivial)); + if name = "proof" then change_data id (inc_proof_method_proofs m) else (); "succeeded (" ^ string_of_int t ^ ")") - fun timed_reconstructor named_thms = - (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) - handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false)) + fun timed_method named_thms = + (with_time (Mirabelle.cpu_time apply_method named_thms), true) + handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) val _ = log separator - val _ = change_data id (inc_reconstructor_calls m) - val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m) + val _ = change_data id (inc_proof_method_calls m) + val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m) in named_thms - |> timed_reconstructor - |>> log o prefix (reconstructor_tag reconstructor id) + |> timed_method + |>> log o prefix (proof_method_tag meth id) |> snd end @@ -717,7 +716,7 @@ if !num_sledgehammer_calls > max_calls then () else let - val reconstructor = Unsynchronized.ref "" + val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val minimize = AList.defined (op =) args minimizeK @@ -728,33 +727,28 @@ Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle TimeLimit.TimeOut => false else false - fun apply_reconstructor m1 m2 = + fun apply_method m1 m2 = if metis_ft then - if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st) + if not (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st) then - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial true m2 name reconstructor - (these (!named_thms))) id st; ()) + (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ()) else () else - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st; ()) + (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ()) in change_data id (set_mini minimize); - Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor - named_thms) id st; + Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; if is_some (!named_thms) then - (apply_reconstructor Unminimized UnminimizedFT; + (apply_method Unminimized UnminimizedFT; if minimize andalso not (null (these (!named_thms))) then - (Mirabelle.catch minimize_tag - (run_minimize args reconstructor named_thms) id st; - apply_reconstructor Minimized MinimizedFT) + (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st; + apply_method Minimized MinimizedFT) else ()) else () end diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 15:19:07 2014 +0100 @@ -28,9 +28,9 @@ val partial_type_encs : string list val default_metis_lam_trans : string - val metis_call : string -> string -> string val forall_of : term -> term -> term val exists_of : term -> term -> term + val type_enc_aliases : (string * string list) list val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term @@ -84,17 +84,6 @@ val default_metis_lam_trans = combsN -fun metis_call type_enc lam_trans = - let - val type_enc = - (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of - [alias] => alias - | _ => type_enc) - val opts = - [] |> type_enc <> partial_typesN ? cons type_enc - |> lam_trans <> default_metis_lam_trans ? cons lam_trans - in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end - fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s | term_name' _ = "" diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 15:19:07 2014 +0100 @@ -129,6 +129,17 @@ | ord => ord in {weight = weight, precedence = precedence} end +fun metis_call type_enc lam_trans = + let + val type_enc = + (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of + [alias] => alias + | _ => type_enc) + val opts = + [] |> type_enc <> partial_typesN ? cons type_enc + |> lam_trans <> default_metis_lam_trans ? cons lam_trans + in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end + exception METIS_UNPROVABLE of unit (* Main function to start Metis proof and reconstruction *) diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:19:07 2014 +0100 @@ -286,7 +286,7 @@ val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof - |> silence_reconstructors debug + |> silence_proof_methods debug val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty @@ -354,9 +354,9 @@ if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") in one_line_proof ^ isar_proof end -fun isar_proof_would_be_a_good_idea (reconstr, play) = +fun isar_proof_would_be_a_good_idea (meth, play) = (case play of - Played _ => reconstr = SMT + Played _ => meth = SMT_Method | Play_Timed_Out _ => true | Play_Failed => true | Not_Played => false) diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 15:19:07 2014 +0100 @@ -100,27 +100,6 @@ |> Skip_Proof.make_thm thy end -fun tac_of_method ctxt (local_facts, global_facts) meth = - Method.insert_tac local_facts THEN' - (case meth of - Metis_Method (type_enc_opt, lam_trans_opt) => - Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] - (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts - | SMT_Method => SMT_Solver.smt_tac ctxt global_facts - | Meson_Method => Meson.meson_tac ctxt global_facts - | _ => - Method.insert_tac global_facts THEN' - (case meth of - 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) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Arith_Method => Arith_Data.arith_tac ctxt - | Blast_Method => blast_tac ctxt - | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) - (* main function for preplaying Isar steps; may throw exceptions *) fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) = let @@ -149,7 +128,7 @@ fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => - HEADGOAL (tac_of_method ctxt facts meth)) + HEADGOAL (tac_of_proof_method ctxt facts meth)) handle ERROR msg => error ("Preplay error: " ^ msg) val play_outcome = take_time timeout prove () diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 15:19:07 2014 +0100 @@ -8,24 +8,13 @@ signature SLEDGEHAMMER_ISAR_PROOF = sig + type proof_method = Sledgehammer_Reconstructor.proof_method + type label = string * int type facts = label list * string list (* local and global facts *) datatype isar_qualifier = Show | Then - datatype proof_method = - Metis_Method of string option * string option | - Meson_Method | - SMT_Method | - Simp_Method | - Simp_Size_Method | - Auto_Method | - Fastforce_Method | - Force_Method | - Arith_Method | - Blast_Method | - Algebra_Method - datatype isar_proof = Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = @@ -38,8 +27,6 @@ val label_ord : label * label -> order val string_of_label : label -> string - val string_of_proof_method : proof_method -> string - val steps_of_isar_proof : isar_proof -> isar_step list val label_of_isar_step : isar_step -> label option @@ -79,19 +66,6 @@ datatype isar_qualifier = Show | Then -datatype proof_method = - Metis_Method of string option * string option | - Meson_Method | - SMT_Method | - Simp_Method | - Simp_Size_Method | - Auto_Method | - Fastforce_Method | - Force_Method | - Arith_Method | - Blast_Method | - Algebra_Method - datatype isar_proof = Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = @@ -105,22 +79,6 @@ fun string_of_label (s, num) = s ^ string_of_int num -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" - | SMT_Method => "smt" - | Simp_Method => "simp" - | Simp_Size_Method => "simp add: size_ne_size_imp_ne" - | Auto_Method => "auto" - | Fastforce_Method => "fastforce" - | Force_Method => "force" - | Arith_Method => "arith" - | Blast_Method => "blast" - | Algebra_Method => "algebra") - fun steps_of_isar_proof (Proof (_, _, steps)) = steps fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:19:07 2014 +0100 @@ -12,7 +12,7 @@ type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact - type reconstructor = Sledgehammer_Reconstructor.reconstructor + type proof_method = Sledgehammer_Reconstructor.proof_method type play_outcome = Sledgehammer_Reconstructor.play_outcome type minimize_command = Sledgehammer_Reconstructor.minimize_command @@ -57,8 +57,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : (reconstructor * play_outcome) Lazy.lazy, - message : reconstructor * play_outcome -> string, + preplay : (proof_method * play_outcome) Lazy.lazy, + message : proof_method * play_outcome -> string, message_tail : string} type prover = @@ -66,23 +66,22 @@ -> prover_problem -> prover_result val SledgehammerN : string - val plain_metis : reconstructor val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string - val extract_reconstructor : params -> reconstructor -> string * (string * string list) list - val is_reconstructor : string -> bool + val extract_proof_method : params -> proof_method -> string * (string * string list) list + val is_proof_method : string -> bool val is_atp : theory -> string -> bool - val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list + val bunch_of_proof_methods : 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 -> ((''a * stature) * 'b) list val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list -> - Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome + Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome val remotify_atp_if_not_installed : theory -> string -> string option val isar_supported_prover_of : theory -> string -> string val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) -> - string -> reconstructor * play_outcome -> 'a + string -> proof_method * play_outcome -> 'a val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context @@ -110,9 +109,8 @@ "Async_Manager". *) val SledgehammerN = "Sledgehammer" -val reconstructor_names = [metisN, smtN] -val plain_metis = Metis (hd partial_type_encs, combsN) -val is_reconstructor = member (op =) reconstructor_names +val proof_method_names = [metisN, smtN] +val is_proof_method = member (op =) proof_method_names val is_atp = member (op =) o supported_atps @@ -167,8 +165,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : (reconstructor * play_outcome) Lazy.lazy, - message : reconstructor * play_outcome -> string, + preplay : (proof_method * play_outcome) Lazy.lazy, + message : proof_method * play_outcome -> string, message_tail : string} type prover = @@ -183,29 +181,30 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -fun bunch_of_reconstructors needs_full_types lam_trans = +fun bunch_of_proof_methods needs_full_types desperate_lam_trans = if needs_full_types then - [Metis (full_type_enc, lam_trans false), - Metis (really_full_type_enc, lam_trans false), - Metis (full_type_enc, lam_trans true), - Metis (really_full_type_enc, lam_trans true), - SMT] + [Metis_Method (SOME full_type_enc, NONE), + Metis_Method (SOME really_full_type_enc, NONE), + Metis_Method (SOME full_type_enc, SOME desperate_lam_trans), + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans), + SMT_Method] else - [Metis (partial_type_enc, lam_trans false), - Metis (full_type_enc, lam_trans false), - Metis (no_typesN, lam_trans true), - Metis (really_full_type_enc, lam_trans true), - SMT] + [Metis_Method (NONE, NONE), + Metis_Method (SOME full_type_enc, NONE), + Metis_Method (SOME no_typesN, SOME desperate_lam_trans), + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans), + SMT_Method] -fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) = +fun extract_proof_method ({type_enc, lam_trans, ...} : params) + (Metis_Method (type_enc', lam_trans')) = let val override_params = - (if is_none type_enc andalso type_enc' = hd partial_type_encs then [] - else [("type_enc", [hd (unalias_type_enc type_enc')])]) @ - (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then [] - else [("lam_trans", [lam_trans'])]) + (if is_none type_enc' andalso is_none type_enc then [] + else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @ + (if is_none lam_trans' andalso is_none lam_trans then [] + else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])]) in (metisN, override_params) end - | extract_reconstructor _ SMT = (smtN, []) + | extract_proof_method _ SMT_Method = (smtN, []) (* based on "Mirabelle.can_apply" and generalized *) fun timed_apply timeout tac state i = @@ -216,49 +215,46 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans - | tac_of_reconstructor SMT = SMT_Solver.smt_tac - -fun timed_reconstructor reconstr debug timeout ths = - timed_apply timeout (silence_reconstructors debug - #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths)) +(* FIXME *) +fun timed_proof_method meth debug timeout ths = + timed_apply timeout (silence_proof_methods debug + #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false)) -fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs = +fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths = let - fun get_preferred reconstrs = - if member (op =) reconstrs preferred then preferred - else List.last reconstrs + fun get_preferred meths = + if member (op =) meths preferred then preferred else List.last meths in if timeout = Time.zeroTime then - (get_preferred reconstrs, Not_Played) + (get_preferred meths, Not_Played) else let val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () val ths = pairs |> sort_wrt (fst o fst) |> map snd - fun play [] [] = (get_preferred reconstrs, Play_Failed) + fun play [] [] = (get_preferred meths, Play_Failed) | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout) - | play timed_out (reconstr :: reconstrs) = + | play timed_out (meth :: meths) = let val _ = if verbose then - Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^ + Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^ "\" for " ^ string_of_time timeout ^ "...") else () val timer = Timer.startRealTimer () in - case timed_reconstructor reconstr debug timeout ths state i of - SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer)) - | _ => play timed_out reconstrs + case timed_proof_method meth debug timeout ths state i of + SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) + | _ => play timed_out meths end - handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs + handle TimeLimit.TimeOut => play (meth :: timed_out) meths in - play [] reconstrs + play [] meths end end @@ -275,9 +271,8 @@ val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy val (min_name, override_params) = (case preplay of - (reconstr, Played _) => - if isar_proofs = SOME true then (maybe_isar_name, []) - else extract_reconstructor params reconstr + (meth, Played _) => + if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth | _ => (maybe_isar_name, [])) in minimize_command override_params min_name end @@ -293,7 +288,7 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = - reconstructor_names @ + proof_method_names @ sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 15:19:07 2014 +0100 @@ -346,18 +346,15 @@ let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof - val reconstrs = - bunch_of_reconstructors needs_full_types (fn desperate => - if desperate then - if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN - else - default_metis_lam_trans) + val meths = + bunch_of_proof_methods needs_full_types + (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN) in (used_facts, Lazy.lazy (fn () => let val used_pairs = used_from |> filter_used_facts false used_facts in play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal - (hd reconstrs) reconstrs + (hd meths) meths end), fn preplay => let @@ -392,7 +389,8 @@ "")) end | SOME failure => - ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, "")) + ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed), + fn _ => string_of_atp_failure failure, "")) in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, message_tail = message_tail} diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 15:19:07 2014 +0100 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_PROVER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature - type reconstructor = Sledgehammer_Reconstructor.reconstructor + type proof_method = Sledgehammer_Reconstructor.proof_method type play_outcome = Sledgehammer_Reconstructor.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params @@ -23,11 +23,11 @@ val auto_minimize_min_facts : int Config.T val auto_minimize_max_time : real Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> - Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option -> + Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option - * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string) - * string) + * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string) + * string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list -> @@ -50,29 +50,25 @@ open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT -fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) +fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) minimize_command ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let - val reconstr = - if name = metisN then - Metis (type_enc |> the_default (hd partial_type_encs), - lam_trans |> the_default default_metis_lam_trans) - else if name = smtN then - SMT - else - raise Fail ("unknown reconstructor: " ^ quote name) + val meth = + if name = metisN then Metis_Method (type_enc, lam_trans) + else if name = smtN then SMT_Method + else raise Fail ("unknown proof_method: " ^ quote name) val used_facts = facts |> map fst in (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts - state subgoal reconstr [reconstr] of + state subgoal meth [meth] of play as (_, Played time) => {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, preplay = Lazy.value play, message = fn play => let - val (_, override_params) = extract_reconstructor params reconstr + val (_, override_params) = extract_proof_method params meth val one_line_params = (play, proof_banner mode name, used_facts, minimize_command override_params name, subgoal, subgoal_count) @@ -93,18 +89,18 @@ fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in - is_reconstructor orf is_atp thy orf is_smt_prover ctxt + is_proof_method orf is_atp thy orf is_smt_prover ctxt end fun is_prover_installed ctxt = - is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) + is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) -val reconstructor_default_max_facts = 20 +val proof_method_default_max_facts = 20 fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in - if is_reconstructor name then - reconstructor_default_max_facts + if is_proof_method name then + proof_method_default_max_facts else if is_atp thy name then fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 else (* is_smt_prover ctxt name *) @@ -113,7 +109,7 @@ fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in - if is_reconstructor name then run_reconstructor mode name + if is_proof_method name then run_proof_method mode name else if is_atp thy name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name ^ ".") @@ -286,10 +282,11 @@ "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", "")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))) - handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, "")) + handle ERROR msg => + (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, "")) end -fun adjust_reconstructor_params override_params +fun adjust_proof_method_params override_params ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout, @@ -299,7 +296,7 @@ (case AList.lookup (op =) override_params name of SOME [s] => SOME s | _ => default_value) - (* Only those options that reconstructors are interested in are considered here. *) + (* Only those options that proof_methods are interested in are considered here. *) val type_enc = lookup_override "type_enc" type_enc val lam_trans = lookup_override "lam_trans" lam_trans in @@ -336,18 +333,18 @@ fun prover_fast_enough () = can_min_fast_enough run_time in (case Lazy.force preplay of - (reconstr as Metis _, Played timeout) => + (meth as Metis_Method _, Played timeout) => if isar_proofs = SOME true then (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved itself. *) (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params)) else if can_min_fast_enough timeout then - (true, extract_reconstructor params reconstr + (true, extract_proof_method params meth ||> (fn override_params => - adjust_reconstructor_params override_params params)) + adjust_proof_method_params override_params params)) else (prover_fast_enough (), (name, params)) - | (SMT, Played timeout) => + | (SMT_Method, Played timeout) => (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved itself. *) (can_min_fast_enough timeout, (name, params)) diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 15:19:07 2014 +0100 @@ -233,9 +233,8 @@ (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT - (bunch_of_reconstructors false (fn desperate => - if desperate then liftingN else default_metis_lam_trans))), + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + SMT_Method (bunch_of_proof_methods false liftingN)), fn preplay => let val one_line_params = @@ -248,7 +247,8 @@ end, if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") | SOME failure => - (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, "")) + (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), + fn _ => string_of_atp_failure failure, "")) in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, message_tail = message_tail} diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:19:07 2014 +0100 @@ -9,9 +9,18 @@ sig type stature = ATP_Problem_Generate.stature - datatype reconstructor = - Metis of string * string | - SMT + datatype proof_method = + Metis_Method of string option * string option | + Meson_Method | + SMT_Method | + Simp_Method | + Simp_Size_Method | + Auto_Method | + Fastforce_Method | + Force_Method | + Arith_Method | + Blast_Method | + Algebra_Method datatype play_outcome = Played of Time.time | @@ -21,16 +30,17 @@ type minimize_command = string list -> string type one_line_params = - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int val smtN : string - val string_of_reconstructor : reconstructor -> string + val string_of_proof_method : proof_method -> string + val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string val play_outcome_ord : play_outcome * play_outcome -> order val one_line_proof_text : int -> one_line_params -> string - val silence_reconstructors : bool -> Proof.context -> Proof.context + val silence_proof_methods : bool -> Proof.context -> Proof.context end; structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = @@ -40,9 +50,18 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct -datatype reconstructor = - Metis of string * string | - SMT +datatype proof_method = + Metis_Method of string option * string option | + Meson_Method | + SMT_Method | + Simp_Method | + Simp_Size_Method | + Auto_Method | + Fastforce_Method | + Force_Method | + Arith_Method | + Blast_Method | + Algebra_Method datatype play_outcome = Played of Time.time | @@ -52,12 +71,46 @@ type minimize_command = string list -> string type one_line_params = - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int val smtN = "smt" -fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | string_of_reconstructor SMT = smtN +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" + | SMT_Method => "smt" + | Simp_Method => "simp" + | Simp_Size_Method => "simp add: size_ne_size_imp_ne" + | Auto_Method => "auto" + | Fastforce_Method => "fastforce" + | Force_Method => "force" + | Arith_Method => "arith" + | Blast_Method => "blast" + | Algebra_Method => "algebra") + +fun tac_of_proof_method ctxt (local_facts, global_facts) meth = + Method.insert_tac local_facts THEN' + (case meth of + Metis_Method (type_enc_opt, lam_trans_opt) => + Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] + (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts + | SMT_Method => SMT_Solver.smt_tac ctxt global_facts + | Meson_Method => Meson.meson_tac ctxt global_facts + | _ => + Method.insert_tac global_facts THEN' + (case meth of + 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) + | Fastforce_Method => Clasimp.fast_force_tac ctxt + | Force_Method => Clasimp.force_tac ctxt + | Arith_Method => Arith_Data.arith_tac ctxt + | Blast_Method => blast_tac ctxt + | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" @@ -94,9 +147,10 @@ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" -fun reconstructor_command reconstr i n used_chaineds num_chained ss = +(* 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_reconstructor reconstr) ss + apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss fun show_time NONE = "" | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" @@ -116,7 +170,7 @@ |> pairself (sort_distinct (string_ord o pairself fst)) fun one_line_proof_text num_chained - ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = + ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts @@ -129,7 +183,7 @@ val try_line = map fst extra - |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained + |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained |> (if failed then enclose "One-line proof reconstruction failed: " ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)" @@ -139,9 +193,9 @@ try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end -(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification - bound exceeded" warnings and the like. *) -fun silence_reconstructors debug = +(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound + exceeded" warnings and the like. *) +fun silence_proof_methods debug = Try0.silence_methods debug #> Config.put SMT_Config.verbose debug diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 14:35:19 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 15:19:07 2014 +0100 @@ -69,10 +69,10 @@ | "" => SOME true | _ => raise Option.Option) handle Option.Option => - let val ss = map quote ((option ? cons "smart") ["true", "false"]) in - error ("Parameter " ^ quote name ^ " must be assigned " ^ - space_implode " " (serial_commas "or" ss) ^ ".") - end + let val ss = map quote ((option ? cons "smart") ["true", "false"]) in + error ("Parameter " ^ quote name ^ " must be assigned " ^ + space_implode " " (serial_commas "or" ss) ^ ".") + end val has_junk = exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) @@ -80,8 +80,8 @@ fun parse_time name s = let val secs = if has_junk s then NONE else Real.fromString s in if is_none secs orelse Real.< (the secs, 0.0) then - error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ - \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") + error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \ + \(e.g., \"60\", \"0.5\") or \"none\".") else seconds (the secs) end