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