26 open ATP_Problem |
26 open ATP_Problem |
27 open ATP_Proof |
27 open ATP_Proof |
28 open ATP_Problem_Generate |
28 open ATP_Problem_Generate |
29 open ATP_Systems |
29 open ATP_Systems |
30 |
30 |
31 val thy_prefix = "$" |
|
32 |
|
33 fun stringN_of_int 0 _ = "" |
31 fun stringN_of_int 0 _ = "" |
34 | stringN_of_int k n = |
32 | stringN_of_int k n = |
35 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
33 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
36 |
34 |
37 fun escape_meta_char c = |
35 fun escape_meta_char c = |
38 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
36 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
39 c = #")" then |
37 c = #")" then |
40 String.str c |
38 String.str c |
41 else |
39 else |
42 (* fixed width, in case more digits follow *) |
40 (* fixed width, in case more digits follow *) |
43 "_" ^ stringN_of_int 3 (Char.ord c) |
41 "~" ^ stringN_of_int 3 (Char.ord c) |
44 val escape_meta = String.translate escape_meta_char |
42 val escape_meta = String.translate escape_meta_char |
45 |
43 |
46 val fact_name_of = escape_meta |
44 val fact_name_of = escape_meta |
47 val thy_name_of = prefix thy_prefix o escape_meta |
45 val thy_name_of = escape_meta |
48 |
46 |
49 fun facts_of thy = |
47 fun facts_of thy = |
50 let val ctxt = Proof_Context.init_global thy in |
48 let val ctxt = Proof_Context.init_global thy in |
51 Sledgehammer_Filter.all_facts ctxt false |
49 Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] |
52 Symtab.empty true [] [] |
|
53 (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
50 (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
54 |> filter (curry (op =) @{typ bool} o fastype_of |
51 |> filter (curry (op =) @{typ bool} o fastype_of |
55 o Object_Logic.atomize_term thy o prop_of o snd) |
52 o Object_Logic.atomize_term thy o prop_of o snd) |
|
53 |> rev |
56 end |
54 end |
57 |
55 |
58 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
56 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
59 fixes that seem to be missing over there; or maybe the two code portions are |
57 fixes that seem to be missing over there; or maybe the two code portions are |
60 not doing the same? *) |
58 not doing the same? *) |
102 |
100 |
103 fun generate_mash_accessibility_file_for_theory thy file_name = |
101 fun generate_mash_accessibility_file_for_theory thy file_name = |
104 let |
102 let |
105 val path = file_name |> Path.explode |
103 val path = file_name |> Path.explode |
106 val _ = File.write path "" |
104 val _ = File.write path "" |
107 fun do_thm parents th seen = |
105 val thy_name_of_thm = theory_of_thm #> Context.theory_name |
108 let |
106 fun do_thm th prevs = |
109 val s = th ^ ": " ^ space_implode " " (parents @ seen) ^ "\n" |
107 let |
|
108 val s = th ^ ": " ^ space_implode " " prevs ^ "\n" |
110 val _ = File.append path s |
109 val _ = File.append path s |
111 in seen @ [th] end |
110 in [th] end |
112 fun do_thy (name, ths) = |
111 val thy_ths = |
113 let |
112 facts_of thy |
114 val ths = sort (theory_ord o pairself theory_of_thm) ths |
113 |> map (snd #> `thy_name_of_thm) |
|
114 |> AList.group (op =) |
|
115 |> sort (theory_ord o pairself (theory_of_thm o hd o snd)) |
|
116 |> map (apsnd (sort (theory_ord o pairself theory_of_thm))) |
|
117 fun do_thy ths = |
|
118 let |
115 val thy = theory_of_thm (hd ths) |
119 val thy = theory_of_thm (hd ths) |
116 val parents = |
120 val parents = |
117 if Context.theory_name thy = Context.theory_name @{theory HOL} then [] |
121 Theory.parents_of thy |
118 else map (thy_name_of o Context.theory_name) (Theory.parents_of thy) |
122 |> map (thy_name_of o Context.theory_name) |
119 val ths = map (fact_name_of o Thm.get_name_hint) ths |
123 |> map_filter (AList.lookup (op =) thy_ths) |
120 val s = |
124 |> map List.last |
121 thy_name_of name ^ ": " ^ space_implode " " (parents @ ths) ^ " \n" |
125 |> map (fact_name_of o Thm.get_name_hint) |
122 val _ = File.append path s |
126 val ths = ths |> map (fact_name_of o Thm.get_name_hint) |
123 val _ = fold (do_thm parents) ths [] |
127 val _ = fold do_thm ths parents |
124 in () end |
128 in () end |
125 val thy_name_of_thm = theory_of_thm #> Context.theory_name |
129 val _ = List.app (do_thy o snd) thy_ths |
126 val thy_ths = |
|
127 facts_of thy |> map (snd #> `thy_name_of_thm) |
|
128 |> AList.group (op =) |
|
129 |> sort (theory_ord o pairself (theory_of_thm o hd o snd)) |
|
130 val _ = List.app do_thy thy_ths |
|
131 in () end |
130 in () end |
132 |
131 |
133 (* TODO: Add types, subterms, intro/dest/elim/simp status *) |
132 (* TODO: Add types, subterms, intro/dest/elim/simp status *) |
134 fun generate_mash_feature_file_for_theory ctxt thy file_name = |
133 fun generate_mash_feature_file_for_theory ctxt thy file_name = |
135 let |
134 let |