50258
|
1 |
signature SLEDGEHAMMER_ANNOTATE =
|
|
2 |
sig
|
|
3 |
val annotate_types : Proof.context -> term -> term
|
|
4 |
end
|
|
5 |
|
|
6 |
structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
|
|
7 |
struct
|
|
8 |
|
|
9 |
(* Util *)
|
|
10 |
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
|
|
11 |
| post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
|
|
12 |
| post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
|
|
13 |
| post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
|
|
14 |
| post_traverse_term_type' f env (Abs (x, T1, b)) s =
|
|
15 |
let
|
|
16 |
val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
|
|
17 |
in f (Abs (x, T1, b')) (T1 --> T2) s' end
|
|
18 |
| post_traverse_term_type' f env (u $ v) s =
|
|
19 |
let
|
|
20 |
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
|
|
21 |
val ((v', s''), _) = post_traverse_term_type' f env v s'
|
|
22 |
in f (u' $ v') T s'' end
|
|
23 |
|
|
24 |
fun post_traverse_term_type f s t =
|
|
25 |
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
|
|
26 |
fun post_fold_term_type f s t =
|
|
27 |
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
|
|
28 |
|
|
29 |
(* Data structures, orders *)
|
|
30 |
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
|
|
31 |
|
|
32 |
structure Var_Set_Tab = Table(
|
|
33 |
type key = indexname list
|
|
34 |
val ord = list_ord Term_Ord.fast_indexname_ord)
|
|
35 |
|
|
36 |
(* (1) Generalize types *)
|
|
37 |
fun generalize_types ctxt t =
|
|
38 |
t |> map_types (fn _ => dummyT)
|
|
39 |
|> Syntax.check_term
|
|
40 |
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
|
|
41 |
|
|
42 |
(* (2) Typing-spot table *)
|
|
43 |
local
|
|
44 |
fun key_of_atype (TVar (z, _)) =
|
|
45 |
Ord_List.insert Term_Ord.fast_indexname_ord z
|
|
46 |
| key_of_atype _ = I
|
|
47 |
fun key_of_type T = fold_atyps key_of_atype T []
|
|
48 |
fun update_tab t T (tab, pos) =
|
|
49 |
(case key_of_type T of
|
|
50 |
[] => tab
|
|
51 |
| key =>
|
|
52 |
let val cost = (size_of_typ T, (size_of_term t, pos)) in
|
|
53 |
case Var_Set_Tab.lookup tab key of
|
|
54 |
NONE => Var_Set_Tab.update_new (key, cost) tab
|
|
55 |
| SOME old_cost =>
|
|
56 |
(case cost_ord (cost, old_cost) of
|
|
57 |
LESS => Var_Set_Tab.update (key, cost) tab
|
|
58 |
| _ => tab)
|
|
59 |
end,
|
|
60 |
pos + 1)
|
|
61 |
in
|
|
62 |
val typing_spot_table =
|
|
63 |
post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
|
|
64 |
end
|
|
65 |
|
|
66 |
(* (3) Reverse-greedy *)
|
|
67 |
fun reverse_greedy typing_spot_tab =
|
|
68 |
let
|
|
69 |
fun update_count z =
|
|
70 |
fold (fn tvar => fn tab =>
|
|
71 |
let val c = Vartab.lookup tab tvar |> the_default 0 in
|
|
72 |
Vartab.update (tvar, c + z) tab
|
|
73 |
end)
|
|
74 |
fun superfluous tcount =
|
|
75 |
forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
|
|
76 |
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
|
|
77 |
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
|
|
78 |
else (spot :: spots, tcount)
|
|
79 |
val (typing_spots, tvar_count_tab) =
|
|
80 |
Var_Set_Tab.fold
|
|
81 |
(fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
|
|
82 |
typing_spot_tab ([], Vartab.empty)
|
|
83 |
|>> sort_distinct (rev_order o cost_ord o pairself snd)
|
|
84 |
in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
|
|
85 |
|
|
86 |
(* (4) Introduce annotations *)
|
|
87 |
fun introduce_annotations ctxt spots t t' =
|
|
88 |
let
|
|
89 |
val thy = Proof_Context.theory_of ctxt
|
|
90 |
val get_types = post_fold_term_type (K cons) []
|
|
91 |
fun match_types tp =
|
|
92 |
fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
|
|
93 |
fun unica' b x [] = if b then [x] else []
|
|
94 |
| unica' b x (y :: ys) =
|
|
95 |
if x = y then unica' false x ys
|
|
96 |
else unica' true y ys |> b ? cons x
|
|
97 |
fun unica ord xs =
|
|
98 |
case sort ord xs of x :: ys => unica' true x ys | [] => []
|
|
99 |
val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
|
|
100 |
fun erase_unica_tfrees env =
|
|
101 |
let
|
|
102 |
val unica =
|
|
103 |
Vartab.fold (add_all_tfree_namesT o snd o snd) env []
|
|
104 |
|> filter_out (Variable.is_declared ctxt)
|
|
105 |
|> unica fast_string_ord
|
|
106 |
val erase_unica = map_atyps
|
|
107 |
(fn T as TFree (s, _) =>
|
|
108 |
if Ord_List.member fast_string_ord unica s then dummyT else T
|
|
109 |
| T => T)
|
|
110 |
in Vartab.map (K (apsnd erase_unica)) env end
|
|
111 |
val env = match_types (t', t) |> erase_unica_tfrees
|
|
112 |
fun get_annot env (TFree _) = (false, (env, dummyT))
|
|
113 |
| get_annot env (T as TVar (v, S)) =
|
|
114 |
let val T' = Envir.subst_type env T in
|
|
115 |
if T' = dummyT then (false, (env, dummyT))
|
|
116 |
else (true, (Vartab.update (v, (S, dummyT)) env, T'))
|
|
117 |
end
|
|
118 |
| get_annot env (Type (S, Ts)) =
|
|
119 |
(case fold_rev (fn T => fn (b, (env, Ts)) =>
|
|
120 |
let
|
|
121 |
val (b', (env', T)) = get_annot env T
|
|
122 |
in (b orelse b', (env', T :: Ts)) end)
|
|
123 |
Ts (false, (env, [])) of
|
|
124 |
(true, (env', Ts)) => (true, (env', Type (S, Ts)))
|
|
125 |
| (false, (env', _)) => (false, (env', dummyT)))
|
|
126 |
fun post1 _ T (env, cp, ps as p :: ps', annots) =
|
|
127 |
if p <> cp then
|
|
128 |
(env, cp + 1, ps, annots)
|
|
129 |
else
|
|
130 |
let val (_, (env', T')) = get_annot env T in
|
|
131 |
(env', cp + 1, ps', (p, T') :: annots)
|
|
132 |
end
|
|
133 |
| post1 _ _ accum = accum
|
|
134 |
val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
|
|
135 |
fun post2 t _ (cp, annots as (p, T) :: annots') =
|
|
136 |
if p <> cp then (t, (cp + 1, annots))
|
|
137 |
else (Type.constraint T t, (cp + 1, annots'))
|
|
138 |
| post2 t _ x = (t, x)
|
|
139 |
in post_traverse_term_type post2 (0, rev annots) t |> fst end
|
|
140 |
|
|
141 |
(* (5) Annotate *)
|
|
142 |
fun annotate_types ctxt t =
|
|
143 |
let
|
|
144 |
val t' = generalize_types ctxt t
|
|
145 |
val typing_spots =
|
|
146 |
t' |> typing_spot_table
|
|
147 |
|> reverse_greedy
|
|
148 |
|> sort int_ord
|
|
149 |
in introduce_annotations ctxt typing_spots t t' end
|
|
150 |
|
|
151 |
end
|