1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Author: Cezary Kaliszyk, University of Innsbruck
5 Sledgehammer's machine-learning-based relevance filter (MaSh).
8 signature SLEDGEHAMMER_MASH =
10 type stature = ATP_Problem_Generate.stature
11 type raw_fact = Sledgehammer_Fact.raw_fact
12 type fact = Sledgehammer_Fact.fact
13 type fact_override = Sledgehammer_Fact.fact_override
14 type params = Sledgehammer_Prover.params
15 type prover_result = Sledgehammer_Prover.prover_result
17 val trace : bool Config.T
18 val duplicates : bool Config.T
26 val learn_isarN : string
27 val learn_proverN : string
28 val relearn_isarN : string
29 val relearn_proverN : string
30 val fact_filters : string list
31 val encode_str : string -> string
32 val encode_strs : string list -> string
33 val decode_str : string -> string
34 val decode_strs : string -> string list
35 val encode_features : (string * real) list -> string
36 val extract_suggestions : string -> string * (string * real) list
38 datatype mash_engine =
45 val is_mash_enabled : unit -> bool
46 val the_mash_engine : unit -> mash_engine
48 val mash_unlearn : Proof.context -> params -> unit
49 val nickname_of_thm : thm -> string
50 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
51 val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
52 val crude_thm_ord : thm * thm -> order
53 val thm_less : thm * thm -> bool
54 val goal_of_thm : theory -> thm -> thm
55 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
57 val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
59 val trim_dependencies : string list -> string list option
60 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
61 val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
62 string Symtab.table * string Symtab.table -> thm -> bool * string list
63 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
64 (string list * ('a * thm)) list
65 val num_extra_feature_facts : int
66 val extra_feature_factor : real
67 val weight_facts_smoothly : 'a list -> ('a * real) list
68 val weight_facts_steeply : 'a list -> ('a * real) list
69 val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
70 ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
71 val add_const_counts : term -> int Symtab.table -> int Symtab.table
72 val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
74 val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
75 val mash_learn_facts : Proof.context -> params -> string -> bool -> int -> bool -> Time.time ->
76 raw_fact list -> string
77 val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
79 val mash_can_suggest_facts : Proof.context -> bool -> bool
80 val generous_max_suggestions : int -> int
81 val mepo_weight : real
82 val mash_weight : real
83 val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
84 term -> raw_fact list -> (string * fact list) list
85 val kill_learners : Proof.context -> params -> unit
86 val running_learners : unit -> unit
89 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
93 open ATP_Problem_Generate
94 open Sledgehammer_Util
95 open Sledgehammer_Fact
96 open Sledgehammer_Prover
97 open Sledgehammer_Prover_Minimize
98 open Sledgehammer_MePo
100 val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
101 val duplicates = Attrib.setup_config_bool @{binding sledgehammer_fact_duplicates} (K false)
103 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
105 fun gen_eq_thm ctxt = if Config.get ctxt duplicates then Thm.eq_thm_strict else Thm.eq_thm_prop
115 val fact_filters = [meshN, mepoN, mashN]
117 val unlearnN = "unlearn"
118 val learn_isarN = "learn_isar"
119 val learn_proverN = "learn_prover"
120 val relearn_isarN = "relearn_isar"
121 val relearn_proverN = "relearn_prover"
123 val hintsN = ".hints"
125 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
127 type xtab = int * int Symtab.table
129 val empty_xtab = (0, Symtab.empty)
131 fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab)
132 fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key))
134 fun mash_state_dir () = Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
135 fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
137 fun wipe_out_mash_state_dir () =
138 let val path = mash_state_dir () in
139 try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path)
144 datatype mash_engine =
152 let val flag1 = Options.default_string @{system_option MaSh} in
153 (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
154 "yes" => SOME MaSh_SML_NB
155 | "py" => SOME MaSh_Py
156 | "sml" => SOME MaSh_SML_NB
157 | "sml_knn" => SOME MaSh_SML_kNN
158 | "sml_knn_cpp" => SOME MaSh_SML_kNN_Cpp
159 | "sml_nb" => SOME MaSh_SML_NB
160 | "sml_nb_cpp" => SOME MaSh_SML_NB_Cpp
164 val is_mash_enabled = is_some o mash_engine
165 val the_mash_engine = the_default MaSh_SML_NB o mash_engine
168 (*** Low-level communication with the Python version of MaSh ***)
170 val save_models_arg = "--saveModels"
171 val shutdown_server_arg = "--shutdownServer"
173 fun wipe_out_file file = ignore (try (File.rm o Path.explode) file)
175 fun write_file banner (xs, f) path =
176 (case banner of SOME s => File.write path s | NONE => ();
177 xs |> chunk_list 500 |> List.app (File.append path o implode o map f))
180 fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs =
182 val (temp_dir, serial) =
183 if overlord then (getenv "ISABELLE_HOME_USER", "")
184 else (getenv "ISABELLE_TMP", serial_string ())
185 val log_file = temp_dir ^ "/mash_log" ^ serial
186 val err_file = temp_dir ^ "/mash_err" ^ serial
187 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
188 val sugg_path = Path.explode sugg_file
189 val cmd_file = temp_dir ^ "/mash_commands" ^ serial
190 val cmd_path = Path.explode cmd_file
191 val model_dir = File.shell_path (mash_state_dir ())
194 "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
195 \PYTHONDONTWRITEBYTECODE=y ./mash.py\
198 \ --outputDir " ^ model_dir ^
199 " --modelFile=" ^ model_dir ^ "/model.pickle\
200 \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
201 \ --log " ^ log_file ^
202 " --inputFile " ^ cmd_file ^
203 " --predictions " ^ sugg_file ^
204 (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
205 (if background then " &" else "")
208 (Isabelle_System.bash command
210 (case try File.read (Path.explode err_file) |> the_default "" of
211 "" => trace_msg ctxt (K "Done")
212 | s => warning ("MaSh error: " ^ elide_string 1000 s)));
213 read_suggs (fn () => try File.read_lines sugg_path |> these))
216 if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
218 write_file (SOME "") ([], K "") sugg_path;
219 write_file (SOME "") write_cmds cmd_path;
220 trace_msg ctxt (fn () => "Running " ^ command);
221 with_cleanup clean_up run_on ()
225 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
229 (* fixed width, in case more digits follow *)
230 "%" ^ stringN_of_int 3 (Char.ord c)
232 fun unmeta_chars accum [] = String.implode (rev accum)
233 | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
234 (case Int.fromString (String.implode [d1, d2, d3]) of
235 SOME n => unmeta_chars (Char.chr n :: accum) cs
236 | NONE => "" (* error *))
237 | unmeta_chars _ (#"%" :: _) = "" (* error *)
238 | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
240 val encode_str = String.translate meta_char
241 val decode_str = String.explode #> unmeta_chars []
243 val encode_strs = map encode_str #> space_implode " "
244 val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
246 (* Avoid scientific notation *)
247 fun safe_str_of_real r =
248 if r < 0.00001 then "0.00001"
249 else if r >= 1000000.0 then "1000000"
250 else Markup.print_real r
252 fun encode_feature (names, weight) =
253 encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
255 val encode_features = map encode_feature #> space_implode " "
257 fun str_of_learn (name, parents, feats, deps) =
258 "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^
259 encode_strs deps ^ "\n"
261 fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
263 fun str_of_query max_suggs (learns, hints, parents, feats) =
264 implode (map str_of_learn learns) ^
265 "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
266 (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
268 (* The suggested weights do not make much sense. *)
269 fun extract_suggestion sugg =
270 (case space_explode "=" sugg of
271 [name, weight] => SOME (decode_str name, Real.fromString weight |> the_default 1.0)
272 | [name] => SOME (decode_str name, 1.0)
275 fun extract_suggestions line =
276 (case space_explode ":" line of
277 [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
283 fun shutdown ctxt overlord =
284 (trace_msg ctxt (K "MaSh_Py shutdown");
285 run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ()))
287 fun save ctxt overlord =
288 (trace_msg ctxt (K "MaSh_Py save");
289 run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ()))
291 fun unlearn ctxt overlord =
292 (trace_msg ctxt (K "MaSh_Py unlearn");
293 shutdown ctxt overlord;
294 wipe_out_mash_state_dir ())
296 fun learn _ _ _ [] = ()
297 | learn ctxt overlord save learns =
298 (trace_msg ctxt (fn () =>
299 "MaSh_Py learn {" ^ elide_string 1000 (space_implode " " (map #1 learns)) ^ "}");
300 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false (learns, str_of_learn)
303 fun relearn _ _ _ [] = ()
304 | relearn ctxt overlord save relearns =
305 (trace_msg ctxt (fn () => "MaSh_Py relearn " ^
306 elide_string 1000 (space_implode " " (map #1 relearns)));
307 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
308 (relearns, str_of_relearn) (K ()))
310 fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
311 (trace_msg ctxt (fn () => "MaSh_Py query " ^ encode_features feats);
312 run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
313 (case suggs () of [] => [] | suggs => snd (extract_suggestions (List.last suggs))))
314 handle List.Empty => [])
319 (*** Standard ML version of MaSh ***)
324 exception BOTTOM of int
326 fun heap cmp bnd al a =
329 let val i31 = i + i + i + 1 in
331 let val x = Unsynchronized.ref i31 in
332 if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
333 if cmp (Array.sub (a, !x), Array.sub (a, i31 + 2)) = LESS then x := i31 + 2 else ();
337 if i31 + 1 < l andalso cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS
338 then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
341 fun trickledown l i e =
342 let val j = maxson l i in
343 if cmp (Array.sub (a, j), e) = GREATER then
344 (Array.update (a, i, Array.sub (a, j)); trickledown l j e)
346 Array.update (a, i, e)
349 fun trickle l i e = trickledown l i e handle BOTTOM i => Array.update (a, i, e)
352 let val j = maxson l i in
353 Array.update (a, i, Array.sub (a, j));
357 fun bubble l i = bubbledown l i handle BOTTOM i => i
360 let val father = (i - 1) div 3 in
361 if cmp (Array.sub (a, father), e) = LESS then
362 (Array.update (a, i, Array.sub (a, father));
363 if father > 0 then trickleup father e else Array.update (a, 0, e))
365 Array.update (a, i, e)
368 fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1))
371 if i < Integer.max 2 (al - bnd) then
374 let val e = Array.sub (a, i) in
375 Array.update (a, i, Array.sub (a, 0));
376 trickleup (bubble i 0) e;
380 for (((al + 1) div 3) - 1);
383 let val e = Array.sub (a, 1) in
384 Array.update (a, 1, Array.sub (a, 0));
385 Array.update (a, 0, e)
391 val number_of_nearest_neighbors = 10 (* FUDGE *)
393 fun select_visible_facts big_number recommends =
395 let val (j, ov) = Array.sub (recommends, at) in
396 Array.update (recommends, at, (j, big_number + ov))
399 exception EXIT of unit
401 fun k_nearest_neighbors dffreq num_facts deps_vec get_sym_ths max_suggs visible_facts conj_feats =
403 val ln_afreq = Math.ln (Real.fromInt num_facts)
404 fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Array.sub (dffreq, feat)))
406 val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
408 fun inc_overlap j v =
409 let val ov = snd (Array.sub (overlaps_sqr, j)) in
410 Array.update (overlaps_sqr, j, (j, v + ov))
417 fun do_th j = if j < num_facts then inc_overlap j w2 else ()
419 List.app do_th (get_sym_ths s)
422 val _ = List.app do_feat conj_feats
423 val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
424 val no_recommends = Unsynchronized.ref 0
425 val recommends = Array.tabulate (num_facts, rpair 0.0)
426 val age = Unsynchronized.ref 500000000.0
428 fun inc_recommend j v =
429 let val ov = snd (Array.sub (recommends, j)) in
430 if ov <= 0.0 then (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
431 else (if ov < !age + 1000.0 then Array.update (recommends, j, (j, v + ov)) else ()) end
433 val k = Unsynchronized.ref 0
435 if k >= num_facts then
439 val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
440 val o1 = Math.sqrt o2
441 val _ = inc_recommend j o1
442 val ds = Vector.sub (deps_vec, j)
443 val l = Real.fromInt (length ds)
445 List.app (fn d => inc_recommend d (o1 / l)) ds
449 if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
453 if !no_recommends >= max_suggs then ()
454 else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
458 if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
462 select_visible_facts 1000000000.0 recommends visible_facts;
463 heap (Real.compare o pairself snd) max_suggs num_facts recommends;
464 ret [] (Integer.max 0 (num_facts - max_suggs))
467 val nb_def_prior_weight = 21 (* FUDGE *)
469 fun learn_facts tfreq sfreq dffreq num_facts depss featss =
471 fun learn_fact th feats deps =
473 fun add_th weight t =
475 val im = Array.sub (sfreq, t)
476 fun fold_fn s sf = Inttab.map_default (s, 0) (Integer.add weight) sf
478 map_array_at tfreq (Integer.add weight) t;
479 Array.update (sfreq, t, fold fold_fn feats im)
482 val add_sym = map_array_at dffreq (Integer.add 1)
484 add_th nb_def_prior_weight th;
485 List.app (add_th 1) deps;
486 List.app add_sym feats
490 if i = num_facts then ()
491 else (learn_fact i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1))
496 fun naive_bayes_query tfreq sfreq dffreq num_facts max_suggs visible_facts conj_feats =
498 val tau = 0.05 (* FUDGE *)
499 val pos_weight = 10.0 (* FUDGE *)
500 val def_val = ~15.0 (* FUDGE *)
502 val ln_afreq = Math.ln (Real.fromInt num_facts)
503 val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) (Array.vector dffreq)
505 fun tfidf feat = Vector.sub (idf, feat)
507 fun log_posterior i =
509 val tfreq = Real.fromInt (Array.sub (tfreq, i))
511 fun fold_feats f (res, sfh) =
512 (case Inttab.lookup sfh f of
514 (res + tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
516 | NONE => (res + tfidf f * def_val, sfh))
518 val (res, sfh) = fold fold_feats conj_feats (Math.ln tfreq, Array.sub (sfreq, i))
520 fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
522 val sum_of_weights = Inttab.fold fold_sfh sfh 0.0
524 res + tau * sum_of_weights
527 val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j)))
530 if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
532 select_visible_facts 100000.0 posterior visible_facts;
533 heap (Real.compare o pairself snd) max_suggs num_facts posterior;
534 ret (Integer.max 0 (num_facts - max_suggs)) []
538 fun naive_bayes_py ctxt overlord num_facts depss featss max_suggs conj_feats =
540 fun name_of_fact j = "f" ^ string_of_int j
541 fun fact_of_name s = the (Int.fromString (unprefix "f" s))
542 fun name_of_feature j = "F" ^ string_of_int j
543 fun parents_of j = if j = 0 then [] else [name_of_fact (j - 1)]
545 val learns = map (fn j => (name_of_fact j, parents_of j,
546 map name_of_feature (Vector.sub (featss, j)),
547 map name_of_fact (Vector.sub (depss, j)))) (0 upto num_facts - 1)
548 val parents' = parents_of num_facts
549 val conj_feats' = map (rpair 1.0 o name_of_feature) conj_feats
551 MaSh_Py.unlearn ctxt overlord;
552 OS.Process.sleep (seconds 2.0); (* hack *)
553 MaSh_Py.query ctxt overlord max_suggs (learns, [], parents', conj_feats')
554 |> map (apfst fact_of_name)
558 fun c_plus_plus_tool tool max_suggs learns cfeats =
560 val ser = string_of_int (serial ()) (* poor person's attempt at thread-safety *)
561 val ocs = TextIO.openOut ("adv_syms" ^ ser)
562 val ocd = TextIO.openOut ("adv_deps" ^ ser)
563 val ocq = TextIO.openOut ("adv_seq" ^ ser)
564 val occ = TextIO.openOut ("adv_conj" ^ ser)
566 fun os oc s = TextIO.output (oc, s)
570 | ol oc f sep (h :: t) = (f h; os oc sep; ol oc f sep t)
572 fun do_learn (name, feats, deps) =
573 (os ocs name; os ocs ":"; ol ocs (os ocs o quote) ", " feats; os ocs "\n";
574 os ocd name; os ocd ":"; ol ocd (os ocd) " " deps; os ocd "\n"; os ocq name; os ocq "\n")
579 "~/misc/" ^ tool ^ " adv_syms" ^ ser ^ " adv_deps" ^ ser ^ " " ^ string_of_int no ^
580 " adv_seq" ^ ser ^ " < adv_conj" ^ ser
582 fst (Isabelle_System.bash_output cmd)
584 |> filter_out (curry (op =) "")
587 (List.app do_learn learns; ol occ (os occ o quote) ", " cfeats;
588 TextIO.closeOut ocs; TextIO.closeOut ocd; TextIO.closeOut ocq; TextIO.closeOut occ;
592 val k_nearest_neighbors_cpp =
593 c_plus_plus_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
594 val naive_bayes_cpp = c_plus_plus_tool "predict/nbayes"
596 fun query ctxt engine (num_facts, fact_tab) (num_feats, feat_tab) visible_facts max_suggs learns0
598 if engine = MaSh_SML_kNN_Cpp then
599 k_nearest_neighbors_cpp max_suggs learns0 conj_feats
600 else if engine = MaSh_SML_NB_Cpp then
601 naive_bayes_cpp max_suggs learns0 conj_feats
604 val learn_ary = Array.array (num_facts, ("", [], []))
606 List.app (fn entry as (fact, _, _) =>
607 Array.update (learn_ary, the (Symtab.lookup fact_tab fact), entry))
609 val learns = Array.foldr (op ::) [] learn_ary
611 val facts = map #1 learns
612 val featss = map (map_filter (Symtab.lookup feat_tab) o #2) learns
613 val depss = map (map_filter (Symtab.lookup fact_tab) o #3) learns
615 val fact_vec = Vector.fromList facts
616 val feats_vec = Vector.fromList featss
617 val deps_vec = Vector.fromList depss
619 val tfreq = Array.array (num_facts, 0)
620 val sfreq = Array.array (num_facts, Inttab.empty)
621 val dffreq = Array.array (num_feats, 0)
623 val _ = learn_facts tfreq sfreq dffreq num_facts deps_vec feats_vec
625 val int_visible_facts = map_filter (Symtab.lookup fact_tab) visible_facts
626 val int_conj_feats = map_filter (Symtab.lookup feat_tab) conj_feats
628 trace_msg ctxt (fn () => "MaSh_SML query " ^ encode_strs conj_feats ^ " from {" ^
629 elide_string 1000 (space_implode " " (take num_facts facts)) ^ "}");
633 val facts_ary = Array.array (num_feats, [])
635 fold (fn feats => fn fact =>
636 (List.app (map_array_at facts_ary (cons fact)) feats; fact + 1))
638 val get_facts = curry Array.sub facts_ary
640 k_nearest_neighbors dffreq num_facts deps_vec get_facts max_suggs int_visible_facts
644 naive_bayes_query tfreq sfreq dffreq num_facts max_suggs int_visible_facts int_conj_feats)
645 |> map (curry Vector.sub fact_vec o fst)
651 (*** Middle-level communication with MaSh ***)
653 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
655 fun str_of_proof_kind Isar_Proof = "i"
656 | str_of_proof_kind Automatic_Proof = "a"
657 | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
659 fun proof_kind_of_str "a" = Automatic_Proof
660 | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
661 | proof_kind_of_str _ (* "i" *) = Isar_Proof
663 fun add_edge_to name parent =
664 Graph.default_node (parent, (Isar_Proof, [], []))
665 #> Graph.add_edge (parent, name)
667 fun add_node kind name parents feats deps (access_G, fact_xtab, feat_xtab) =
668 ((Graph.new_node (name, (kind, feats, deps)) access_G
669 handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
670 |> fold (add_edge_to name) parents,
671 maybe_add_to_xtab name fact_xtab,
672 fold maybe_add_to_xtab feats feat_xtab)
674 fun try_graph ctxt when def f =
677 Graph.CYCLES (cycle :: _) =>
678 (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
680 (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
681 | Graph.UNDEF name =>
682 (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
684 if Exn.is_interrupt exn then
687 (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
691 string_of_int (length (Graph.keys G)) ^ " node(s), " ^
692 string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^
693 string_of_int (length (Graph.maximals G)) ^ " maximal"
696 {access_G : (proof_kind * string list * string list) Graph.T,
699 num_known_facts : int, (* ### FIXME: kill *)
700 dirty_facts : string list option}
703 {access_G = Graph.empty,
704 fact_xtab = empty_xtab,
705 feat_xtab = empty_xtab,
707 dirty_facts = SOME []} : mash_state
709 val empty_graphxx = (Graph.empty, empty_xtab, empty_xtab)
713 val version = "*** MaSh version 20140625 ***"
715 exception FILE_VERSION_TOO_NEW of unit
717 fun extract_node line =
718 (case space_explode ":" line of
720 (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of
721 ([kind, name], [parents, feats, deps]) =>
722 SOME (proof_kind_of_str kind, decode_str name, decode_strs parents, decode_strs feats,
727 fun load_state ctxt overlord (time_state as (memory_time, _)) =
728 let val path = mash_state_file () in
729 (case try OS.FileSys.modTime (Path.implode (Path.expand path)) of
732 if Time.>= (memory_time, disk_time) then
736 (case try File.read_lines path of
737 SOME (version' :: node_lines) =>
739 fun extract_line_and_add_node line =
740 (case extract_node line of
741 NONE => I (* should not happen *)
742 | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps)
744 val ((access_G, fact_xtab, feat_xtab), num_known_facts) =
745 (case string_ord (version', version) of
747 (try_graph ctxt "loading state" empty_graphxx (fn () =>
748 fold extract_line_and_add_node node_lines empty_graphxx),
751 (* cannot parse old file *)
752 (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
753 else wipe_out_mash_state_dir ();
755 | GREATER => raise FILE_VERSION_TOO_NEW ())
757 trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
758 {access_G = access_G, fact_xtab = fact_xtab, feat_xtab = feat_xtab,
759 num_known_facts = num_known_facts, dirty_facts = SOME []}
761 | _ => empty_state)))
764 fun str_of_entry (kind, name, parents, feats, deps) =
765 str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
766 encode_strs feats ^ "; " ^ encode_strs deps ^ "\n"
768 fun save_state _ (time_state as (_, {dirty_facts = SOME [], ...})) = time_state
769 | save_state ctxt (memory_time, {access_G, fact_xtab, feat_xtab, num_known_facts, dirty_facts}) =
771 fun append_entry (name, ((kind, feats, deps), (parents, _))) =
772 cons (kind, name, Graph.Keys.dest parents, feats, deps)
774 val path = mash_state_file ()
776 (case try OS.FileSys.modTime (Path.implode path) of
778 | SOME disk_time => if Time.< (disk_time, memory_time) then dirty_facts else NONE)
779 val (banner, entries) =
780 (case dirty_facts' of
781 SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
782 | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
784 write_file banner (entries, str_of_entry) path;
785 trace_msg ctxt (fn () =>
786 "Saved fact graph (" ^ graph_info access_G ^
788 SOME dirty_facts => "; " ^ string_of_int (length dirty_facts) ^ " dirty fact(s)"
791 {access_G = access_G, fact_xtab = fact_xtab, feat_xtab = feat_xtab,
792 num_known_facts = num_known_facts, dirty_facts = SOME []})
795 val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
799 fun map_state ctxt overlord f =
800 Synchronized.change global_state (load_state ctxt overlord ##> f #> save_state ctxt)
801 handle FILE_VERSION_TOO_NEW () => ()
803 fun peek_state ctxt overlord f =
804 Synchronized.change_result global_state (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
806 fun clear_state ctxt overlord =
807 (* "MaSh_Py.unlearn" also removes the state file *)
808 Synchronized.change global_state (fn _ =>
809 (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
810 else wipe_out_mash_state_dir ();
811 (Time.zeroTime, empty_state)))
815 fun mash_unlearn ctxt ({overlord, ...} : params) =
816 (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
819 (*** Isabelle helpers ***)
821 val local_prefix = "local" ^ Long_Name.separator
823 fun elided_backquote_thm threshold th =
824 elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
826 val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm
828 fun nickname_of_thm th =
829 if Thm.has_name_hint th then
830 let val hint = Thm.get_name_hint th in
831 (* There must be a better way to detect local facts. *)
832 (case try (unprefix local_prefix) hint of
834 thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
835 elided_backquote_thm 50 th
839 elided_backquote_thm 200 th
841 fun find_suggested_facts ctxt facts =
843 fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
844 val tab = fold add facts Symtab.empty
846 Symtab.lookup tab nick
847 |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
848 in map_filter lookup end
850 fun scaled_avg [] = 0
851 | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
854 | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
856 fun normalize_scores _ [] = []
857 | normalize_scores max_facts xs =
858 map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
860 fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
861 distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
862 | mesh_facts fact_eq max_facts mess =
864 val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
866 fun score_in fact (global_weight, (sels, unks)) =
867 let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
868 (case find_index (curry fact_eq fact o fst) sels of
869 ~1 => if member fact_eq unks fact then NONE else SOME 0.0
870 | rank => score_at rank)
873 fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
875 fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
876 |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
877 |> map snd |> take max_facts
880 val default_weight = 1.0
881 fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
882 fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
883 fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
884 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
885 val local_feature = ("local", 16.0 (* FUDGE *))
887 fun crude_theory_ord p =
888 if Theory.subthy p then
889 if Theory.eq_thy p then EQUAL else LESS
890 else if Theory.subthy (swap p) then
893 (case int_ord (pairself (length o Theory.ancestors_of) p) of
894 EQUAL => string_ord (pairself Context.theory_name p)
897 fun crude_thm_ord p =
898 (case crude_theory_ord (pairself theory_of_thm p) of
900 (* The hack below is necessary because of odd dependencies that are not reflected in the theory
902 let val q = pairself nickname_of_thm p in
903 (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
904 (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
905 EQUAL => string_ord q
910 val thm_less_eq = Theory.subthy o pairself theory_of_thm
911 fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
913 val freezeT = Type.legacy_freeze_type
915 fun freeze (t $ u) = freeze t $ freeze u
916 | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
917 | freeze (Var ((s, _), T)) = Free (s, freezeT T)
918 | freeze (Const (s, T)) = Const (s, freezeT T)
919 | freeze (Free (s, T)) = Free (s, freezeT T)
922 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
924 fun run_prover_for_mash ctxt params prover goal_name facts goal =
927 {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
928 subgoal_count = 1, factss = [("", facts)]}
930 get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem
933 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
935 val pat_tvar_prefix = "_"
936 val pat_var_prefix = "_"
938 (* try "Long_Name.base_name" for shorter names *)
939 fun massage_long_name s = s
941 val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
943 fun crude_str_of_typ (Type (s, [])) = massage_long_name s
944 | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts)
945 | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
946 | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
948 fun maybe_singleton_str _ "" = []
949 | maybe_singleton_str pref s = [pref ^ s]
951 val max_pat_breadth = 10 (* FUDGE *)
953 fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
955 val thy = Proof_Context.theory_of ctxt
957 val fixes = map snd (Variable.dest_fixes ctxt)
958 val classes = Sign.classes_of thy
960 fun add_classes @{sort type} = I
962 fold (`(Sorts.super_classes classes)
964 #> subtract (op =) @{sort type} #> map massage_long_name
965 #> map class_feature_of
966 #> union (eq_fst (op =))) S
968 fun pattify_type 0 _ = []
969 | pattify_type _ (Type (s, [])) =
970 if member (op =) bad_types s then [] else [massage_long_name s]
971 | pattify_type depth (Type (s, U :: Ts)) =
974 val ps = take max_pat_breadth (pattify_type depth T)
975 val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U)
977 map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
979 | pattify_type _ (TFree (_, S)) =
980 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
981 | pattify_type _ (TVar (_, S)) =
982 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
984 fun add_type_pat depth T =
985 union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
987 fun add_type_pats 0 _ = I
988 | add_type_pats depth t =
989 add_type_pat depth t #> add_type_pats (depth - 1) t
992 add_type_pats type_max_depth T
993 #> fold_atyps_sorts (add_classes o snd) T
995 fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
996 | add_subtypes T = add_type T
998 val base_weight_of_const = 16.0 (* FUDGE *)
999 val weight_of_const =
1000 (if num_facts = 0 orelse Symtab.is_empty const_tab then
1001 K base_weight_of_const
1004 let val count = Symtab.lookup const_tab s |> the_default 1 in
1005 base_weight_of_const + Real.fromInt num_facts / Real.fromInt count
1008 fun pattify_term _ 0 _ = []
1009 | pattify_term _ _ (Const (s, _)) =
1010 if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
1011 | pattify_term _ _ (Free (s, T)) =
1012 maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
1014 |> (if member (op =) fixes s then
1015 cons (free_feature_of (massage_long_name
1016 (thy_name ^ Long_Name.separator ^ s)))
1019 | pattify_term _ _ (Var (_, T)) =
1020 maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
1021 | pattify_term Ts _ (Bound j) =
1022 maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
1023 |> map (rpair default_weight)
1024 | pattify_term Ts depth (t $ u) =
1026 val ps = take max_pat_breadth (pattify_term Ts depth t)
1027 val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
1029 map_product (fn ppw as (p, pw) =>
1031 | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
1033 | pattify_term _ _ _ = []
1035 fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
1037 fun add_term_pats _ 0 _ = I
1038 | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
1040 fun add_term Ts = add_term_pats Ts term_max_depth
1042 fun add_subterms Ts t =
1043 (case strip_comb t of
1044 (Const (s, T), args) =>
1045 (not (is_widely_irrelevant_const s) ? add_term Ts t)
1047 #> fold (add_subterms Ts) args
1050 Free (_, T) => add_term Ts t #> add_subtypes T
1051 | Var (_, T) => add_subtypes T
1052 | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body
1054 #> fold (add_subterms Ts) args)
1056 fold (add_subterms []) ts []
1059 val term_max_depth = 2
1060 val type_max_depth = 1
1062 (* TODO: Generate type classes for types? *)
1063 fun features_of ctxt thy num_facts const_tab (scope, _) ts =
1064 let val thy_name = Context.theory_name thy in
1065 thy_feature_of thy_name ::
1066 term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
1067 |> scope <> Global ? cons local_feature
1070 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
1071 from such proofs. *)
1072 val max_dependencies = 20
1074 val prover_default_max_facts = 25
1076 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
1077 val typedef_dep = nickname_of_thm @{thm CollectI}
1078 (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to
1079 "someI_ex" (and to some internal constructions). *)
1080 val class_some_dep = nickname_of_thm @{thm someI_ex}
1083 @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value}
1084 |> map nickname_of_thm
1086 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
1088 @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep
1089 type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases
1090 type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct
1091 type_definition.Rep_range type_definition.Abs_image}
1092 |> map nickname_of_thm
1094 fun is_size_def [dep] th =
1095 (case first_field ".rec" dep of
1097 (case first_field ".size" (nickname_of_thm th) of
1098 SOME (pref', _) => pref = pref'
1101 | is_size_def _ _ = false
1103 fun trim_dependencies deps =
1104 if length deps > max_dependencies then NONE else SOME deps
1106 fun isar_dependencies_of name_tabs th =
1107 thms_in_proof max_dependencies (SOME name_tabs) th
1108 |> Option.map (fn deps =>
1109 if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
1110 exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
1111 is_size_def deps th then
1116 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
1118 (case isar_dependencies_of name_tabs th of
1119 SOME [] => (false, [])
1122 val isar_deps = these isar_deps0
1123 val thy = Proof_Context.theory_of ctxt
1124 val goal = goal_of_thm thy th
1125 val name = nickname_of_thm th
1126 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
1127 val facts = facts |> filter (fn (_, th') => thm_less (th', th))
1129 fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
1131 fun is_dep dep (_, th) = nickname_of_thm th = dep
1133 fun add_isar_dep facts dep accum =
1134 if exists (is_dep dep) accum then
1137 (case find_first (is_dep dep) facts of
1138 SOME ((_, status), th) => accum @ [(("", status), th)]
1139 | NONE => accum (* should not happen *))
1143 |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
1147 |> fold (add_isar_dep facts) isar_deps
1149 val num_isar_deps = length isar_deps
1151 if verbose andalso auto_level = 0 then
1152 Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
1153 string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
1157 (case run_prover_for_mash ctxt params prover name facts goal of
1158 {outcome = NONE, used_facts, ...} =>
1159 (if verbose andalso auto_level = 0 then
1160 let val num_facts = length used_facts in
1161 Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
1162 plural_s num_facts ^ ".")
1166 (true, map fst used_facts))
1167 | _ => (false, isar_deps))
1171 (*** High-level communication with MaSh ***)
1173 (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
1175 fun chunks_and_parents_for chunks th =
1177 fun insert_parent new parents =
1178 let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in
1179 parents |> forall (fn p => not (thm_less_eq (new, p))) parents ? cons new
1182 fun rechunk seen (rest as th' :: ths) =
1183 if thm_less_eq (th', th) then (rev seen, rest)
1184 else rechunk (th' :: seen) ths
1186 fun do_chunk [] accum = accum
1187 | do_chunk (chunk as hd_chunk :: _) (chunks, parents) =
1188 if thm_less_eq (hd_chunk, th) then
1189 (chunk :: chunks, insert_parent hd_chunk parents)
1190 else if thm_less_eq (List.last chunk, th) then
1191 let val (front, back as hd_back :: _) = rechunk [] chunk in
1192 (front :: back :: chunks, insert_parent hd_back parents)
1195 (chunk :: chunks, parents)
1197 fold_rev do_chunk chunks ([], [])
1199 ||> map nickname_of_thm
1202 fun attach_parents_to_facts _ [] = []
1203 | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
1205 fun do_facts _ [] = []
1206 | do_facts (_, parents) [fact] = [(parents, fact)]
1207 | do_facts (chunks, parents)
1208 ((fact as (_, th)) :: (facts as (_, th') :: _)) =
1210 val chunks = app_hd (cons th) chunks
1211 val chunks_and_parents' =
1212 if thm_less_eq (th, th') andalso thy_name_of_thm th = thy_name_of_thm th' then
1213 (chunks, [nickname_of_thm th])
1215 chunks_and_parents_for chunks th'
1217 (parents, fact) :: do_facts chunks_and_parents' facts
1221 |> do_facts (chunks_and_parents_for [[]] th)
1222 |> drop (length old_facts)
1225 fun maximal_wrt_graph G keys =
1227 val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
1229 fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name
1231 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
1233 fun find_maxes _ (maxs, []) = map snd maxs
1234 | find_maxes seen (maxs, new :: news) =
1235 find_maxes (seen |> num_keys (Graph.imm_succs G new) > 1 ? Symtab.default (new, ()))
1236 (if Symtab.defined tab new then
1238 val newp = Graph.all_preds G [new]
1239 fun is_ancestor x yp = member (op =) yp x
1240 val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp))
1242 if exists (is_ancestor new o fst) maxs then (maxs, news)
1243 else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news)
1246 (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news))
1248 find_maxes Symtab.empty ([], Graph.maximals G)
1251 fun maximal_wrt_access_graph access_G facts =
1252 map (nickname_of_thm o snd) facts
1253 |> maximal_wrt_graph access_G
1255 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
1257 val chained_feature_factor = 0.5 (* FUDGE *)
1258 val extra_feature_factor = 0.1 (* FUDGE *)
1259 val num_extra_feature_facts = 0 (* FUDGE *) (* TODO: keep or eliminate? *)
1262 fun weight_of_proximity_fact rank =
1263 Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
1265 fun weight_facts_smoothly facts =
1266 facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
1269 fun steep_weight_of_fact rank =
1270 Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
1272 fun weight_facts_steeply facts =
1273 facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
1275 val max_proximity_facts = 100
1277 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
1279 val inter_fact = inter (eq_snd Thm.eq_thm_prop)
1280 val raw_mash = find_suggested_facts ctxt facts suggs
1281 val proximate = take max_proximity_facts facts
1282 val unknown_chained = inter_fact raw_unknown chained
1283 val unknown_proximate = inter_fact raw_unknown proximate
1285 [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
1286 (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
1287 (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
1288 val unknown = raw_unknown
1289 |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
1291 (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
1294 fun add_const_counts t =
1295 fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t [])
1297 fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts =
1299 val thy = Proof_Context.theory_of ctxt
1300 val thy_name = Context.theory_name thy
1301 val engine = the_mash_engine ()
1303 val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
1304 val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
1305 val num_facts = length facts
1307 (* Weights appear to hurt kNN more than they help. *)
1308 val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN
1309 ? fold (add_const_counts o prop_of o snd) facts
1311 fun fact_has_right_theory (_, th) =
1312 thy_name = Context.theory_name (theory_of_thm th)
1314 fun chained_or_extra_features_of factor (((_, stature), th), weight) =
1316 |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
1317 |> map (apsnd (fn r => weight * factor * r))
1319 fun query_args access_G =
1321 val parents = maximal_wrt_access_graph access_G facts
1323 |> filter (is_fact_in_graph access_G o snd)
1324 |> map (nickname_of_thm o snd)
1327 features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
1328 val chained_feats = chained
1330 |> map (chained_or_extra_features_of chained_feature_factor)
1331 |> rpair [] |-> fold (union (eq_fst (op =)))
1334 |> take (Int.max (0, num_extra_feature_facts - length chained))
1335 |> filter fact_has_right_theory
1336 |> weight_facts_steeply
1337 |> map (chained_or_extra_features_of extra_feature_factor)
1338 |> rpair [] |-> fold (union (eq_fst (op =)))
1339 val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
1340 |> debug ? sort (Real.compare o swap o pairself snd)
1342 (parents, hints, feats)
1345 val ((access_G, fact_xtab, feat_xtab), py_suggs) =
1346 peek_state ctxt overlord (fn {access_G, fact_xtab, feat_xtab, ...} =>
1347 ((access_G, fact_xtab, feat_xtab),
1348 if Graph.is_empty access_G then
1349 (trace_msg ctxt (K "Nothing has been learned yet"); [])
1350 else if engine = MaSh_Py then
1351 let val (parents, hints, feats) = query_args access_G in
1352 MaSh_Py.query ctxt overlord max_facts ([], hints, parents, feats)
1359 if engine = MaSh_Py then
1363 val (parents, hints, feats0) = query_args access_G
1364 val feats = map fst feats0
1365 val visible_facts = Graph.all_preds access_G parents
1367 (if null hints then [] else [(hintsN, feats, hints)]) @ (* ### FIXME *)
1368 Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
1370 MaSh_SML.query ctxt engine fact_xtab feat_xtab visible_facts max_facts learns feats
1373 val unknown = filter_out (is_fact_in_graph access_G o snd) facts
1375 find_mash_suggestions ctxt max_facts (py_suggs @ sml_suggs) facts chained unknown
1376 |> pairself (map fact_of_raw_fact)
1379 fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
1380 (learns, (access_G, fact_xtab, feat_xtab)) =
1382 fun maybe_learn_from from (accum as (parents, access_G)) =
1383 try_graph ctxt "updating graph" accum (fn () =>
1384 (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
1386 val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps))
1387 val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
1388 val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
1390 val fact_xtab = maybe_add_to_xtab name fact_xtab
1391 val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
1393 ((name, parents, feats, deps) :: learns, (access_G, fact_xtab, feat_xtab))
1396 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, access_G) =
1398 fun maybe_relearn_from from (accum as (parents, access_G)) =
1399 try_graph ctxt "updating graph" accum (fn () =>
1400 (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
1402 access_G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
1403 val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps
1405 ((name, deps) :: relearns, access_G)
1408 fun flop_wrt_access_graph name =
1409 Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
1411 val learn_timeout_slack = 20.0
1413 fun launch_thread timeout task =
1415 val hard_timeout = time_mult learn_timeout_slack timeout
1416 val birth_time = Time.now ()
1417 val death_time = Time.+ (birth_time, hard_timeout)
1418 val desc = ("Machine learner for Sledgehammer", "")
1420 Async_Manager.thread MaShN birth_time death_time desc task
1423 fun learned_proof_name () =
1424 Date.fmt ".%Y%m%d.%H%M%S." (Date.fromTimeLocal (Time.now ())) ^ serial_string ()
1426 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
1427 if is_mash_enabled () then
1428 launch_thread timeout (fn () =>
1430 val thy = Proof_Context.theory_of ctxt
1431 val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t])
1433 map_state ctxt overlord
1434 (fn state as {access_G, fact_xtab, feat_xtab, num_known_facts, dirty_facts} =>
1436 val parents = maximal_wrt_access_graph access_G facts
1438 |> filter (is_fact_in_graph access_G)
1439 |> map nickname_of_thm
1441 if the_mash_engine () = MaSh_Py then
1442 (MaSh_Py.learn ctxt overlord true [("", parents, feats, deps)]; state)
1445 val name = learned_proof_name ()
1446 val (access_G, fact_xtab, feat_xtab) =
1447 add_node Automatic_Proof name parents feats deps
1448 (access_G, fact_xtab, feat_xtab)
1450 {access_G = access_G, fact_xtab = fact_xtab, feat_xtab = feat_xtab,
1451 num_known_facts = num_known_facts + 1,
1452 dirty_facts = Option.map (cons name) dirty_facts}
1460 fun sendback sub = Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
1462 val commit_timeout = seconds 30.0
1464 (* The timeout is understood in a very relaxed fashion. *)
1465 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level
1466 run_prover learn_timeout facts =
1468 val timer = Timer.startRealTimer ()
1469 fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
1471 val engine = the_mash_engine ()
1472 val {access_G, ...} = peek_state ctxt overlord I
1473 val is_in_access_G = is_fact_in_graph access_G o snd
1474 val no_new_facts = forall is_in_access_G facts
1476 if no_new_facts andalso not run_prover then
1477 if auto_level < 2 then
1478 "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
1479 (if auto_level = 0 andalso not run_prover then
1480 "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
1487 val name_tabs = build_name_tables nickname_of_thm facts
1489 fun deps_of status th =
1490 if status = Non_Rec_Def orelse status = Rec_Def then
1492 else if run_prover then
1493 prover_dependencies_of ctxt params prover auto_level facts name_tabs th
1494 |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
1496 isar_dependencies_of name_tabs th
1498 fun do_commit [] [] [] state = state
1499 | do_commit learns relearns flops
1500 {access_G, fact_xtab, feat_xtab, num_known_facts, dirty_facts} =
1502 val (learns, (access_G, fact_xtab, feat_xtab)) =
1503 fold (learn_wrt_access_graph ctxt) learns ([], (access_G, fact_xtab, feat_xtab))
1504 val (relearns, access_G) =
1505 fold (relearn_wrt_access_graph ctxt) relearns ([], access_G)
1507 val was_empty = Graph.is_empty access_G
1508 val access_G = access_G |> fold flop_wrt_access_graph flops
1509 val num_known_facts = num_known_facts + length learns
1511 (case (was_empty, dirty_facts) of
1512 (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
1515 if engine = MaSh_Py then
1516 (MaSh_Py.learn ctxt overlord (save andalso null relearns) (rev learns);
1517 MaSh_Py.relearn ctxt overlord save relearns)
1520 {access_G = access_G, fact_xtab = fact_xtab, feat_xtab = feat_xtab,
1521 num_known_facts = num_known_facts, dirty_facts = dirty_facts}
1524 fun commit last learns relearns flops =
1525 (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
1526 map_state ctxt overlord (do_commit (rev learns) relearns flops);
1527 if not last andalso auto_level = 0 then
1528 let val num_proofs = length learns + length relearns in
1529 Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
1530 (if run_prover then "automatic" else "Isar") ^ " proof" ^
1531 plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
1536 fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
1537 | learn_new_fact (parents, ((_, stature as (_, status)), th))
1538 (learns, (n, next_commit, _)) =
1540 val name = nickname_of_thm th
1542 map fst (features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th])
1543 val deps = deps_of status th |> these
1544 val n = n |> not (null deps) ? Integer.add 1
1545 val learns = (name, parents, feats, deps) :: learns
1546 val (learns, next_commit) =
1547 if Time.> (Timer.checkRealTimer timer, next_commit) then
1548 (commit false learns [] []; ([], next_commit_time ()))
1550 (learns, next_commit)
1551 val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
1553 (learns, (n, next_commit, timed_out))
1557 if no_new_facts then
1561 val new_facts = facts
1562 |> sort (crude_thm_ord o pairself snd)
1563 |> attach_parents_to_facts []
1564 |> filter_out (is_in_access_G o snd)
1565 val (learns, (n, _, _)) =
1566 ([], (0, next_commit_time (), false))
1567 |> fold learn_new_fact new_facts
1569 commit true learns [] []; n
1572 fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
1573 | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (n, next_commit, _)) =
1575 val name = nickname_of_thm th
1576 val (n, relearns, flops) =
1577 (case deps_of status th of
1578 SOME deps => (n + 1, (name, deps) :: relearns, flops)
1579 | NONE => (n, relearns, name :: flops))
1580 val (relearns, flops, next_commit) =
1581 if Time.> (Timer.checkRealTimer timer, next_commit) then
1582 (commit false [] relearns flops; ([], [], next_commit_time ()))
1584 (relearns, flops, next_commit)
1585 val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
1587 ((relearns, flops), (n, next_commit, timed_out))
1591 if not run_prover then
1595 val max_isar = 1000 * max_dependencies
1597 fun priority_of th =
1598 random_range 0 max_isar +
1599 (case try (Graph.get_node access_G) (nickname_of_thm th) of
1600 SOME (Isar_Proof, _, deps) => ~100 * length deps
1601 | SOME (Automatic_Proof, _, _) => 2 * max_isar
1602 | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
1605 val old_facts = facts
1606 |> filter is_in_access_G
1607 |> map (`(priority_of o snd))
1608 |> sort (int_ord o pairself fst)
1610 val ((relearns, flops), (n, _, _)) =
1611 (([], []), (n, next_commit_time (), false))
1612 |> fold relearn_old_fact old_facts
1614 commit true [] relearns flops; n
1617 if verbose orelse auto_level < 2 then
1618 "Learned " ^ string_of_int n ^ " nontrivial " ^
1619 (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
1620 (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "."
1626 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
1628 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
1629 val ctxt = ctxt |> Config.put instantiate_inducts false
1630 val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
1631 |> sort (crude_thm_ord o pairself snd o swap)
1632 val num_facts = length facts
1633 val prover = hd provers
1635 fun learn auto_level run_prover =
1636 mash_learn_facts ctxt params prover true auto_level run_prover one_year facts
1637 |> Output.urgent_message
1640 (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
1641 plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
1642 string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
1644 Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
1645 \can safely stop the learning process at any point.";
1648 (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
1649 plural_s num_facts ^ " for Isar proofs...");
1653 fun mash_can_suggest_facts ctxt overlord =
1654 not (Graph.is_empty (#access_G (peek_state ctxt overlord I)))
1656 (* Generate more suggestions than requested, because some might be thrown out later for various
1657 reasons (e.g., duplicates). *)
1658 fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25
1660 val mepo_weight = 0.5
1661 val mash_weight = 0.5
1663 val max_facts_to_learn_before_query = 100
1665 (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer
1667 val min_secs_for_learning = 15
1669 fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...}) prover max_facts
1670 ({add, only, ...} : fact_override) hyp_ts concl_t facts =
1671 if not (subset (op =) (the_list fact_filter, fact_filters)) then
1672 error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
1674 [("", map fact_of_raw_fact facts)]
1675 else if max_facts <= 0 orelse null facts then
1679 fun maybe_launch_thread () =
1680 if not (Async_Manager.has_running_threads MaShN) andalso
1681 Time.toSeconds timeout >= min_secs_for_learning then
1682 let val timeout = time_mult learn_timeout_slack timeout in
1683 launch_thread timeout
1684 (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
1689 fun maybe_learn () =
1690 if is_mash_enabled () andalso learn then
1692 val {access_G, num_known_facts, ...} = peek_state ctxt overlord I
1693 val is_in_access_G = is_fact_in_graph access_G o snd
1695 if length facts - num_known_facts <= max_facts_to_learn_before_query then
1696 (case length (filter_out is_in_access_G facts) of
1698 | num_facts_to_learn =>
1699 if num_facts_to_learn <= max_facts_to_learn_before_query then
1700 (mash_learn_facts ctxt params prover false 2 false timeout facts
1701 |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
1704 (maybe_launch_thread (); false))
1706 (maybe_launch_thread (); false)
1711 val (save, effective_fact_filter) =
1712 (case fact_filter of
1713 SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
1715 if is_mash_enabled () then
1716 (maybe_learn (), if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
1720 val unique_facts = drop_duplicate_facts facts
1721 val add_ths = Attrib.eval_thms ctxt add
1723 fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
1725 fun add_and_take accepts =
1729 (unique_facts |> filter in_add |> map fact_of_raw_fact) @ (accepts |> filter_out in_add))
1733 (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
1734 |> weight_facts_steeply, [])
1737 mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
1738 |>> weight_facts_steeply
1741 (* the order is important for the "case" expression below *)
1742 [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
1743 |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
1744 |> Par_List.map (apsnd (fn f => f ()))
1745 val mesh = mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take
1747 if the_mash_engine () = MaSh_Py andalso save then MaSh_Py.save ctxt overlord else ();
1748 (case (fact_filter, mess) of
1749 (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
1750 [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
1751 (mashN, mash |> map fst |> add_and_take)]
1752 | _ => [(effective_fact_filter, mesh)])
1755 fun kill_learners ctxt ({overlord, ...} : params) =
1756 (Async_Manager.kill_threads MaShN "learner";
1757 if the_mash_engine () = MaSh_Py then MaSh_Py.shutdown ctxt overlord else ())
1759 fun running_learners () = Async_Manager.running_threads MaShN "learner"