equal
deleted
inserted
replaced
35 |> map (apsnd (map nickname_of)) |
35 |> map (apsnd (map nickname_of)) |
36 |
36 |
37 fun has_thy thy th = |
37 fun has_thy thy th = |
38 Context.theory_name thy = Context.theory_name (theory_of_thm th) |
38 Context.theory_name thy = Context.theory_name (theory_of_thm th) |
39 |
39 |
|
40 fun all_non_technical_facts ctxt thy = |
|
41 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
|
42 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
|
43 |> filter_out (is_thm_technical o snd) |
|
44 end |
|
45 |
40 fun parent_facts thy thy_map = |
46 fun parent_facts thy thy_map = |
41 let |
47 let |
42 fun add_last thy = |
48 fun add_last thy = |
43 case AList.lookup (op =) thy_map (Context.theory_name thy) of |
49 case AList.lookup (op =) thy_map (Context.theory_name thy) of |
44 SOME (last_fact :: _) => insert (op =) last_fact |
50 SOME (last_fact :: _) => insert (op =) last_fact |
63 fun do_fact fact prevs = |
69 fun do_fact fact prevs = |
64 let |
70 let |
65 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" |
71 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" |
66 val _ = File.append path s |
72 val _ = File.append path s |
67 in [fact] end |
73 in [fact] end |
68 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
|
69 val thy_map = |
74 val thy_map = |
70 all_facts ctxt false Symtab.empty [] [] css |
75 all_non_technical_facts ctxt thy |
71 |> not include_thy ? filter_out (has_thy thy o snd) |
76 |> not include_thy ? filter_out (has_thy thy o snd) |
72 |> thy_map_from_facts |
77 |> thy_map_from_facts |
73 fun do_thy facts = |
78 fun do_thy facts = |
74 let |
79 let |
75 val thy = thy_of_fact thy (hd facts) |
80 val thy = thy_of_fact thy (hd facts) |
79 |
84 |
80 fun generate_features ctxt prover thy include_thy file_name = |
85 fun generate_features ctxt prover thy include_thy file_name = |
81 let |
86 let |
82 val path = file_name |> Path.explode |
87 val path = file_name |> Path.explode |
83 val _ = File.write path "" |
88 val _ = File.write path "" |
84 val css = clasimpset_rule_table_of ctxt |
|
85 val facts = |
89 val facts = |
86 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
90 all_non_technical_facts ctxt thy |
87 |> not include_thy ? filter_out (has_thy thy o snd) |
91 |> not include_thy ? filter_out (has_thy thy o snd) |
88 fun do_fact ((_, stature), th) = |
92 fun do_fact ((_, stature), th) = |
89 let |
93 let |
90 val name = nickname_of th |
94 val name = nickname_of th |
91 val feats = |
95 val feats = |
96 |
100 |
97 fun generate_isar_dependencies ctxt thy include_thy file_name = |
101 fun generate_isar_dependencies ctxt thy include_thy file_name = |
98 let |
102 let |
99 val path = file_name |> Path.explode |
103 val path = file_name |> Path.explode |
100 val _ = File.write path "" |
104 val _ = File.write path "" |
101 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
|
102 val ths = |
105 val ths = |
103 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
106 all_non_technical_facts ctxt thy |
104 |> not include_thy ? filter_out (has_thy thy o snd) |
107 |> not include_thy ? filter_out (has_thy thy o snd) |
105 |> map snd |
108 |> map snd |
106 val all_names = all_names ths |
109 val all_names = all_names ths |
107 fun do_thm th = |
110 fun do_thm th = |
108 let |
111 let |
116 file_name = |
119 file_name = |
117 let |
120 let |
118 val path = file_name |> Path.explode |
121 val path = file_name |> Path.explode |
119 val _ = File.write path "" |
122 val _ = File.write path "" |
120 val prover = hd provers |
123 val prover = hd provers |
121 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
|
122 val facts = |
124 val facts = |
123 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
125 all_non_technical_facts ctxt thy |
124 |> not include_thy ? filter_out (has_thy thy o snd) |
126 |> not include_thy ? filter_out (has_thy thy o snd) |
125 val ths = facts |> map snd |
127 val ths = facts |> map snd |
126 val all_names = all_names ths |
128 val all_names = all_names ths |
127 fun do_thm th = |
129 fun do_thm th = |
128 let |
130 let |
135 fun generate_commands ctxt (params as {provers, ...}) thy file_name = |
137 fun generate_commands ctxt (params as {provers, ...}) thy file_name = |
136 let |
138 let |
137 val path = file_name |> Path.explode |
139 val path = file_name |> Path.explode |
138 val _ = File.write path "" |
140 val _ = File.write path "" |
139 val prover = hd provers |
141 val prover = hd provers |
140 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
142 val facts = all_non_technical_facts ctxt thy |
141 val facts = |
|
142 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
|
143 val (new_facts, old_facts) = |
143 val (new_facts, old_facts) = |
144 facts |> List.partition (has_thy thy o snd) |
144 facts |> List.partition (has_thy thy o snd) |
145 |>> sort (thm_ord o pairself snd) |
145 |>> sort (thm_ord o pairself snd) |
146 val ths = facts |> map snd |
146 val ths = facts |> map snd |
147 val all_names = all_names ths |
147 val all_names = all_names ths |
166 file_name = |
166 file_name = |
167 let |
167 let |
168 val path = file_name |> Path.explode |
168 val path = file_name |> Path.explode |
169 val _ = File.write path "" |
169 val _ = File.write path "" |
170 val prover = hd provers |
170 val prover = hd provers |
171 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
171 val facts = all_non_technical_facts ctxt thy |
172 val facts = |
|
173 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
|
174 val (new_facts, old_facts) = |
172 val (new_facts, old_facts) = |
175 facts |> List.partition (has_thy thy o snd) |
173 facts |> List.partition (has_thy thy o snd) |
176 |>> sort (thm_ord o pairself snd) |
174 |>> sort (thm_ord o pairself snd) |
177 fun do_fact (fact as (_, th)) old_facts = |
175 fun do_fact (fact as (_, th)) old_facts = |
178 let |
176 let |