author | blanchet |
Sun, 02 Feb 2014 20:53:51 +0100 | |
changeset 55243 | 66709d41601e |
parent 55213 | dcb36a2540bc |
child 55286 | 7bbbd9393ce0 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54821
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML |
55212 | 2 |
Author: Steffen Juilf Smolka, TU Muenchen |
50263 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
||
55212 | 5 |
Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints |
6 |
suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it |
|
7 |
incomplete. |
|
52369
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
8 |
|
55212 | 9 |
When configuring the pretty printer appropriately, the constraints will show up as type annotations |
10 |
when printing the term. This allows the term to be printed and reparsed without a change of types. |
|
52369
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
11 |
|
55213 | 12 |
Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax. |
50263 | 13 |
*) |
14 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54821
diff
changeset
|
15 |
signature SLEDGEHAMMER_ISAR_ANNOTATE = |
50258 | 16 |
sig |
55213 | 17 |
val annotate_types_in_term : Proof.context -> term -> term |
54504 | 18 |
end; |
50258 | 19 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54821
diff
changeset
|
20 |
structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE = |
50258 | 21 |
struct |
22 |
||
23 |
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s |
|
24 |
| post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s |
|
25 |
| post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s |
|
26 |
| post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s |
|
27 |
| post_traverse_term_type' f env (Abs (x, T1, b)) s = |
|
55243 | 28 |
let val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s in |
29 |
f (Abs (x, T1, b')) (T1 --> T2) s' |
|
30 |
end |
|
50258 | 31 |
| post_traverse_term_type' f env (u $ v) s = |
32 |
let |
|
33 |
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s |
|
34 |
val ((v', s''), _) = post_traverse_term_type' f env v s' |
|
35 |
in f (u' $ v') T s'' end |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54821
diff
changeset
|
36 |
handle Bind => raise Fail "Sledgehammer_Isar_Annotate: post_traverse_term_type'" |
50258 | 37 |
|
38 |
fun post_traverse_term_type f s t = |
|
39 |
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst |
|
40 |
fun post_fold_term_type f s t = |
|
41 |
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd |
|
42 |
||
52452 | 43 |
fun fold_map_atypes f T s = |
44 |
case T of |
|
45 |
Type (name, Ts) => |
|
46 |
let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in |
|
47 |
(Type (name, Ts), s) |
|
48 |
end |
|
49 |
| _ => f T s |
|
50 |
||
51 |
val indexname_ord = Term_Ord.fast_indexname_ord |
|
50258 | 52 |
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) |
55243 | 53 |
|
50258 | 54 |
structure Var_Set_Tab = Table( |
55 |
type key = indexname list |
|
52452 | 56 |
val ord = list_ord indexname_ord) |
50258 | 57 |
|
58 |
fun generalize_types ctxt t = |
|
52369
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
59 |
let |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
60 |
val erase_types = map_types (fn _ => dummyT) |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
61 |
(* use schematic type variables *) |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
62 |
val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
63 |
val infer_types = singleton (Type_Infer_Context.infer_types ctxt) |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
64 |
in |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
65 |
t |> erase_types |> infer_types |
0b395800fdf0
uncheck terms before annotation to avoid awkward syntax
smolkas
parents:
52366
diff
changeset
|
66 |
end |
50258 | 67 |
|
52452 | 68 |
fun match_types ctxt t1 t2 = |
69 |
let |
|
70 |
val thy = Proof_Context.theory_of ctxt |
|
71 |
val get_types = post_fold_term_type (K cons) [] |
|
72 |
in |
|
73 |
fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
54821
diff
changeset
|
74 |
handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types" |
52452 | 75 |
end |
76 |
||
77 |
fun handle_trivial_tfrees ctxt (t', subst) = |
|
78 |
let |
|
55243 | 79 |
val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I) |
52452 | 80 |
|
81 |
val trivial_tfree_names = |
|
82 |
Vartab.fold add_tfree_names subst [] |
|
83 |
|> filter_out (Variable.is_declared ctxt) |
|
55243 | 84 |
|> distinct (op =) |
52452 | 85 |
val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names |
86 |
||
87 |
val trivial_tvar_names = |
|
88 |
Vartab.fold |
|
89 |
(fn (tvar_name, (_, TFree (tfree_name, _))) => |
|
90 |
tfree_name_trivial tfree_name ? cons tvar_name |
|
91 |
| _ => I) |
|
92 |
subst |
|
93 |
[] |
|
94 |
|> sort indexname_ord |
|
95 |
val tvar_name_trivial = Ord_List.member indexname_ord trivial_tvar_names |
|
96 |
||
97 |
val t' = |
|
98 |
t' |> map_types |
|
99 |
(map_type_tvar |
|
100 |
(fn (idxn, sort) => |
|
101 |
if tvar_name_trivial idxn then dummyT else TVar (idxn, sort))) |
|
102 |
||
103 |
val subst = |
|
104 |
subst |> fold Vartab.delete trivial_tvar_names |
|
105 |
|> Vartab.map |
|
106 |
(K (apsnd (map_type_tfree |
|
107 |
(fn (name, sort) => |
|
108 |
if tfree_name_trivial name then dummyT |
|
109 |
else TFree (name, sort))))) |
|
110 |
in |
|
111 |
(t', subst) |
|
112 |
end |
|
113 |
||
54821 | 114 |
fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z |
50258 | 115 |
| key_of_atype _ = I |
116 |
fun key_of_type T = fold_atyps key_of_atype T [] |
|
55243 | 117 |
|
50258 | 118 |
fun update_tab t T (tab, pos) = |
55243 | 119 |
((case key_of_type T of |
50258 | 120 |
[] => tab |
121 |
| key => |
|
122 |
let val cost = (size_of_typ T, (size_of_term t, pos)) in |
|
55243 | 123 |
(case Var_Set_Tab.lookup tab key of |
50258 | 124 |
NONE => Var_Set_Tab.update_new (key, cost) tab |
125 |
| SOME old_cost => |
|
126 |
(case cost_ord (cost, old_cost) of |
|
55243 | 127 |
LESS => Var_Set_Tab.update (key, cost) tab |
128 |
| _ => tab)) |
|
129 |
end), |
|
50258 | 130 |
pos + 1) |
131 |
||
55243 | 132 |
val typing_spot_table = post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst |
133 |
||
50258 | 134 |
fun reverse_greedy typing_spot_tab = |
135 |
let |
|
136 |
fun update_count z = |
|
137 |
fold (fn tvar => fn tab => |
|
138 |
let val c = Vartab.lookup tab tvar |> the_default 0 in |
|
139 |
Vartab.update (tvar, c + z) tab |
|
140 |
end) |
|
55243 | 141 |
fun superfluous tcount = forall (fn tvar => the (Vartab.lookup tcount tvar) > 1) |
50258 | 142 |
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) = |
143 |
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount) |
|
144 |
else (spot :: spots, tcount) |
|
55243 | 145 |
|
50258 | 146 |
val (typing_spots, tvar_count_tab) = |
55243 | 147 |
Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) |
50258 | 148 |
typing_spot_tab ([], Vartab.empty) |
149 |
|>> sort_distinct (rev_order o cost_ord o pairself snd) |
|
55243 | 150 |
in |
151 |
fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst |
|
152 |
end |
|
50258 | 153 |
|
52452 | 154 |
fun introduce_annotations subst spots t t' = |
50258 | 155 |
let |
52452 | 156 |
fun subst_atype (T as TVar (idxn, S)) subst = |
54821 | 157 |
(Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst) |
52452 | 158 |
| subst_atype T subst = (T, subst) |
55243 | 159 |
|
52452 | 160 |
val subst_type = fold_map_atypes subst_atype |
55243 | 161 |
|
52452 | 162 |
fun collect_annot _ T (subst, cp, ps as p :: ps', annots) = |
50258 | 163 |
if p <> cp then |
52452 | 164 |
(subst, cp + 1, ps, annots) |
50258 | 165 |
else |
52452 | 166 |
let val (T, subst) = subst_type T subst in |
55243 | 167 |
(subst, cp + 1, ps', (p, T) :: annots) |
50258 | 168 |
end |
52452 | 169 |
| collect_annot _ _ x = x |
55243 | 170 |
|
171 |
val (_, _, _, annots) = post_fold_term_type collect_annot (subst, 0, spots, []) t' |
|
172 |
||
52452 | 173 |
fun insert_annot t _ (cp, annots as (p, T) :: annots') = |
54821 | 174 |
if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots')) |
52452 | 175 |
| insert_annot t _ x = (t, x) |
52110
411db77f96f2
prevent pretty printer from automatically annotating numerals
smolkas
parents:
51877
diff
changeset
|
176 |
in |
55243 | 177 |
t |> post_traverse_term_type insert_annot (0, rev annots) |> fst |
52110
411db77f96f2
prevent pretty printer from automatically annotating numerals
smolkas
parents:
51877
diff
changeset
|
178 |
end |
50258 | 179 |
|
55213 | 180 |
fun annotate_types_in_term ctxt t = |
50258 | 181 |
let |
182 |
val t' = generalize_types ctxt t |
|
52452 | 183 |
val subst = match_types ctxt t' t |
184 |
val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt |
|
55243 | 185 |
val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord |
186 |
in |
|
187 |
introduce_annotations subst typing_spots t t' |
|
188 |
end |
|
50258 | 189 |
|
54504 | 190 |
end; |