30 |
30 |
31 fun thy_map_from_facts ths = |
31 fun thy_map_from_facts ths = |
32 ths |> sort (thm_ord o swap o pairself snd) |
32 ths |> sort (thm_ord o swap o pairself snd) |
33 |> map (snd #> `(theory_of_thm #> Context.theory_name)) |
33 |> map (snd #> `(theory_of_thm #> Context.theory_name)) |
34 |> AList.coalesce (op =) |
34 |> AList.coalesce (op =) |
35 |> map (apsnd (map Thm.get_name_hint)) |
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 parent_facts thy thy_map = |
40 fun parent_facts thy thy_map = |
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 nickname_of) #> 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 |
59 val _ = File.write path "" |
59 val _ = File.write path "" |
81 val facts = |
81 val facts = |
82 all_facts_of thy css_table |
82 all_facts_of thy css_table |
83 |> not include_thy ? filter_out (has_thy thy o snd) |
83 |> not include_thy ? filter_out (has_thy thy o snd) |
84 fun do_fact ((_, (_, status)), th) = |
84 fun do_fact ((_, (_, status)), th) = |
85 let |
85 let |
86 val name = Thm.get_name_hint th |
86 val name = nickname_of th |
87 val feats = |
87 val feats = |
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 |
99 |> not include_thy ? filter_out (has_thy thy o snd) |
99 |> not include_thy ? filter_out (has_thy thy o snd) |
100 |> map snd |
100 |> map snd |
101 val all_names = all_names ths |
101 val all_names = all_names ths |
102 fun do_thm th = |
102 fun do_thm th = |
103 let |
103 let |
104 val name = Thm.get_name_hint th |
104 val name = nickname_of th |
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 |
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) = nickname_of th = dep |
122 fun add_isar_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 *) |
128 fun fix_name ((_, stature), th) = |
128 fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th) |
129 ((fn () => th |> Thm.get_name_hint, stature), th) |
|
130 fun do_thm th = |
129 fun do_thm th = |
131 let |
130 let |
132 val name = Thm.get_name_hint th |
131 val name = nickname_of th |
133 val goal = goal_of_thm thy th |
132 val goal = goal_of_thm thy th |
134 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
133 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
135 val deps = |
134 val deps = |
136 case isabelle_dependencies_of all_names th of |
135 case isabelle_dependencies_of all_names th of |
137 [] => [] |
136 [] => [] |
166 |>> sort (thm_ord o pairself snd) |
165 |>> sort (thm_ord o pairself snd) |
167 val ths = facts |> map snd |
166 val ths = facts |> map snd |
168 val all_names = all_names ths |
167 val all_names = all_names ths |
169 fun do_fact ((_, (_, status)), th) prevs = |
168 fun do_fact ((_, (_, status)), th) prevs = |
170 let |
169 let |
171 val name = Thm.get_name_hint th |
170 val name = nickname_of th |
172 val feats = features_of ctxt prover thy status [prop_of th] |
171 val feats = features_of ctxt prover thy status [prop_of th] |
173 val deps = isabelle_dependencies_of all_names th |
172 val deps = isabelle_dependencies_of all_names th |
174 val kind = Thm.legacy_get_kind th |
173 val kind = Thm.legacy_get_kind th |
175 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
174 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
176 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
175 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
194 val (new_facts, old_facts) = |
193 val (new_facts, old_facts) = |
195 facts |> List.partition (has_thy thy o snd) |
194 facts |> List.partition (has_thy thy o snd) |
196 |>> sort (thm_ord o pairself snd) |
195 |>> sort (thm_ord o pairself snd) |
197 fun do_fact (fact as (_, th)) old_facts = |
196 fun do_fact (fact as (_, th)) old_facts = |
198 let |
197 let |
199 val name = Thm.get_name_hint th |
198 val name = nickname_of th |
200 val goal = goal_of_thm thy th |
199 val goal = goal_of_thm thy th |
201 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
200 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
202 val kind = Thm.legacy_get_kind th |
201 val kind = Thm.legacy_get_kind th |
203 val _ = |
202 val _ = |
204 if kind <> "" then |
203 if kind <> "" then |