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