54 |
54 |
55 val thy_name_of_fact = hd o Long_Name.explode |
55 val thy_name_of_fact = hd o Long_Name.explode |
56 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
56 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
57 |
57 |
58 val all_names = map (rpair () o nickname_of) #> Symtab.make |
58 val all_names = map (rpair () o nickname_of) #> Symtab.make |
59 |
|
60 fun smart_dependencies_of ctxt params prover facts all_names th = |
|
61 case atp_dependencies_of ctxt params prover 0 facts all_names th of |
|
62 SOME deps => deps |
|
63 | NONE => isar_dependencies_of all_names th |> these |
|
64 |
59 |
65 fun generate_accessibility ctxt thy include_thy file_name = |
60 fun generate_accessibility ctxt thy include_thy file_name = |
66 let |
61 let |
67 val path = file_name |> Path.explode |
62 val path = file_name |> Path.explode |
68 val _ = File.write path "" |
63 val _ = File.write path "" |
127 val ths = facts |> map snd |
122 val ths = facts |> map snd |
128 val all_names = all_names ths |
123 val all_names = all_names ths |
129 fun do_thm th = |
124 fun do_thm th = |
130 let |
125 let |
131 val name = nickname_of th |
126 val name = nickname_of th |
132 val deps = smart_dependencies_of ctxt params prover facts all_names th |
127 val deps = |
|
128 atp_dependencies_of ctxt params prover 0 facts all_names th |
|
129 |> snd |> these |
133 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
130 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
134 in File.append path s end |
131 in File.append path s end |
135 in List.app do_thm ths end |
132 in List.app do_thm ths end |
136 |
133 |
137 fun generate_commands ctxt (params as {provers, ...}) thy file_name = |
134 fun generate_commands ctxt (params as {provers, ...}) thy file_name = |
141 val prover = hd provers |
138 val prover = hd provers |
142 val facts = all_non_technical_facts ctxt thy |
139 val facts = all_non_technical_facts ctxt thy |
143 val (new_facts, old_facts) = |
140 val (new_facts, old_facts) = |
144 facts |> List.partition (has_thy thy o snd) |
141 facts |> List.partition (has_thy thy o snd) |
145 |>> sort (thm_ord o pairself snd) |
142 |>> sort (thm_ord o pairself snd) |
146 val ths = facts |> map snd |
143 val all_names = all_names (map snd facts) |
147 val all_names = all_names ths |
|
148 fun do_fact ((_, stature), th) prevs = |
144 fun do_fact ((_, stature), th) prevs = |
149 let |
145 let |
150 val name = nickname_of th |
146 val name = nickname_of th |
151 val feats = features_of ctxt prover thy stature [prop_of th] |
147 val feats = features_of ctxt prover thy stature [prop_of th] |
152 val deps = smart_dependencies_of ctxt params prover facts all_names th |
148 val deps = |
|
149 atp_dependencies_of ctxt params prover 0 facts all_names th |
|
150 |> snd |> these |
153 val kind = Thm.legacy_get_kind th |
151 val kind = Thm.legacy_get_kind th |
154 val core = |
152 val core = |
155 escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ |
153 escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ |
156 escape_metas feats |
154 escape_metas feats |
157 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
155 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |