wenzelm@2957
|
1 |
(* Title: Pure/type_infer.ML
|
wenzelm@2957
|
2 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
|
wenzelm@2957
|
3 |
|
wenzelm@22698
|
4 |
Simple type inference.
|
wenzelm@2957
|
5 |
*)
|
wenzelm@2957
|
6 |
|
wenzelm@2957
|
7 |
signature TYPE_INFER =
|
wenzelm@2957
|
8 |
sig
|
wenzelm@8087
|
9 |
val anyT: sort -> typ
|
wenzelm@8611
|
10 |
val polymorphicT: typ -> typ
|
wenzelm@24682
|
11 |
val constrain: typ -> term -> term
|
wenzelm@24504
|
12 |
val is_param: indexname -> bool
|
wenzelm@14788
|
13 |
val param: int -> string * sort -> typ
|
wenzelm@22771
|
14 |
val paramify_vars: typ -> typ
|
wenzelm@18339
|
15 |
val paramify_dummies: typ -> int -> typ * int
|
wenzelm@24764
|
16 |
val fixate_params: Name.context -> term list -> term list
|
wenzelm@22698
|
17 |
val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
|
wenzelm@24485
|
18 |
val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
|
wenzelm@27263
|
19 |
(string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
|
wenzelm@27263
|
20 |
term list -> term list
|
wenzelm@2957
|
21 |
end;
|
wenzelm@2957
|
22 |
|
wenzelm@2957
|
23 |
structure TypeInfer: TYPE_INFER =
|
wenzelm@2957
|
24 |
struct
|
wenzelm@2957
|
25 |
|
wenzelm@2957
|
26 |
|
wenzelm@22698
|
27 |
(** type parameters and constraints **)
|
wenzelm@2957
|
28 |
|
wenzelm@22698
|
29 |
fun anyT S = TFree ("'_dummy_", S);
|
wenzelm@2957
|
30 |
|
wenzelm@22698
|
31 |
(*indicate polymorphic Vars*)
|
wenzelm@22698
|
32 |
fun polymorphicT T = Type ("_polymorphic_", [T]);
|
wenzelm@2957
|
33 |
|
wenzelm@27263
|
34 |
val constrain = Syntax.type_constraint;
|
wenzelm@2957
|
35 |
|
wenzelm@2957
|
36 |
|
wenzelm@22698
|
37 |
(* user parameters *)
|
wenzelm@2957
|
38 |
|
wenzelm@24504
|
39 |
fun is_param (x, _: int) = String.isPrefix "?" x;
|
wenzelm@22698
|
40 |
fun param i (x, S) = TVar (("?" ^ x, i), S);
|
wenzelm@2957
|
41 |
|
wenzelm@32002
|
42 |
val paramify_vars =
|
wenzelm@32146
|
43 |
Same.commit
|
wenzelm@32146
|
44 |
(Term_Subst.map_atypsT_same
|
wenzelm@32146
|
45 |
(fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
|
wenzelm@22771
|
46 |
|
wenzelm@22698
|
47 |
val paramify_dummies =
|
wenzelm@22698
|
48 |
let
|
wenzelm@22698
|
49 |
fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
|
wenzelm@22698
|
50 |
|
wenzelm@22698
|
51 |
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
|
wenzelm@22698
|
52 |
| paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
|
wenzelm@22698
|
53 |
| paramify (Type (a, Ts)) maxidx =
|
wenzelm@22698
|
54 |
let val (Ts', maxidx') = fold_map paramify Ts maxidx
|
wenzelm@22698
|
55 |
in (Type (a, Ts'), maxidx') end
|
wenzelm@22698
|
56 |
| paramify T maxidx = (T, maxidx);
|
wenzelm@22698
|
57 |
in paramify end;
|
wenzelm@2957
|
58 |
|
wenzelm@24764
|
59 |
fun fixate_params name_context ts =
|
wenzelm@24764
|
60 |
let
|
wenzelm@24764
|
61 |
fun subst_param (xi, S) (inst, used) =
|
wenzelm@24764
|
62 |
if is_param xi then
|
wenzelm@24764
|
63 |
let
|
wenzelm@24848
|
64 |
val [a] = Name.invents used Name.aT 1;
|
wenzelm@24764
|
65 |
val used' = Name.declare a used;
|
wenzelm@24764
|
66 |
in (((xi, S), TFree (a, S)) :: inst, used') end
|
wenzelm@24764
|
67 |
else (inst, used);
|
wenzelm@24764
|
68 |
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
|
wenzelm@24764
|
69 |
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
|
wenzelm@31979
|
70 |
in (map o map_types) (Term_Subst.instantiateT inst) ts end;
|
wenzelm@24764
|
71 |
|
wenzelm@2957
|
72 |
|
wenzelm@2957
|
73 |
|
wenzelm@2957
|
74 |
(** pretyps and preterms **)
|
wenzelm@2957
|
75 |
|
berghofe@32141
|
76 |
(*parameters may get instantiated, anything else is rigid*)
|
wenzelm@2957
|
77 |
datatype pretyp =
|
wenzelm@2957
|
78 |
PType of string * pretyp list |
|
wenzelm@2957
|
79 |
PTFree of string * sort |
|
wenzelm@2957
|
80 |
PTVar of indexname * sort |
|
berghofe@32141
|
81 |
Param of int * sort;
|
wenzelm@2957
|
82 |
|
wenzelm@2957
|
83 |
datatype preterm =
|
wenzelm@2957
|
84 |
PConst of string * pretyp |
|
wenzelm@2957
|
85 |
PFree of string * pretyp |
|
wenzelm@2957
|
86 |
PVar of indexname * pretyp |
|
wenzelm@2957
|
87 |
PBound of int |
|
wenzelm@2957
|
88 |
PAbs of string * pretyp * preterm |
|
wenzelm@2957
|
89 |
PAppl of preterm * preterm |
|
wenzelm@2957
|
90 |
Constraint of preterm * pretyp;
|
wenzelm@2957
|
91 |
|
wenzelm@2957
|
92 |
|
wenzelm@2957
|
93 |
(* utils *)
|
wenzelm@2957
|
94 |
|
wenzelm@32146
|
95 |
fun deref tye (T as Param (i, S)) =
|
wenzelm@32146
|
96 |
(case Inttab.lookup tye i of
|
wenzelm@32146
|
97 |
NONE => T
|
wenzelm@32146
|
98 |
| SOME U => deref tye U)
|
berghofe@32141
|
99 |
| deref tye T = T;
|
wenzelm@2957
|
100 |
|
wenzelm@16195
|
101 |
fun fold_pretyps f (PConst (_, T)) x = f T x
|
wenzelm@16195
|
102 |
| fold_pretyps f (PFree (_, T)) x = f T x
|
wenzelm@16195
|
103 |
| fold_pretyps f (PVar (_, T)) x = f T x
|
wenzelm@16195
|
104 |
| fold_pretyps _ (PBound _) x = x
|
wenzelm@16195
|
105 |
| fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
|
wenzelm@16195
|
106 |
| fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x)
|
wenzelm@16195
|
107 |
| fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x);
|
wenzelm@2957
|
108 |
|
wenzelm@2957
|
109 |
|
wenzelm@2957
|
110 |
|
wenzelm@2957
|
111 |
(** raw typs/terms to pretyps/preterms **)
|
wenzelm@2957
|
112 |
|
wenzelm@20668
|
113 |
(* pretyp_of *)
|
wenzelm@2957
|
114 |
|
berghofe@32141
|
115 |
fun pretyp_of is_para typ params_idx =
|
wenzelm@2957
|
116 |
let
|
berghofe@32141
|
117 |
val (params', idx) = fold_atyps
|
wenzelm@20668
|
118 |
(fn TVar (xi as (x, _), S) =>
|
berghofe@32141
|
119 |
(fn ps_idx as (ps, idx) =>
|
wenzelm@24504
|
120 |
if is_para xi andalso not (Vartab.defined ps xi)
|
berghofe@32141
|
121 |
then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx)
|
berghofe@32141
|
122 |
| _ => I) typ params_idx;
|
wenzelm@2957
|
123 |
|
berghofe@32141
|
124 |
fun pre_of (TVar (v as (xi, _))) idx =
|
wenzelm@20735
|
125 |
(case Vartab.lookup params' xi of
|
skalberg@15531
|
126 |
NONE => PTVar v
|
berghofe@32141
|
127 |
| SOME p => p, idx)
|
berghofe@32141
|
128 |
| pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1)
|
berghofe@32141
|
129 |
| pre_of (TFree v) idx = (PTFree v, idx)
|
berghofe@32141
|
130 |
| pre_of (T as Type (a, Ts)) idx =
|
berghofe@32141
|
131 |
if T = dummyT then (Param (idx, []), idx + 1)
|
berghofe@32141
|
132 |
else
|
berghofe@32141
|
133 |
let val (Ts', idx') = fold_map pre_of Ts idx
|
berghofe@32141
|
134 |
in (PType (a, Ts'), idx') end;
|
berghofe@32141
|
135 |
|
berghofe@32141
|
136 |
val (ptyp, idx') = pre_of typ idx;
|
berghofe@32141
|
137 |
in (ptyp, (params', idx')) end;
|
wenzelm@2957
|
138 |
|
wenzelm@2957
|
139 |
|
wenzelm@20668
|
140 |
(* preterm_of *)
|
wenzelm@2957
|
141 |
|
berghofe@32141
|
142 |
fun preterm_of const_type is_para tm (vparams, params, idx) =
|
wenzelm@2957
|
143 |
let
|
berghofe@32141
|
144 |
fun add_vparm xi (ps_idx as (ps, idx)) =
|
wenzelm@20735
|
145 |
if not (Vartab.defined ps xi) then
|
berghofe@32141
|
146 |
(Vartab.update (xi, Param (idx, [])) ps, idx + 1)
|
berghofe@32141
|
147 |
else ps_idx;
|
wenzelm@2957
|
148 |
|
berghofe@32141
|
149 |
val (vparams', idx') = fold_aterms
|
wenzelm@20668
|
150 |
(fn Var (_, Type ("_polymorphic_", _)) => I
|
wenzelm@20668
|
151 |
| Var (xi, _) => add_vparm xi
|
wenzelm@20668
|
152 |
| Free (x, _) => add_vparm (x, ~1)
|
wenzelm@20668
|
153 |
| _ => I)
|
berghofe@32141
|
154 |
tm (vparams, idx);
|
wenzelm@20735
|
155 |
fun var_param xi = the (Vartab.lookup vparams' xi);
|
wenzelm@2957
|
156 |
|
wenzelm@24504
|
157 |
val preT_of = pretyp_of is_para;
|
berghofe@32141
|
158 |
fun polyT_of T idx = apsnd snd (pretyp_of (K true) T (Vartab.empty, idx));
|
wenzelm@2957
|
159 |
|
wenzelm@22698
|
160 |
fun constraint T t ps =
|
wenzelm@20668
|
161 |
if T = dummyT then (t, ps)
|
wenzelm@2957
|
162 |
else
|
wenzelm@20668
|
163 |
let val (T', ps') = preT_of T ps
|
wenzelm@20668
|
164 |
in (Constraint (t, T'), ps') end;
|
wenzelm@2957
|
165 |
|
berghofe@32141
|
166 |
fun pre_of (Const (c, T)) (ps, idx) =
|
wenzelm@2957
|
167 |
(case const_type c of
|
berghofe@32141
|
168 |
SOME U =>
|
berghofe@32141
|
169 |
let val (pU, idx') = polyT_of U idx
|
berghofe@32141
|
170 |
in constraint T (PConst (c, pU)) (ps, idx') end
|
skalberg@15531
|
171 |
| NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
|
berghofe@32141
|
172 |
| pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
|
berghofe@32141
|
173 |
let val (pT, idx') = polyT_of T idx
|
berghofe@32141
|
174 |
in (PVar (xi, pT), (ps, idx')) end
|
berghofe@32141
|
175 |
| pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx
|
berghofe@32141
|
176 |
| pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx
|
berghofe@32141
|
177 |
| pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx =
|
berghofe@32141
|
178 |
pre_of t ps_idx |-> constraint T
|
berghofe@32141
|
179 |
| pre_of (Bound i) ps_idx = (PBound i, ps_idx)
|
berghofe@32141
|
180 |
| pre_of (Abs (x, T, t)) ps_idx =
|
wenzelm@2957
|
181 |
let
|
berghofe@32141
|
182 |
val (T', ps_idx') = preT_of T ps_idx;
|
berghofe@32141
|
183 |
val (t', ps_idx'') = pre_of t ps_idx';
|
berghofe@32141
|
184 |
in (PAbs (x, T', t'), ps_idx'') end
|
berghofe@32141
|
185 |
| pre_of (t $ u) ps_idx =
|
wenzelm@2957
|
186 |
let
|
berghofe@32141
|
187 |
val (t', ps_idx') = pre_of t ps_idx;
|
berghofe@32141
|
188 |
val (u', ps_idx'') = pre_of u ps_idx';
|
berghofe@32141
|
189 |
in (PAppl (t', u'), ps_idx'') end;
|
wenzelm@2957
|
190 |
|
berghofe@32141
|
191 |
val (tm', (params', idx'')) = pre_of tm (params, idx');
|
berghofe@32141
|
192 |
in (tm', (vparams', params', idx'')) end;
|
wenzelm@2957
|
193 |
|
wenzelm@2957
|
194 |
|
wenzelm@2957
|
195 |
|
wenzelm@2957
|
196 |
(** pretyps/terms to typs/terms **)
|
wenzelm@2957
|
197 |
|
wenzelm@2957
|
198 |
(* add_parms *)
|
wenzelm@2957
|
199 |
|
wenzelm@32146
|
200 |
fun add_parmsT tye T =
|
wenzelm@32146
|
201 |
(case deref tye T of
|
berghofe@32141
|
202 |
PType (_, Ts) => fold (add_parmsT tye) Ts
|
berghofe@32141
|
203 |
| Param (i, _) => insert (op =) i
|
wenzelm@32146
|
204 |
| _ => I);
|
wenzelm@2957
|
205 |
|
berghofe@32141
|
206 |
fun add_parms tye = fold_pretyps (add_parmsT tye);
|
wenzelm@2957
|
207 |
|
wenzelm@2957
|
208 |
|
wenzelm@2957
|
209 |
(* add_names *)
|
wenzelm@2957
|
210 |
|
wenzelm@32146
|
211 |
fun add_namesT tye T =
|
wenzelm@32146
|
212 |
(case deref tye T of
|
berghofe@32141
|
213 |
PType (_, Ts) => fold (add_namesT tye) Ts
|
berghofe@32141
|
214 |
| PTFree (x, _) => Name.declare x
|
berghofe@32141
|
215 |
| PTVar ((x, _), _) => Name.declare x
|
wenzelm@32146
|
216 |
| Param _ => I);
|
wenzelm@2957
|
217 |
|
berghofe@32141
|
218 |
fun add_names tye = fold_pretyps (add_namesT tye);
|
wenzelm@2957
|
219 |
|
wenzelm@2957
|
220 |
|
wenzelm@2957
|
221 |
(* simple_typ/term_of *)
|
wenzelm@2957
|
222 |
|
wenzelm@32146
|
223 |
fun simple_typ_of tye f T =
|
wenzelm@32146
|
224 |
(case deref tye T of
|
berghofe@32141
|
225 |
PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts)
|
berghofe@32141
|
226 |
| PTFree v => TFree v
|
berghofe@32141
|
227 |
| PTVar v => TVar v
|
wenzelm@32146
|
228 |
| Param (i, S) => TVar (f i, S));
|
wenzelm@2957
|
229 |
|
wenzelm@2957
|
230 |
(*convert types, drop constraints*)
|
berghofe@32141
|
231 |
fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
|
berghofe@32141
|
232 |
| simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T)
|
berghofe@32141
|
233 |
| simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T)
|
berghofe@32141
|
234 |
| simple_term_of tye f (PBound i) = Bound i
|
berghofe@32141
|
235 |
| simple_term_of tye f (PAbs (x, T, t)) =
|
berghofe@32141
|
236 |
Abs (x, simple_typ_of tye f T, simple_term_of tye f t)
|
berghofe@32141
|
237 |
| simple_term_of tye f (PAppl (t, u)) =
|
berghofe@32141
|
238 |
simple_term_of tye f t $ simple_term_of tye f u
|
berghofe@32141
|
239 |
| simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t;
|
wenzelm@2957
|
240 |
|
wenzelm@2957
|
241 |
|
berghofe@32141
|
242 |
(* typs_terms_of *)
|
wenzelm@2957
|
243 |
|
berghofe@32141
|
244 |
fun typs_terms_of tye used maxidx (Ts, ts) =
|
wenzelm@2957
|
245 |
let
|
berghofe@32141
|
246 |
val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used);
|
berghofe@32141
|
247 |
val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts []));
|
berghofe@32141
|
248 |
val names = Name.invents used' ("?" ^ Name.aT) (length parms);
|
berghofe@32141
|
249 |
val tab = Inttab.make (parms ~~ names);
|
berghofe@32141
|
250 |
fun f i = (the (Inttab.lookup tab i), maxidx + 1);
|
berghofe@32141
|
251 |
in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end;
|
wenzelm@2957
|
252 |
|
wenzelm@2957
|
253 |
|
wenzelm@2957
|
254 |
|
berghofe@32141
|
255 |
(** order-sorted unification of types **)
|
wenzelm@2957
|
256 |
|
berghofe@32141
|
257 |
exception NO_UNIFIER of string * pretyp Inttab.table;
|
wenzelm@2957
|
258 |
|
wenzelm@19465
|
259 |
fun unify pp tsig =
|
wenzelm@2957
|
260 |
let
|
wenzelm@2957
|
261 |
|
wenzelm@2957
|
262 |
(* adjust sorts of parameters *)
|
wenzelm@2957
|
263 |
|
wenzelm@19465
|
264 |
fun not_of_sort x S' S =
|
wenzelm@14828
|
265 |
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
|
wenzelm@14828
|
266 |
Pretty.string_of_sort pp S;
|
wenzelm@2957
|
267 |
|
berghofe@32141
|
268 |
fun meet (_, []) tye_idx = tye_idx
|
berghofe@32141
|
269 |
| meet (Param (i, S'), S) (tye_idx as (tye, idx)) =
|
berghofe@32141
|
270 |
if Type.subsort tsig (S', S) then tye_idx
|
berghofe@32141
|
271 |
else (Inttab.update_new (i,
|
berghofe@32141
|
272 |
Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1)
|
berghofe@32141
|
273 |
| meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
|
berghofe@32141
|
274 |
meets (Ts, Type.arity_sorts pp tsig a S
|
berghofe@32141
|
275 |
handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
|
berghofe@32141
|
276 |
| meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
|
berghofe@32141
|
277 |
if Type.subsort tsig (S', S) then tye_idx
|
berghofe@32141
|
278 |
else raise NO_UNIFIER (not_of_sort x S' S, tye)
|
berghofe@32141
|
279 |
| meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) =
|
berghofe@32141
|
280 |
if Type.subsort tsig (S', S) then tye_idx
|
berghofe@32141
|
281 |
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
|
berghofe@32141
|
282 |
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
|
berghofe@32141
|
283 |
meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
|
berghofe@32141
|
284 |
| meets _ tye_idx = tye_idx;
|
wenzelm@2957
|
285 |
|
wenzelm@2957
|
286 |
|
wenzelm@35013
|
287 |
(* occurs check and assignment *)
|
wenzelm@2957
|
288 |
|
berghofe@32141
|
289 |
fun occurs_check tye i (Param (i', S)) =
|
berghofe@32141
|
290 |
if i = i' then raise NO_UNIFIER ("Occurs check!", tye)
|
wenzelm@32146
|
291 |
else
|
wenzelm@32146
|
292 |
(case Inttab.lookup tye i' of
|
berghofe@32141
|
293 |
NONE => ()
|
berghofe@32141
|
294 |
| SOME T => occurs_check tye i T)
|
berghofe@32141
|
295 |
| occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
|
berghofe@32141
|
296 |
| occurs_check _ _ _ = ();
|
wenzelm@2957
|
297 |
|
berghofe@37235
|
298 |
fun assign i (T as Param (i', _)) S tye_idx =
|
berghofe@32141
|
299 |
if i = i' then tye_idx
|
berghofe@37235
|
300 |
else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
|
berghofe@37235
|
301 |
| assign i T S (tye_idx as (tye, _)) =
|
berghofe@37235
|
302 |
(occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
|
wenzelm@2957
|
303 |
|
wenzelm@2957
|
304 |
|
wenzelm@2957
|
305 |
(* unification *)
|
wenzelm@2957
|
306 |
|
wenzelm@32146
|
307 |
fun unif (T1, T2) (tye_idx as (tye, idx)) =
|
wenzelm@32146
|
308 |
(case (deref tye T1, deref tye T2) of
|
berghofe@32141
|
309 |
(Param (i, S), T) => assign i T S tye_idx
|
berghofe@32141
|
310 |
| (T, Param (i, S)) => assign i T S tye_idx
|
berghofe@32141
|
311 |
| (PType (a, Ts), PType (b, Us)) =>
|
wenzelm@2979
|
312 |
if a <> b then
|
berghofe@32141
|
313 |
raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
|
berghofe@32141
|
314 |
else fold unif (Ts ~~ Us) tye_idx
|
wenzelm@32146
|
315 |
| (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
|
wenzelm@2957
|
316 |
|
wenzelm@2957
|
317 |
in unif end;
|
wenzelm@2957
|
318 |
|
wenzelm@2957
|
319 |
|
wenzelm@2957
|
320 |
|
wenzelm@2957
|
321 |
(** type inference **)
|
wenzelm@2957
|
322 |
|
wenzelm@22698
|
323 |
(* appl_error *)
|
wenzelm@22698
|
324 |
|
wenzelm@14828
|
325 |
fun appl_error pp why t T u U =
|
wenzelm@8087
|
326 |
["Type error in application: " ^ why,
|
wenzelm@8087
|
327 |
"",
|
wenzelm@8087
|
328 |
Pretty.string_of (Pretty.block
|
wenzelm@14828
|
329 |
[Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
|
wenzelm@14828
|
330 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
|
wenzelm@8087
|
331 |
Pretty.string_of (Pretty.block
|
wenzelm@14828
|
332 |
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
|
wenzelm@14828
|
333 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
|
wenzelm@8087
|
334 |
""];
|
wenzelm@8087
|
335 |
|
nipkow@5635
|
336 |
|
berghofe@32141
|
337 |
(* infer *)
|
wenzelm@2957
|
338 |
|
wenzelm@19465
|
339 |
fun infer pp tsig =
|
wenzelm@2957
|
340 |
let
|
wenzelm@2979
|
341 |
(* errors *)
|
wenzelm@2957
|
342 |
|
wenzelm@2979
|
343 |
fun unif_failed msg =
|
wenzelm@14828
|
344 |
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
|
wenzelm@2979
|
345 |
|
berghofe@32141
|
346 |
fun prep_output tye bs ts Ts =
|
wenzelm@2957
|
347 |
let
|
berghofe@32141
|
348 |
val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
|
wenzelm@19012
|
349 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs';
|
wenzelm@27263
|
350 |
fun prep t =
|
wenzelm@27263
|
351 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
|
wenzelm@27263
|
352 |
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
|
wenzelm@27263
|
353 |
in (map prep ts', Ts') end;
|
wenzelm@2979
|
354 |
|
wenzelm@2979
|
355 |
fun err_loose i =
|
wenzelm@3784
|
356 |
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
|
wenzelm@2979
|
357 |
|
berghofe@32141
|
358 |
fun err_appl msg tye bs t T u U =
|
wenzelm@2979
|
359 |
let
|
berghofe@32141
|
360 |
val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
|
wenzelm@3510
|
361 |
val why =
|
wenzelm@3510
|
362 |
(case T' of
|
wenzelm@14828
|
363 |
Type ("fun", _) => "Incompatible operand type"
|
wenzelm@14828
|
364 |
| _ => "Operator not of function type");
|
wenzelm@14828
|
365 |
val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
|
wenzelm@3784
|
366 |
in raise TYPE (text, [T', U'], [t', u']) end;
|
wenzelm@2979
|
367 |
|
berghofe@32141
|
368 |
fun err_constraint msg tye bs t T U =
|
wenzelm@2979
|
369 |
let
|
berghofe@32141
|
370 |
val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
|
wenzelm@2979
|
371 |
val text = cat_lines
|
wenzelm@2979
|
372 |
[unif_failed msg,
|
nipkow@5635
|
373 |
"Cannot meet type constraint:", "",
|
wenzelm@14828
|
374 |
Pretty.string_of (Pretty.block
|
wenzelm@14828
|
375 |
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
|
wenzelm@14828
|
376 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
|
wenzelm@14828
|
377 |
Pretty.string_of (Pretty.block
|
wenzelm@14828
|
378 |
[Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
|
wenzelm@3784
|
379 |
in raise TYPE (text, [T', U'], [t']) end;
|
wenzelm@2979
|
380 |
|
wenzelm@2979
|
381 |
|
wenzelm@2979
|
382 |
(* main *)
|
wenzelm@2979
|
383 |
|
wenzelm@19465
|
384 |
val unif = unify pp tsig;
|
wenzelm@2957
|
385 |
|
berghofe@32141
|
386 |
fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx)
|
berghofe@32141
|
387 |
| inf _ (PFree (_, T)) tye_idx = (T, tye_idx)
|
berghofe@32141
|
388 |
| inf _ (PVar (_, T)) tye_idx = (T, tye_idx)
|
berghofe@32141
|
389 |
| inf bs (PBound i) tye_idx =
|
berghofe@32141
|
390 |
(snd (nth bs i handle Subscript => err_loose i), tye_idx)
|
berghofe@32141
|
391 |
| inf bs (PAbs (x, T, t)) tye_idx =
|
berghofe@32141
|
392 |
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
|
berghofe@32141
|
393 |
in (PType ("fun", [T, U]), tye_idx') end
|
berghofe@32141
|
394 |
| inf bs (PAppl (t, u)) tye_idx =
|
wenzelm@2957
|
395 |
let
|
berghofe@32141
|
396 |
val (T, tye_idx') = inf bs t tye_idx;
|
berghofe@32141
|
397 |
val (U, (tye, idx)) = inf bs u tye_idx';
|
berghofe@32141
|
398 |
val V = Param (idx, []);
|
wenzelm@2957
|
399 |
val U_to_V = PType ("fun", [U, V]);
|
berghofe@32141
|
400 |
val tye_idx'' = unif (U_to_V, T) (tye, idx + 1)
|
berghofe@32141
|
401 |
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
|
berghofe@32141
|
402 |
in (V, tye_idx'') end
|
berghofe@32141
|
403 |
| inf bs (Constraint (t, U)) tye_idx =
|
berghofe@32141
|
404 |
let val (T, tye_idx') = inf bs t tye_idx in
|
berghofe@32141
|
405 |
(T,
|
berghofe@32141
|
406 |
unif (T, U) tye_idx'
|
wenzelm@32146
|
407 |
handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
|
wenzelm@2957
|
408 |
end;
|
wenzelm@2957
|
409 |
|
wenzelm@2957
|
410 |
in inf [] end;
|
wenzelm@2957
|
411 |
|
wenzelm@2957
|
412 |
|
wenzelm@22698
|
413 |
(* infer_types *)
|
wenzelm@2957
|
414 |
|
wenzelm@27263
|
415 |
fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts =
|
wenzelm@2957
|
416 |
let
|
wenzelm@22698
|
417 |
(*constrain vars*)
|
wenzelm@22698
|
418 |
val get_type = the_default dummyT o var_type;
|
wenzelm@22698
|
419 |
val constrain_vars = Term.map_aterms
|
wenzelm@24682
|
420 |
(fn Free (x, T) => constrain T (Free (x, get_type (x, ~1)))
|
wenzelm@24682
|
421 |
| Var (xi, T) => constrain T (Var (xi, get_type xi))
|
wenzelm@22698
|
422 |
| t => t);
|
wenzelm@22698
|
423 |
|
wenzelm@27263
|
424 |
(*convert to preterms*)
|
wenzelm@27263
|
425 |
val ts = burrow_types check_typs raw_ts;
|
berghofe@32141
|
426 |
val (ts', (_, _, idx)) =
|
berghofe@32141
|
427 |
fold_map (preterm_of const_type is_param o constrain_vars) ts
|
berghofe@32141
|
428 |
(Vartab.empty, Vartab.empty, 0);
|
wenzelm@2957
|
429 |
|
wenzelm@27263
|
430 |
(*do type inference*)
|
berghofe@32141
|
431 |
val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx);
|
berghofe@32141
|
432 |
in #2 (typs_terms_of tye used maxidx ([], ts')) end;
|
wenzelm@14788
|
433 |
|
wenzelm@2957
|
434 |
end;
|