fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200
@@ -114,7 +114,7 @@
end
fun all_non_tautological_facts_of thy css_table =
- Sledgehammer_Fact.all_facts_of thy css_table
+ Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
|> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
@@ -39,7 +39,7 @@
val path = file_name |> Path.explode
val lines = path |> File.read_lines
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val all_names = all_names (facts |> map snd)
val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
--- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200
@@ -63,7 +63,7 @@
val _ = File.append path s
in [fact] end
val thy_map =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
|> thy_map_from_facts
fun do_thy facts =
@@ -79,7 +79,7 @@
val _ = File.write path ""
val css_table = clasimpset_rule_table_of ctxt
val facts =
- all_facts_of thy css_table
+ all_facts_of (Proof_Context.init_global thy) css_table
|> not include_thy ? filter_out (has_thy thy o snd)
fun do_fact ((_, stature), th) =
let
@@ -95,7 +95,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val ths =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
val all_names = all_names ths
@@ -114,7 +114,7 @@
val _ = File.write path ""
val prover = hd provers
val facts =
- all_facts_of thy Termtab.empty
+ all_facts_of (Proof_Context.init_global thy) Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
val all_names = all_names ths
@@ -132,7 +132,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -162,7 +162,7 @@
val _ = File.write path ""
val prover = hd provers
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
@@ -23,12 +23,13 @@
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
+ val backquote_thm : thm -> string
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
- val all_facts_of : theory -> status Termtab.table -> fact list
+ val all_facts_of : Proof.context -> status Termtab.table -> fact list
val nearly_all_facts :
Proof.context -> bool -> fact_override -> unit Symtab.table
-> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -212,9 +213,9 @@
is_that_fact thm
end
-fun hackish_string_for_term ctxt t =
+fun hackish_string_for_term thy t =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) (Syntax.string_of_term ctxt) t
+ (print_mode_value ())) (Syntax.string_of_term_global thy) t
|> String.translate (fn c => if Char.isPrint c then str c else "")
|> simplify_spaces
@@ -240,6 +241,11 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
+fun backquote_thm th =
+ th |> prop_of |> close_form
+ |> hackish_string_for_term (theory_of_thm th)
+ |> backquote
+
fun clasimpset_rule_table_of ctxt =
let
val thy = Proof_Context.theory_of ctxt
@@ -302,13 +308,14 @@
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
+ val thy = Proof_Context.theory_of ctxt
fun varify_noninducts (t as Free (s, T)) =
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
| varify_noninducts t = t
val p_inst =
concl_prop |> map_aterms varify_noninducts |> close_form
|> lambda (Free ind_x)
- |> hackish_string_for_term ctxt
+ |> hackish_string_for_term thy
in
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
@@ -374,8 +381,6 @@
else
let
val multi = length ths > 1
- val backquote_thm =
- backquote o hackish_string_for_term ctxt o close_form o prop_of
fun check_thms a =
case try (Proof_Context.get_thms ctxt) a of
NONE => false
@@ -392,7 +397,7 @@
val new =
(((fn () =>
if name0 = "" then
- th |> backquote_thm
+ backquote_thm th
else
[Facts.extern ctxt facts name0,
Name_Space.extern ctxt full_space name0]
@@ -415,11 +420,9 @@
|> op @
end
-fun all_facts_of thy css_table =
- let val ctxt = Proof_Context.init_global thy in
- all_facts ctxt false Symtab.empty [] [] css_table
- |> rev (* try to restore the original order of facts, for MaSh *)
- end
+fun all_facts_of ctxt css_table =
+ all_facts ctxt false Symtab.empty [] [] css_table
+ |> rev (* try to restore the original order of facts, for MaSh *)
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
hyp_ts concl_t =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
@@ -101,9 +101,10 @@
val relearn_atpN = "relearn_atp"
fun mash_home () = getenv "MASH_HOME"
-fun mash_state_dir () =
+fun mash_model_dir () =
getenv "ISABELLE_HOME_USER" ^ "/mash"
|> tap (Isabelle_System.mkdir o Path.explode)
+val mash_state_dir = mash_model_dir
fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
@@ -115,14 +116,14 @@
String.str c
else
(* fixed width, in case more digits follow *)
- "\\" ^ stringN_of_int 3 (Char.ord c)
+ "$" ^ stringN_of_int 3 (Char.ord c)
fun unmeta_chars accum [] = String.implode (rev accum)
- | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
+ | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
(case Int.fromString (String.implode [d1, d2, d3]) of
SOME n => unmeta_chars (Char.chr n :: accum) cs
| NONE => "" (* error *))
- | unmeta_chars _ (#"\\" :: _) = "" (* error *)
+ | unmeta_chars _ (#"$" :: _) = "" (* error *)
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
val escape_meta = String.translate meta_char
@@ -149,13 +150,16 @@
val local_prefix = "local" ^ Long_Name.separator
fun nickname_of th =
- let val hint = Thm.get_name_hint th in
- (* FIXME: There must be a better way to detect local facts. *)
- case try (unprefix local_prefix) hint of
- SOME suff =>
- parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
- | NONE => hint
- end
+ if Thm.has_name_hint th then
+ let val hint = Thm.get_name_hint th in
+ (* FIXME: There must be a better way to detect local facts. *)
+ case try (unprefix local_prefix) hint of
+ SOME suf =>
+ parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
+ | NONE => hint
+ end
+ else
+ backquote_thm th
fun suggested_facts suggs facts =
let
@@ -369,56 +373,47 @@
(*** Low-level communication with MaSh ***)
+(* more friendly than "try o File.rm" for those who keep the files open in their
+ text editor *)
+fun wipe_out file = File.write file ""
+
fun write_file (xs, f) file =
let val path = Path.explode file in
- File.write path "";
+ wipe_out path;
xs |> chunk_list 500
|> List.app (File.append path o space_implode "" o map f)
end
-fun mash_info overlord =
- if overlord then (getenv "ISABELLE_HOME_USER", "")
- else (getenv "ISABELLE_TMP", serial_string ())
-
-fun and_rm_files overlord flags files =
- if overlord then
- ""
- else
- " && rm -f" ^ flags ^ " -- " ^
- space_implode " " (map File.shell_quote files)
-
-fun run_mash ctxt overlord (temp_dir, serial) async core =
+fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
let
- val log_file = temp_dir ^ "/mash_log" ^ serial
+ val (temp_dir, serial) =
+ if overlord then (getenv "ISABELLE_HOME_USER", "")
+ else (getenv "ISABELLE_TMP", serial_string ())
+ val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
val err_file = temp_dir ^ "/mash_err" ^ serial
- val command =
- "(" ^ mash_home () ^ "/mash --quiet --outputDir " ^ mash_state_dir () ^
- " --log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^
- and_rm_files overlord "" [log_file, err_file] ^
- (if async then " &" else "")
- in
- trace_msg ctxt (fn () =>
- (if async then "Launching " else "Running ") ^ command);
- write_file ([], K "") log_file;
- write_file ([], K "") err_file;
- Isabelle_System.bash command;
- if not async then trace_msg ctxt (K "Done") else ()
- end
-
-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
val cmd_file = temp_dir ^ "/mash_commands" ^ serial
+ val core =
+ "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
+ " --numberOfPredictions " ^ string_of_int max_suggs ^
+ (if save then " --saveModel" else "")
+ val command =
+ mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
+ " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
in
write_file ([], K "") sugg_file;
write_file write_cmds cmd_file;
- run_mash ctxt overlord info false
- ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
- " --numberOfPredictions " ^ string_of_int max_suggs ^
- (if save then " --saveModel" else "") ^
- (and_rm_files overlord "" [sugg_file, cmd_file]));
- read_suggs (fn () => File.read_lines (Path.explode sugg_file))
+ trace_msg ctxt (fn () => "Running " ^ command);
+ Isabelle_System.bash command;
+ read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
+ |> tap (fn _ => trace_msg ctxt (fn () =>
+ case try File.read (Path.explode err_file) of
+ NONE => "Done"
+ | SOME "" => "Done"
+ | SOME s => "Error: " ^ elide_string 1000 s))
+ |> not overlord
+ ? tap (fn _ => List.app (wipe_out o Path.explode)
+ [err_file, sugg_file, cmd_file])
end
fun str_of_update (name, parents, feats, deps) =
@@ -429,24 +424,28 @@
"? " ^ escape_metas parents ^ "; " ^ escape_metas feats
fun mash_CLEAR ctxt =
- let val path = mash_state_dir () |> Path.explode in
+ let val path = mash_model_dir () |> Path.explode in
trace_msg ctxt (K "MaSh CLEAR");
- File.fold_dir (fn file => fn () =>
- File.rm (Path.append path (Path.basic file)))
- path ()
+ File.fold_dir (fn file => fn _ =>
+ try File.rm (Path.append path (Path.basic file)))
+ path NONE;
+ ()
end
fun mash_ADD _ _ [] = ()
| 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 0 (upds, str_of_update) (K ()))
+ run_mash_tool 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 max_suggs
+ run_mash_tool ctxt overlord false max_suggs
([query], str_of_query)
- (fn suggs => snd (extract_query (List.last (suggs ()))))
+ (fn suggs =>
+ case suggs () of
+ [] => []
+ | suggs => snd (extract_query (List.last suggs)))
handle List.Empty => [])
@@ -529,8 +528,7 @@
fun mash_unlearn ctxt =
Synchronized.change global_state (fn _ =>
- (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
- (true, empty_state)))
+ (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
end
@@ -642,16 +640,20 @@
|> sort (thm_ord o pairself snd)
val num_new_facts = length new_facts
in
- "MaShing" ^
(if not auto then
- " " ^ string_of_int num_new_facts ^ " fact" ^
- plural_s num_new_facts ^
- (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "")
+ "MaShing" ^
+ (if not auto then
+ " " ^ string_of_int num_new_facts ^ " fact" ^
+ plural_s num_new_facts ^
+ (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")"
+ else "")
+ else
+ "") ^ "..."
else
- "") ^ "..."
+ "")
|> Output.urgent_message;
if null new_facts then
- if verbose orelse not auto then
+ if not auto then
"Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
sendback relearn_atpN ^ " to learn from scratch."
else
@@ -694,6 +696,7 @@
(if atp then atp_dependencies_of ctxt params prover auto facts
else isar_dependencies_of) all_names th
|> trim_deps
+ val n = n |> not (null deps) ? Integer.add 1
val upds = (name, parents, feats, deps) :: upds
val (upds, next_commit) =
if Time.> (Timer.checkRealTimer timer, next_commit) then
@@ -702,7 +705,7 @@
(upds, next_commit)
val timed_out =
Time.> (Timer.checkRealTimer timer, learn_timeout)
- in (upds, ([name], n + 1, next_commit, timed_out)) end
+ in (upds, ([name], n, next_commit, timed_out)) end
val parents = parents_wrt_facts facts fact_graph
val (upds, (_, n, _, _)) =
([], (parents, 0, next_commit_time (), false))
@@ -710,7 +713,7 @@
in
commit true upds;
if verbose orelse not auto then
- "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
+ "Learned " ^ string_of_int n ^ " nontrivial proof" ^ plural_s n ^
(if verbose then
" in " ^ string_from_time (Timer.checkRealTimer timer)
else
@@ -722,9 +725,8 @@
fun mash_learn ctxt (params as {provers, ...}) atp =
let
- val thy = Proof_Context.theory_of ctxt
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of ctxt css_table
in
mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
|> Output.urgent_message
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
@@ -256,7 +256,7 @@
end
fun maybe_minimize ctxt mode do_learn name
- (params as {debug, verbose, isar_proof, minimize, ...})
+ (params as {verbose, isar_proof, minimize, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
message_tail} : prover_result) =
@@ -310,19 +310,8 @@
in
case used_facts of
SOME used_facts =>
- (if debug andalso not (null used_facts) then
- tag_list 1 facts
- |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
- |> filter_used_facts used_facts
- |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
- |> commas
- |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
- else
- ();
- {outcome = NONE, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail})
+ {outcome = NONE, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
| NONE => result
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200
@@ -84,12 +84,24 @@
? filter_out (curry (op =) Induction o snd o snd o fst
o untranslated_fact)
|> take num_facts}
+ fun print_used_facts used_facts =
+ tag_list 1 facts
+ |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
+ |> filter_used_facts used_facts
+ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+ |> commas
+ |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+ " proof (of " ^ string_of_int (length facts) ^ "): ") "."
+ |> Output.urgent_message
fun really_go () =
problem
|> get_minimizing_prover ctxt mode
(mash_learn_proof ctxt params name (prop_of goal)
(map untranslated_fact facts))
name params minimize_command
+ |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
+ print_used_facts used_facts
+ | _ => ())
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
@@ -228,7 +240,7 @@
hyp_ts concl_t
|> map (apfst (apfst (fn name => name ())))
|> tap (fn facts =>
- if debug then
+ if verbose then
label ^ plural_s (length provers) ^ ": " ^
(if null facts then
"Found no relevant facts."