# HG changeset patch # User blanchet # Date 1391437998 -3600 # Node ID 7bbbd9393ce0c444d367efd7574f2ff7ca4cd9ee # Parent e88ad20035f4bafa7ad75f54e83b85d756199e53 tuning diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 15:33:18 2014 +0100 @@ -33,6 +33,7 @@ open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact +open Sledgehammer_Reconstructor open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize @@ -49,13 +50,11 @@ NONE |> fold (fn candidate => fn accum as SOME _ => accum - | NONE => if member (op =) codes candidate then SOME candidate - else NONE) - ordered_outcome_codes + | NONE => if member (op =) codes candidate then SOME candidate else NONE) + ordered_outcome_codes |> the_default unknownN -fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i - n goal = +fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = (quote name, (if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts @@ -211,88 +210,91 @@ fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts." - else case factss of - [(_, facts)] => string_of_facts facts - | _ => - factss - |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) - |> space_implode "\n\n" + else + (case factss of + [(_, facts)] => string_of_facts facts + | _ => + factss + |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) + |> space_implode "\n\n") fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode output_result i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." - else case subgoal_count state of - 0 => + else + (case subgoal_count state of + 0 => ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state))) - | n => - let - val _ = Proof.assert_backward state - val print = - if mode = Normal andalso is_none output_result then Output.urgent_message else K () - val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug) - val ctxt = Proof.context_of state - val {facts = chained, goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt - val ho_atp = exists (is_ho_atp ctxt) provers - val reserved = reserved_isar_keyword_table () - val css = clasimpset_rule_table_of ctxt - val all_facts = - nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts - concl_t - val _ = () |> not blocking ? kill_provers - val _ = case find_first (not o is_prover_supported ctxt) provers of - SOME name => error ("No such prover: " ^ name ^ ".") - | NONE => () - val _ = print "Sledgehammering..." - val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) + | n => + let + val _ = Proof.assert_backward state + val print = + if mode = Normal andalso is_none output_result then Output.urgent_message else K () + val state = state |> Proof.map_context (silence_proof_methods debug) + val ctxt = Proof.context_of state + val {facts = chained, goal, ...} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt + val ho_atp = exists (is_ho_atp ctxt) provers + val reserved = reserved_isar_keyword_table () + val css = clasimpset_rule_table_of ctxt + val all_facts = + nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts + concl_t + val _ = () |> not blocking ? kill_provers + val _ = + (case find_first (not o is_prover_supported ctxt) provers of + SOME name => error ("No such prover: " ^ name ^ ".") + | NONE => ()) + val _ = print "Sledgehammering..." + val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) - val spying_str_of_factss = - commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) + val spying_str_of_factss = + commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) - fun get_factss provers = - let - val max_max_facts = - case max_facts of - SOME n => n - | NONE => - 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers - |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) - val _ = spying spy (fn () => (state, i, "All", - "Filtering " ^ string_of_int (length all_facts) ^ " facts")); - in - all_facts - |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t - |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) - |> spy ? tap (fn factss => spying spy (fn () => - (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) - end + fun get_factss provers = + let + val max_max_facts = + (case max_facts of + SOME n => n + | NONE => + 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers + |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) + val _ = spying spy (fn () => (state, i, "All", + "Filtering " ^ string_of_int (length all_facts) ^ " facts")); + in + all_facts + |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t + |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) + |> spy ? tap (fn factss => spying spy (fn () => + (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) + end - fun launch_provers state = - let - val factss = get_factss provers - val problem = - {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = factss} - val learn = mash_learn_proof ctxt params (prop_of goal) all_facts - val launch = launch_prover params mode output_result minimize_command only learn - in - if mode = Auto_Try then - (unknownN, state) - |> fold (fn prover => fn accum as (outcome_code, _) => - if outcome_code = someN then accum - else launch problem prover) - provers - else - provers - |> (if blocking then Par_List.map else map) (launch problem #> fst) - |> max_outcome_code |> rpair state - end - in - (if blocking then launch_provers state - else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) - handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) - end - |> `(fn (outcome_code, _) => outcome_code = someN) + fun launch_provers state = + let + val factss = get_factss provers + val problem = + {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, + factss = factss} + val learn = mash_learn_proof ctxt params (prop_of goal) all_facts + val launch = launch_prover params mode output_result minimize_command only learn + in + if mode = Auto_Try then + (unknownN, state) + |> fold (fn prover => fn accum as (outcome_code, _) => + if outcome_code = someN then accum + else launch problem prover) + provers + else + provers + |> (if blocking then Par_List.map else map) (launch problem #> fst) + |> max_outcome_code |> rpair state + end + in + (if blocking then launch_provers state + else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) + handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) + end + |> `(fn (outcome_code, _) => outcome_code = someN)) end; diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 15:33:18 2014 +0100 @@ -131,12 +131,12 @@ member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = - case space_explode " " s of + (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss - | _ => false + | _ => false) fun unalias_raw_param (name, value) = - case AList.lookup (op =) alias_params name of + (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then @@ -145,13 +145,14 @@ error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \ \(cf. " ^ quote name' ^ ").") | NONE => - case AList.lookup (op =) negated_alias_params name of - SOME name' => (name', case value of - ["false"] => ["true"] - | ["true"] => ["false"] - | [] => ["false"] - | _ => value) - | NONE => (name, value) + (case AList.lookup (op =) negated_alias_params name of + SOME name' => (name', + (case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value)) + | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" @@ -266,9 +267,10 @@ val type_enc = if mode = Auto_Try then NONE - else case lookup_string "type_enc" of - "smart" => NONE - | s => (type_enc_of_string Strict s; SOME s) + else + (case lookup_string "type_enc" of + "smart" => NONE + | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 15:33:18 2014 +0100 @@ -110,18 +110,18 @@ fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s | normT (TVar (z as (_, S))) = (fn ((knownT, nT), accum) => - case find_index (equal z) knownT of + (case find_index (equal z) knownT of ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) - | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))) + | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))) | normT (T as TFree _) = pair T fun norm (t $ u) = norm t ##>> norm u #>> op $ | norm (Const (s, T)) = normT T #>> curry Const s | norm (Var (z as (_, T))) = normT T #> (fn (T, (accumT, (known, n))) => - case find_index (equal z) known of + (case find_index (equal z) known of ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) - | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))) + | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) | norm (Bound j) = pair (Bound j) @@ -138,11 +138,11 @@ Induction else let val t = normalize_vars t in - case Termtab.lookup css t of + (case Termtab.lookup css t of SOME status => status | NONE => let val concl = Logic.strip_imp_concl t in - case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of + (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of SOME lrhss => let val prems = Logic.strip_imp_prems t @@ -150,8 +150,8 @@ in Termtab.lookup css t' |> the_default General end - | NONE => General - end + | NONE => General) + end) end end @@ -165,15 +165,14 @@ map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args |> implode fun nth_name j = - case xref of + (case xref of Facts.Fact s => backquote s ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => make_name reserved true - (nth (maps (explode_interval (length ths)) intervals) j) name ^ - bracket + (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) fun add_nth th (j, rest) = let val name = nth_name j in (j + 1, ((name, stature_of_thm false [] chained css name th), th) @@ -364,9 +363,9 @@ corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) fun un_class_ify s = - case first_field "_class" s of + (case first_field "_class" s of SOME (pref, suf) => [s, pref ^ suf] - | NONE => [s] + | NONE => [s]) fun build_name_tables name_of facts = let @@ -388,7 +387,7 @@ |> Net.entries fun struct_induct_rule_on th = - case Logic.strip_horn (prop_of th) of + (case Logic.strip_horn (prop_of th) of (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => if not (is_TVar ind_T) andalso length prems > 1 andalso @@ -397,7 +396,7 @@ SOME (p_name, ind_T) else NONE - | _ => NONE + | _ => NONE) val instantiate_induct_timeout = seconds 0.01 @@ -420,14 +419,15 @@ handle Type.TYPE_MATCH => false fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = - case struct_induct_rule_on th of + (case struct_induct_rule_on th of SOME (p_name, ind_T) => let val thy = Proof_Context.theory_of ctxt in - stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) - |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout - (instantiate_induct_rule ctxt stmt p_name ax))) + stmt_xs + |> filter (fn (_, T) => type_match thy (T, ind_T)) + |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout + (instantiate_induct_rule ctxt stmt p_name ax))) end - | NONE => [ax] + | NONE => [ax]) fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) @@ -482,9 +482,9 @@ val n = length ths val multi = n > 1 fun check_thms a = - case try (Proof_Context.get_thms ctxt) a of + (case try (Proof_Context.get_thms ctxt) a of NONE => false - | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') + | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) => (j - 1, diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:33:18 2014 +0100 @@ -284,9 +284,7 @@ |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically - val ctxt = ctxt - |> enrich_context_with_local_facts canonical_isar_proof - |> silence_proof_methods debug + val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 15:33:18 2014 +0100 @@ -41,12 +41,12 @@ post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd fun fold_map_atypes f T s = - case T of + (case T of Type (name, Ts) => - let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in - (Type (name, Ts), s) - end - | _ => f T s + let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in + (Type (name, Ts), s) + end + | _ => f T s) val indexname_ord = Term_Ord.fast_indexname_ord val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 15:33:18 2014 +0100 @@ -178,9 +178,9 @@ fun run_on () = (Isabelle_System.bash command |> tap (fn _ => - case try File.read (Path.explode err_file) |> the_default "" of + (case try File.read (Path.explode err_file) |> the_default "" of "" => trace_msg ctxt (K "Done") - | s => warning ("MaSh error: " ^ elide_string 1000 s)); + | s => warning ("MaSh error: " ^ elide_string 1000 s))); read_suggs (fn () => try File.read_lines sugg_path |> these)) fun clean_up () = if overlord then () @@ -243,17 +243,16 @@ (* The suggested weights don't make much sense. *) fun extract_suggestion sugg = - case space_explode "=" sugg of + (case space_explode "=" sugg of [name, _ (* weight *)] => SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *)) | [name] => SOME (unencode_str name (* , 1.0 *)) - | _ => NONE + | _ => NONE) fun extract_suggestions line = - case space_explode ":" line of - [goal, suggs] => - (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) - | _ => ("", []) + (case space_explode ":" line of + [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) + | _ => ("", [])) structure MaSh = struct @@ -294,11 +293,10 @@ fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); - run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) - (fn suggs => - case suggs () of - [] => [] - | suggs => snd (extract_suggestions (List.last suggs))) + run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs => + (case suggs () of + [] => [] + | suggs => snd (extract_suggestions (List.last suggs)))) handle List.Empty => []) end; @@ -362,48 +360,47 @@ exception FILE_VERSION_TOO_NEW of unit fun extract_node line = - case space_explode ":" line of + (case space_explode ":" line of [head, parents] => (case space_explode " " head of - [kind, name] => - SOME (unencode_str name, unencode_strs parents, - try proof_kind_of_str kind |> the_default Isar_Proof) - | _ => NONE) - | _ => NONE + [kind, name] => + SOME (unencode_str name, unencode_strs parents, + try proof_kind_of_str kind |> the_default Isar_Proof) + | _ => NONE) + | _ => NONE) fun load_state _ _ (state as (true, _)) = state | load_state ctxt overlord _ = let val path = mash_state_file () in (true, - case try File.read_lines path of + (case try File.read_lines path of SOME (version' :: node_lines) => let fun add_edge_to name parent = Graph.default_node (parent, Isar_Proof) #> Graph.add_edge (parent, name) fun add_node line = - case extract_node line of + (case extract_node line of NONE => I (* shouldn't happen *) | SOME (name, parents, kind) => - update_access_graph_node (name, kind) - #> fold (add_edge_to name) parents + update_access_graph_node (name, kind) #> fold (add_edge_to name) parents) val (access_G, num_known_facts) = - case string_ord (version', version) of + (case string_ord (version', version) of EQUAL => (try_graph ctxt "loading state" Graph.empty (fn () => - fold add_node node_lines Graph.empty), + fold add_node node_lines Graph.empty), length node_lines) | LESS => (* can't parse old file *) (MaSh.unlearn ctxt overlord; (Graph.empty, 0)) - | GREATER => raise FILE_VERSION_TOO_NEW () + | GREATER => raise FILE_VERSION_TOO_NEW ()) in trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")"); {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []} end - | _ => empty_state) + | _ => empty_state)) end fun save_state _ (state as {dirty = SOME [], ...}) = state @@ -415,10 +412,9 @@ fun append_entry (name, (kind, (parents, _))) = cons (name, Graph.Keys.dest parents, kind) val (banner, entries) = - case dirty of - SOME names => - (NONE, fold (append_entry o Graph.get_entry access_G) names []) - | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []) + (case dirty of + SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) + | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])) in write_file banner (entries, str_of_entry) (mash_state_file ()); trace_msg ctxt (fn () => @@ -471,11 +467,11 @@ if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* There must be a better way to detect local facts. *) - case try (unprefix local_prefix) hint of + (case try (unprefix local_prefix) hint of SOME suf => - thy_name_of_thm th ^ Long_Name.separator ^ suf ^ - Long_Name.separator ^ elided_backquote_thm 50 th - | NONE => hint + thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^ + elided_backquote_thm 50 th + | NONE => hint) end else elided_backquote_thm 200 th @@ -512,9 +508,9 @@ let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in - case find_index (curry fact_eq fact o fst) sels of + (case find_index (curry fact_eq fact o fst) sels of ~1 => if member fact_eq unks fact then NONE else SOME 0.0 - | rank => score_at rank + | rank => score_at rank) end fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] @@ -536,20 +532,21 @@ if Theory.eq_thy p then EQUAL else LESS else if Theory.subthy (swap p) then GREATER - else case int_ord (pairself (length o Theory.ancestors_of) p) of - EQUAL => string_ord (pairself Context.theory_name p) - | order => order + else + (case int_ord (pairself (length o Theory.ancestors_of) p) of + EQUAL => string_ord (pairself Context.theory_name p) + | order => order) fun crude_thm_ord p = - case crude_theory_ord (pairself theory_of_thm p) of + (case crude_theory_ord (pairself theory_of_thm p) of EQUAL => let val q = pairself nickname_of_thm p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) - case bool_ord (pairself (String.isSuffix "_def") (swap q)) of + (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q - | ord => ord + | ord => ord) end - | ord => ord + | ord => ord) val thm_less_eq = Theory.subthy o pairself theory_of_thm fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) @@ -724,7 +721,7 @@ add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t fun add_term Ts = add_term_pats Ts term_max_depth fun add_subterms Ts t = - case strip_comb t of + (case strip_comb t of (Const (s, T), args) => (not (is_widely_irrelevant_const s) ? add_term Ts t) #> add_subtypes T @@ -735,7 +732,7 @@ | Var (_, T) => add_subtypes T | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body | _ => I) - #> fold (add_subterms Ts) args + #> fold (add_subterms Ts) args) in [] |> fold (add_subterms []) ts end val term_max_depth = 2 @@ -805,7 +802,7 @@ fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = - case isar_dependencies_of name_tabs th of + (case isar_dependencies_of name_tabs th of [] => (false, []) | isar_deps => let @@ -819,9 +816,10 @@ fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum - else case find_first (is_dep dep) facts of - SOME ((_, status), th) => accum @ [(("", status), th)] - | NONE => accum (* shouldn't happen *) + else + (case find_first (is_dep dep) facts of + SOME ((_, status), th) => accum @ [(("", status), th)] + | NONE => accum (* shouldn't happen *)) val mepo_facts = facts |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE @@ -838,7 +836,7 @@ |> Output.urgent_message else (); - case run_prover_for_mash ctxt params prover name facts goal of + (case run_prover_for_mash ctxt params prover name facts goal of {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in @@ -849,8 +847,8 @@ else (); (true, map fst used_facts)) - | _ => (false, isar_deps) - end + | _ => (false, isar_deps)) + end) (*** High-level communication with MaSh ***) @@ -1140,9 +1138,9 @@ val access_G = access_G |> fold flop_wrt_access_graph flops val num_known_facts = num_known_facts + length learns val dirty = - case (was_empty, dirty, relearns) of + (case (was_empty, dirty, relearns) of (false, SOME names, []) => SOME (map #1 learns @ names) - | _ => NONE + | _ => NONE) in MaSh.learn ctxt overlord (save andalso null relearns) (rev learns); MaSh.relearn ctxt overlord save relearns; @@ -1202,9 +1200,9 @@ let val name = nickname_of_thm th val (n, relearns, flops) = - case deps_of status th of + (case deps_of status th of SOME deps => (n + 1, (name, deps) :: relearns, flops) - | NONE => (n, relearns, name :: flops) + | NONE => (n, relearns, name :: flops)) val (relearns, flops, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then (commit false [] relearns flops; @@ -1325,7 +1323,7 @@ in if length facts - num_known_facts <= max_facts_to_learn_before_query then - case length (filter_out is_in_access_G facts) of + (case length (filter_out is_in_access_G facts) of 0 => false | num_facts_to_learn => if num_facts_to_learn <= max_facts_to_learn_before_query then @@ -1333,21 +1331,21 @@ |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s)); true) else - (maybe_launch_thread (); false) + (maybe_launch_thread (); false)) else (maybe_launch_thread (); false) end else false val (save, effective_fact_filter) = - case fact_filter of + (case fact_filter of SOME ff => (ff <> mepoN andalso maybe_learn (), ff) | NONE => if is_mash_enabled () then (maybe_learn (), if mash_can_suggest_facts ctxt overlord then meshN else mepoN) else - (false, mepoN) + (false, mepoN)) val unique_facts = drop_duplicate_facts facts val add_ths = Attrib.eval_thms ctxt add @@ -1373,11 +1371,11 @@ val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take in if save then MaSh.save ctxt overlord else (); - case (fact_filter, mess) of + (case (fact_filter, mess) of (NONE, [(_, (mepo, _)), (_, (mash, _))]) => [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), (mashN, mash |> map fst |> add_and_take)] - | _ => [(effective_fact_filter, mesh)] + | _ => [(effective_fact_filter, mesh)]) end fun kill_learners ctxt ({overlord, ...} : params) = diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 15:33:18 2014 +0100 @@ -171,7 +171,7 @@ (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x)) #> fold (do_term false) ts and do_term ext_arg t = - case strip_comb t of + (case strip_comb t of (Const x, ts) => do_const true x ts | (Free x, ts) => do_const false x ts | (Abs (_, T, t'), ts) => @@ -182,11 +182,11 @@ ? add_pconst_to_table (pseudo_abs_name, PType (order_of_type T + 1, []))) #> fold (do_term false) (t' :: ts) - | (_, ts) => fold (do_term false) ts + | (_, ts) => fold (do_term false) ts) and do_term_or_formula ext_arg T = if T = HOLogic.boolT then do_formula else do_term ext_arg and do_formula t = - case t of + (case t of Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t' | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2 | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => @@ -212,7 +212,7 @@ do_formula (t1 $ Bound ~1) #> do_formula t' | (t0 as Const (_, @{typ bool})) $ t1 => do_term false t0 #> do_formula t1 (* theory constant *) - | _ => do_term false t + | _ => do_term false t) in do_formula end fun pconsts_in_fact thy t = @@ -233,17 +233,16 @@ theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) fun pair_consts_fact thy fudge fact = - case fact |> snd |> theory_const_prop_of fudge - |> pconsts_in_fact thy of + (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of [] => NONE - | consts => SOME ((fact, consts), NONE) + | consts => SOME ((fact, consts), NONE)) (* A two-dimensional symbol table counts frequencies of constants. It's keyed first by constant name and second by its list of type instantiations. For the latter, we need a linear ordering on "pattern list". *) fun patternT_ord p = - case p of + (case p of (Type (s, ps), Type (t, qs)) => (case fast_string_ord (s, t) of EQUAL => dict_ord patternT_ord (ps, qs) @@ -253,7 +252,7 @@ | (Type _, TVar _) => GREATER | (Type _, TFree _) => LESS | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t) - | (TFree _, _) => GREATER + | (TFree _, _) => GREATER) fun ptype_ord (PType (m, ps), PType (n, qs)) = (case dict_ord patternT_ord (ps, qs) of EQUAL => int_ord (m, n) @@ -269,11 +268,11 @@ |> Symtab.map_default (s, PType_Tab.empty) #> fold do_term ts and do_term t = - case strip_comb t of + (case strip_comb t of (Const x, ts) => do_const true x ts | (Free x, ts) => do_const false x ts | (Abs (_, _, t'), ts) => fold do_term (t' :: ts) - | (_, ts) => fold do_term ts + | (_, ts) => fold do_term ts) in do_term o theory_const_prop_of fudge o snd end fun pow_int _ 0 = 1.0 @@ -356,7 +355,7 @@ fun fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts = - case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab) + (case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab) ||> filter_out (pconst_hyper_mem swap rel_const_tab) of ([], _) => 0.0 | (rel, irrel) => @@ -373,7 +372,7 @@ o irrel_pconst_weight fudge const_tab chained_const_tab) irrel val res = rel_weight / (rel_weight + irrel_weight) - in if Real.isFinite res then res else 0.0 end + in if Real.isFinite res then res else 0.0 end) fun take_most_relevant ctxt max_facts remaining_max ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) @@ -411,15 +410,16 @@ let fun aux _ _ NONE = NONE | aux t args (SOME tab) = - case t of + (case t of t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 [] | Const (s, _) => (if is_widely_irrelevant_const s then SOME tab - else case Symtab.lookup tab s of - NONE => SOME (Symtab.update (s, length args) tab) - | SOME n => if n = length args then SOME tab else NONE) - | _ => SOME tab + else + (case Symtab.lookup tab s of + NONE => SOME (Symtab.update (s, length args) tab) + | SOME n => if n = length args then SOME tab else NONE)) + | _ => SOME tab) in aux (prop_of th) [] end (* FIXME: This is currently only useful for polymorphic type encodings. *) @@ -507,11 +507,10 @@ :: hopeful) = let val weight = - case cached_weight of + (case cached_weight of SOME w => w | NONE => - fact_weight fudge stature const_tab rel_const_tab - chained_const_tab fact_consts + fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts) in if weight >= thres then relevant ((ax, weight) :: candidates) rejects hopeful diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:33:18 2014 +0100 @@ -215,10 +215,8 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -(* 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 timed_proof_method meth timeout ths = + timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained @@ -248,9 +246,9 @@ () val timer = Timer.startRealTimer () in - case timed_proof_method meth debug timeout ths state i of + (case timed_proof_method meth timeout ths state i of SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) - | _ => play timed_out meths + | _ => play timed_out meths) end handle TimeLimit.TimeOut => play (meth :: timed_out) meths in diff -r e88ad20035f4 -r 7bbbd9393ce0 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:19:07 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:33:18 2014 +0100 @@ -38,7 +38,6 @@ 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_proof_methods : bool -> Proof.context -> Proof.context end;