10 type params = Sledgehammer_Provers.params |
10 type params = Sledgehammer_Provers.params |
11 |
11 |
12 val generate_accessibility : theory -> bool -> string -> unit |
12 val generate_accessibility : theory -> bool -> string -> unit |
13 val generate_features : |
13 val generate_features : |
14 Proof.context -> string -> theory -> bool -> string -> unit |
14 Proof.context -> string -> theory -> bool -> string -> unit |
15 val generate_isa_dependencies : |
15 val generate_isar_dependencies : |
16 theory -> bool -> string -> unit |
16 theory -> bool -> string -> unit |
17 val generate_prover_dependencies : |
17 val generate_atp_dependencies : |
18 Proof.context -> params -> theory -> bool -> string -> unit |
18 Proof.context -> params -> theory -> bool -> string -> unit |
19 val generate_commands : Proof.context -> string -> theory -> string -> unit |
19 val generate_commands : Proof.context -> string -> theory -> string -> unit |
20 val generate_iter_suggestions : |
20 val generate_iter_suggestions : |
21 Proof.context -> params -> theory -> int -> string -> unit |
21 Proof.context -> params -> theory -> int -> string -> unit |
22 end; |
22 end; |
48 |
48 |
49 val thy_name_of_fact = hd o Long_Name.explode |
49 val thy_name_of_fact = hd o Long_Name.explode |
50 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
50 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
51 |
51 |
52 val all_names = |
52 val all_names = |
53 filter_out (is_likely_tautology_or_too_meta) |
53 filter_out is_likely_tautology_or_too_meta |
54 #> map (rpair () o Thm.get_name_hint) #> Symtab.make |
54 #> map (rpair () o Thm.get_name_hint) #> Symtab.make |
55 |
55 |
56 fun generate_accessibility thy include_thy file_name = |
56 fun generate_accessibility thy include_thy file_name = |
57 let |
57 let |
58 val path = file_name |> Path.explode |
58 val path = file_name |> Path.explode |
69 fun do_thy facts = |
69 fun do_thy facts = |
70 let |
70 let |
71 val thy = thy_of_fact thy (hd facts) |
71 val thy = thy_of_fact thy (hd facts) |
72 val parents = parent_facts thy thy_map |
72 val parents = parent_facts thy thy_map |
73 in fold do_fact facts parents; () end |
73 in fold do_fact facts parents; () end |
74 in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end |
74 in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end |
75 |
75 |
76 fun generate_features ctxt prover thy include_thy file_name = |
76 fun generate_features ctxt prover thy include_thy file_name = |
77 let |
77 let |
78 val path = file_name |> Path.explode |
78 val path = file_name |> Path.explode |
79 val _ = File.write path "" |
79 val _ = File.write path "" |
88 features_of ctxt prover (theory_of_thm th) status [prop_of th] |
88 features_of ctxt prover (theory_of_thm th) status [prop_of th] |
89 val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" |
89 val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" |
90 in File.append path s end |
90 in File.append path s end |
91 in List.app do_fact facts end |
91 in List.app do_fact facts end |
92 |
92 |
93 fun generate_isa_dependencies thy include_thy file_name = |
93 fun generate_isar_dependencies thy include_thy file_name = |
94 let |
94 let |
95 val path = file_name |> Path.explode |
95 val path = file_name |> Path.explode |
96 val _ = File.write path "" |
96 val _ = File.write path "" |
97 val ths = |
97 val ths = |
98 all_facts_of thy Termtab.empty |
98 all_facts_of thy Termtab.empty |
105 val deps = isabelle_dependencies_of all_names th |
105 val deps = isabelle_dependencies_of all_names th |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
107 in File.append path s end |
107 in File.append path s end |
108 in List.app do_thm ths end |
108 in List.app do_thm ths end |
109 |
109 |
110 fun generate_prover_dependencies ctxt (params as {provers, max_facts, ...}) thy |
110 fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy |
111 include_thy file_name = |
111 include_thy file_name = |
112 let |
112 let |
113 val path = file_name |> Path.explode |
113 val path = file_name |> Path.explode |
114 val _ = File.write path "" |
114 val _ = File.write path "" |
115 val prover = hd provers |
115 val prover = hd provers |
116 val facts = |
116 val facts = |
117 all_facts_of thy Termtab.empty |
117 all_facts_of thy Termtab.empty |
118 |> not include_thy ? filter_out (has_thy thy o snd) |
118 |> not include_thy ? filter_out (has_thy thy o snd) |
119 val ths = facts |> map snd |
119 val ths = facts |> map snd |
120 val all_names = all_names ths |
120 val all_names = all_names ths |
121 fun is_dep dep (_, th) = Thm.get_name_hint th = dep |
121 fun is_dep dep (_, th) = Thm.get_name_hint th = dep |
122 fun add_isa_dep facts dep accum = |
122 fun add_isar_dep facts dep accum = |
123 if exists (is_dep dep) accum then |
123 if exists (is_dep dep) accum then |
124 accum |
124 accum |
125 else case find_first (is_dep dep) facts of |
125 else case find_first (is_dep dep) facts of |
126 SOME ((name, status), th) => accum @ [((name, status), th)] |
126 SOME ((name, status), th) => accum @ [((name, status), th)] |
127 | NONE => accum (* shouldn't happen *) |
127 | NONE => accum (* shouldn't happen *) |
133 val goal = goal_of_thm thy th |
133 val goal = goal_of_thm thy th |
134 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
134 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
135 val deps = |
135 val deps = |
136 case isabelle_dependencies_of all_names th of |
136 case isabelle_dependencies_of all_names th of |
137 [] => [] |
137 [] => [] |
138 | isa_dep as [_] => isa_dep (* can hardly beat that *) |
138 | isar_dep as [_] => isar_dep (* can hardly beat that *) |
139 | isa_deps => |
139 | isar_deps => |
140 let |
140 let |
141 val facts = |
141 val facts = |
142 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
142 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
143 val facts = |
143 val facts = |
144 facts |> iterative_relevant_facts ctxt params prover |
144 facts |> iterative_relevant_facts ctxt params prover |
145 (the max_facts) NONE hyp_ts concl_t |
145 (the max_facts) NONE hyp_ts concl_t |
146 |> fold (add_isa_dep facts) isa_deps |
146 |> fold (add_isar_dep facts) isar_deps |
147 |> map fix_name |
147 |> map fix_name |
148 in |
148 in |
149 case run_prover_for_mash ctxt params prover facts goal of |
149 case run_prover_for_mash ctxt params prover facts goal of |
150 {outcome = NONE, used_facts, ...} => |
150 {outcome = NONE, used_facts, ...} => |
151 used_facts |> map fst |> sort string_ord |
151 used_facts |> map fst |> sort string_ord |
152 | _ => isa_deps |
152 | _ => isar_deps |
153 end |
153 end |
154 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
154 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
155 in File.append path s end |
155 in File.append path s end |
156 in List.app do_thm ths end |
156 in List.app do_thm ths end |
157 |
157 |