equal
deleted
inserted
replaced
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_isa_dependencies : |
16 Proof.context -> string -> theory -> bool -> string -> unit |
16 theory -> bool -> string -> unit |
17 val generate_prover_dependencies : |
17 val generate_prover_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 |
47 in add_parent thy [] end |
47 in add_parent thy [] 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 fun all_names ctxt prover = |
52 val all_names = |
53 filter_out (is_likely_tautology ctxt prover orf is_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 |
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 ctxt prover thy include_thy file_name = |
93 fun generate_isa_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 |
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 ctxt prover 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 = Thm.get_name_hint 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" |
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 ctxt prover 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_isa_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 |
163 val facts = all_facts_of thy css_table |
163 val facts = all_facts_of thy css_table |
164 val (new_facts, old_facts) = |
164 val (new_facts, old_facts) = |
165 facts |> List.partition (has_thy thy o snd) |
165 facts |> List.partition (has_thy thy o snd) |
166 |>> sort (thm_ord o pairself snd) |
166 |>> sort (thm_ord o pairself snd) |
167 val ths = facts |> map snd |
167 val ths = facts |> map snd |
168 val all_names = all_names ctxt prover ths |
168 val all_names = all_names ths |
169 fun do_fact ((_, (_, status)), th) prevs = |
169 fun do_fact ((_, (_, status)), th) prevs = |
170 let |
170 let |
171 val name = Thm.get_name_hint th |
171 val name = Thm.get_name_hint th |
172 val feats = features_of ctxt prover thy status [prop_of th] |
172 val feats = features_of ctxt prover thy status [prop_of th] |
173 val deps = isabelle_dependencies_of all_names th |
173 val deps = isabelle_dependencies_of all_names th |