28 val escape_metas : string list -> string |
28 val escape_metas : string list -> string |
29 val unescape_meta : string -> string |
29 val unescape_meta : string -> string |
30 val unescape_metas : string -> string list |
30 val unescape_metas : string -> string list |
31 val encode_features : (string * real) list -> string |
31 val encode_features : (string * real) list -> string |
32 val extract_query : string -> string * (string * real) list |
32 val extract_query : string -> string * (string * real) list |
33 val mash_UNLEARN : Proof.context -> unit |
33 |
34 val mash_LEARN : |
34 structure MaSh: |
35 Proof.context -> bool |
35 sig |
36 -> (string * string list * (string * real) list * string list) list -> unit |
36 val unlearn : Proof.context -> unit |
37 val mash_RELEARN : |
37 val learn : |
38 Proof.context -> bool -> (string * string list) list -> unit |
38 Proof.context -> bool |
39 val mash_QUERY : |
39 -> (string * string list * (string * real) list * string list) list -> unit |
40 Proof.context -> bool -> int -> string list * (string * real) list |
40 val relearn : |
41 -> (string * real) list |
41 Proof.context -> bool -> (string * string list) list -> unit |
|
42 val query : |
|
43 Proof.context -> bool -> int -> string list * (string * real) list |
|
44 -> (string * real) list |
|
45 end |
|
46 |
42 val mash_unlearn : Proof.context -> unit |
47 val mash_unlearn : Proof.context -> unit |
43 val nickname_of_thm : thm -> string |
48 val nickname_of_thm : thm -> string |
44 val find_suggested_facts : |
49 val find_suggested_facts : |
45 (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list |
50 (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list |
46 val mesh_facts : |
51 val mesh_facts : |
213 [goal, suggs] => |
218 [goal, suggs] => |
214 (unescape_meta goal, |
219 (unescape_meta goal, |
215 map_filter extract_suggestion (space_explode " " suggs)) |
220 map_filter extract_suggestion (space_explode " " suggs)) |
216 | _ => ("", []) |
221 | _ => ("", []) |
217 |
222 |
218 fun mash_UNLEARN ctxt = |
223 structure MaSh = |
|
224 struct |
|
225 |
|
226 fun unlearn ctxt = |
219 let val path = mash_model_dir () in |
227 let val path = mash_model_dir () in |
220 trace_msg ctxt (K "MaSh UNLEARN"); |
228 trace_msg ctxt (K "MaSh unlearn"); |
221 try (File.fold_dir (fn file => fn _ => |
229 try (File.fold_dir (fn file => fn _ => |
222 try File.rm (Path.append path (Path.basic file))) |
230 try File.rm (Path.append path (Path.basic file))) |
223 path) NONE; |
231 path) NONE; |
224 () |
232 () |
225 end |
233 end |
226 |
234 |
227 fun mash_LEARN _ _ [] = () |
235 fun learn _ _ [] = () |
228 | mash_LEARN ctxt overlord learns = |
236 | learn ctxt overlord learns = |
229 (trace_msg ctxt (fn () => "MaSh LEARN " ^ |
237 (trace_msg ctxt (fn () => "MaSh learn " ^ |
230 elide_string 1000 (space_implode " " (map #1 learns))); |
238 elide_string 1000 (space_implode " " (map #1 learns))); |
231 run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ())) |
239 run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ())) |
232 |
240 |
233 fun mash_RELEARN _ _ [] = () |
241 fun relearn _ _ [] = () |
234 | mash_RELEARN ctxt overlord relearns = |
242 | relearn ctxt overlord relearns = |
235 (trace_msg ctxt (fn () => "MaSh RELEARN " ^ |
243 (trace_msg ctxt (fn () => "MaSh relearn " ^ |
236 elide_string 1000 (space_implode " " (map #1 relearns))); |
244 elide_string 1000 (space_implode " " (map #1 relearns))); |
237 run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) |
245 run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) |
238 |
246 |
239 fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = |
247 fun query ctxt overlord max_suggs (query as (_, feats)) = |
240 (trace_msg ctxt (fn () => "MaSh QUERY " ^ encode_features feats); |
248 (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
241 run_mash_tool ctxt overlord false max_suggs |
249 run_mash_tool ctxt overlord false max_suggs |
242 ([query], str_of_query) |
250 ([query], str_of_query) |
243 (fn suggs => |
251 (fn suggs => |
244 case suggs () of |
252 case suggs () of |
245 [] => [] |
253 [] => [] |
246 | suggs => snd (extract_query (List.last suggs))) |
254 | suggs => snd (extract_query (List.last suggs))) |
247 handle List.Empty => []) |
255 handle List.Empty => []) |
|
256 |
|
257 end; |
248 |
258 |
249 |
259 |
250 (*** Middle-level communication with MaSh ***) |
260 (*** Middle-level communication with MaSh ***) |
251 |
261 |
252 datatype proof_kind = |
262 datatype proof_kind = |
379 Synchronized.change_result global_state |
389 Synchronized.change_result global_state |
380 (perhaps (try (load ctxt)) #> `snd #>> f) |
390 (perhaps (try (load ctxt)) #> `snd #>> f) |
381 |
391 |
382 fun clear_state ctxt = |
392 fun clear_state ctxt = |
383 Synchronized.change global_state (fn _ => |
393 Synchronized.change global_state (fn _ => |
384 (mash_UNLEARN ctxt; (* also removes the state file *) |
394 (MaSh.unlearn ctxt; (* also removes the state file *) |
385 (true, empty_state))) |
395 (true, empty_state))) |
386 |
396 |
387 end |
397 end |
388 |
398 |
389 val mash_unlearn = clear_state |
399 val mash_unlearn = clear_state |
776 let |
786 let |
777 val parents = maximal_in_graph access_G facts |
787 val parents = maximal_in_graph access_G facts |
778 val feats = |
788 val feats = |
779 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) |
789 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) |
780 in |
790 in |
781 (access_G, mash_QUERY ctxt overlord max_facts (parents, feats)) |
791 (access_G, MaSh.query ctxt overlord max_facts (parents, feats)) |
782 end) |
792 end) |
783 val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) |
793 val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) |
784 val unknown = facts |> filter_out (is_fact_in_graph access_G) |
794 val unknown = facts |> filter_out (is_fact_in_graph access_G) |
785 in find_mash_suggestions max_facts suggs facts chained unknown end |
795 in find_mash_suggestions max_facts suggs facts chained unknown end |
786 |
796 |
832 val feats = features_of ctxt prover thy (Local, General) [t] |
842 val feats = features_of ctxt prover thy (Local, General) [t] |
833 val deps = used_ths |> map nickname_of_thm |
843 val deps = used_ths |> map nickname_of_thm |
834 in |
844 in |
835 peek_state ctxt (fn {access_G, ...} => |
845 peek_state ctxt (fn {access_G, ...} => |
836 let val parents = maximal_in_graph access_G facts in |
846 let val parents = maximal_in_graph access_G facts in |
837 mash_LEARN ctxt overlord [(name, parents, feats, deps)] |
847 MaSh.learn ctxt overlord [(name, parents, feats, deps)] |
838 end); |
848 end); |
839 (true, "") |
849 (true, "") |
840 end) |
850 end) |
841 |
851 |
842 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) |
852 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) |
890 val dirty = |
900 val dirty = |
891 case (was_empty, dirty, relearns) of |
901 case (was_empty, dirty, relearns) of |
892 (false, SOME names, []) => SOME (map #1 learns @ names) |
902 (false, SOME names, []) => SOME (map #1 learns @ names) |
893 | _ => NONE |
903 | _ => NONE |
894 in |
904 in |
895 mash_LEARN ctxt overlord (rev learns); |
905 MaSh.learn ctxt overlord (rev learns); |
896 mash_RELEARN ctxt overlord relearns; |
906 MaSh.relearn ctxt overlord relearns; |
897 {access_G = access_G, dirty = dirty} |
907 {access_G = access_G, dirty = dirty} |
898 end |
908 end |
899 fun commit last learns relearns flops = |
909 fun commit last learns relearns flops = |
900 (if debug andalso auto_level = 0 then |
910 (if debug andalso auto_level = 0 then |
901 Output.urgent_message "Committing..." |
911 Output.urgent_message "Committing..." |