--- 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;
--- 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"
--- 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,
--- 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
--- 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)
--- 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) =
--- 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
--- 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
--- 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;