7 signature SLEDGEHAMMER_FILTER_MASH = |
7 signature SLEDGEHAMMER_FILTER_MASH = |
8 sig |
8 sig |
9 type status = ATP_Problem_Generate.status |
9 type status = ATP_Problem_Generate.status |
10 type stature = ATP_Problem_Generate.stature |
10 type stature = ATP_Problem_Generate.stature |
11 type params = Sledgehammer_Provers.params |
11 type params = Sledgehammer_Provers.params |
12 type relevance_override = Sledgehammer_Fact.relevance_override |
12 type fact_override = Sledgehammer_Fact.fact_override |
13 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
13 type relevance_fudge = Sledgehammer_Provers.relevance_fudge |
14 type prover_result = Sledgehammer_Provers.prover_result |
14 type prover_result = Sledgehammer_Provers.prover_result |
15 |
15 |
16 val fact_name_of : string -> string |
16 val fact_name_of : string -> string |
17 val all_non_tautological_facts_of : |
17 val all_non_tautological_facts_of : |
22 val has_thy : theory -> thm -> bool |
22 val has_thy : theory -> thm -> bool |
23 val parent_thms : (string * thm list) list -> theory -> string list |
23 val parent_thms : (string * thm list) list -> theory -> string list |
24 val features_of : theory -> status * thm -> string list |
24 val features_of : theory -> status * thm -> string list |
25 val isabelle_dependencies_of : string list -> thm -> string list |
25 val isabelle_dependencies_of : string list -> thm -> string list |
26 val goal_of_thm : theory -> thm -> thm |
26 val goal_of_thm : theory -> thm -> thm |
27 val iter_facts : |
|
28 Proof.context -> params -> int -> thm |
|
29 -> (((unit -> string) * stature) * thm) list |
|
30 -> (((unit -> string) * stature) * thm) list |
|
31 val run_prover : |
27 val run_prover : |
32 Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm |
28 Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm |
33 -> prover_result |
29 -> prover_result |
34 val generate_accessibility : theory -> bool -> string -> unit |
30 val generate_accessibility : theory -> bool -> string -> unit |
35 val generate_features : theory -> bool -> string -> unit |
31 val generate_features : theory -> bool -> string -> unit |
43 val can_learn_thy : theory -> bool |
39 val can_learn_thy : theory -> bool |
44 val learn_thy : theory -> real -> unit |
40 val learn_thy : theory -> real -> unit |
45 val learn_proof : theory -> term -> thm list -> unit |
41 val learn_proof : theory -> term -> thm list -> unit |
46 |
42 |
47 val relevant_facts : |
43 val relevant_facts : |
48 Proof.context -> params -> string -> int -> relevance_override -> thm list |
44 Proof.context -> params -> string -> int -> fact_override -> term list |
49 -> term list -> term -> (((unit -> string) * stature) * thm) list |
45 -> term -> (((unit -> string) * stature) * thm) list |
50 -> (((unit -> string) * stature) * thm) list |
46 -> (((unit -> string) * stature) * thm) list |
51 end; |
47 end; |
52 |
48 |
53 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = |
49 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = |
54 struct |
50 struct |
77 tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ |
73 tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ |
78 space_implode " " feats) |
74 space_implode " " feats) |
79 |
75 |
80 |
76 |
81 (*** Isabelle helpers ***) |
77 (*** Isabelle helpers ***) |
82 |
|
83 val fact_name_of = prefix fact_prefix o ascii_of |
|
84 |
78 |
85 fun escape_meta_char c = |
79 fun escape_meta_char c = |
86 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
80 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
87 c = #")" orelse c = #"," then |
81 c = #")" orelse c = #"," then |
88 String.str c |
82 String.str c |
253 | freeze (Free (s, T)) = Free (s, freezeT T) |
247 | freeze (Free (s, T)) = Free (s, freezeT T) |
254 | freeze t = t |
248 | freeze t = t |
255 |
249 |
256 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init |
250 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init |
257 |
251 |
258 fun iter_facts ctxt (params as {provers, ...}) max_relevant goal = |
|
259 let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 in |
|
260 iterative_relevant_facts ctxt params (hd provers) max_relevant NONE |
|
261 no_relevance_override [] hyp_ts concl_t |
|
262 end |
|
263 |
|
264 fun run_prover ctxt (params as {provers, ...}) facts goal = |
252 fun run_prover ctxt (params as {provers, ...}) facts goal = |
265 let |
253 let |
266 val problem = |
254 val problem = |
267 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, |
255 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, |
268 facts = facts |> map (apfst (apfst (fn name => name ()))) |
256 facts = facts |> map (apfst (apfst (fn name => name ()))) |
323 val deps = isabelle_dependencies_of all_names th |
311 val deps = isabelle_dependencies_of all_names th |
324 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
312 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
325 in File.append path s end |
313 in File.append path s end |
326 in List.app do_thm ths end |
314 in List.app do_thm ths end |
327 |
315 |
328 fun generate_atp_dependencies ctxt (params as {max_relevant, ...}) thy |
316 fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy |
329 include_thy file_name = |
317 include_thy file_name = |
330 let |
318 let |
331 val path = file_name |> Path.explode |
319 val path = file_name |> Path.explode |
332 val _ = File.write path "" |
320 val _ = File.write path "" |
333 val facts = |
321 val facts = |
346 ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th) |
334 ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th) |
347 fun do_thm th = |
335 fun do_thm th = |
348 let |
336 let |
349 val name = Thm.get_name_hint th |
337 val name = Thm.get_name_hint th |
350 val goal = goal_of_thm thy th |
338 val goal = goal_of_thm thy th |
|
339 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
351 val deps = |
340 val deps = |
352 case isabelle_dependencies_of all_names th of |
341 case isabelle_dependencies_of all_names th of |
353 [] => [] |
342 [] => [] |
354 | isa_dep as [_] => isa_dep (* can hardly beat that *) |
343 | isa_dep as [_] => isa_dep (* can hardly beat that *) |
355 | isa_deps => |
344 | isa_deps => |
356 let |
345 let |
357 val facts = |
346 val facts = |
358 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
347 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
359 val facts = |
348 val facts = |
360 facts |> iter_facts ctxt params (the max_relevant) goal |
349 facts |> iterative_relevant_facts ctxt params (hd provers) |
|
350 (the max_relevant) NONE hyp_ts concl_t |
361 |> fold (add_isa_dep facts) isa_deps |
351 |> fold (add_isa_dep facts) isa_deps |
362 |> map fix_name |
352 |> map fix_name |
363 in |
353 in |
364 case run_prover ctxt params facts goal of |
354 case run_prover ctxt params facts goal of |
365 {outcome = NONE, used_facts, ...} => |
355 {outcome = NONE, used_facts, ...} => |
383 true |
373 true |
384 |
374 |
385 fun learn_thy thy timeout = |
375 fun learn_thy thy timeout = |
386 () |
376 () |
387 |
377 |
388 fun learn_proof thy t thms = |
378 fun learn_proof thy t ths = |
389 () |
379 () |
390 |
380 |
391 fun relevant_facts ctxt params prover max_relevant |
381 fun relevant_facts ctxt params prover max_relevant |
392 (override as {add, only, ...}) chained_ths hyp_ts concl_t |
382 ({add, only, ...} : fact_override) hyp_ts concl_t facts = |
393 facts = |
|
394 if only then |
383 if only then |
395 facts |
384 facts |
396 else if max_relevant <= 0 then |
385 else if max_relevant <= 0 then |
397 [] |
386 [] |
398 else |
387 else |
399 let |
388 let |
400 val add_ths = Attrib.eval_thms ctxt add |
389 val add_ths = Attrib.eval_thms ctxt add |
401 fun prepend_facts ths facts = |
390 fun prepend_facts ths accepts = |
402 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
391 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
403 (facts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
392 (accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
404 |> take max_relevant |
393 |> take max_relevant |
405 in |
394 in |
406 iterative_relevant_facts ctxt params prover max_relevant NONE override |
395 iterative_relevant_facts ctxt params prover max_relevant NONE |
407 chained_ths hyp_ts concl_t facts |
396 hyp_ts concl_t facts |
408 |> not (null add_ths) ? prepend_facts add_ths |
397 |> not (null add_ths) ? prepend_facts add_ths |
409 end |
398 end |
410 |
399 |
411 end; |
400 end; |