# HG changeset patch # User blanchet # Date 1391172167 -3600 # Node ID 11dd3d1da83bbf3b7450225029c6a2a69402904d # Parent 42ad887a1c7cc4b73a4eae7f801ddf9c906c3254 compile diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 13:42:47 2014 +0100 @@ -455,8 +455,6 @@ |> max_mono_itersLST) val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name - val is_appropriate_prop = - Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of @@ -472,8 +470,6 @@ : Sledgehammer_Prover.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let - val _ = if is_appropriate_prop concl_t then () - else raise Fail "inappropriate" val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name val reserved = Sledgehammer_Util.reserved_isar_keyword_table () val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt @@ -483,7 +479,6 @@ hyp_ts concl_t val factss = facts - |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/Nitpick_Examples/minipick.ML --- a/src/HOL/Nitpick_Examples/minipick.ML Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/Nitpick_Examples/minipick.ML Fri Jan 31 13:42:47 2014 +0100 @@ -456,7 +456,7 @@ fun problem_for (total, k) = kodkod_problem_from_term ctxt total (K k) default_raw_infinite t in - (totalsNitpick_Commands, 1 upto n) + (totals, 1 upto n) |-> map_product pair |> map problem_for |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt) diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Fri Jan 31 13:42:47 2014 +0100 @@ -26,7 +26,7 @@ ML {* val do_it = false (* switch to "true" to generate the files *) -val params = Sledgehammer_Commands.default_params @{context} [] +val params = Sledgehammer_Commands.default_params @{theory} [] val range = (1, NONE) val linearize = false val dir = "List" diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jan 31 13:42:47 2014 +0100 @@ -29,7 +29,7 @@ ML {* val do_it = false (* switch to "true" to generate the files *) val thys = [@{theory List}] -val params as {provers, ...} = Sledgehammer_Commands.default_params @{context} [] +val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} [] val prover = hd provers val range = (1, NONE) val step = 1 diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 13:42:47 2014 +0100 @@ -1,4 +1,4 @@ -Nitpick_Commands(* Title: HOL/TPTP/atp_problem_import.ML +(* Title: HOL/TPTP/atp_problem_import.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 13:42:47 2014 +0100 @@ -77,9 +77,6 @@ val is_reconstructor : string -> bool val is_atp : theory -> string -> bool val is_ho_atp: Proof.context -> string -> bool - val is_unit_equational_atp : Proof.context -> string -> bool - val is_unit_equality : term -> bool - val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool val supported_provers : Proof.context -> unit val kill_provers : unit -> unit val running_provers : unit -> unit @@ -146,7 +143,6 @@ | NONE => false) end -val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ) val is_ho_atp = is_atp_of_format is_format_higher_order fun remotify_atp_if_supported_and_not_already_remote thy name = @@ -161,28 +157,6 @@ if is_atp thy name andalso is_atp_installed thy name then SOME name else remotify_atp_if_supported_and_not_already_remote thy name -fun is_if (@{const_name If}, _) = true - | is_if _ = false - -(* Beware of "if and only if" (which is translated as such) and "If" (which is - translated to conditional equations). *) -fun is_good_unit_equality T t u = - T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u]) - -fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t - | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) = - is_unit_equality t - | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) = - is_unit_equality t - | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) = - is_good_unit_equality T t u - | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) = - is_good_unit_equality T t u - | is_unit_equality _ = false - -fun is_appropriate_prop_of_prover ctxt name = - if is_unit_equational_atp ctxt name then is_unit_equality else K true - fun supported_provers ctxt = let val thy = Proof_Context.theory_of ctxt diff -r 42ad887a1c7c -r 11dd3d1da83b src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jan 31 13:32:13 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jan 31 13:42:47 2014 +0100 @@ -48,26 +48,21 @@ | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = - case (pos, t) of + (case (pos, t) of (_, @{const Trueprop} $ t1) => do_formula pos t1 - | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => - do_formula pos t' + | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t' + | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t' + | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t' | (_, @{const "==>"} $ t1 $ t2) => - do_formula (not pos) t1 andalso - (t2 = @{prop False} orelse do_formula pos t2) + do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2) | (_, @{const HOL.implies} $ t1 $ t2) => - do_formula (not pos) t1 andalso - (t2 = @{const False} orelse do_formula pos t2) + do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2) | (_, @{const Not} $ t1) => do_formula (not pos) t1 | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 - | _ => false + | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form @@ -137,18 +132,17 @@ error ("No such directory: " ^ quote dest_dir ^ ".") val exec = exec () val command0 = - case find_first (fn var => getenv var <> "") (fst exec) of + (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (snd exec) in - case find_first File.exists paths of + (case find_first File.exists paths of SOME path => path - | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".") + | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")) end - | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ - " is not set.") + | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set.")) fun split_time s = let @@ -167,8 +161,7 @@ fun run () = let - (* If slicing is disabled, we expand the last slice to fill the entire - time available. *) + (* If slicing is disabled, we expand the last slice to fill the entire time available. *) val all_slices = best_slices ctxt val actual_slices = get_slices slice all_slices fun max_facts_of_slices f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0 @@ -196,19 +189,15 @@ in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) - |> maps (fn (name, rths) => - map (pair name o zero_var_indexes o snd) rths) + |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end - fun run_slice time_left (cache_key, cache_value) - (slice, (time_frac, - (key as ((best_max_facts, best_fact_filter), format, - best_type_enc, best_lam_trans, - best_uncurried_aliases), - extra))) = + fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, + (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, + best_uncurried_aliases), + extra))) = let - val effective_fact_filter = - fact_filter |> the_default best_fact_filter + val effective_fact_filter = fact_filter |> the_default best_fact_filter val facts = get_facts_of_filter effective_fact_filter factss val num_facts = Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge @@ -236,14 +225,8 @@ else () val readable_names = not (Config.get ctxt atp_full_names) - val lam_trans = - case lam_trans of - SOME s => s - | NONE => best_lam_trans - val uncurried_aliases = - case uncurried_aliases of - SOME b => b - | NONE => best_uncurried_aliases + val lam_trans = lam_trans |> the_default best_lam_trans + val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases val value as (atp_problem, _, fact_names, _, _) = if cache_key = SOME key then cache_value @@ -253,9 +236,8 @@ |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd prop_of) - |> prepare_atp_problem ctxt format prem_role type_enc atp_mode - lam_trans uncurried_aliases - readable_names true hyp_ts concl_t + |> prepare_atp_problem ctxt format prem_role type_enc atp_mode lam_trans + uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem @@ -288,11 +270,11 @@ NONE => (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof |> Option.map (sort string_ord) of - SOME facts => - let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in - if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure - end - | NONE => NONE) + SOME facts => + let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in + if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure + end + | NONE => NONE) | _ => outcome) in ((SOME key, value), (output, run_time, facts, atp_proof, outcome)) @@ -300,11 +282,8 @@ val timer = Timer.startRealTimer () - fun maybe_run_slice slice - (result as (cache, (_, run_time0, _, _, SOME _))) = - let - val time_left = Time.- (timeout, Timer.checkRealTimer timer) - in + fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _))) = + let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in if Time.<= (time_left, Time.zeroTime) then result else @@ -321,17 +300,17 @@ (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) - fun clean_up () = - if dest_dir = "" then (try File.rm prob_path; ()) else () + fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _)) = if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output + val ((_, (_, pool, fact_names, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome)) = with_cleanup clean_up run () |> tap export + val important_message = - if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 - then + if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else ""