author | blanchet |
Mon, 09 Sep 2013 18:12:41 +0200 | |
changeset 53481 | 0721fc9d0fe7 |
parent 53480 | 247817dbb990 |
child 53482 | 662149d02915 |
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 |
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
38 |
val max_thm_instances: int Config.T |
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
|
39 |
|
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
|
40 |
(* monomorphization *) |
51575 | 41 |
val monomorph: (term -> typ list Symtab.table) -> Proof.context -> |
42 |
(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
|
43 |
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
|
44 |
|
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 |
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
|
46 |
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
|
47 |
|
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 |
(* 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
|
49 |
|
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 |
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
|
51 |
|
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 |
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
|
53 |
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
|
54 |
|
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 |
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
|
56 |
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
|
57 |
|
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 |
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
|
59 |
|
51575 | 60 |
fun clear_grounds grounds = Symtab.map (K (K [])) grounds |
61 |
||
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
|
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 |
|
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 |
(* 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
|
65 |
|
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
|
66 |
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5) |
51575 | 67 |
|
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
|
68 |
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
|
69 |
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
|
70 |
|
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
71 |
val max_thm_instances = |
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
72 |
Attrib.setup_config_int @{binding max_thm_instances} (K 20) |
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
73 |
|
43116 | 74 |
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
|
75 |
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
|
76 |
val max = Config.get ctxt max_rounds |
43117 | 77 |
fun round i x = if i > max then x else round (i + 1) (f ctxt i x) |
78 |
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
|
79 |
|
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
80 |
fun reached_thm_instance_limit ctxt n = |
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
51575
diff
changeset
|
81 |
n >= Config.get ctxt max_thm_instances |
51575 | 82 |
|
83 |
||
84 |
||
85 |
(* theorem information and related functions *) |
|
86 |
||
87 |
datatype thm_info = |
|
88 |
Ground of thm | |
|
89 |
Ignored | |
|
90 |
Schematic of { |
|
91 |
id: int, |
|
92 |
theorem: thm, |
|
93 |
tvars: (indexname * sort) list, |
|
94 |
schematics: (string * typ) list, |
|
95 |
initial_round: int} |
|
96 |
||
97 |
||
98 |
fun fold_grounds f = fold (fn Ground thm => f thm | _ => I) |
|
99 |
||
100 |
||
101 |
fun fold_schematic f thm_info = |
|
102 |
(case thm_info of |
|
103 |
Schematic {id, theorem, tvars, schematics, initial_round} => |
|
104 |
f id theorem tvars schematics initial_round |
|
105 |
| _ => I) |
|
106 |
||
107 |
||
108 |
fun fold_schematics pred f = |
|
109 |
let |
|
110 |
fun apply id thm tvars schematics initial_round x = |
|
111 |
if pred initial_round then f id thm tvars schematics x else x |
|
112 |
in fold (fold_schematic apply) end |
|
113 |
||
114 |
||
115 |
||
116 |
(* collecting data *) |
|
117 |
||
118 |
(* |
|
119 |
Theorems with type variables that cannot be instantiated should be ignored. |
|
120 |
A type variable has only a chance to be instantiated if it occurs in the |
|
121 |
type of one of the schematic constants. |
|
122 |
*) |
|
123 |
fun groundable all_tvars schematics = |
|
124 |
let val tvars' = Symtab.fold (fold Term.add_tvarsT o snd) schematics [] |
|
125 |
in forall (member (op =) tvars') all_tvars end |
|
126 |
||
127 |
||
128 |
fun prepare schematic_consts_of rthms = |
|
43116 | 129 |
let |
51575 | 130 |
fun prep (initial_round, thm) ((id, idx), consts) = |
131 |
if Term.exists_type typ_has_tvars (Thm.prop_of thm) then |
|
132 |
let |
|
133 |
(* increase indices to avoid clashes of type variables *) |
|
134 |
val thm' = Thm.incr_indexes idx thm |
|
135 |
val idx' = Thm.maxidx_of thm' + 1 |
|
136 |
||
137 |
val tvars = Term.add_tvars (Thm.prop_of thm') [] |
|
138 |
val schematics = schematic_consts_of (Thm.prop_of thm') |
|
139 |
val schematics' = |
|
140 |
Symtab.fold (fn (n, Ts) => fold (cons o pair n) Ts) schematics [] |
|
141 |
||
142 |
(* collect the names of all constants that need to be instantiated *) |
|
143 |
val consts' = |
|
144 |
consts |
|
145 |
|> Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics |
|
146 |
||
147 |
val thm_info = |
|
148 |
if not (groundable tvars schematics) then Ignored |
|
149 |
else |
|
150 |
Schematic { |
|
151 |
id = id, |
|
152 |
theorem = thm', |
|
153 |
tvars = tvars, |
|
154 |
schematics = schematics', |
|
155 |
initial_round = initial_round} |
|
156 |
in (thm_info, ((id + 1, idx'), consts')) end |
|
157 |
else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts)) |
|
158 |
||
159 |
in fold_map prep rthms ((0, 0), Symtab.empty) ||> snd end |
|
160 |
||
161 |
||
162 |
||
163 |
(* collecting instances *) |
|
164 |
||
165 |
fun instantiate thy subst = |
|
166 |
let |
|
167 |
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) |
|
168 |
fun cert' subst = Vartab.fold (cons o cert) subst [] |
|
169 |
in Thm.instantiate (cert' subst, []) end |
|
170 |
||
171 |
||
172 |
fun add_new_grounds used_grounds new_grounds thm = |
|
173 |
let |
|
174 |
fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T |
|
175 |
fun add (Const (c as (n, _))) = |
|
176 |
if mem used_grounds c orelse mem new_grounds c then I |
|
177 |
else if not (Symtab.defined used_grounds n) then I |
|
178 |
else Symtab.insert_list (op =) c |
|
179 |
| add _ = I |
|
180 |
in Term.fold_aterms add (Thm.prop_of thm) end |
|
181 |
||
182 |
||
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
183 |
fun add_insts max_instances ctxt round used_grounds new_grounds id thm tvars |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
184 |
schematics cx = |
51575 | 185 |
let |
186 |
exception ENOUGH of |
|
187 |
typ list Symtab.table * (int * (int * thm) list Inttab.table) |
|
188 |
||
189 |
val thy = Proof_Context.theory_of ctxt |
|
190 |
||
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
191 |
fun add subst (cx as (next_grounds, (n, insts))) = |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
192 |
if n >= max_instances then |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
193 |
raise ENOUGH cx |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
194 |
else |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
195 |
let |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
196 |
val thm' = instantiate thy subst thm |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
197 |
val rthm = (round, thm') |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
198 |
val rthms = Inttab.lookup_list insts id; |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
199 |
val n_insts' = |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
200 |
if member (eq_snd Thm.eq_thm) rthms rthm orelse |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
201 |
reached_thm_instance_limit ctxt (length rthms) then |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
202 |
(n, insts) |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
203 |
else |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
204 |
(n + 1, Inttab.cons_list (id, rthm) insts) |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
205 |
val next_grounds' = |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
206 |
add_new_grounds used_grounds new_grounds thm' next_grounds |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
207 |
in (next_grounds', n_insts') end |
51575 | 208 |
|
209 |
fun with_grounds (n, T) f subst (n', Us) = |
|
210 |
let |
|
211 |
fun matching U = (* one-step refinement of the given substitution *) |
|
212 |
(case try (Sign.typ_match thy (T, U)) subst of |
|
213 |
NONE => I |
|
214 |
| SOME subst' => f subst') |
|
215 |
in if n = n' then fold matching Us else I end |
|
216 |
||
217 |
fun with_matching_ground c subst f = |
|
218 |
(* Try new grounds before already used grounds. Otherwise only |
|
219 |
substitutions already seen in previous rounds get enumerated. *) |
|
220 |
Symtab.fold (with_grounds c (f true) subst) new_grounds #> |
|
221 |
Symtab.fold (with_grounds c (f false) subst) used_grounds |
|
222 |
||
223 |
fun is_complete subst = |
|
224 |
(* Check if a substitution is defined for all TVars of the theorem, |
|
225 |
which guarantees that the instantiation with this substitution results |
|
226 |
in a ground theorem since all matchings that led to this substitution |
|
227 |
are with ground types only. *) |
|
228 |
subset (op =) (tvars, Vartab.fold (cons o apsnd fst) subst []) |
|
229 |
||
230 |
fun for_schematics _ [] _ = I |
|
231 |
| for_schematics used_new (c :: cs) subst = |
|
232 |
with_matching_ground c subst (fn new => fn subst' => |
|
233 |
if is_complete subst' then |
|
234 |
if used_new orelse new then add subst' |
|
235 |
else I |
|
236 |
else for_schematics (used_new orelse new) cs subst') #> |
|
237 |
for_schematics used_new cs subst |
|
43116 | 238 |
in |
51575 | 239 |
(* Enumerate all substitutions that lead to a ground instance of the |
240 |
theorem not seen before. A necessary condition for such a new ground |
|
241 |
instance is the usage of at least one ground from the new_grounds |
|
242 |
table. The approach used here is to match all schematics of the theorem |
|
243 |
with all relevant grounds. *) |
|
244 |
for_schematics false schematics Vartab.empty cx |
|
245 |
handle ENOUGH cx' => cx' |
|
43116 | 246 |
end |
247 |
||
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
|
248 |
|
51575 | 249 |
fun is_new round initial_round = (round = initial_round) |
250 |
fun is_active round initial_round = (round > initial_round) |
|
251 |
||
252 |
||
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
253 |
fun find_instances max_instances thm_infos ctxt round |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
254 |
(known_grounds, new_grounds, insts) = |
51575 | 255 |
let |
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
256 |
val add_new = add_insts max_instances ctxt round |
51575 | 257 |
fun consider_all pred f (cx as (_, (n, _))) = |
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
258 |
if n >= max_instances then cx else fold_schematics pred f thm_infos cx |
51575 | 259 |
|
260 |
val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds) |
|
261 |
val empty_grounds = clear_grounds known_grounds' |
|
262 |
||
263 |
val (new_grounds', insts') = |
|
264 |
(Symtab.empty, insts) |
|
265 |
|> consider_all (is_active round) (add_new known_grounds new_grounds) |
|
266 |
|> consider_all (is_new round) (add_new empty_grounds known_grounds') |
|
267 |
||
268 |
in (known_grounds', new_grounds', insts') end |
|
269 |
||
270 |
||
271 |
fun add_ground_types thm = |
|
272 |
let fun add (n, T) = Symtab.map_entry n (insert (op =) T) |
|
273 |
in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end |
|
274 |
||
275 |
||
276 |
fun collect_instances ctxt thm_infos consts = |
|
277 |
let |
|
278 |
val known_grounds = fold_grounds add_ground_types thm_infos consts |
|
279 |
val empty_grounds = clear_grounds known_grounds |
|
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
280 |
val max_instances = |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
281 |
Config.get ctxt max_new_instances |
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
282 |
|> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos |
51575 | 283 |
in |
284 |
(empty_grounds, known_grounds, (0, Inttab.empty)) |
|
53481
0721fc9d0fe7
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
blanchet
parents:
53480
diff
changeset
|
285 |
|> limit_rounds ctxt (find_instances max_instances thm_infos) |
51575 | 286 |
|> (fn (_, _, (_, insts)) => insts) |
287 |
end |
|
288 |
||
289 |
||
290 |
||
291 |
(* monomorphization *) |
|
292 |
||
293 |
fun instantiated_thms _ (Ground thm) = [(0, thm)] |
|
294 |
| instantiated_thms _ Ignored = [] |
|
295 |
| instantiated_thms insts (Schematic {id, ...}) = Inttab.lookup_list insts id |
|
296 |
||
297 |
||
298 |
fun monomorph schematic_consts_of ctxt rthms = |
|
299 |
let |
|
300 |
val (thm_infos, consts) = prepare schematic_consts_of rthms |
|
301 |
val insts = |
|
302 |
if Symtab.is_empty consts then Inttab.empty |
|
303 |
else collect_instances ctxt thm_infos consts |
|
304 |
in map (instantiated_thms insts) thm_infos end |
|
305 |
||
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
|
306 |
end |