1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 14:35:19 2014 +0100
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 15:19:07 2014 +0100
1.3 @@ -19,7 +19,7 @@
1.4 (*refers to minimization attempted by Mirabelle*)
1.5 val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*)
1.6
1.7 -val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
1.8 +val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
1.9 val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
1.10
1.11 val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
1.12 @@ -43,8 +43,7 @@
1.13
1.14 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
1.15 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
1.16 -fun reconstructor_tag reconstructor id =
1.17 - "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
1.18 +fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
1.19
1.20 val separator = "-----"
1.21
1.22 @@ -130,16 +129,16 @@
1.23 proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
1.24 nontriv_success, proofs, time, timeout, lemmas, posns)
1.25
1.26 -datatype reconstructor_mode =
1.27 +datatype proof_method_mode =
1.28 Unminimized | Minimized | UnminimizedFT | MinimizedFT
1.29
1.30 datatype data = Data of {
1.31 sh: sh_data,
1.32 min: min_data,
1.33 - re_u: re_data, (* reconstructor with unminimized set of lemmas *)
1.34 - re_m: re_data, (* reconstructor with minimized set of lemmas *)
1.35 - re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
1.36 - re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
1.37 + re_u: re_data, (* proof method with unminimized set of lemmas *)
1.38 + re_m: re_data, (* proof method with minimized set of lemmas *)
1.39 + re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *)
1.40 + re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *)
1.41 mini: bool (* with minimization *)
1.42 }
1.43
1.44 @@ -218,39 +217,39 @@
1.45 fun inc_min_ab_ratios r = map_min_data
1.46 (fn (succs, ab_ratios) => (succs, ab_ratios+r))
1.47
1.48 -val inc_reconstructor_calls = map_re_data
1.49 +val inc_proof_method_calls = map_re_data
1.50 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.51 => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
1.52
1.53 -val inc_reconstructor_success = map_re_data
1.54 +val inc_proof_method_success = map_re_data
1.55 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.56 => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
1.57
1.58 -val inc_reconstructor_nontriv_calls = map_re_data
1.59 +val inc_proof_method_nontriv_calls = map_re_data
1.60 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.61 => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
1.62
1.63 -val inc_reconstructor_nontriv_success = map_re_data
1.64 +val inc_proof_method_nontriv_success = map_re_data
1.65 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.66 => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
1.67
1.68 -val inc_reconstructor_proofs = map_re_data
1.69 +val inc_proof_method_proofs = map_re_data
1.70 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.71 => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
1.72
1.73 -fun inc_reconstructor_time m t = map_re_data
1.74 +fun inc_proof_method_time m t = map_re_data
1.75 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.76 => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
1.77
1.78 -val inc_reconstructor_timeout = map_re_data
1.79 +val inc_proof_method_timeout = map_re_data
1.80 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.81 => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
1.82
1.83 -fun inc_reconstructor_lemmas m n = map_re_data
1.84 +fun inc_proof_method_lemmas m n = map_re_data
1.85 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.86 => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
1.87
1.88 -fun inc_reconstructor_posns m pos = map_re_data
1.89 +fun inc_proof_method_posns m pos = map_re_data
1.90 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
1.91 => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
1.92
1.93 @@ -292,19 +291,19 @@
1.94 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
1.95 re_nontriv_success, re_proofs, re_time, re_timeout,
1.96 (lemmas, lems_sos, lems_max), re_posns) =
1.97 - (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
1.98 - log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
1.99 + (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls);
1.100 + log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^
1.101 " (proof: " ^ str re_proofs ^ ")");
1.102 - log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
1.103 + log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout);
1.104 log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
1.105 - log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
1.106 - log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
1.107 + log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls);
1.108 + log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^
1.109 " (proof: " ^ str re_proofs ^ ")");
1.110 - log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
1.111 - log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
1.112 - log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
1.113 - log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
1.114 - log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
1.115 + log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas);
1.116 + log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos);
1.117 + log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max);
1.118 + log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time));
1.119 + log ("Average time for successful " ^ tag ^ "proof method calls: " ^
1.120 str3 (avg_time re_time re_success));
1.121 if tag=""
1.122 then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
1.123 @@ -325,7 +324,7 @@
1.124 fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
1.125 fun log_re tag m =
1.126 log_re_data log tag sh_calls (tuple_of_re_data m)
1.127 - fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
1.128 + fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
1.129 (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
1.130 in
1.131 if sh_calls > 0
1.132 @@ -334,14 +333,14 @@
1.133 log_sh_data log (tuple_of_sh_data sh);
1.134 log "";
1.135 if not mini
1.136 - then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
1.137 + then log_proof_method ("", re_u) ("fully-typed ", re_uft)
1.138 else
1.139 app_if re_u (fn () =>
1.140 - (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
1.141 + (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
1.142 log "";
1.143 app_if re_m (fn () =>
1.144 (log_min_data log (tuple_of_min_data min); log "";
1.145 - log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
1.146 + log_proof_method ("", re_m) ("fully-typed ", re_mft))))))
1.147 else ()
1.148 end
1.149
1.150 @@ -385,8 +384,8 @@
1.151 andalso not (String.isSubstring "may fail" s)
1.152
1.153 (* Fragile hack *)
1.154 -fun reconstructor_from_msg args msg =
1.155 - (case AList.lookup (op =) args reconstructorK of
1.156 +fun proof_method_from_msg args msg =
1.157 + (case AList.lookup (op =) args proof_methodK of
1.158 SOME name => name
1.159 | NONE =>
1.160 if exists good_line (split_lines msg) then
1.161 @@ -460,7 +459,7 @@
1.162 fun failed failure =
1.163 ({outcome = SOME failure, used_facts = [], used_from = [],
1.164 run_time = Time.zeroTime,
1.165 - preplay = Lazy.value (Sledgehammer_Prover.plain_metis,
1.166 + preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE),
1.167 Sledgehammer_Reconstructor.Play_Failed),
1.168 message = K "", message_tail = ""}, ~1)
1.169 val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
1.170 @@ -501,7 +500,7 @@
1.171
1.172 in
1.173
1.174 -fun run_sledgehammer trivial args reconstructor named_thms id
1.175 +fun run_sledgehammer trivial args proof_method named_thms id
1.176 ({pre=st, log, pos, ...}: Mirabelle.run_args) =
1.177 let
1.178 val thy = Proof.theory_of st
1.179 @@ -557,7 +556,7 @@
1.180 change_data id (inc_sh_max_lems (length names));
1.181 change_data id (inc_sh_time_isa time_isa);
1.182 change_data id (inc_sh_time_prover time_prover);
1.183 - reconstructor := reconstructor_from_msg args msg;
1.184 + proof_method := proof_method_from_msg args msg;
1.185 named_thms := SOME (map_filter get_thms names);
1.186 log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
1.187 string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
1.188 @@ -572,7 +571,7 @@
1.189
1.190 end
1.191
1.192 -fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
1.193 +fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
1.194 let
1.195 val thy = Proof.theory_of st
1.196 val {goal, ...} = Proof.goal st
1.197 @@ -614,7 +613,7 @@
1.198 change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
1.199 if length named_thms' = n0
1.200 then log (minimize_tag id ^ "already minimal")
1.201 - else (reconstructor := reconstructor_from_msg args msg;
1.202 + else (meth := proof_method_from_msg args msg;
1.203 named_thms := SOME named_thms';
1.204 log (minimize_tag id ^ "succeeded:\n" ^ msg))
1.205 )
1.206 @@ -629,10 +628,10 @@
1.207 ("slice", "false"),
1.208 ("timeout", timeout |> Time.toSeconds |> string_of_int)]
1.209
1.210 -fun run_reconstructor trivial full m name reconstructor named_thms id
1.211 +fun run_proof_method trivial full m name meth named_thms id
1.212 ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
1.213 let
1.214 - fun do_reconstructor named_thms ctxt =
1.215 + fun do_method named_thms ctxt =
1.216 let
1.217 val ref_of_str =
1.218 suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
1.219 @@ -646,56 +645,56 @@
1.220 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
1.221 (override_params prover type_enc (my_timeout time_slice)) fact_override
1.222 in
1.223 - if !reconstructor = "sledgehammer_tac" then
1.224 + if !meth = "sledgehammer_tac" then
1.225 sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
1.226 ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
1.227 ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
1.228 ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
1.229 ORELSE' SMT_Solver.smt_tac ctxt thms
1.230 - else if !reconstructor = "smt" then
1.231 + else if !meth = "smt" then
1.232 SMT_Solver.smt_tac ctxt thms
1.233 else if full then
1.234 Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
1.235 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
1.236 - else if String.isPrefix "metis (" (!reconstructor) then
1.237 + else if String.isPrefix "metis (" (!meth) then
1.238 let
1.239 val (type_encs, lam_trans) =
1.240 - !reconstructor
1.241 + !meth
1.242 |> Outer_Syntax.scan Position.start
1.243 |> filter Token.is_proper |> tl
1.244 |> Metis_Tactic.parse_metis_options |> fst
1.245 |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
1.246 ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
1.247 in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
1.248 - else if !reconstructor = "metis" then
1.249 + else if !meth = "metis" then
1.250 Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
1.251 else
1.252 K all_tac
1.253 end
1.254 - fun apply_reconstructor named_thms =
1.255 - Mirabelle.can_apply timeout (do_reconstructor named_thms) st
1.256 + fun apply_method named_thms =
1.257 + Mirabelle.can_apply timeout (do_method named_thms) st
1.258
1.259 fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
1.260 - | with_time (true, t) = (change_data id (inc_reconstructor_success m);
1.261 + | with_time (true, t) = (change_data id (inc_proof_method_success m);
1.262 if trivial then ()
1.263 - else change_data id (inc_reconstructor_nontriv_success m);
1.264 - change_data id (inc_reconstructor_lemmas m (length named_thms));
1.265 - change_data id (inc_reconstructor_time m t);
1.266 - change_data id (inc_reconstructor_posns m (pos, trivial));
1.267 - if name = "proof" then change_data id (inc_reconstructor_proofs m) else ();
1.268 + else change_data id (inc_proof_method_nontriv_success m);
1.269 + change_data id (inc_proof_method_lemmas m (length named_thms));
1.270 + change_data id (inc_proof_method_time m t);
1.271 + change_data id (inc_proof_method_posns m (pos, trivial));
1.272 + if name = "proof" then change_data id (inc_proof_method_proofs m) else ();
1.273 "succeeded (" ^ string_of_int t ^ ")")
1.274 - fun timed_reconstructor named_thms =
1.275 - (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
1.276 - handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false))
1.277 + fun timed_method named_thms =
1.278 + (with_time (Mirabelle.cpu_time apply_method named_thms), true)
1.279 + handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false))
1.280 | ERROR msg => ("error: " ^ msg, false)
1.281
1.282 val _ = log separator
1.283 - val _ = change_data id (inc_reconstructor_calls m)
1.284 - val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m)
1.285 + val _ = change_data id (inc_proof_method_calls m)
1.286 + val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m)
1.287 in
1.288 named_thms
1.289 - |> timed_reconstructor
1.290 - |>> log o prefix (reconstructor_tag reconstructor id)
1.291 + |> timed_method
1.292 + |>> log o prefix (proof_method_tag meth id)
1.293 |> snd
1.294 end
1.295
1.296 @@ -717,7 +716,7 @@
1.297 if !num_sledgehammer_calls > max_calls then ()
1.298 else
1.299 let
1.300 - val reconstructor = Unsynchronized.ref ""
1.301 + val meth = Unsynchronized.ref ""
1.302 val named_thms =
1.303 Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
1.304 val minimize = AList.defined (op =) args minimizeK
1.305 @@ -728,33 +727,28 @@
1.306 Try0.try0 (SOME try_timeout) ([], [], [], []) pre
1.307 handle TimeLimit.TimeOut => false
1.308 else false
1.309 - fun apply_reconstructor m1 m2 =
1.310 + fun apply_method m1 m2 =
1.311 if metis_ft
1.312 then
1.313 - if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
1.314 - (run_reconstructor trivial false m1 name reconstructor
1.315 - (these (!named_thms))) id st)
1.316 + if not (Mirabelle.catch_result (proof_method_tag meth) false
1.317 + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st)
1.318 then
1.319 - (Mirabelle.catch_result (reconstructor_tag reconstructor) false
1.320 - (run_reconstructor trivial true m2 name reconstructor
1.321 - (these (!named_thms))) id st; ())
1.322 + (Mirabelle.catch_result (proof_method_tag meth) false
1.323 + (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ())
1.324 else ()
1.325 else
1.326 - (Mirabelle.catch_result (reconstructor_tag reconstructor) false
1.327 - (run_reconstructor trivial false m1 name reconstructor
1.328 - (these (!named_thms))) id st; ())
1.329 + (Mirabelle.catch_result (proof_method_tag meth) false
1.330 + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
1.331 in
1.332 change_data id (set_mini minimize);
1.333 - Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
1.334 - named_thms) id st;
1.335 + Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
1.336 if is_some (!named_thms)
1.337 then
1.338 - (apply_reconstructor Unminimized UnminimizedFT;
1.339 + (apply_method Unminimized UnminimizedFT;
1.340 if minimize andalso not (null (these (!named_thms)))
1.341 then
1.342 - (Mirabelle.catch minimize_tag
1.343 - (run_minimize args reconstructor named_thms) id st;
1.344 - apply_reconstructor Minimized MinimizedFT)
1.345 + (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st;
1.346 + apply_method Minimized MinimizedFT)
1.347 else ())
1.348 else ()
1.349 end
2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 14:35:19 2014 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 15:19:07 2014 +0100
2.3 @@ -28,9 +28,9 @@
2.4 val partial_type_encs : string list
2.5 val default_metis_lam_trans : string
2.6
2.7 - val metis_call : string -> string -> string
2.8 val forall_of : term -> term -> term
2.9 val exists_of : term -> term -> term
2.10 + val type_enc_aliases : (string * string list) list
2.11 val unalias_type_enc : string -> string list
2.12 val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
2.13 (string, string atp_type) atp_term -> term
2.14 @@ -84,17 +84,6 @@
2.15
2.16 val default_metis_lam_trans = combsN
2.17
2.18 -fun metis_call type_enc lam_trans =
2.19 - let
2.20 - val type_enc =
2.21 - (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
2.22 - [alias] => alias
2.23 - | _ => type_enc)
2.24 - val opts =
2.25 - [] |> type_enc <> partial_typesN ? cons type_enc
2.26 - |> lam_trans <> default_metis_lam_trans ? cons lam_trans
2.27 - in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
2.28 -
2.29 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
2.30 | term_name' _ = ""
2.31
3.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 14:35:19 2014 +0100
3.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 15:19:07 2014 +0100
3.3 @@ -129,6 +129,17 @@
3.4 | ord => ord
3.5 in {weight = weight, precedence = precedence} end
3.6
3.7 +fun metis_call type_enc lam_trans =
3.8 + let
3.9 + val type_enc =
3.10 + (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
3.11 + [alias] => alias
3.12 + | _ => type_enc)
3.13 + val opts =
3.14 + [] |> type_enc <> partial_typesN ? cons type_enc
3.15 + |> lam_trans <> default_metis_lam_trans ? cons lam_trans
3.16 + in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
3.17 +
3.18 exception METIS_UNPROVABLE of unit
3.19
3.20 (* Main function to start Metis proof and reconstruction *)
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 14:35:19 2014 +0100
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:19:07 2014 +0100
4.3 @@ -286,7 +286,7 @@
4.4
4.5 val ctxt = ctxt
4.6 |> enrich_context_with_local_facts canonical_isar_proof
4.7 - |> silence_reconstructors debug
4.8 + |> silence_proof_methods debug
4.9
4.10 val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
4.11
4.12 @@ -354,9 +354,9 @@
4.13 if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
4.14 in one_line_proof ^ isar_proof end
4.15
4.16 -fun isar_proof_would_be_a_good_idea (reconstr, play) =
4.17 +fun isar_proof_would_be_a_good_idea (meth, play) =
4.18 (case play of
4.19 - Played _ => reconstr = SMT
4.20 + Played _ => meth = SMT_Method
4.21 | Play_Timed_Out _ => true
4.22 | Play_Failed => true
4.23 | Not_Played => false)
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:35:19 2014 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 15:19:07 2014 +0100
5.3 @@ -100,27 +100,6 @@
5.4 |> Skip_Proof.make_thm thy
5.5 end
5.6
5.7 -fun tac_of_method ctxt (local_facts, global_facts) meth =
5.8 - Method.insert_tac local_facts THEN'
5.9 - (case meth of
5.10 - Metis_Method (type_enc_opt, lam_trans_opt) =>
5.11 - Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
5.12 - (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
5.13 - | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
5.14 - | Meson_Method => Meson.meson_tac ctxt global_facts
5.15 - | _ =>
5.16 - Method.insert_tac global_facts THEN'
5.17 - (case meth of
5.18 - Simp_Method => Simplifier.asm_full_simp_tac ctxt
5.19 - | Simp_Size_Method =>
5.20 - Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
5.21 - | Auto_Method => K (Clasimp.auto_tac ctxt)
5.22 - | Fastforce_Method => Clasimp.fast_force_tac ctxt
5.23 - | Force_Method => Clasimp.force_tac ctxt
5.24 - | Arith_Method => Arith_Data.arith_tac ctxt
5.25 - | Blast_Method => blast_tac ctxt
5.26 - | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
5.27 -
5.28 (* main function for preplaying Isar steps; may throw exceptions *)
5.29 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
5.30 let
5.31 @@ -149,7 +128,7 @@
5.32
5.33 fun prove () =
5.34 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
5.35 - HEADGOAL (tac_of_method ctxt facts meth))
5.36 + HEADGOAL (tac_of_proof_method ctxt facts meth))
5.37 handle ERROR msg => error ("Preplay error: " ^ msg)
5.38
5.39 val play_outcome = take_time timeout prove ()
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 14:35:19 2014 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 15:19:07 2014 +0100
6.3 @@ -8,24 +8,13 @@
6.4
6.5 signature SLEDGEHAMMER_ISAR_PROOF =
6.6 sig
6.7 + type proof_method = Sledgehammer_Reconstructor.proof_method
6.8 +
6.9 type label = string * int
6.10 type facts = label list * string list (* local and global facts *)
6.11
6.12 datatype isar_qualifier = Show | Then
6.13
6.14 - datatype proof_method =
6.15 - Metis_Method of string option * string option |
6.16 - Meson_Method |
6.17 - SMT_Method |
6.18 - Simp_Method |
6.19 - Simp_Size_Method |
6.20 - Auto_Method |
6.21 - Fastforce_Method |
6.22 - Force_Method |
6.23 - Arith_Method |
6.24 - Blast_Method |
6.25 - Algebra_Method
6.26 -
6.27 datatype isar_proof =
6.28 Proof of (string * typ) list * (label * term) list * isar_step list
6.29 and isar_step =
6.30 @@ -38,8 +27,6 @@
6.31 val label_ord : label * label -> order
6.32 val string_of_label : label -> string
6.33
6.34 - val string_of_proof_method : proof_method -> string
6.35 -
6.36 val steps_of_isar_proof : isar_proof -> isar_step list
6.37
6.38 val label_of_isar_step : isar_step -> label option
6.39 @@ -79,19 +66,6 @@
6.40
6.41 datatype isar_qualifier = Show | Then
6.42
6.43 -datatype proof_method =
6.44 - Metis_Method of string option * string option |
6.45 - Meson_Method |
6.46 - SMT_Method |
6.47 - Simp_Method |
6.48 - Simp_Size_Method |
6.49 - Auto_Method |
6.50 - Fastforce_Method |
6.51 - Force_Method |
6.52 - Arith_Method |
6.53 - Blast_Method |
6.54 - Algebra_Method
6.55 -
6.56 datatype isar_proof =
6.57 Proof of (string * typ) list * (label * term) list * isar_step list
6.58 and isar_step =
6.59 @@ -105,22 +79,6 @@
6.60
6.61 fun string_of_label (s, num) = s ^ string_of_int num
6.62
6.63 -fun string_of_proof_method meth =
6.64 - (case meth of
6.65 - Metis_Method (NONE, NONE) => "metis"
6.66 - | Metis_Method (type_enc_opt, lam_trans_opt) =>
6.67 - "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
6.68 - | Meson_Method => "meson"
6.69 - | SMT_Method => "smt"
6.70 - | Simp_Method => "simp"
6.71 - | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
6.72 - | Auto_Method => "auto"
6.73 - | Fastforce_Method => "fastforce"
6.74 - | Force_Method => "force"
6.75 - | Arith_Method => "arith"
6.76 - | Blast_Method => "blast"
6.77 - | Algebra_Method => "algebra")
6.78 -
6.79 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
6.80
6.81 fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 14:35:19 2014 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:19:07 2014 +0100
7.3 @@ -12,7 +12,7 @@
7.4 type stature = ATP_Problem_Generate.stature
7.5 type type_enc = ATP_Problem_Generate.type_enc
7.6 type fact = Sledgehammer_Fact.fact
7.7 - type reconstructor = Sledgehammer_Reconstructor.reconstructor
7.8 + type proof_method = Sledgehammer_Reconstructor.proof_method
7.9 type play_outcome = Sledgehammer_Reconstructor.play_outcome
7.10 type minimize_command = Sledgehammer_Reconstructor.minimize_command
7.11
7.12 @@ -57,8 +57,8 @@
7.13 used_facts : (string * stature) list,
7.14 used_from : fact list,
7.15 run_time : Time.time,
7.16 - preplay : (reconstructor * play_outcome) Lazy.lazy,
7.17 - message : reconstructor * play_outcome -> string,
7.18 + preplay : (proof_method * play_outcome) Lazy.lazy,
7.19 + message : proof_method * play_outcome -> string,
7.20 message_tail : string}
7.21
7.22 type prover =
7.23 @@ -66,23 +66,22 @@
7.24 -> prover_problem -> prover_result
7.25
7.26 val SledgehammerN : string
7.27 - val plain_metis : reconstructor
7.28 val overlord_file_location_of_prover : string -> string * string
7.29 val proof_banner : mode -> string -> string
7.30 - val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
7.31 - val is_reconstructor : string -> bool
7.32 + val extract_proof_method : params -> proof_method -> string * (string * string list) list
7.33 + val is_proof_method : string -> bool
7.34 val is_atp : theory -> string -> bool
7.35 - val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
7.36 + val bunch_of_proof_methods : bool -> string -> proof_method list
7.37 val is_fact_chained : (('a * stature) * 'b) -> bool
7.38 val filter_used_facts :
7.39 bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
7.40 ((''a * stature) * 'b) list
7.41 val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
7.42 - Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
7.43 + Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
7.44 val remotify_atp_if_not_installed : theory -> string -> string option
7.45 val isar_supported_prover_of : theory -> string -> string
7.46 val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
7.47 - string -> reconstructor * play_outcome -> 'a
7.48 + string -> proof_method * play_outcome -> 'a
7.49 val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
7.50 Proof.context
7.51
7.52 @@ -110,9 +109,8 @@
7.53 "Async_Manager". *)
7.54 val SledgehammerN = "Sledgehammer"
7.55
7.56 -val reconstructor_names = [metisN, smtN]
7.57 -val plain_metis = Metis (hd partial_type_encs, combsN)
7.58 -val is_reconstructor = member (op =) reconstructor_names
7.59 +val proof_method_names = [metisN, smtN]
7.60 +val is_proof_method = member (op =) proof_method_names
7.61
7.62 val is_atp = member (op =) o supported_atps
7.63
7.64 @@ -167,8 +165,8 @@
7.65 used_facts : (string * stature) list,
7.66 used_from : fact list,
7.67 run_time : Time.time,
7.68 - preplay : (reconstructor * play_outcome) Lazy.lazy,
7.69 - message : reconstructor * play_outcome -> string,
7.70 + preplay : (proof_method * play_outcome) Lazy.lazy,
7.71 + message : proof_method * play_outcome -> string,
7.72 message_tail : string}
7.73
7.74 type prover =
7.75 @@ -183,29 +181,30 @@
7.76 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
7.77 | _ => "Try this")
7.78
7.79 -fun bunch_of_reconstructors needs_full_types lam_trans =
7.80 +fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
7.81 if needs_full_types then
7.82 - [Metis (full_type_enc, lam_trans false),
7.83 - Metis (really_full_type_enc, lam_trans false),
7.84 - Metis (full_type_enc, lam_trans true),
7.85 - Metis (really_full_type_enc, lam_trans true),
7.86 - SMT]
7.87 + [Metis_Method (SOME full_type_enc, NONE),
7.88 + Metis_Method (SOME really_full_type_enc, NONE),
7.89 + Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
7.90 + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
7.91 + SMT_Method]
7.92 else
7.93 - [Metis (partial_type_enc, lam_trans false),
7.94 - Metis (full_type_enc, lam_trans false),
7.95 - Metis (no_typesN, lam_trans true),
7.96 - Metis (really_full_type_enc, lam_trans true),
7.97 - SMT]
7.98 + [Metis_Method (NONE, NONE),
7.99 + Metis_Method (SOME full_type_enc, NONE),
7.100 + Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
7.101 + Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
7.102 + SMT_Method]
7.103
7.104 -fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
7.105 +fun extract_proof_method ({type_enc, lam_trans, ...} : params)
7.106 + (Metis_Method (type_enc', lam_trans')) =
7.107 let
7.108 val override_params =
7.109 - (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
7.110 - else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
7.111 - (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
7.112 - else [("lam_trans", [lam_trans'])])
7.113 + (if is_none type_enc' andalso is_none type_enc then []
7.114 + else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
7.115 + (if is_none lam_trans' andalso is_none lam_trans then []
7.116 + else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
7.117 in (metisN, override_params) end
7.118 - | extract_reconstructor _ SMT = (smtN, [])
7.119 + | extract_proof_method _ SMT_Method = (smtN, [])
7.120
7.121 (* based on "Mirabelle.can_apply" and generalized *)
7.122 fun timed_apply timeout tac state i =
7.123 @@ -216,49 +215,46 @@
7.124 TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
7.125 end
7.126
7.127 -fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
7.128 - | tac_of_reconstructor SMT = SMT_Solver.smt_tac
7.129 -
7.130 -fun timed_reconstructor reconstr debug timeout ths =
7.131 - timed_apply timeout (silence_reconstructors debug
7.132 - #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
7.133 +(* FIXME *)
7.134 +fun timed_proof_method meth debug timeout ths =
7.135 + timed_apply timeout (silence_proof_methods debug
7.136 + #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
7.137
7.138 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
7.139
7.140 fun filter_used_facts keep_chained used =
7.141 filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
7.142
7.143 -fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
7.144 +fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
7.145 let
7.146 - fun get_preferred reconstrs =
7.147 - if member (op =) reconstrs preferred then preferred
7.148 - else List.last reconstrs
7.149 + fun get_preferred meths =
7.150 + if member (op =) meths preferred then preferred else List.last meths
7.151 in
7.152 if timeout = Time.zeroTime then
7.153 - (get_preferred reconstrs, Not_Played)
7.154 + (get_preferred meths, Not_Played)
7.155 else
7.156 let
7.157 val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
7.158 val ths = pairs |> sort_wrt (fst o fst) |> map snd
7.159 - fun play [] [] = (get_preferred reconstrs, Play_Failed)
7.160 + fun play [] [] = (get_preferred meths, Play_Failed)
7.161 | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
7.162 - | play timed_out (reconstr :: reconstrs) =
7.163 + | play timed_out (meth :: meths) =
7.164 let
7.165 val _ =
7.166 if verbose then
7.167 - Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
7.168 + Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
7.169 "\" for " ^ string_of_time timeout ^ "...")
7.170 else
7.171 ()
7.172 val timer = Timer.startRealTimer ()
7.173 in
7.174 - case timed_reconstructor reconstr debug timeout ths state i of
7.175 - SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
7.176 - | _ => play timed_out reconstrs
7.177 + case timed_proof_method meth debug timeout ths state i of
7.178 + SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
7.179 + | _ => play timed_out meths
7.180 end
7.181 - handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
7.182 + handle TimeLimit.TimeOut => play (meth :: timed_out) meths
7.183 in
7.184 - play [] reconstrs
7.185 + play [] meths
7.186 end
7.187 end
7.188
7.189 @@ -275,9 +271,8 @@
7.190 val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
7.191 val (min_name, override_params) =
7.192 (case preplay of
7.193 - (reconstr, Played _) =>
7.194 - if isar_proofs = SOME true then (maybe_isar_name, [])
7.195 - else extract_reconstructor params reconstr
7.196 + (meth, Played _) =>
7.197 + if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
7.198 | _ => (maybe_isar_name, []))
7.199 in minimize_command override_params min_name end
7.200
7.201 @@ -293,7 +288,7 @@
7.202 let
7.203 val thy = Proof_Context.theory_of ctxt
7.204 val (remote_provers, local_provers) =
7.205 - reconstructor_names @
7.206 + proof_method_names @
7.207 sort_strings (supported_atps thy) @
7.208 sort_strings (SMT_Solver.available_solvers_of ctxt)
7.209 |> List.partition (String.isPrefix remote_prefix)
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 14:35:19 2014 +0100
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 15:19:07 2014 +0100
8.3 @@ -346,18 +346,15 @@
8.4 let
8.5 val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
8.6 val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
8.7 - val reconstrs =
8.8 - bunch_of_reconstructors needs_full_types (fn desperate =>
8.9 - if desperate then
8.10 - if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN
8.11 - else
8.12 - default_metis_lam_trans)
8.13 + val meths =
8.14 + bunch_of_proof_methods needs_full_types
8.15 + (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
8.16 in
8.17 (used_facts,
8.18 Lazy.lazy (fn () =>
8.19 let val used_pairs = used_from |> filter_used_facts false used_facts in
8.20 play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
8.21 - (hd reconstrs) reconstrs
8.22 + (hd meths) meths
8.23 end),
8.24 fn preplay =>
8.25 let
8.26 @@ -392,7 +389,8 @@
8.27 ""))
8.28 end
8.29 | SOME failure =>
8.30 - ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
8.31 + ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
8.32 + fn _ => string_of_atp_failure failure, ""))
8.33 in
8.34 {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
8.35 preplay = preplay, message = message, message_tail = message_tail}
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 14:35:19 2014 +0100
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 15:19:07 2014 +0100
9.3 @@ -8,7 +8,7 @@
9.4 signature SLEDGEHAMMER_PROVER_MINIMIZE =
9.5 sig
9.6 type stature = ATP_Problem_Generate.stature
9.7 - type reconstructor = Sledgehammer_Reconstructor.reconstructor
9.8 + type proof_method = Sledgehammer_Reconstructor.proof_method
9.9 type play_outcome = Sledgehammer_Reconstructor.play_outcome
9.10 type mode = Sledgehammer_Prover.mode
9.11 type params = Sledgehammer_Prover.params
9.12 @@ -23,11 +23,11 @@
9.13 val auto_minimize_min_facts : int Config.T
9.14 val auto_minimize_max_time : real Config.T
9.15 val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
9.16 - Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
9.17 + Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
9.18 ((string * stature) * thm list) list ->
9.19 ((string * stature) * thm list) list option
9.20 - * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
9.21 - * string)
9.22 + * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string)
9.23 + * string)
9.24 val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
9.25
9.26 val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
9.27 @@ -50,29 +50,25 @@
9.28 open Sledgehammer_Prover_ATP
9.29 open Sledgehammer_Prover_SMT
9.30
9.31 -fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
9.32 +fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
9.33 minimize_command
9.34 ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
9.35 let
9.36 - val reconstr =
9.37 - if name = metisN then
9.38 - Metis (type_enc |> the_default (hd partial_type_encs),
9.39 - lam_trans |> the_default default_metis_lam_trans)
9.40 - else if name = smtN then
9.41 - SMT
9.42 - else
9.43 - raise Fail ("unknown reconstructor: " ^ quote name)
9.44 + val meth =
9.45 + if name = metisN then Metis_Method (type_enc, lam_trans)
9.46 + else if name = smtN then SMT_Method
9.47 + else raise Fail ("unknown proof_method: " ^ quote name)
9.48 val used_facts = facts |> map fst
9.49 in
9.50 (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
9.51 - state subgoal reconstr [reconstr] of
9.52 + state subgoal meth [meth] of
9.53 play as (_, Played time) =>
9.54 {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
9.55 preplay = Lazy.value play,
9.56 message =
9.57 fn play =>
9.58 let
9.59 - val (_, override_params) = extract_reconstructor params reconstr
9.60 + val (_, override_params) = extract_proof_method params meth
9.61 val one_line_params =
9.62 (play, proof_banner mode name, used_facts, minimize_command override_params name,
9.63 subgoal, subgoal_count)
9.64 @@ -93,18 +89,18 @@
9.65
9.66 fun is_prover_supported ctxt =
9.67 let val thy = Proof_Context.theory_of ctxt in
9.68 - is_reconstructor orf is_atp thy orf is_smt_prover ctxt
9.69 + is_proof_method orf is_atp thy orf is_smt_prover ctxt
9.70 end
9.71
9.72 fun is_prover_installed ctxt =
9.73 - is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
9.74 + is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
9.75
9.76 -val reconstructor_default_max_facts = 20
9.77 +val proof_method_default_max_facts = 20
9.78
9.79 fun default_max_facts_of_prover ctxt name =
9.80 let val thy = Proof_Context.theory_of ctxt in
9.81 - if is_reconstructor name then
9.82 - reconstructor_default_max_facts
9.83 + if is_proof_method name then
9.84 + proof_method_default_max_facts
9.85 else if is_atp thy name then
9.86 fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
9.87 else (* is_smt_prover ctxt name *)
9.88 @@ -113,7 +109,7 @@
9.89
9.90 fun get_prover ctxt mode name =
9.91 let val thy = Proof_Context.theory_of ctxt in
9.92 - if is_reconstructor name then run_reconstructor mode name
9.93 + if is_proof_method name then run_proof_method mode name
9.94 else if is_atp thy name then run_atp mode name
9.95 else if is_smt_prover ctxt name then run_smt_solver mode name
9.96 else error ("No such prover: " ^ name ^ ".")
9.97 @@ -286,10 +282,11 @@
9.98 "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
9.99 \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
9.100 | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
9.101 - handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
9.102 + handle ERROR msg =>
9.103 + (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
9.104 end
9.105
9.106 -fun adjust_reconstructor_params override_params
9.107 +fun adjust_proof_method_params override_params
9.108 ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
9.109 uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
9.110 max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
9.111 @@ -299,7 +296,7 @@
9.112 (case AList.lookup (op =) override_params name of
9.113 SOME [s] => SOME s
9.114 | _ => default_value)
9.115 - (* Only those options that reconstructors are interested in are considered here. *)
9.116 + (* Only those options that proof_methods are interested in are considered here. *)
9.117 val type_enc = lookup_override "type_enc" type_enc
9.118 val lam_trans = lookup_override "lam_trans" lam_trans
9.119 in
9.120 @@ -336,18 +333,18 @@
9.121 fun prover_fast_enough () = can_min_fast_enough run_time
9.122 in
9.123 (case Lazy.force preplay of
9.124 - (reconstr as Metis _, Played timeout) =>
9.125 + (meth as Metis_Method _, Played timeout) =>
9.126 if isar_proofs = SOME true then
9.127 (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
9.128 itself. *)
9.129 (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
9.130 else if can_min_fast_enough timeout then
9.131 - (true, extract_reconstructor params reconstr
9.132 + (true, extract_proof_method params meth
9.133 ||> (fn override_params =>
9.134 - adjust_reconstructor_params override_params params))
9.135 + adjust_proof_method_params override_params params))
9.136 else
9.137 (prover_fast_enough (), (name, params))
9.138 - | (SMT, Played timeout) =>
9.139 + | (SMT_Method, Played timeout) =>
9.140 (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
9.141 itself. *)
9.142 (can_min_fast_enough timeout, (name, params))
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 14:35:19 2014 +0100
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 15:19:07 2014 +0100
10.3 @@ -233,9 +233,8 @@
10.4 (case outcome of
10.5 NONE =>
10.6 (Lazy.lazy (fn () =>
10.7 - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
10.8 - (bunch_of_reconstructors false (fn desperate =>
10.9 - if desperate then liftingN else default_metis_lam_trans))),
10.10 + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
10.11 + SMT_Method (bunch_of_proof_methods false liftingN)),
10.12 fn preplay =>
10.13 let
10.14 val one_line_params =
10.15 @@ -248,7 +247,8 @@
10.16 end,
10.17 if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
10.18 | SOME failure =>
10.19 - (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
10.20 + (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
10.21 + fn _ => string_of_atp_failure failure, ""))
10.22 in
10.23 {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
10.24 preplay = preplay, message = message, message_tail = message_tail}
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 14:35:19 2014 +0100
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:19:07 2014 +0100
11.3 @@ -9,9 +9,18 @@
11.4 sig
11.5 type stature = ATP_Problem_Generate.stature
11.6
11.7 - datatype reconstructor =
11.8 - Metis of string * string |
11.9 - SMT
11.10 + datatype proof_method =
11.11 + Metis_Method of string option * string option |
11.12 + Meson_Method |
11.13 + SMT_Method |
11.14 + Simp_Method |
11.15 + Simp_Size_Method |
11.16 + Auto_Method |
11.17 + Fastforce_Method |
11.18 + Force_Method |
11.19 + Arith_Method |
11.20 + Blast_Method |
11.21 + Algebra_Method
11.22
11.23 datatype play_outcome =
11.24 Played of Time.time |
11.25 @@ -21,16 +30,17 @@
11.26
11.27 type minimize_command = string list -> string
11.28 type one_line_params =
11.29 - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
11.30 + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
11.31
11.32 val smtN : string
11.33
11.34 - val string_of_reconstructor : reconstructor -> string
11.35 + val string_of_proof_method : proof_method -> string
11.36 + val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
11.37 val string_of_play_outcome : play_outcome -> string
11.38 val play_outcome_ord : play_outcome * play_outcome -> order
11.39
11.40 val one_line_proof_text : int -> one_line_params -> string
11.41 - val silence_reconstructors : bool -> Proof.context -> Proof.context
11.42 + val silence_proof_methods : bool -> Proof.context -> Proof.context
11.43 end;
11.44
11.45 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
11.46 @@ -40,9 +50,18 @@
11.47 open ATP_Problem_Generate
11.48 open ATP_Proof_Reconstruct
11.49
11.50 -datatype reconstructor =
11.51 - Metis of string * string |
11.52 - SMT
11.53 +datatype proof_method =
11.54 + Metis_Method of string option * string option |
11.55 + Meson_Method |
11.56 + SMT_Method |
11.57 + Simp_Method |
11.58 + Simp_Size_Method |
11.59 + Auto_Method |
11.60 + Fastforce_Method |
11.61 + Force_Method |
11.62 + Arith_Method |
11.63 + Blast_Method |
11.64 + Algebra_Method
11.65
11.66 datatype play_outcome =
11.67 Played of Time.time |
11.68 @@ -52,12 +71,46 @@
11.69
11.70 type minimize_command = string list -> string
11.71 type one_line_params =
11.72 - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
11.73 + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
11.74
11.75 val smtN = "smt"
11.76
11.77 -fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
11.78 - | string_of_reconstructor SMT = smtN
11.79 +fun string_of_proof_method meth =
11.80 + (case meth of
11.81 + Metis_Method (NONE, NONE) => "metis"
11.82 + | Metis_Method (type_enc_opt, lam_trans_opt) =>
11.83 + "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
11.84 + | Meson_Method => "meson"
11.85 + | SMT_Method => "smt"
11.86 + | Simp_Method => "simp"
11.87 + | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
11.88 + | Auto_Method => "auto"
11.89 + | Fastforce_Method => "fastforce"
11.90 + | Force_Method => "force"
11.91 + | Arith_Method => "arith"
11.92 + | Blast_Method => "blast"
11.93 + | Algebra_Method => "algebra")
11.94 +
11.95 +fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
11.96 + Method.insert_tac local_facts THEN'
11.97 + (case meth of
11.98 + Metis_Method (type_enc_opt, lam_trans_opt) =>
11.99 + Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
11.100 + (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
11.101 + | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
11.102 + | Meson_Method => Meson.meson_tac ctxt global_facts
11.103 + | _ =>
11.104 + Method.insert_tac global_facts THEN'
11.105 + (case meth of
11.106 + Simp_Method => Simplifier.asm_full_simp_tac ctxt
11.107 + | Simp_Size_Method =>
11.108 + Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
11.109 + | Auto_Method => K (Clasimp.auto_tac ctxt)
11.110 + | Fastforce_Method => Clasimp.fast_force_tac ctxt
11.111 + | Force_Method => Clasimp.force_tac ctxt
11.112 + | Arith_Method => Arith_Data.arith_tac ctxt
11.113 + | Blast_Method => blast_tac ctxt
11.114 + | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
11.115
11.116 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
11.117 | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
11.118 @@ -94,9 +147,10 @@
11.119 name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
11.120 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
11.121
11.122 -fun reconstructor_command reconstr i n used_chaineds num_chained ss =
11.123 +(* FIXME *)
11.124 +fun proof_method_command meth i n used_chaineds num_chained ss =
11.125 (* unusing_chained_facts used_chaineds num_chained ^ *)
11.126 - apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
11.127 + apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
11.128
11.129 fun show_time NONE = ""
11.130 | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
11.131 @@ -116,7 +170,7 @@
11.132 |> pairself (sort_distinct (string_ord o pairself fst))
11.133
11.134 fun one_line_proof_text num_chained
11.135 - ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
11.136 + ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
11.137 let
11.138 val (chained, extra) = split_used_facts used_facts
11.139
11.140 @@ -129,7 +183,7 @@
11.141
11.142 val try_line =
11.143 map fst extra
11.144 - |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
11.145 + |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
11.146 |> (if failed then
11.147 enclose "One-line proof reconstruction failed: "
11.148 ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
11.149 @@ -139,9 +193,9 @@
11.150 try_line ^ minimize_line minimize_command (map fst (extra @ chained))
11.151 end
11.152
11.153 -(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
11.154 - bound exceeded" warnings and the like. *)
11.155 -fun silence_reconstructors debug =
11.156 +(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
11.157 + exceeded" warnings and the like. *)
11.158 +fun silence_proof_methods debug =
11.159 Try0.silence_methods debug
11.160 #> Config.put SMT_Config.verbose debug
11.161
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 14:35:19 2014 +0100
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 15:19:07 2014 +0100
12.3 @@ -69,10 +69,10 @@
12.4 | "" => SOME true
12.5 | _ => raise Option.Option)
12.6 handle Option.Option =>
12.7 - let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
12.8 - error ("Parameter " ^ quote name ^ " must be assigned " ^
12.9 - space_implode " " (serial_commas "or" ss) ^ ".")
12.10 - end
12.11 + let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
12.12 + error ("Parameter " ^ quote name ^ " must be assigned " ^
12.13 + space_implode " " (serial_commas "or" ss) ^ ".")
12.14 + end
12.15
12.16 val has_junk =
12.17 exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
12.18 @@ -80,8 +80,8 @@
12.19 fun parse_time name s =
12.20 let val secs = if has_junk s then NONE else Real.fromString s in
12.21 if is_none secs orelse Real.< (the secs, 0.0) then
12.22 - error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
12.23 - \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
12.24 + error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
12.25 + \(e.g., \"60\", \"0.5\") or \"none\".")
12.26 else
12.27 seconds (the secs)
12.28 end