author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 51575 | 907efc894051 |
child 53480 | 247817dbb990 |
permissions | -rw-r--r-- |
43107 | 1 |
(* Title: HOL/Tools/monomorph.ML |
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
3 |
|
51575 | 4 |
Monomorphization of theorems, i.e., computation of ground instances for |
5 |
theorems with type variables. This procedure is incomplete in general, |
|
6 |
but works well for most practical problems. |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
7 |
|
51575 | 8 |
Monomorphization is essentially an enumeration of substitutions that map |
9 |
schematic types to ground types. Applying these substitutions to theorems |
|
10 |
with type variables results in monomorphized ground instances. The |
|
11 |
enumeration is driven by schematic constants (constants occurring with |
|
12 |
type variables) and all ground instances of such constants (occurrences |
|
13 |
without type variables). The enumeration is organized in rounds in which |
|
14 |
all substitutions for the schematic constants are computed that are induced |
|
15 |
by the ground instances. Any new ground instance may induce further |
|
16 |
substitutions in a subsequent round. To prevent nontermination, there is |
|
17 |
an upper limit of rounds involved and of the number of monomorphized ground |
|
18 |
instances computed. |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
19 |
|
51575 | 20 |
Theorems to be monomorphized must be tagged with a number indicating the |
21 |
initial round in which they participate first. The initial round is |
|
22 |
ignored for theorems without type variables. For any other theorem, the |
|
23 |
initial round must be greater than zero. Returned monomorphized theorems |
|
24 |
carry a number showing from which monomorphization round they emerged. |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
25 |
*) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
26 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
27 |
signature MONOMORPH = |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
28 |
sig |
51575 | 29 |
(* utility functions *) |
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
30 |
val typ_has_tvars: typ -> bool |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
31 |
val all_schematic_consts_of: term -> typ list Symtab.table |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
32 |
val add_schematic_consts_of: term -> typ list Symtab.table -> |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
33 |
typ list Symtab.table |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
34 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
35 |
(* configuration options *) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
36 |
val max_rounds: int Config.T |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
37 |
val max_new_instances: int Config.T |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
38 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
39 |
(* monomorphization *) |
51575 | 40 |
val monomorph: (term -> typ list Symtab.table) -> Proof.context -> |
41 |
(int * thm) list -> (int * thm) list list |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
42 |
end |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
43 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
44 |
structure Monomorph: MONOMORPH = |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
45 |
struct |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
46 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
47 |
(* utility functions *) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
48 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
49 |
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
50 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
51 |
fun add_schematic_const (c as (_, T)) = |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
52 |
if typ_has_tvars T then Symtab.insert_list (op =) c else I |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
53 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
54 |
fun add_schematic_consts_of t = |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
55 |
Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
56 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
57 |
fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
58 |
|
51575 | 59 |
fun clear_grounds grounds = Symtab.map (K (K [])) grounds |
60 |
||
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
61 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
62 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
63 |
(* configuration options *) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
64 |
|
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
65 |
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5) |
51575 | 66 |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
67 |
val max_new_instances = |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
68 |
Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300) |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
69 |
|
43116 | 70 |
fun limit_rounds ctxt f = |
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
71 |
let |
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
72 |
val max = Config.get ctxt max_rounds |
43117 | 73 |
fun round i x = if i > max then x else round (i + 1) (f ctxt i x) |
74 |
in round 1 end |
|
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
75 |
|
51575 | 76 |
fun reached_limit ctxt n = (n >= Config.get ctxt max_new_instances) |
77 |
||
78 |
||
79 |
||
80 |
(* theorem information and related functions *) |
|
81 |
||
82 |
datatype thm_info = |
|
83 |
Ground of thm | |
|
84 |
Ignored | |
|
85 |
Schematic of { |
|
86 |
id: int, |
|
87 |
theorem: thm, |
|
88 |
tvars: (indexname * sort) list, |
|
89 |
schematics: (string * typ) list, |
|
90 |
initial_round: int} |
|
91 |
||
92 |
||
93 |
fun fold_grounds f = fold (fn Ground thm => f thm | _ => I) |
|
94 |
||
95 |
||
96 |
fun fold_schematic f thm_info = |
|
97 |
(case thm_info of |
|
98 |
Schematic {id, theorem, tvars, schematics, initial_round} => |
|
99 |
f id theorem tvars schematics initial_round |
|
100 |
| _ => I) |
|
101 |
||
102 |
||
103 |
fun fold_schematics pred f = |
|
104 |
let |
|
105 |
fun apply id thm tvars schematics initial_round x = |
|
106 |
if pred initial_round then f id thm tvars schematics x else x |
|
107 |
in fold (fold_schematic apply) end |
|
108 |
||
109 |
||
110 |
||
111 |
(* collecting data *) |
|
112 |
||
113 |
(* |
|
114 |
Theorems with type variables that cannot be instantiated should be ignored. |
|
115 |
A type variable has only a chance to be instantiated if it occurs in the |
|
116 |
type of one of the schematic constants. |
|
117 |
*) |
|
118 |
fun groundable all_tvars schematics = |
|
119 |
let val tvars' = Symtab.fold (fold Term.add_tvarsT o snd) schematics [] |
|
120 |
in forall (member (op =) tvars') all_tvars end |
|
121 |
||
122 |
||
123 |
fun prepare schematic_consts_of rthms = |
|
43116 | 124 |
let |
51575 | 125 |
fun prep (initial_round, thm) ((id, idx), consts) = |
126 |
if Term.exists_type typ_has_tvars (Thm.prop_of thm) then |
|
127 |
let |
|
128 |
(* increase indices to avoid clashes of type variables *) |
|
129 |
val thm' = Thm.incr_indexes idx thm |
|
130 |
val idx' = Thm.maxidx_of thm' + 1 |
|
131 |
||
132 |
val tvars = Term.add_tvars (Thm.prop_of thm') [] |
|
133 |
val schematics = schematic_consts_of (Thm.prop_of thm') |
|
134 |
val schematics' = |
|
135 |
Symtab.fold (fn (n, Ts) => fold (cons o pair n) Ts) schematics [] |
|
136 |
||
137 |
(* collect the names of all constants that need to be instantiated *) |
|
138 |
val consts' = |
|
139 |
consts |
|
140 |
|> Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics |
|
141 |
||
142 |
val thm_info = |
|
143 |
if not (groundable tvars schematics) then Ignored |
|
144 |
else |
|
145 |
Schematic { |
|
146 |
id = id, |
|
147 |
theorem = thm', |
|
148 |
tvars = tvars, |
|
149 |
schematics = schematics', |
|
150 |
initial_round = initial_round} |
|
151 |
in (thm_info, ((id + 1, idx'), consts')) end |
|
152 |
else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts)) |
|
153 |
||
154 |
in fold_map prep rthms ((0, 0), Symtab.empty) ||> snd end |
|
155 |
||
156 |
||
157 |
||
158 |
(* collecting instances *) |
|
159 |
||
160 |
fun instantiate thy subst = |
|
161 |
let |
|
162 |
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) |
|
163 |
fun cert' subst = Vartab.fold (cons o cert) subst [] |
|
164 |
in Thm.instantiate (cert' subst, []) end |
|
165 |
||
166 |
||
167 |
fun add_new_grounds used_grounds new_grounds thm = |
|
168 |
let |
|
169 |
fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T |
|
170 |
fun add (Const (c as (n, _))) = |
|
171 |
if mem used_grounds c orelse mem new_grounds c then I |
|
172 |
else if not (Symtab.defined used_grounds n) then I |
|
173 |
else Symtab.insert_list (op =) c |
|
174 |
| add _ = I |
|
175 |
in Term.fold_aterms add (Thm.prop_of thm) end |
|
176 |
||
177 |
||
178 |
fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx = |
|
179 |
let |
|
180 |
exception ENOUGH of |
|
181 |
typ list Symtab.table * (int * (int * thm) list Inttab.table) |
|
182 |
||
183 |
val thy = Proof_Context.theory_of ctxt |
|
184 |
||
185 |
fun add subst (next_grounds, (n, insts)) = |
|
186 |
let |
|
187 |
val thm' = instantiate thy subst thm |
|
188 |
val rthm = (round, thm') |
|
189 |
val n_insts' = |
|
190 |
if member (eq_snd Thm.eq_thm) (Inttab.lookup_list insts id) rthm then |
|
191 |
(n, insts) |
|
192 |
else (n + 1, Inttab.cons_list (id, rthm) insts) |
|
193 |
val next_grounds' = |
|
194 |
add_new_grounds used_grounds new_grounds thm' next_grounds |
|
195 |
val cx' = (next_grounds', n_insts') |
|
196 |
in if reached_limit ctxt n then raise ENOUGH cx' else cx' end |
|
197 |
||
198 |
fun with_grounds (n, T) f subst (n', Us) = |
|
199 |
let |
|
200 |
fun matching U = (* one-step refinement of the given substitution *) |
|
201 |
(case try (Sign.typ_match thy (T, U)) subst of |
|
202 |
NONE => I |
|
203 |
| SOME subst' => f subst') |
|
204 |
in if n = n' then fold matching Us else I end |
|
205 |
||
206 |
fun with_matching_ground c subst f = |
|
207 |
(* Try new grounds before already used grounds. Otherwise only |
|
208 |
substitutions already seen in previous rounds get enumerated. *) |
|
209 |
Symtab.fold (with_grounds c (f true) subst) new_grounds #> |
|
210 |
Symtab.fold (with_grounds c (f false) subst) used_grounds |
|
211 |
||
212 |
fun is_complete subst = |
|
213 |
(* Check if a substitution is defined for all TVars of the theorem, |
|
214 |
which guarantees that the instantiation with this substitution results |
|
215 |
in a ground theorem since all matchings that led to this substitution |
|
216 |
are with ground types only. *) |
|
217 |
subset (op =) (tvars, Vartab.fold (cons o apsnd fst) subst []) |
|
218 |
||
219 |
fun for_schematics _ [] _ = I |
|
220 |
| for_schematics used_new (c :: cs) subst = |
|
221 |
with_matching_ground c subst (fn new => fn subst' => |
|
222 |
if is_complete subst' then |
|
223 |
if used_new orelse new then add subst' |
|
224 |
else I |
|
225 |
else for_schematics (used_new orelse new) cs subst') #> |
|
226 |
for_schematics used_new cs subst |
|
43116 | 227 |
in |
51575 | 228 |
(* Enumerate all substitutions that lead to a ground instance of the |
229 |
theorem not seen before. A necessary condition for such a new ground |
|
230 |
instance is the usage of at least one ground from the new_grounds |
|
231 |
table. The approach used here is to match all schematics of the theorem |
|
232 |
with all relevant grounds. *) |
|
233 |
for_schematics false schematics Vartab.empty cx |
|
234 |
handle ENOUGH cx' => cx' |
|
43116 | 235 |
end |
236 |
||
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
237 |
|
51575 | 238 |
fun is_new round initial_round = (round = initial_round) |
239 |
fun is_active round initial_round = (round > initial_round) |
|
240 |
||
241 |
||
242 |
fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) = |
|
243 |
let |
|
244 |
val add_new = add_insts ctxt round |
|
245 |
fun consider_all pred f (cx as (_, (n, _))) = |
|
246 |
if reached_limit ctxt n then cx |
|
247 |
else fold_schematics pred f thm_infos cx |
|
248 |
||
249 |
val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds) |
|
250 |
val empty_grounds = clear_grounds known_grounds' |
|
251 |
||
252 |
val (new_grounds', insts') = |
|
253 |
(Symtab.empty, insts) |
|
254 |
|> consider_all (is_active round) (add_new known_grounds new_grounds) |
|
255 |
|> consider_all (is_new round) (add_new empty_grounds known_grounds') |
|
256 |
||
257 |
in (known_grounds', new_grounds', insts') end |
|
258 |
||
259 |
||
260 |
fun add_ground_types thm = |
|
261 |
let fun add (n, T) = Symtab.map_entry n (insert (op =) T) |
|
262 |
in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end |
|
263 |
||
264 |
||
265 |
fun collect_instances ctxt thm_infos consts = |
|
266 |
let |
|
267 |
val known_grounds = fold_grounds add_ground_types thm_infos consts |
|
268 |
val empty_grounds = clear_grounds known_grounds |
|
269 |
in |
|
270 |
(empty_grounds, known_grounds, (0, Inttab.empty)) |
|
271 |
|> limit_rounds ctxt (find_instances thm_infos) |
|
272 |
|> (fn (_, _, (_, insts)) => insts) |
|
273 |
end |
|
274 |
||
275 |
||
276 |
||
277 |
(* monomorphization *) |
|
278 |
||
279 |
fun instantiated_thms _ (Ground thm) = [(0, thm)] |
|
280 |
| instantiated_thms _ Ignored = [] |
|
281 |
| instantiated_thms insts (Schematic {id, ...}) = Inttab.lookup_list insts id |
|
282 |
||
283 |
||
284 |
fun monomorph schematic_consts_of ctxt rthms = |
|
285 |
let |
|
286 |
val (thm_infos, consts) = prepare schematic_consts_of rthms |
|
287 |
val insts = |
|
288 |
if Symtab.is_empty consts then Inttab.empty |
|
289 |
else collect_instances ctxt thm_infos consts |
|
290 |
in map (instantiated_thms insts) thm_infos end |
|
291 |
||
43041
218e3943d504
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff
changeset
|
292 |
end |