--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
@@ -35,9 +35,11 @@
val supported_proversN = "supported_provers"
val kill_proversN = "kill_provers"
val running_proversN = "running_provers"
+val unlearnN = "unlearn"
+val learnN = "learn"
+val relearnN = "relearn"
val kill_learnersN = "kill_learners"
val running_learnersN = "running_learners"
-val unlearnN = "unlearn"
val refresh_tptpN = "refresh_tptp"
val auto = Unsynchronized.ref false
@@ -245,8 +247,7 @@
end)]
end
-val infinity_time_in_secs = 60 * 60 * 24 * 365
-val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
+val the_timeout = the_default infinite_timeout
fun extract_params mode default_params override_params =
let
@@ -383,12 +384,16 @@
kill_provers ()
else if subcommand = running_proversN then
running_provers ()
+ else if subcommand = unlearnN then
+ mash_unlearn ctxt
+ else if subcommand = learnN orelse subcommand = relearnN then
+ (if subcommand = relearnN then mash_unlearn ctxt else ();
+ mash_learn ctxt (get_params Normal ctxt
+ (("verbose", ["true"]) :: override_params)))
else if subcommand = kill_learnersN then
kill_learners ()
else if subcommand = running_learnersN then
running_learners ()
- else if subcommand = unlearnN then
- mash_unlearn ctxt
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
@@ -53,10 +53,11 @@
val mash_suggest_facts :
Proof.context -> params -> string -> int -> term list -> term
-> ('a * thm) list -> ('a * thm) list * ('a * thm) list
+ val mash_learn_proof :
+ Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
val mash_learn_thy :
Proof.context -> params -> theory -> Time.time -> fact list -> string
- val mash_learn_proof :
- Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
+ val mash_learn : Proof.context -> params -> unit
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
-> term -> fact list -> fact list
@@ -350,12 +351,12 @@
write_file write_access (in_dir ^ "/mash_accessibility");
write_file write_feats (in_dir ^ "/mash_features");
write_file write_deps (in_dir ^ "/mash_dependencies");
- run_mash ctxt overlord info true
+ run_mash ctxt overlord info false
("--init --inputDir " ^ in_dir ^
and_rm_files overlord " -r" [in_dir])
end
-fun run_mash_commands ctxt overlord async save max_suggs write_cmds read_suggs =
+fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
let
val info as (temp_dir, serial) = mash_info overlord
val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
@@ -363,7 +364,7 @@
in
write_file ([], K "") sugg_file;
write_file write_cmds cmd_file;
- run_mash ctxt overlord info async
+ run_mash ctxt overlord info false
("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
" --numberOfPredictions " ^ string_of_int max_suggs ^
(if save then " --saveModel" else "") ^
@@ -400,11 +401,11 @@
| mash_ADD ctxt overlord upds =
(trace_msg ctxt (fn () => "MaSh ADD " ^
elide_string 1000 (space_implode " " (map #1 upds)));
- run_mash_commands ctxt overlord true true 0 (upds, str_of_update) (K ()))
+ run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
(trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
- run_mash_commands ctxt overlord false false max_suggs
+ run_mash_commands ctxt overlord false max_suggs
([query], str_of_query)
(fn suggs => snd (extract_query (List.last (suggs ()))))
handle List.Empty => [])
@@ -548,6 +549,26 @@
val pass1_learn_timeout_factor = 0.5
+fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val prover = hd provers
+ val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
+ val feats = features_of ctxt prover thy General [t]
+ val deps = used_ths |> map nickname_of
+ in
+ mash_map ctxt (fn {thys, fact_graph} =>
+ let
+ val parents = parents_wrt_facts facts fact_graph
+ val upds = [(name, parents, feats, deps)]
+ val (upds, fact_graph) =
+ ([], fact_graph) |> fold (update_fact_graph ctxt) upds
+ in
+ mash_ADD ctxt overlord upds;
+ {thys = thys, fact_graph = fact_graph}
+ end)
+ end
+
(* Too many dependencies is a sign that a decision procedure is at work. There
isn't much too learn from such proofs. *)
val max_dependencies = 10
@@ -596,13 +617,12 @@
([], fact_graph) |> fold (update_fact_graph ctxt) upds
in
(mash_INIT_or_ADD ctxt overlord (rev upds);
- {thys = thys |> add_thys_for thy,
- fact_graph = fact_graph})
+ {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
end
in
mash_map ctxt trans;
if verbose then
- "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
+ "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
(if verbose then
" in " ^ string_from_time (Timer.checkRealTimer timer)
else
@@ -612,24 +632,16 @@
end
end
-fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
+fun mash_learn ctxt params =
let
val thy = Proof_Context.theory_of ctxt
- val prover = hd provers
- val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
- val feats = features_of ctxt prover thy General [t]
- val deps = used_ths |> map nickname_of
+ val _ = Output.urgent_message "MaShing..."
+ val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val facts = all_facts_of thy css_table
in
- mash_map ctxt (fn {thys, fact_graph} =>
- let
- val parents = parents_wrt_facts facts fact_graph
- val upds = [(name, parents, feats, deps)]
- val (upds, fact_graph) =
- ([], fact_graph) |> fold (update_fact_graph ctxt) upds
- in
- mash_ADD ctxt overlord upds;
- {thys = thys, fact_graph = fact_graph}
- end)
+ mash_learn_thy ctxt params thy infinite_timeout facts
+ |> (fn "" => "Learned nothing." | msg => msg)
+ |> Output.urgent_message
end
(* The threshold should be large enough so that MaSh doesn't kick in for Auto
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:46 2012 +0200
@@ -9,6 +9,7 @@
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
+ val infinite_timeout : Time.time
val time_mult : real -> Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -27,6 +28,8 @@
val serial_commas = Try.serial_commas
val simplify_spaces = strip_spaces false (K true)
+val infinite_timeout = seconds 31536000.0 (* one year *)
+
fun time_mult k t =
Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))