author | boehmes |
Fri, 12 Nov 2010 15:56:06 +0100 | |
changeset 40512 | fd218201da5e |
parent 40424 | 7550b2cba1cb |
child 41063 | 0828bfa70b20 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smt_monomorph.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Monomorphization of theorems, i.e., computation of all (necessary) instances. |
|
5 |
*) |
|
6 |
||
7 |
signature SMT_MONOMORPH = |
|
8 |
sig |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
9 |
val monomorph: (int * thm) list -> Proof.context -> |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
10 |
(int * thm) list * Proof.context |
36898 | 11 |
end |
12 |
||
13 |
structure SMT_Monomorph: SMT_MONOMORPH = |
|
14 |
struct |
|
15 |
||
16 |
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false) |
|
17 |
||
18 |
val ignored = member (op =) [ |
|
19 |
@{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If}, |
|
40512
fd218201da5e
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
boehmes
parents:
40424
diff
changeset
|
20 |
@{const_name HOL.eq}] |
36898 | 21 |
|
22 |
fun is_const f (n, T) = not (ignored n) andalso f T |
|
23 |
fun add_const_if f g (Const c) = if is_const f c then g c else I |
|
24 |
| add_const_if _ _ _ = I |
|
25 |
||
26 |
fun collect_consts_if f g thm = |
|
27 |
Term.fold_aterms (add_const_if f g) (Thm.prop_of thm) |
|
28 |
||
29 |
fun add_consts f = |
|
30 |
collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T)) |
|
31 |
||
39687 | 32 |
val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord) |
36898 | 33 |
fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm [] |
34 |
||
35 |
||
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
36 |
fun incr_indexes irules = |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
37 |
let |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
38 |
fun inc (i, thm) idx = |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
39 |
((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1) |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
40 |
in fst (fold_map inc irules 0) end |
36898 | 41 |
|
42 |
||
43 |
(* Compute all substitutions from the types "Ts" to all relevant |
|
44 |
types in "grounds", with respect to the given substitution. *) |
|
45 |
fun new_substitutions thy grounds (n, T) subst = |
|
46 |
if not (typ_has_tvars T) then [subst] |
|
47 |
else |
|
48 |
Symtab.lookup_list grounds n |
|
49 |
|> map_filter (try (fn U => Sign.typ_match thy (T, U) subst)) |
|
50 |
|> cons subst |
|
51 |
||
52 |
||
53 |
(* Instantiate a set of constants with a substitution. Also collect |
|
54 |
all new ground instances for the next round of specialization. *) |
|
55 |
fun apply_subst grounds consts subst = |
|
56 |
let |
|
57 |
fun is_new_ground (n, T) = not (typ_has_tvars T) andalso |
|
58 |
not (member (op =) (Symtab.lookup_list grounds n) T) |
|
59 |
||
60 |
fun apply_const (n, T) new_grounds = |
|
61 |
let val c = (n, Envir.subst_type subst T) |
|
62 |
in |
|
63 |
new_grounds |
|
64 |
|> is_new_ground c ? Symtab.insert_list (op =) c |
|
65 |
|> pair c |
|
66 |
end |
|
67 |
in fold_map apply_const consts #>> pair subst end |
|
68 |
||
69 |
||
70 |
(* Compute new substitutions for the theorem "thm", based on |
|
71 |
previously found substitutions. |
|
72 |
Also collect new grounds, i.e., instantiated constants |
|
73 |
(without schematic types) which do not occur in any of the |
|
74 |
previous rounds. Note that thus no schematic type variables are |
|
75 |
shared among theorems. *) |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
76 |
fun specialize thy all_grounds new_grounds (irule, scs) = |
36898 | 77 |
let |
78 |
fun spec (subst, consts) next_grounds = |
|
79 |
[subst] |
|
80 |
|> fold (maps o new_substitutions thy new_grounds) consts |
|
81 |
|> rpair next_grounds |
|
82 |
|-> fold_map (apply_subst all_grounds consts) |
|
83 |
in |
|
84 |
fold_map spec scs #>> (fn scss => |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
85 |
(irule, fold (fold (insert (eq_snd (op =)))) scss [])) |
36898 | 86 |
end |
87 |
||
88 |
||
89 |
(* Compute all necessary substitutions. |
|
90 |
Instead of operating on the propositions of the theorems, the |
|
91 |
computation uses only the constants occurring with schematic type |
|
92 |
variables in the propositions. To ease comparisons, such sets of |
|
93 |
costants are always kept in their initial order. *) |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
94 |
fun incremental_monomorph ctxt limit all_grounds new_grounds irules = |
36898 | 95 |
let |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
96 |
val thy = ProofContext.theory_of ctxt |
36898 | 97 |
val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds) |
98 |
val spec = specialize thy all_grounds' new_grounds |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
99 |
val (irs, new_grounds') = fold_map spec irules Symtab.empty |
36898 | 100 |
in |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
101 |
if Symtab.is_empty new_grounds' then irs |
36898 | 102 |
else if limit > 0 |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
103 |
then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
104 |
else |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
105 |
(SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached") |
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
106 |
(); irs) |
36898 | 107 |
end |
108 |
||
109 |
||
110 |
fun filter_most_specific thy = |
|
111 |
let |
|
112 |
fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U) |
|
113 |
||
114 |
fun is_trivial subst = Vartab.is_empty subst orelse |
|
115 |
forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst) |
|
116 |
||
117 |
fun match general specific = |
|
118 |
(case try (fold2 typ_match general specific) Vartab.empty of |
|
119 |
NONE => false |
|
120 |
| SOME subst => not (is_trivial subst)) |
|
121 |
||
122 |
fun most_specific _ [] = [] |
|
123 |
| most_specific css ((ss, cs) :: scs) = |
|
124 |
let val substs = most_specific (cs :: css) scs |
|
125 |
in |
|
126 |
if exists (match cs) css orelse exists (match cs o snd) scs |
|
127 |
then substs else ss :: substs |
|
128 |
end |
|
129 |
||
130 |
in most_specific [] end |
|
131 |
||
132 |
||
133 |
fun instantiate thy Tenv = |
|
134 |
let |
|
135 |
fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U |
|
136 |
| replace _ T = T |
|
137 |
||
138 |
fun complete (vT as (v, _)) subst = |
|
139 |
subst |
|
140 |
|> not (Vartab.defined subst v) ? Vartab.update vT |
|
39020 | 141 |
|> Vartab.map (K (apsnd (Term.map_atyps (replace vT)))) |
36898 | 142 |
|
143 |
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) |
|
144 |
||
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
145 |
fun inst (i, thm) subst = |
36898 | 146 |
let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) [] |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
147 |
in (i, Thm.instantiate (cTs, []) thm) end |
36898 | 148 |
|
149 |
in uncurry (map o inst) end |
|
150 |
||
151 |
||
152 |
fun mono_all ctxt _ [] monos = (monos, ctxt) |
|
153 |
| mono_all ctxt limit polys monos = |
|
154 |
let |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
155 |
fun invent_types (_, thm) ctxt = |
36898 | 156 |
let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) |
157 |
in |
|
158 |
ctxt |
|
159 |
|> Variable.invent_types Ss |
|
160 |
|>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs |
|
161 |
end |
|
162 |
val (Tenvs, ctxt') = fold_map invent_types polys ctxt |
|
163 |
||
164 |
val thy = ProofContext.theory_of ctxt' |
|
165 |
||
166 |
val ths = polys |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
167 |
|> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)])) |
36898 | 168 |
|
169 |
(* all constant names occurring with schematic types *) |
|
170 |
val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths [] |
|
171 |
||
172 |
(* all known instances with non-schematic types *) |
|
173 |
val grounds = |
|
174 |
Symtab.make (map (rpair []) ns) |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
175 |
|> fold (add_consts (K true) o snd) monos |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
176 |
|> fold (add_consts (not o typ_has_tvars) o snd) polys |
36898 | 177 |
in |
178 |
polys |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
179 |
|> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)])) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
180 |
|> incremental_monomorph ctxt' limit Symtab.empty grounds |
36898 | 181 |
|> map (apsnd (filter_most_specific thy)) |
182 |
|> flat o map2 (instantiate thy) Tenvs |
|
183 |
|> append monos |
|
184 |
|> rpair ctxt' |
|
185 |
end |
|
186 |
||
187 |
||
188 |
(* Instantiate all polymorphic constants (i.e., constants occurring |
|
189 |
both with ground types and type variables) with all (necessary) |
|
190 |
ground types; thereby create copies of theorems containing those |
|
191 |
constants. |
|
192 |
To prevent non-termination, there is an upper limit for the |
|
193 |
number of recursions involved in the fixpoint construction. |
|
194 |
The initial set of theorems must not contain any schematic term |
|
195 |
variables, and the final list of theorems does not contain any |
|
196 |
schematic type variables anymore. *) |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
197 |
fun monomorph irules ctxt = |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
198 |
irules |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
199 |
|> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd) |
36898 | 200 |
|>> incr_indexes |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40161
diff
changeset
|
201 |
|-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit) |
36898 | 202 |
|
203 |
end |