91 schematics: typ list Symtab.table, |
84 schematics: typ list Symtab.table, |
92 initial_round: int } |
85 initial_round: int } |
93 |
86 |
94 fun prepare schematic_consts_of rthms = |
87 fun prepare schematic_consts_of rthms = |
95 let |
88 let |
96 val empty_subst = ((0, false, false), Vartab.empty) |
89 val empty_sub = ((0, false, false), Vartab.empty) |
97 |
90 |
98 fun prep (r, thm) ((i, idx), (consts, substs)) = |
91 fun prep (r, thm) ((i, idx), (consts, subs)) = |
99 if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then |
92 if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then |
100 (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, substs))) |
93 (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs))) |
101 else |
94 else |
102 let |
95 let |
103 (* increase indices to avoid clashes of type variables *) |
96 (* increase indices to avoid clashes of type variables *) |
104 val thm' = Thm.incr_indexes idx thm |
97 val thm' = Thm.incr_indexes idx thm |
105 val idx' = Thm.maxidx_of thm' + 1 |
98 val idx' = Thm.maxidx_of thm' + 1 |
106 val schematics = schematic_consts_of (Thm.prop_of thm') |
99 val schematics = schematic_consts_of (Thm.prop_of thm') |
107 val consts' = |
100 val consts' = |
108 Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts |
101 Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts |
109 val substs' = Inttab.update (i, [empty_subst]) substs |
102 val subs' = Inttab.update (i, [empty_sub]) subs |
110 val thm_info = Schematic { |
103 val thm_info = Schematic { |
111 index = i, |
104 index = i, |
112 theorem = thm', |
105 theorem = thm', |
113 tvars = Term.add_tvars (Thm.prop_of thm') [], |
106 tvars = Term.add_tvars (Thm.prop_of thm') [], |
114 schematics = schematics, |
107 schematics = schematics, |
115 initial_round = r } |
108 initial_round = r } |
116 in (thm_info, ((i+1, idx'), (consts', substs'))) end |
109 in (thm_info, ((i+1, idx'), (consts', subs'))) end |
117 in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end |
110 in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end |
118 |
111 |
119 |
112 |
120 |
113 |
121 (** collecting substitutions **) |
114 (** collecting substitutions **) |
122 |
115 |
123 fun add_relevant_instances known_grounds (Const (c as (n, T))) = |
116 fun exceeded limit = (limit <= 0) |
124 if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I |
117 fun exceeded_limit (limit, _, _) = exceeded limit |
125 else if member (op =) (Symtab.lookup_list known_grounds n) T then I |
118 |
126 else Symtab.insert_list (op =) c |
119 |
127 | add_relevant_instances _ _ = I |
120 fun with_all_grounds cx grounds f = |
128 |
121 if exceeded_limit cx then I else Symtab.fold f grounds |
129 fun collect_instances known_grounds thm = |
122 |
130 Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm) |
123 fun with_all_type_combinations cx schematics f (n, Ts) = |
131 |
124 if exceeded_limit cx then I |
132 |
125 else fold_product f (Symtab.lookup_list schematics n) Ts |
133 fun exceeded_limit (limit, _, _) = (limit <= 0) |
126 |
134 |
127 fun derive_new_substs thy cx new_grounds schematics subst = |
135 fun with_substs index f (limit, substitutions, next_grounds) = |
128 with_all_grounds cx new_grounds |
136 let |
129 (with_all_type_combinations cx schematics (fn T => fn U => |
137 val substs = Inttab.lookup_list substitutions index |
130 (case try (Sign.typ_match thy (T, U)) subst of |
138 val (limit', substs', next_grounds') = f (limit, substs, next_grounds) |
131 NONE => I |
139 in (limit', Inttab.update (index, substs') substitutions, next_grounds') end |
132 | SOME subst' => cons subst'))) [] |
140 |
133 |
141 fun with_grounds grounds f cx = |
134 |
142 if exceeded_limit cx then cx else Symtab.fold f grounds cx |
135 fun same_subst subst' (_, subst) = subst' |> Vartab.forall (fn (n, (_, T)) => |
143 |
136 Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) |
144 fun with_all_combinations schematics f (n, Ts) cx = |
137 |
145 if exceeded_limit cx then cx |
138 fun known_subst sub subs1 subs2 subst = |
146 else fold_product f (Symtab.lookup_list schematics n) Ts cx |
139 same_subst subst sub orelse exists (same_subst subst) subs1 orelse |
147 |
140 exists (same_subst subst) subs2 |
148 fun with_partial_substs f T U (cx as (limit, substs, next_grounds)) = |
141 |
149 if exceeded_limit cx then cx |
142 fun within_limit f cx = if exceeded_limit cx then cx else f cx |
150 else fold_env (f (T, U)) substs (limit, [], next_grounds) |
143 |
151 |
144 fun fold_partial_substs derive add = within_limit ( |
152 |
145 let |
153 fun same_subst subst = |
146 fun fold_partial [] cx = cx |
154 Vartab.forall (fn (n, (_, T)) => |
147 | fold_partial (sub :: subs) (limit, subs', next) = |
155 Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) |
148 if exceeded limit then (limit, sub :: subs @ subs', next) |
156 |
149 else sub |> (fn ((generation, full, _), subst) => |
157 (* FIXME: necessary? would it have an impact? |
150 if full then fold_partial subs (limit, sub :: subs', next) |
158 comparing substitutions can be tricky ... *) |
151 else |
159 fun known substs1 substs2 subst = false |
152 (case filter_out (known_subst sub subs subs') (derive subst) of |
160 |
153 [] => fold_partial subs (limit, sub :: subs', next) |
161 fun refine ctxt known_grounds new_grounds info = |
154 | substs => |
|
155 (limit, ((generation, full, true), subst) :: subs', next) |
|
156 |> fold (within_limit o add) substs |
|
157 |> fold_partial subs)) |
|
158 in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end) |
|
159 |
|
160 |
|
161 fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx = |
162 let |
162 let |
163 val thy = Proof_Context.theory_of ctxt |
163 val thy = Proof_Context.theory_of ctxt |
164 val count_partial = Config.get ctxt complete_instances |
164 val count_partial = Config.get ctxt complete_instances |
165 val (round, index, _, tvars, schematics) = info |
|
166 |
|
167 fun refine_subst TU = try (Sign.typ_match thy TU) |
|
168 |
165 |
169 fun add_new_ground subst n T = |
166 fun add_new_ground subst n T = |
170 let val T' = Envir.subst_type subst T |
167 let val T' = Envir.subst_type subst T |
171 in |
168 in |
172 (* FIXME: maybe keep types in a table or net for known_grounds, |
169 (* FIXME: maybe keep types in a table or net for known_grounds, |
173 that might improve efficiency here |
170 that might improve efficiency here |
174 *) |
171 *) |
175 if member (op =) (Symtab.lookup_list known_grounds n) T' then I |
172 if typ_has_tvars T' then I |
|
173 else if member (op =) (Symtab.lookup_list known_grounds n) T' then I |
176 else Symtab.cons_list (n, T') |
174 else Symtab.cons_list (n, T') |
177 end |
175 end |
178 |
176 |
179 fun refine_step subst limit next_grounds substs = |
177 fun add_new_subst subst (limit, subs, next_grounds) = |
180 let |
178 let |
181 val full = forall (Vartab.defined subst o fst) tvars |
179 val full = forall (Vartab.defined subst o fst) tvars |
182 val limit' = |
180 val limit' = |
183 if full orelse count_partial then limit - 1 else limit |
181 if full orelse count_partial then limit - 1 else limit |
184 val sub = ((round, full, false), subst) |
182 val sub = ((round, full, false), subst) |
185 val next_grounds' = |
183 val next_grounds' = |
186 (schematics, next_grounds) |
184 (schematics, next_grounds) |
187 |-> Symtab.fold (uncurry (fold o add_new_ground subst)) |
185 |-> Symtab.fold (uncurry (fold o add_new_ground subst)) |
188 in (limit', sub :: substs, next_grounds') end |
186 in (limit', sub :: subs, next_grounds') end |
189 |
|
190 fun refine_substs TU substs sub (cx as (limit, substs', next_grounds)) = |
|
191 let val ((generation, full, _), subst) = sub |
|
192 in |
|
193 if exceeded_limit cx orelse full then |
|
194 (limit, sub :: substs', next_grounds) |
|
195 else |
|
196 (case refine_subst TU subst of |
|
197 NONE => (limit, sub :: substs', next_grounds) |
|
198 | SOME subst' => |
|
199 if (same_subst subst orf known substs substs') subst' then |
|
200 (limit, sub :: substs', next_grounds) |
|
201 else |
|
202 substs' |
|
203 |> cons ((generation, full, true), subst) |
|
204 |> refine_step subst' limit next_grounds) |
|
205 end |
|
206 in |
187 in |
207 with_substs index ( |
188 fold_partial_substs (derive_new_substs thy cx new_grounds schematics) |
208 with_grounds new_grounds (with_all_combinations schematics ( |
189 add_new_subst cx |
209 with_partial_substs refine_substs))) |
|
210 end |
190 end |
|
191 |
|
192 |
|
193 (* |
|
194 'known_grounds' are all constant names known to occur schematically |
|
195 associated with all ground instances considered so far |
|
196 *) |
|
197 fun add_relevant_instances known_grounds (Const (c as (n, T))) = |
|
198 if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I |
|
199 else if member (op =) (Symtab.lookup_list known_grounds n) T then I |
|
200 else Symtab.insert_list (op =) c |
|
201 | add_relevant_instances _ _ = I |
|
202 |
|
203 fun collect_instances known_grounds thm = |
|
204 Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm) |
211 |
205 |
212 |
206 |
213 fun make_subst_ctxt ctxt thm_infos known_grounds substitutions = |
207 fun make_subst_ctxt ctxt thm_infos known_grounds substitutions = |
214 let |
208 let |
215 val limit = Config.get ctxt max_new_instances |
209 val limit = Config.get ctxt max_new_instances |
217 fun add_ground_consts (Ground thm) = collect_instances known_grounds thm |
211 fun add_ground_consts (Ground thm) = collect_instances known_grounds thm |
218 | add_ground_consts (Schematic _) = I |
212 | add_ground_consts (Schematic _) = I |
219 val initial_grounds = fold add_ground_consts thm_infos Symtab.empty |
213 val initial_grounds = fold add_ground_consts thm_infos Symtab.empty |
220 in (known_grounds, (limit, substitutions, initial_grounds)) end |
214 in (known_grounds, (limit, substitutions, initial_grounds)) end |
221 |
215 |
222 fun with_new round f thm_info = |
216 fun is_new round initial_round = (round = initial_round) |
223 (case thm_info of |
217 fun is_active round initial_round = (round > initial_round) |
|
218 |
|
219 fun fold_schematic pred f = fold (fn |
224 Schematic {index, theorem, tvars, schematics, initial_round} => |
220 Schematic {index, theorem, tvars, schematics, initial_round} => |
225 if initial_round <> round then I |
221 if pred initial_round then f theorem (index, tvars, schematics) else I |
226 else f (round, index, theorem, tvars, schematics) |
|
227 | Ground _ => I) |
222 | Ground _ => I) |
228 |
223 |
229 fun with_active round f thm_info = |
224 fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) = |
230 (case thm_info of |
225 let |
231 Schematic {index, theorem, tvars, schematics, initial_round} => |
226 val (limit', isubs', next_grounds') = |
232 if initial_round < round then I |
227 (limit, Inttab.lookup_list subs index, next_grounds) |
233 else f (round, index, theorem, tvars, schematics) |
228 |> f (tvars, schematics) |
234 | Ground _ => I) |
229 in (limit', Inttab.update (index, isubs') subs, next_grounds') end |
235 |
230 |
236 fun collect_substitutions thm_infos ctxt round (known_grounds, subst_ctxt) = |
231 fun collect_substitutions thm_infos ctxt round subst_ctxt = |
237 let val (limit, substitutions, next_grounds) = subst_ctxt |
232 let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt |
238 in |
233 in |
239 (* |
234 if exceeded limit then subst_ctxt |
240 'known_grounds' are all constant names known to occur schematically |
|
241 associated with all ground instances considered so far |
|
242 *) |
|
243 if exceeded_limit subst_ctxt then (true, (known_grounds, subst_ctxt)) |
|
244 else |
235 else |
245 let |
236 let |
246 fun collect (_, _, thm, _, _) = collect_instances known_grounds thm |
237 fun collect thm _ = collect_instances known_grounds thm |
247 val new = fold (with_new round collect) thm_infos next_grounds |
238 val new = fold_schematic (is_new round) collect thm_infos next_grounds |
|
239 |
248 val known' = Symtab.merge_list (op =) (known_grounds, new) |
240 val known' = Symtab.merge_list (op =) (known_grounds, new) |
|
241 val step = focus o refine ctxt round known' |
249 in |
242 in |
250 if Symtab.is_empty new then (true, (known_grounds, subst_ctxt)) |
243 (limit, subs, Symtab.empty) |
251 else |
244 |> not (Symtab.is_empty new) ? |
252 (limit, substitutions, Symtab.empty) |
245 fold_schematic (is_active round) (step new) thm_infos |
253 |> fold (with_active round (refine ctxt known_grounds new)) thm_infos |
246 |> fold_schematic (is_new round) (step known') thm_infos |
254 |> fold (with_new round (refine ctxt Symtab.empty known')) thm_infos |
247 |> pair known' |
255 |> pair false o pair known' |
|
256 end |
248 end |
257 end |
249 end |
258 |
250 |
259 |
251 |
260 |
252 |
288 if full then SOME (generation, f subst) |
280 if full then SOME (generation, f subst) |
289 else Option.map (pair generation o f o complete tvars subst) mT |
281 else Option.map (pair generation o f o complete tvars subst) mT |
290 |
282 |
291 fun inst (Ground thm) = [(0, thm)] |
283 fun inst (Ground thm) = [(0, thm)] |
292 | inst (Schematic {theorem, tvars, index, ...}) = |
284 | inst (Schematic {theorem, tvars, index, ...}) = |
293 Inttab.lookup_list substitutions index |
285 Inttab.lookup_list subs index |
294 |> map_filter (with_subst tvars (instantiate theorem)) |
286 |> map_filter (with_subst tvars (instantiate theorem)) |
295 in (map inst thm_infos, ctxt) end |
287 in (map inst thm_infos, ctxt) end |
296 |
288 |
297 fun instantiate_all ctxt thm_infos (_, (_, substitutions, _)) = |
289 fun instantiate_all ctxt thm_infos (_, (_, subs, _)) = |
298 if Config.get ctxt complete_instances then |
290 if Config.get ctxt complete_instances then |
299 let |
291 let fun is_refined ((_, _, refined), _) = refined |
300 fun refined ((_, _, true), _) = true |
|
301 | refined _ = false |
|
302 in |
292 in |
303 (Inttab.map (K (filter_out refined)) substitutions, thm_infos) |
293 (Inttab.map (K (filter_out is_refined)) subs, thm_infos) |
304 |-> instantiate_all' (new_super_type ctxt thm_infos) |
294 |-> instantiate_all' (new_super_type ctxt thm_infos) |
305 end |
295 end |
306 else instantiate_all' (NONE, ctxt) substitutions thm_infos |
296 else instantiate_all' (NONE, ctxt) subs thm_infos |
307 |
297 |
308 |
298 |
309 |
299 |
310 (** overall procedure **) |
300 (** overall procedure **) |
311 |
301 |
312 fun limit_rounds ctxt f = |
302 fun limit_rounds ctxt f = |
313 let |
303 let |
314 val max = Config.get ctxt max_rounds |
304 val max = Config.get ctxt max_rounds |
315 |
305 fun round i x = if i > max then x else round (i + 1) (f ctxt i x) |
316 fun round _ (true, x) = x |
306 in round 1 end |
317 | round i (_, x) = |
|
318 if i <= max then round (i + 1) (f ctxt i x) |
|
319 else ( |
|
320 show_info ctxt "Warning: Monomorphization limit reached"; |
|
321 x) |
|
322 in round 1 o pair false end |
|
323 |
307 |
324 fun monomorph schematic_consts_of rthms ctxt = |
308 fun monomorph schematic_consts_of rthms ctxt = |
325 let |
309 let |
326 val (thm_infos, (known_grounds, substitutions)) = |
310 val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms |
327 prepare schematic_consts_of rthms |
|
328 in |
311 in |
329 if Symtab.is_empty known_grounds then |
312 if Symtab.is_empty known_grounds then |
330 (map (single o pair 0 o snd) rthms, ctxt) |
313 (map (single o pair 0 o snd) rthms, ctxt) |
331 else |
314 else |
332 make_subst_ctxt ctxt thm_infos known_grounds substitutions |
315 make_subst_ctxt ctxt thm_infos known_grounds subs |
333 |> limit_rounds ctxt (collect_substitutions thm_infos) |
316 |> limit_rounds ctxt (collect_substitutions thm_infos) |
334 |> instantiate_all ctxt thm_infos |
317 |> instantiate_all ctxt thm_infos |
335 end |
318 end |
336 |
319 |
337 |
320 |