256
|
1 |
(* Title: Pure/type.ML
|
0
|
2 |
ID: $Id$
|
416
|
3 |
Author: Tobias Nipkow & Lawrence C Paulson
|
0
|
4 |
|
416
|
5 |
Type classes and sorts. Type signatures. Type unification and inference.
|
256
|
6 |
|
|
7 |
TODO:
|
416
|
8 |
move type unification and inference to type_unify.ML (TypeUnify) (?)
|
|
9 |
rename args -> tycons, coreg -> arities (?)
|
|
10 |
clean err msgs
|
0
|
11 |
*)
|
|
12 |
|
|
13 |
signature TYPE =
|
|
14 |
sig
|
256
|
15 |
structure Symtab: SYMTAB
|
416
|
16 |
val str_of_sort: sort -> string
|
|
17 |
val str_of_arity: string * sort list * sort -> string
|
0
|
18 |
type type_sig
|
200
|
19 |
val rep_tsig: type_sig ->
|
256
|
20 |
{classes: class list,
|
|
21 |
subclass: (class * class list) list,
|
|
22 |
default: sort,
|
|
23 |
args: (string * int) list,
|
|
24 |
abbrs: (string * (indexname list * typ)) list,
|
|
25 |
coreg: (string * (class * sort list) list) list}
|
0
|
26 |
val defaultS: type_sig -> sort
|
416
|
27 |
val tsig0: type_sig
|
256
|
28 |
val logical_types: type_sig -> string list
|
|
29 |
val extend_tsig: type_sig ->
|
|
30 |
(class * class list) list * sort * (string list * int) list *
|
|
31 |
(string list * (sort list * class)) list -> type_sig
|
422
|
32 |
val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
|
|
33 |
val ext_tsig_defsort: type_sig -> sort -> type_sig
|
582
|
34 |
val ext_tsig_types: type_sig -> (string * int) list -> type_sig
|
256
|
35 |
val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list
|
|
36 |
-> type_sig
|
|
37 |
val merge_tsigs: type_sig * type_sig -> type_sig
|
416
|
38 |
val subsort: type_sig -> sort * sort -> bool
|
|
39 |
val norm_sort: type_sig -> sort -> sort
|
|
40 |
val rem_sorts: typ -> typ
|
256
|
41 |
val cert_typ: type_sig -> typ -> typ
|
|
42 |
val norm_typ: type_sig -> typ -> typ
|
0
|
43 |
val freeze: (indexname -> bool) -> term -> term
|
|
44 |
val freeze_vars: typ -> typ
|
565
|
45 |
val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) *
|
256
|
46 |
(indexname -> sort option) * typ * term -> term * (indexname * typ) list
|
|
47 |
val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
|
0
|
48 |
val thaw_vars: typ -> typ
|
256
|
49 |
val typ_errors: type_sig -> typ * string list -> string list
|
0
|
50 |
val typ_instance: type_sig * typ * typ -> bool
|
256
|
51 |
val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
|
|
52 |
-> (indexname * typ) list
|
|
53 |
val unify: type_sig -> (typ * typ) * (indexname * typ) list
|
|
54 |
-> (indexname * typ) list
|
450
|
55 |
val raw_unify: typ * typ -> bool
|
0
|
56 |
val varifyT: typ -> typ
|
|
57 |
val varify: term * string list -> term
|
|
58 |
exception TUNIFY
|
256
|
59 |
exception TYPE_MATCH
|
0
|
60 |
end;
|
|
61 |
|
416
|
62 |
functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE =
|
0
|
63 |
struct
|
|
64 |
|
256
|
65 |
structure Symtab = Symtab;
|
0
|
66 |
|
|
67 |
|
416
|
68 |
(*** type classes and sorts ***)
|
|
69 |
|
|
70 |
(*
|
|
71 |
Classes denote (possibly empty) collections of types (e.g. sets of types)
|
|
72 |
and are partially ordered by 'inclusion'. They are represented by strings.
|
|
73 |
|
|
74 |
Sorts are intersections of finitely many classes. They are represented by
|
|
75 |
lists of classes.
|
|
76 |
*)
|
0
|
77 |
|
|
78 |
type domain = sort list;
|
416
|
79 |
|
|
80 |
|
|
81 |
(* print sorts and arities *)
|
0
|
82 |
|
416
|
83 |
fun str_of_sort [c] = c
|
565
|
84 |
| str_of_sort cs = enclose "{" "}" (commas cs);
|
416
|
85 |
|
565
|
86 |
fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
|
416
|
87 |
|
|
88 |
fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
|
|
89 |
| str_of_arity (t, SS, S) =
|
|
90 |
t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
|
256
|
91 |
|
|
92 |
|
|
93 |
|
416
|
94 |
(*** type signatures ***)
|
256
|
95 |
|
|
96 |
(*
|
|
97 |
classes:
|
|
98 |
a list of all declared classes;
|
0
|
99 |
|
256
|
100 |
subclass:
|
416
|
101 |
an association list representing the subclass relation; (c, cs) is
|
256
|
102 |
interpreted as "c is a proper subclass of all elemenst of cs"; note that
|
|
103 |
c itself is not a memeber of cs;
|
|
104 |
|
|
105 |
default:
|
|
106 |
the default sort attached to all unconstrained type vars;
|
|
107 |
|
|
108 |
args:
|
|
109 |
an association list of all declared types with the number of their
|
|
110 |
arguments;
|
|
111 |
|
|
112 |
abbrs:
|
|
113 |
an association list of type abbreviations;
|
|
114 |
|
|
115 |
coreg:
|
|
116 |
a two-fold association list of all type arities; (t, al) means that type
|
|
117 |
constructor t has the arities in al; an element (c, ss) of al represents
|
|
118 |
the arity (ss)c;
|
0
|
119 |
*)
|
|
120 |
|
256
|
121 |
datatype type_sig =
|
|
122 |
TySg of {
|
|
123 |
classes: class list,
|
|
124 |
subclass: (class * class list) list,
|
|
125 |
default: sort,
|
|
126 |
args: (string * int) list,
|
|
127 |
abbrs: (string * (indexname list * typ)) list,
|
|
128 |
coreg: (string * (class * domain) list) list};
|
|
129 |
|
189
|
130 |
fun rep_tsig (TySg comps) = comps;
|
0
|
131 |
|
256
|
132 |
fun defaultS (TySg {default, ...}) = default;
|
|
133 |
|
|
134 |
|
582
|
135 |
(* error messages *)
|
256
|
136 |
|
416
|
137 |
fun undcl_class c = "Undeclared class " ^ quote c;
|
256
|
138 |
val err_undcl_class = error o undcl_class;
|
0
|
139 |
|
422
|
140 |
fun err_dup_classes cs =
|
|
141 |
error ("Duplicate declaration of class(es) " ^ commas_quote cs);
|
416
|
142 |
|
|
143 |
fun undcl_type c = "Undeclared type constructor " ^ quote c;
|
256
|
144 |
val err_undcl_type = error o undcl_type;
|
|
145 |
|
582
|
146 |
fun err_neg_args c =
|
|
147 |
error ("Negative number of arguments of type constructor " ^ quote c);
|
|
148 |
|
416
|
149 |
fun err_dup_tycon c =
|
|
150 |
error ("Duplicate declaration of type constructor " ^ quote c);
|
|
151 |
|
|
152 |
fun err_dup_tyabbr c =
|
|
153 |
error ("Duplicate declaration of type abbreviation " ^ quote c);
|
|
154 |
|
|
155 |
fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
|
|
156 |
val err_ty_confl = error o ty_confl;
|
0
|
157 |
|
|
158 |
|
|
159 |
(* 'leq' checks the partial order on classes according to the
|
|
160 |
statements in the association list 'a' (i.e.'subclass')
|
|
161 |
*)
|
|
162 |
|
256
|
163 |
fun less a (C, D) = case assoc (a, C) of
|
0
|
164 |
Some(ss) => D mem ss
|
256
|
165 |
| None => err_undcl_class (C) ;
|
0
|
166 |
|
256
|
167 |
fun leq a (C, D) = C = D orelse less a (C, D);
|
0
|
168 |
|
|
169 |
|
416
|
170 |
(* logical_types *)
|
0
|
171 |
|
416
|
172 |
(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
|
|
173 |
and c <= logic*)
|
0
|
174 |
|
416
|
175 |
fun logical_types tsig =
|
|
176 |
let
|
|
177 |
val TySg {subclass, coreg, args, ...} = tsig;
|
|
178 |
|
|
179 |
fun log_class c = leq subclass (c, logicC);
|
|
180 |
fun log_type t = exists (log_class o #1) (assocs coreg t);
|
|
181 |
in
|
|
182 |
filter log_type (map #1 args)
|
0
|
183 |
end;
|
|
184 |
|
162
|
185 |
|
256
|
186 |
(* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
|
|
187 |
S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
|
0
|
188 |
with C1 <= C2 (according to an association list 'a')
|
|
189 |
*)
|
|
190 |
|
256
|
191 |
fun sortorder a (S1, S2) =
|
|
192 |
forall (fn C2 => exists (fn C1 => leq a (C1, C2)) S1) S2;
|
0
|
193 |
|
|
194 |
|
|
195 |
(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
|
|
196 |
there exists no class in S which is <= C;
|
|
197 |
the resulting set is minimal if S was minimal
|
|
198 |
*)
|
|
199 |
|
256
|
200 |
fun inj a (C, S) =
|
0
|
201 |
let fun inj1 [] = [C]
|
256
|
202 |
| inj1 (D::T) = if leq a (D, C) then D::T
|
|
203 |
else if leq a (C, D) then inj1 T
|
0
|
204 |
else D::(inj1 T)
|
|
205 |
in inj1 S end;
|
|
206 |
|
|
207 |
|
|
208 |
(* 'union_sort' forms the minimal union set of two sorts S1 and S2
|
|
209 |
under the assumption that S2 is minimal *)
|
256
|
210 |
(* FIXME rename to inter_sort (?) *)
|
0
|
211 |
|
|
212 |
fun union_sort a = foldr (inj a);
|
|
213 |
|
|
214 |
|
|
215 |
(* 'elementwise_union' forms elementwise the minimal union set of two
|
|
216 |
sort lists under the assumption that the two lists have the same length
|
256
|
217 |
*)
|
0
|
218 |
|
256
|
219 |
fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2);
|
|
220 |
|
0
|
221 |
|
|
222 |
(* 'lew' checks for two sort lists the ordering for all corresponding list
|
|
223 |
elements (i.e. sorts) *)
|
|
224 |
|
256
|
225 |
fun lew a (w1, w2) = forall (sortorder a) (w1~~w2);
|
|
226 |
|
0
|
227 |
|
256
|
228 |
(* 'is_min' checks if a class C is minimal in a given sort S under the
|
|
229 |
assumption that S contains C *)
|
0
|
230 |
|
256
|
231 |
fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
|
0
|
232 |
|
|
233 |
|
|
234 |
(* 'min_sort' reduces a sort to its minimal classes *)
|
|
235 |
|
|
236 |
fun min_sort a S = distinct(filter (is_min a S) S);
|
|
237 |
|
|
238 |
|
|
239 |
(* 'min_domain' minimizes the domain sorts of type declarationsl;
|
256
|
240 |
the function will be applied on the type declarations in extensions *)
|
0
|
241 |
|
|
242 |
fun min_domain subclass =
|
256
|
243 |
let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
|
0
|
244 |
in map one_min end;
|
|
245 |
|
|
246 |
|
|
247 |
(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
|
256
|
248 |
and gives back a list of those range classes whose domains meet the
|
0
|
249 |
predicate 'pred' *)
|
256
|
250 |
|
0
|
251 |
fun min_filter a pred ars =
|
256
|
252 |
let fun filt ([], l) = l
|
|
253 |
| filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
|
|
254 |
else filt (xs, l)
|
|
255 |
in filt (ars, []) end;
|
0
|
256 |
|
|
257 |
|
|
258 |
(* 'cod_above' filters all arities whose domains are elementwise >= than
|
256
|
259 |
a given domain 'w' and gives back a list of the corresponding range
|
0
|
260 |
classes *)
|
|
261 |
|
256
|
262 |
fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
|
|
263 |
|
|
264 |
|
0
|
265 |
|
200
|
266 |
(*Instantiation of type variables in types*)
|
|
267 |
(*Pre: instantiations obey restrictions! *)
|
|
268 |
fun inst_typ tye =
|
256
|
269 |
let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
|
200
|
270 |
| inst(T as TFree _) = T
|
256
|
271 |
| inst(T as TVar(v, _)) =
|
|
272 |
(case assoc(tye, v) of Some U => inst U | None => T)
|
200
|
273 |
in inst end;
|
0
|
274 |
|
|
275 |
(* 'least_sort' returns for a given type its maximum sort:
|
|
276 |
- type variables, free types: the sort brought with
|
|
277 |
- type constructors: recursive determination of the maximum sort of the
|
256
|
278 |
arguments if the type is declared in 'coreg' of the
|
|
279 |
given type signature *)
|
0
|
280 |
|
256
|
281 |
fun least_sort (tsig as TySg{subclass, coreg, ...}) =
|
|
282 |
let fun ls(T as Type(a, Ts)) =
|
|
283 |
(case assoc (coreg, a) of
|
|
284 |
Some(ars) => cod_above(subclass, map ls Ts, ars)
|
|
285 |
| None => raise TYPE(undcl_type a, [T], []))
|
|
286 |
| ls(TFree(a, S)) = S
|
|
287 |
| ls(TVar(a, S)) = S
|
0
|
288 |
in ls end;
|
|
289 |
|
|
290 |
|
256
|
291 |
fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =
|
|
292 |
if sortorder subclass ((least_sort tsig T), S) then ()
|
|
293 |
else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
|
0
|
294 |
|
|
295 |
|
|
296 |
(*Instantiation of type variables in types *)
|
256
|
297 |
fun inst_typ_tvars(tsig, tye) =
|
|
298 |
let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
|
|
299 |
| inst(T as TFree _) = T
|
|
300 |
| inst(T as TVar(v, S)) = (case assoc(tye, v) of
|
|
301 |
None => T | Some(U) => (check_has_sort(tsig, U, S); U))
|
0
|
302 |
in inst end;
|
|
303 |
|
|
304 |
(*Instantiation of type variables in terms *)
|
256
|
305 |
fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
|
200
|
306 |
|
|
307 |
|
|
308 |
(* expand_typ *)
|
|
309 |
|
256
|
310 |
fun expand_typ (TySg {abbrs, ...}) ty =
|
|
311 |
let
|
|
312 |
fun exptyp (Type (a, Ts)) =
|
|
313 |
(case assoc (abbrs, a) of
|
|
314 |
Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U)
|
|
315 |
| None => Type (a, map exptyp Ts))
|
|
316 |
| exptyp T = T
|
|
317 |
in
|
|
318 |
exptyp ty
|
|
319 |
end;
|
|
320 |
|
|
321 |
|
|
322 |
(* norm_typ *) (* FIXME norm sorts *)
|
|
323 |
|
|
324 |
val norm_typ = expand_typ;
|
|
325 |
|
|
326 |
|
|
327 |
|
|
328 |
(** type matching **)
|
200
|
329 |
|
0
|
330 |
exception TYPE_MATCH;
|
|
331 |
|
256
|
332 |
(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
|
|
333 |
fun typ_match tsig =
|
|
334 |
let
|
|
335 |
fun match (subs, (TVar (v, S), T)) =
|
|
336 |
(case assoc (subs, v) of
|
|
337 |
None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
|
|
338 |
handle TYPE _ => raise TYPE_MATCH)
|
422
|
339 |
| Some U => if U = T then subs else raise TYPE_MATCH)
|
256
|
340 |
| match (subs, (Type (a, Ts), Type (b, Us))) =
|
|
341 |
if a <> b then raise TYPE_MATCH
|
|
342 |
else foldl match (subs, Ts ~~ Us)
|
422
|
343 |
| match (subs, (TFree x, TFree y)) =
|
256
|
344 |
if x = y then subs else raise TYPE_MATCH
|
|
345 |
| match _ = raise TYPE_MATCH;
|
|
346 |
in match end;
|
0
|
347 |
|
|
348 |
|
256
|
349 |
fun typ_instance (tsig, T, U) =
|
|
350 |
(typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
|
|
351 |
|
|
352 |
|
|
353 |
|
|
354 |
(** build type signatures **)
|
|
355 |
|
416
|
356 |
fun make_tsig (classes, subclass, default, args, abbrs, coreg) =
|
|
357 |
TySg {classes = classes, subclass = subclass, default = default,
|
|
358 |
args = args, abbrs = abbrs, coreg = coreg};
|
|
359 |
|
|
360 |
val tsig0 = make_tsig ([], [], [], [], [], []);
|
256
|
361 |
|
0
|
362 |
|
401
|
363 |
(* sorts *)
|
|
364 |
|
416
|
365 |
fun subsort (TySg {subclass, ...}) (S1, S2) =
|
|
366 |
sortorder subclass (S1, S2);
|
|
367 |
|
401
|
368 |
fun norm_sort (TySg {subclass, ...}) S =
|
|
369 |
sort_strings (min_sort subclass S);
|
|
370 |
|
416
|
371 |
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
|
|
372 |
| rem_sorts (TFree (x, _)) = TFree (x, [])
|
|
373 |
| rem_sorts (TVar (xi, _)) = TVar (xi, []);
|
401
|
374 |
|
|
375 |
|
0
|
376 |
|
|
377 |
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
|
|
378 |
|
256
|
379 |
fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
|
0
|
380 |
|
|
381 |
|
416
|
382 |
(* typ_errors *)
|
256
|
383 |
|
416
|
384 |
(*check validity of (not necessarily normal) type; accumulate error messages*)
|
256
|
385 |
|
416
|
386 |
fun typ_errors tsig (typ, errors) =
|
256
|
387 |
let
|
416
|
388 |
val TySg {classes, args, abbrs, ...} = tsig;
|
|
389 |
|
|
390 |
fun class_err (errs, c) =
|
|
391 |
if c mem classes then errs
|
|
392 |
else undcl_class c ins errs;
|
256
|
393 |
|
|
394 |
val sort_err = foldl class_err;
|
0
|
395 |
|
256
|
396 |
fun typ_errs (Type (c, Us), errs) =
|
|
397 |
let
|
|
398 |
val errs' = foldr typ_errs (Us, errs);
|
|
399 |
fun nargs n =
|
|
400 |
if n = length Us then errs'
|
416
|
401 |
else ("Wrong number of arguments: " ^ quote c) ins errs';
|
256
|
402 |
in
|
|
403 |
(case assoc (args, c) of
|
|
404 |
Some n => nargs n
|
|
405 |
| None =>
|
|
406 |
(case assoc (abbrs, c) of
|
|
407 |
Some (vs, _) => nargs (length vs)
|
416
|
408 |
| None => undcl_type c ins errs))
|
256
|
409 |
end
|
|
410 |
| typ_errs (TFree (_, S), errs) = sort_err (errs, S)
|
416
|
411 |
| typ_errs (TVar ((x, i), S), errs) =
|
|
412 |
if i < 0 then
|
|
413 |
("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
|
|
414 |
else sort_err (errs, S);
|
256
|
415 |
in
|
416
|
416 |
typ_errs (typ, errors)
|
256
|
417 |
end;
|
|
418 |
|
|
419 |
|
|
420 |
(* cert_typ *)
|
|
421 |
|
|
422 |
(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
|
|
423 |
|
|
424 |
fun cert_typ tsig ty =
|
|
425 |
(case typ_errors tsig (ty, []) of
|
|
426 |
[] => norm_typ tsig ty
|
|
427 |
| errs => raise_type (cat_lines errs) [ty] []);
|
|
428 |
|
|
429 |
|
|
430 |
|
422
|
431 |
(** merge type signatures **)
|
256
|
432 |
|
422
|
433 |
(*'assoc_union' merges two association lists if the contents associated
|
|
434 |
the keys are lists*)
|
0
|
435 |
|
422
|
436 |
fun assoc_union (as1, []) = as1
|
|
437 |
| assoc_union (as1, (key, l2) :: as2) =
|
|
438 |
(case assoc (as1, key) of
|
|
439 |
Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2)
|
|
440 |
| None => assoc_union ((key, l2) :: as1, as2));
|
0
|
441 |
|
|
442 |
|
422
|
443 |
(* merge subclass *)
|
0
|
444 |
|
422
|
445 |
fun merge_subclass (subclass1, subclass2) =
|
|
446 |
let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in
|
|
447 |
if exists (op mem) subclass then
|
|
448 |
error ("Cyclic class structure!") (* FIXME improve msg, raise TERM *)
|
|
449 |
else subclass
|
416
|
450 |
end;
|
|
451 |
|
|
452 |
|
422
|
453 |
(* coregularity *)
|
0
|
454 |
|
|
455 |
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
|
|
456 |
|
256
|
457 |
fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of
|
0
|
458 |
Some(w1) => if w = w1 then () else
|
256
|
459 |
error("There are two declarations\n" ^
|
416
|
460 |
str_of_arity(t, w, [s]) ^ " and\n" ^
|
|
461 |
str_of_arity(t, w1, [s]) ^ "\n" ^
|
0
|
462 |
"with the same result class.")
|
|
463 |
| None => ();
|
|
464 |
|
|
465 |
(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
|
|
466 |
such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
|
|
467 |
|
256
|
468 |
fun subs (classes, subclass) C =
|
|
469 |
let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl
|
|
470 |
in foldl sub ([], classes) end;
|
0
|
471 |
|
256
|
472 |
fun coreg_err(t, (w1, C), (w2, D)) =
|
416
|
473 |
error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and "
|
|
474 |
^ str_of_arity(t, w2, [D]) ^ " are in conflict");
|
0
|
475 |
|
256
|
476 |
fun restr2 classes (subclass, coreg) (t, (s, w)) =
|
|
477 |
let fun restr ([], test) = ()
|
416
|
478 |
| restr (s1::Ss, test) =
|
|
479 |
(case assoc2 (coreg, (t, s1)) of
|
|
480 |
Some dom =>
|
|
481 |
if lew subclass (test (w, dom))
|
|
482 |
then restr (Ss, test)
|
|
483 |
else coreg_err (t, (w, s), (dom, s1))
|
256
|
484 |
| None => restr (Ss, test))
|
|
485 |
fun forward (t, (s, w)) =
|
|
486 |
let val s_sups = case assoc (subclass, s) of
|
|
487 |
Some(s_sups) => s_sups | None => err_undcl_class(s);
|
|
488 |
in restr (s_sups, I) end
|
|
489 |
fun backward (t, (s, w)) =
|
|
490 |
let val s_subs = subs (classes, subclass) s
|
|
491 |
in restr (s_subs, fn (x, y) => (y, x)) end
|
|
492 |
in (backward (t, (s, w)); forward (t, (s, w))) end;
|
0
|
493 |
|
|
494 |
|
256
|
495 |
fun varying_decls t =
|
|
496 |
error ("Type constructor " ^ quote t ^ " has varying number of arguments");
|
0
|
497 |
|
|
498 |
|
422
|
499 |
(* 'merge_coreg' builds the union of two 'coreg' lists;
|
|
500 |
it only checks the two restriction conditions and inserts afterwards
|
|
501 |
all elements of the second list into the first one *)
|
|
502 |
|
|
503 |
fun merge_coreg classes subclass1 =
|
|
504 |
let fun test_ar classes (t, ars1) (coreg1, (s, w)) =
|
|
505 |
(is_unique_decl coreg1 (t, (s, w));
|
|
506 |
restr2 classes (subclass1, coreg1) (t, (s, w));
|
|
507 |
overwrite (coreg1, (t, (s, w) ins ars1)));
|
|
508 |
|
|
509 |
fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of
|
|
510 |
Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)
|
|
511 |
| None => c::coreg1
|
|
512 |
in foldl merge_c end;
|
|
513 |
|
|
514 |
fun merge_args (args, (t, n)) =
|
|
515 |
(case assoc (args, t) of
|
|
516 |
Some m => if m = n then args else varying_decls t
|
|
517 |
| None => (t, n) :: args);
|
|
518 |
|
|
519 |
(* FIXME raise TERM *)
|
|
520 |
fun merge_abbrs (abbrs1, abbrs2) =
|
|
521 |
let
|
|
522 |
val abbrs = abbrs1 union abbrs2;
|
|
523 |
val names = map fst abbrs;
|
|
524 |
in
|
|
525 |
(case duplicates names of
|
|
526 |
[] => abbrs
|
|
527 |
| dups => error ("Duplicate declaration of type abbreviations: " ^
|
|
528 |
commas_quote dups))
|
|
529 |
end;
|
|
530 |
|
|
531 |
|
|
532 |
(* 'merge_tsigs' takes the above declared functions to merge two type
|
|
533 |
signatures *)
|
|
534 |
|
|
535 |
fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,
|
|
536 |
coreg=coreg1, abbrs=abbrs1},
|
|
537 |
TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,
|
|
538 |
coreg=coreg2, abbrs=abbrs2}) =
|
|
539 |
let val classes' = classes1 union classes2;
|
|
540 |
val subclass' = merge_subclass (subclass1, subclass2);
|
|
541 |
val args' = foldl merge_args (args1, args2)
|
|
542 |
val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);
|
|
543 |
val default' = min_sort subclass' (default1 @ default2);
|
|
544 |
val abbrs' = merge_abbrs(abbrs1, abbrs2);
|
|
545 |
in TySg{classes=classes' , default=default', subclass=subclass', args=args',
|
|
546 |
coreg=coreg' , abbrs = abbrs' }
|
|
547 |
end;
|
|
548 |
|
|
549 |
|
|
550 |
|
|
551 |
(*** extend type signatures ***)
|
|
552 |
|
|
553 |
(** add classes **)
|
|
554 |
|
|
555 |
(* FIXME use? *)
|
|
556 |
fun add_classes classes cs =
|
|
557 |
(case cs inter classes of
|
|
558 |
[] => cs @ classes
|
|
559 |
| dups => err_dup_classes cs);
|
|
560 |
|
|
561 |
|
|
562 |
(* 'add_class' adds a new class to the list of all existing classes *)
|
|
563 |
|
|
564 |
fun add_class (classes, (s, _)) =
|
|
565 |
if s mem classes then error("Class " ^ s ^ " declared twice.")
|
|
566 |
else s :: classes;
|
|
567 |
|
|
568 |
|
|
569 |
(*'add_subclass' adds a tuple consisting of a new class (the new class has
|
|
570 |
already been inserted into the 'classes' list) and its superclasses (they
|
|
571 |
must be declared in 'classes' too) to the 'subclass' list of the given type
|
|
572 |
signature; furthermore all inherited superclasses according to the
|
|
573 |
superclasses brought with are inserted and there is a check that there are
|
|
574 |
no cycles (i.e. C <= D <= C, with C <> D);*)
|
|
575 |
|
|
576 |
fun add_subclass classes (subclass, (s, ges)) =
|
|
577 |
let fun upd (subclass, s') = if s' mem classes then
|
|
578 |
let val ges' = the (assoc (subclass, s))
|
|
579 |
in case assoc (subclass, s') of
|
|
580 |
Some sups => if s mem sups
|
|
581 |
then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
|
|
582 |
else overwrite (subclass, (s, sups union ges'))
|
|
583 |
| None => subclass
|
|
584 |
end
|
|
585 |
else err_undcl_class(s')
|
|
586 |
in foldl upd (subclass@[(s, ges)], ges) end;
|
|
587 |
|
|
588 |
|
|
589 |
(* 'extend_classes' inserts all new classes into the corresponding
|
|
590 |
lists ('classes', 'subclass') if possible *)
|
|
591 |
|
|
592 |
fun extend_classes (classes, subclass, newclasses) =
|
|
593 |
if newclasses = [] then (classes, subclass) else
|
|
594 |
let val classes' = foldl add_class (classes, newclasses);
|
|
595 |
val subclass' = foldl (add_subclass classes') (subclass, newclasses);
|
|
596 |
in (classes', subclass') end;
|
|
597 |
|
|
598 |
|
|
599 |
(* ext_tsig_subclass *)
|
|
600 |
|
|
601 |
fun ext_tsig_subclass tsig pairs =
|
|
602 |
let
|
|
603 |
val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
|
|
604 |
|
|
605 |
(* FIXME clean! *)
|
|
606 |
val subclass' =
|
|
607 |
merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
|
|
608 |
in
|
|
609 |
make_tsig (classes, subclass', default, args, abbrs, coreg)
|
|
610 |
end;
|
|
611 |
|
|
612 |
|
|
613 |
(* ext_tsig_defsort *)
|
|
614 |
|
|
615 |
fun ext_tsig_defsort (TySg {classes, subclass, args, abbrs, coreg, ...}) default =
|
|
616 |
make_tsig (classes, subclass, default, args, abbrs, coreg);
|
|
617 |
|
|
618 |
|
|
619 |
|
582
|
620 |
(** add types **) (* FIXME check *)
|
|
621 |
|
|
622 |
fun ext_tsig_types (TySg {classes, subclass, default, args, abbrs, coreg}) ts =
|
|
623 |
let
|
|
624 |
fun check_type (c, n) =
|
|
625 |
if n < 0 then err_neg_args c
|
|
626 |
else if is_some (assoc (args, c)) then err_dup_tycon c
|
|
627 |
else if is_some (assoc (abbrs, c)) then err_ty_confl c
|
|
628 |
else ();
|
|
629 |
in
|
|
630 |
seq check_type ts;
|
|
631 |
make_tsig (classes, subclass, default, ts @ args, abbrs,
|
|
632 |
map (rpair [] o #1) ts @ coreg) (* FIXME (t, []) needed? *)
|
|
633 |
end;
|
|
634 |
|
|
635 |
|
|
636 |
|
|
637 |
(** add type abbreviations **)
|
|
638 |
|
|
639 |
fun abbr_errors tsig (a, (lhs_vs, rhs)) =
|
|
640 |
let
|
|
641 |
val TySg {args, abbrs, ...} = tsig;
|
|
642 |
val rhs_vs = map #1 (typ_tvars rhs);
|
|
643 |
val show_idxs = commas_quote o map fst;
|
|
644 |
|
|
645 |
val dup_lhs_vars =
|
|
646 |
(case duplicates lhs_vs of
|
|
647 |
[] => []
|
|
648 |
| vs => ["Duplicate variables on lhs: " ^ show_idxs vs]);
|
|
649 |
|
|
650 |
val extra_rhs_vars =
|
|
651 |
(case gen_rems (op =) (rhs_vs, lhs_vs) of
|
|
652 |
[] => []
|
|
653 |
| vs => ["Extra variables on rhs: " ^ show_idxs vs]);
|
|
654 |
|
|
655 |
val tycon_confl =
|
|
656 |
if is_none (assoc (args, a)) then []
|
|
657 |
else [ty_confl a];
|
|
658 |
|
|
659 |
val dup_abbr =
|
|
660 |
if is_none (assoc (abbrs, a)) then []
|
|
661 |
else ["Duplicate declaration of abbreviation"];
|
|
662 |
in
|
|
663 |
dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
|
|
664 |
typ_errors tsig (rhs, [])
|
|
665 |
end;
|
|
666 |
|
|
667 |
fun add_abbr (tsig, abbr as (a, _)) =
|
|
668 |
let val TySg {classes, subclass, default, args, coreg, abbrs} = tsig in
|
|
669 |
(case abbr_errors tsig abbr of
|
|
670 |
[] => make_tsig (classes, subclass, default, args, abbr :: abbrs, coreg)
|
|
671 |
| errs => (seq writeln errs;
|
|
672 |
error ("The error(s) above occurred in type abbreviation " ^ quote a)))
|
|
673 |
end;
|
|
674 |
|
|
675 |
fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);
|
|
676 |
|
|
677 |
|
|
678 |
|
422
|
679 |
(** add arities **)
|
|
680 |
|
0
|
681 |
(* 'coregular' checks
|
|
682 |
- the two restriction conditions 'is_unique_decl' and 'restr2'
|
256
|
683 |
- if the classes in the new type declarations are known in the
|
0
|
684 |
given type signature
|
|
685 |
- if one type constructor has always the same number of arguments;
|
256
|
686 |
if one type declaration has passed all checks it is inserted into
|
0
|
687 |
the 'coreg' association list of the given type signatrure *)
|
|
688 |
|
256
|
689 |
fun coregular (classes, subclass, args) =
|
|
690 |
let fun ex C = if C mem classes then () else err_undcl_class(C);
|
0
|
691 |
|
256
|
692 |
fun addar(w, C) (coreg, t) = case assoc(args, t) of
|
0
|
693 |
Some(n) => if n <> length w then varying_decls(t) else
|
256
|
694 |
(is_unique_decl coreg (t, (C, w));
|
|
695 |
(seq o seq) ex w;
|
|
696 |
restr2 classes (subclass, coreg) (t, (C, w));
|
416
|
697 |
let val ars = the (assoc(coreg, t))
|
256
|
698 |
in overwrite(coreg, (t, (C, w) ins ars)) end)
|
|
699 |
| None => err_undcl_type(t);
|
0
|
700 |
|
256
|
701 |
fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)
|
0
|
702 |
|
|
703 |
in addts end;
|
|
704 |
|
|
705 |
|
|
706 |
(* 'close' extends the 'coreg' association list after all new type
|
|
707 |
declarations have been inserted successfully:
|
|
708 |
for every declaration t:(Ss)C , for all classses D with C <= D:
|
|
709 |
if there is no declaration t:(Ss')C' with C < C' and C' <= D
|
|
710 |
then insert the declaration t:(Ss)D into 'coreg'
|
|
711 |
this means, if there exists a declaration t:(Ss)C and there is
|
|
712 |
no declaration t:(Ss')D with C <=D then the declaration holds
|
256
|
713 |
for all range classes more general than C *)
|
|
714 |
|
|
715 |
fun close (coreg, subclass) =
|
|
716 |
let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
|
0
|
717 |
Some(sups) =>
|
256
|
718 |
let fun close_sup (l, sup) =
|
|
719 |
if exists (fn s'' => less subclass (s, s'') andalso
|
|
720 |
leq subclass (s'', sup)) sl
|
0
|
721 |
then l
|
256
|
722 |
else (sup, dom)::l
|
|
723 |
in foldl close_sup (l, sups) end
|
0
|
724 |
| None => l;
|
256
|
725 |
fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
|
0
|
726 |
in map ext coreg end;
|
|
727 |
|
422
|
728 |
|
|
729 |
(** add types **)
|
|
730 |
|
582
|
731 |
(* FIXME old *)
|
416
|
732 |
fun add_types (aca, (ts, n)) =
|
|
733 |
let
|
|
734 |
fun add_type ((args, coreg, abbrs), t) =
|
|
735 |
case assoc(args, t) of (* FIXME from new *)
|
|
736 |
Some _ => twice(t)
|
|
737 |
| None =>
|
|
738 |
(case assoc(abbrs, t) of
|
|
739 |
Some _ => tyab_conflict(t)
|
|
740 |
| None => ((t, n)::args, (t, [])::coreg, abbrs))
|
|
741 |
in
|
|
742 |
if n < 0 then (* FIXME err_neg_args *)
|
|
743 |
error ("Type constructor cannot have negative number of arguments")
|
|
744 |
else foldl add_type (aca, ts)
|
0
|
745 |
end;
|
|
746 |
|
256
|
747 |
|
422
|
748 |
|
256
|
749 |
(* 'extend_tsig' takes the above described check- and extend-functions to
|
0
|
750 |
extend a given type signature with new classes and new type declarations *)
|
|
751 |
|
256
|
752 |
fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs})
|
582
|
753 |
(newclasses, [], types, arities) =
|
416
|
754 |
let
|
|
755 |
val (classes', subclass') = extend_classes(classes, subclass, newclasses);
|
256
|
756 |
val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types);
|
422
|
757 |
|
416
|
758 |
val coreg'' =
|
|
759 |
foldl (coregular (classes', subclass', args'))
|
|
760 |
(coreg', min_domain subclass' arities);
|
256
|
761 |
val coreg''' = close (coreg'', subclass');
|
416
|
762 |
in
|
582
|
763 |
TySg {classes = classes', subclass = subclass', default = default,
|
416
|
764 |
args = args', coreg = coreg''', abbrs = abbrs}
|
|
765 |
end;
|
0
|
766 |
|
|
767 |
|
416
|
768 |
|
|
769 |
|
|
770 |
(*** type unification and inference ***)
|
0
|
771 |
|
|
772 |
(*
|
|
773 |
|
|
774 |
Input:
|
|
775 |
- a 'raw' term which contains only dummy types and some explicit type
|
|
776 |
constraints encoded as terms.
|
|
777 |
- the expected type of the term.
|
|
778 |
|
|
779 |
Output:
|
|
780 |
- the correctly typed term
|
|
781 |
- the substitution needed to unify the actual type of the term with its
|
|
782 |
expected type; only the TVars in the expected type are included.
|
|
783 |
|
|
784 |
During type inference all TVars in the term have negative index. This keeps
|
|
785 |
them apart from normal TVars, which is essential, because at the end the type
|
|
786 |
of the term is unified with the expected type, which contains normal TVars.
|
|
787 |
|
565
|
788 |
1. Add initial type information to the term (attach_types).
|
0
|
789 |
This freezes (freeze_vars) TVars in explicitly provided types (eg
|
|
790 |
constraints or defaults) by turning them into TFrees.
|
|
791 |
2. Carry out type inference, possibly introducing new negative TVars.
|
|
792 |
3. Unify actual and expected type.
|
|
793 |
4. Turn all (negative) TVars into unique new TFrees (freeze).
|
|
794 |
5. Thaw all TVars frozen in step 1 (thaw_vars).
|
|
795 |
|
|
796 |
*)
|
|
797 |
|
|
798 |
(*Raised if types are not unifiable*)
|
|
799 |
exception TUNIFY;
|
|
800 |
|
|
801 |
val tyvar_count = ref(~1);
|
|
802 |
|
|
803 |
fun tyinit() = (tyvar_count := ~1);
|
|
804 |
|
|
805 |
fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
|
|
806 |
|
|
807 |
(*
|
|
808 |
Generate new TVar. Index is < ~1 to distinguish it from TVars generated from
|
|
809 |
variable names (see id_type). Name is arbitrary because index is new.
|
|
810 |
*)
|
|
811 |
|
256
|
812 |
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
|
0
|
813 |
|
|
814 |
(*Occurs check: type variable occurs in type?*)
|
|
815 |
fun occ v tye =
|
256
|
816 |
let fun occ(Type(_, Ts)) = exists occ Ts
|
0
|
817 |
| occ(TFree _) = false
|
256
|
818 |
| occ(TVar(w, _)) = v=w orelse
|
|
819 |
(case assoc(tye, w) of
|
0
|
820 |
None => false
|
|
821 |
| Some U => occ U);
|
|
822 |
in occ end;
|
|
823 |
|
256
|
824 |
(*Chase variable assignments in tye.
|
|
825 |
If devar (T, tye) returns a type var then it must be unassigned.*)
|
|
826 |
fun devar (T as TVar(v, _), tye) = (case assoc(tye, v) of
|
|
827 |
Some U => devar (U, tye)
|
0
|
828 |
| None => T)
|
256
|
829 |
| devar (T, tye) = T;
|
0
|
830 |
|
|
831 |
|
|
832 |
(* 'dom' returns for a type constructor t the list of those domains
|
|
833 |
which deliver a given range class C *)
|
|
834 |
|
256
|
835 |
fun dom coreg t C = case assoc2 (coreg, (t, C)) of
|
0
|
836 |
Some(Ss) => Ss
|
|
837 |
| None => raise TUNIFY;
|
|
838 |
|
|
839 |
|
|
840 |
(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
|
|
841 |
(i.e. a set of range classes ); the union is carried out elementwise
|
|
842 |
for the seperate sorts in the domains *)
|
|
843 |
|
256
|
844 |
fun Dom (subclass, coreg) (t, S) =
|
0
|
845 |
let val domlist = map (dom coreg t) S;
|
|
846 |
in if null domlist then []
|
256
|
847 |
else foldl (elementwise_union subclass) (hd domlist, tl domlist)
|
0
|
848 |
end;
|
|
849 |
|
|
850 |
|
256
|
851 |
fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =
|
|
852 |
let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
|
|
853 |
fun Wk(T as TVar(v, S')) =
|
|
854 |
if sortorder subclass (S', S) then tye
|
|
855 |
else (v, gen_tyvar(union_sort subclass (S', S)))::tye
|
|
856 |
| Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
|
|
857 |
else raise TUNIFY
|
|
858 |
| Wk(T as Type(f, Ts)) =
|
|
859 |
if null S then tye
|
|
860 |
else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)
|
0
|
861 |
in Wk(T) end;
|
|
862 |
|
|
863 |
|
|
864 |
(* Order-sorted Unification of Types (U) *)
|
|
865 |
|
|
866 |
(* Precondition: both types are well-formed w.r.t. type constructor arities *)
|
256
|
867 |
fun unify (tsig as TySg{subclass, coreg, ...}) =
|
|
868 |
let fun unif ((T, U), tye) =
|
|
869 |
case (devar(T, tye), devar(U, tye)) of
|
|
870 |
(T as TVar(v, S1), U as TVar(w, S2)) =>
|
0
|
871 |
if v=w then tye else
|
256
|
872 |
if sortorder subclass (S1, S2) then (w, T)::tye else
|
|
873 |
if sortorder subclass (S2, S1) then (v, U)::tye
|
|
874 |
else let val nu = gen_tyvar (union_sort subclass (S1, S2))
|
|
875 |
in (v, nu)::(w, nu)::tye end
|
|
876 |
| (T as TVar(v, S), U) =>
|
|
877 |
if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
|
|
878 |
| (U, T as TVar (v, S)) =>
|
|
879 |
if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
|
|
880 |
| (Type(a, Ts), Type(b, Us)) =>
|
|
881 |
if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
|
|
882 |
| (T, U) => if T=U then tye else raise TUNIFY
|
0
|
883 |
in unif end;
|
|
884 |
|
|
885 |
|
450
|
886 |
(* raw_unify (ignores sorts) *)
|
|
887 |
|
|
888 |
fun raw_unify (ty1, ty2) =
|
|
889 |
(unify tsig0 ((rem_sorts ty1, rem_sorts ty2), []); true)
|
|
890 |
handle TUNIFY => false;
|
|
891 |
|
|
892 |
|
0
|
893 |
(*Type inference for polymorphic term*)
|
|
894 |
fun infer tsig =
|
256
|
895 |
let fun inf(Ts, Const (_, T), tye) = (T, tye)
|
|
896 |
| inf(Ts, Free (_, T), tye) = (T, tye)
|
|
897 |
| inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
|
0
|
898 |
handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
|
256
|
899 |
| inf(Ts, Var (_, T), tye) = (T, tye)
|
|
900 |
| inf(Ts, Abs (_, T, body), tye) =
|
|
901 |
let val (U, tye') = inf(T::Ts, body, tye) in (T-->U, tye') end
|
0
|
902 |
| inf(Ts, f$u, tye) =
|
256
|
903 |
let val (U, tyeU) = inf(Ts, u, tye);
|
|
904 |
val (T, tyeT) = inf(Ts, f, tyeU);
|
0
|
905 |
fun err s =
|
|
906 |
raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
|
256
|
907 |
in case T of
|
|
908 |
Type("fun", [T1, T2]) =>
|
|
909 |
( (T2, unify tsig ((T1, U), tyeT))
|
0
|
910 |
handle TUNIFY => err"type mismatch in application" )
|
256
|
911 |
| TVar _ =>
|
0
|
912 |
let val T2 = gen_tyvar([])
|
|
913 |
in (T2, unify tsig ((T, U-->T2), tyeT))
|
|
914 |
handle TUNIFY => err"type mismatch in application"
|
|
915 |
end
|
|
916 |
| _ => err"rator must have function type"
|
|
917 |
end
|
|
918 |
in inf end;
|
|
919 |
|
256
|
920 |
fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)
|
0
|
921 |
| freeze_vars(T as TFree _) = T
|
256
|
922 |
| freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);
|
0
|
923 |
|
|
924 |
(* Attach a type to a constant *)
|
256
|
925 |
fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
|
0
|
926 |
|
|
927 |
(*Find type of ident. If not in table then use ident's name for tyvar
|
|
928 |
to get consistent typing.*)
|
256
|
929 |
fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
|
|
930 |
fun type_of_ixn(types, ixn as (a, _)) =
|
565
|
931 |
case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
|
|
932 |
|
|
933 |
fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
|
0
|
934 |
|
565
|
935 |
fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
|
|
936 |
| constrainAbs _ = sys_error "constrainAbs";
|
256
|
937 |
|
0
|
938 |
|
565
|
939 |
(* attach_types *)
|
|
940 |
|
0
|
941 |
(*
|
256
|
942 |
Attach types to a term. Input is a "parse tree" containing dummy types.
|
|
943 |
Type constraints are translated and checked for validity wrt tsig. TVars in
|
|
944 |
constraints are frozen.
|
0
|
945 |
|
256
|
946 |
The atoms in the resulting term satisfy the following spec:
|
0
|
947 |
|
256
|
948 |
Const (a, T):
|
|
949 |
T is a renamed copy of the generic type of a; renaming decreases index of
|
|
950 |
all TVars by new_tvar_inx(), which is less than ~1. The index of all
|
|
951 |
TVars in the generic type must be 0 for this to work!
|
0
|
952 |
|
256
|
953 |
Free (a, T), Var (ixn, T):
|
|
954 |
T is either the frozen default type of a or TVar (("'"^a, ~1), [])
|
0
|
955 |
|
256
|
956 |
Abs (a, T, _):
|
|
957 |
T is either a type constraint or TVar (("'" ^ a, i), []), where i is
|
|
958 |
generated by new_tvar_inx(). Thus different abstractions can have the
|
|
959 |
bound variables of the same name but different types.
|
0
|
960 |
*)
|
|
961 |
|
565
|
962 |
(* FIXME consitency of sort_env / sorts (!?) *)
|
256
|
963 |
|
565
|
964 |
(* FIXME check *)
|
|
965 |
|
|
966 |
fun attach_types (tsig, const_type, types, sorts) tm =
|
256
|
967 |
let
|
565
|
968 |
val sort_env = Syntax.raw_term_sorts tm;
|
|
969 |
fun def_sort xi = if_none (sorts xi) (defaultS tsig);
|
256
|
970 |
|
565
|
971 |
fun prepareT t =
|
|
972 |
freeze_vars (cert_typ tsig (Syntax.typ_of_term sort_env def_sort t));
|
256
|
973 |
|
|
974 |
fun add (Const (a, _)) =
|
565
|
975 |
(case const_type a of
|
256
|
976 |
Some T => type_const (a, T)
|
|
977 |
| None => raise_type ("No such constant: " ^ quote a) [] [])
|
|
978 |
| add (Free (a, _)) =
|
565
|
979 |
(case const_type a of
|
256
|
980 |
Some T => type_const (a, T)
|
|
981 |
| None => Free (a, type_of_ixn (types, (a, ~1))))
|
|
982 |
| add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
|
565
|
983 |
| add (Bound i) = Bound i
|
256
|
984 |
| add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
|
|
985 |
| add ((f as Const (a, _) $ t1) $ t2) =
|
|
986 |
if a = Syntax.constrainC then
|
|
987 |
constrain (add t1, prepareT t2)
|
|
988 |
else if a = Syntax.constrainAbsC then
|
|
989 |
constrainAbs (add t1, prepareT t2)
|
|
990 |
else add f $ add t2
|
|
991 |
| add (f $ t) = add f $ add t;
|
565
|
992 |
in add tm end;
|
0
|
993 |
|
|
994 |
|
|
995 |
(* Post-Processing *)
|
|
996 |
|
|
997 |
(*Instantiation of type variables in terms*)
|
|
998 |
fun inst_types tye = map_term_types (inst_typ tye);
|
|
999 |
|
|
1000 |
(*Delete explicit constraints -- occurrences of "_constrain" *)
|
256
|
1001 |
fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
|
|
1002 |
| unconstrain ((f as Const(a, _)) $ t) =
|
0
|
1003 |
if a=Syntax.constrainC then unconstrain t
|
|
1004 |
else unconstrain f $ unconstrain t
|
|
1005 |
| unconstrain (f$t) = unconstrain f $ unconstrain t
|
|
1006 |
| unconstrain (t) = t;
|
|
1007 |
|
|
1008 |
|
|
1009 |
(* Turn all TVars which satisfy p into new TFrees *)
|
|
1010 |
fun freeze p t =
|
256
|
1011 |
let val fs = add_term_tfree_names(t, []);
|
|
1012 |
val inxs = filter p (add_term_tvar_ixns(t, []));
|
0
|
1013 |
val vmap = inxs ~~ variantlist(map #1 inxs, fs);
|
256
|
1014 |
fun free(Type(a, Ts)) = Type(a, map free Ts)
|
|
1015 |
| free(T as TVar(v, S)) =
|
|
1016 |
(case assoc(vmap, v) of None => T | Some(a) => TFree(a, S))
|
0
|
1017 |
| free(T as TFree _) = T
|
|
1018 |
in map_term_types free t end;
|
|
1019 |
|
|
1020 |
(* Thaw all TVars that were frozen in freeze_vars *)
|
256
|
1021 |
fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)
|
|
1022 |
| thaw_vars(T as TFree(a, S)) = (case explode a of
|
|
1023 |
"?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
|
|
1024 |
in TVar(("'"^b, i), S) end
|
|
1025 |
| _ => T)
|
0
|
1026 |
| thaw_vars(T) = T;
|
|
1027 |
|
|
1028 |
|
|
1029 |
fun restrict tye =
|
256
|
1030 |
let fun clean(tye1, ((a, i), T)) =
|
|
1031 |
if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1
|
|
1032 |
in foldl clean ([], tye) end
|
0
|
1033 |
|
|
1034 |
|
|
1035 |
(*Infer types for term t using tables. Check that t's type and T unify *)
|
|
1036 |
|
565
|
1037 |
fun infer_term (tsig, const_type, types, sorts, T, t) =
|
|
1038 |
let
|
|
1039 |
val u = attach_types (tsig, const_type, types, sorts) t;
|
|
1040 |
val (U, tye) = infer tsig ([], u, []);
|
|
1041 |
val uu = unconstrain u;
|
|
1042 |
val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
|
|
1043 |
("Term does not have expected type", [T, U], [inst_types tye uu])
|
|
1044 |
val Ttye = restrict tye' (*restriction to TVars in T*)
|
|
1045 |
val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
|
|
1046 |
(*all is a dummy term which contains all exported TVars*)
|
|
1047 |
val Const(_, Type(_, Ts)) $ u'' =
|
|
1048 |
map_term_types thaw_vars (freeze (fn (_, i) => i < 0) all)
|
|
1049 |
(*turn all internally generated TVars into TFrees
|
|
1050 |
and thaw all initially frozen TVars*)
|
|
1051 |
in
|
|
1052 |
(u'', (map fst Ttye) ~~ Ts)
|
|
1053 |
end;
|
0
|
1054 |
|
|
1055 |
fun infer_types args = (tyinit(); infer_term args);
|
|
1056 |
|
|
1057 |
|
|
1058 |
(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
|
256
|
1059 |
fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)
|
|
1060 |
| varifyT (TFree (a, S)) = TVar ((a, 0), S)
|
|
1061 |
| varifyT T = T;
|
0
|
1062 |
|
|
1063 |
(* Turn TFrees except those in fixed into new TVars *)
|
256
|
1064 |
fun varify (t, fixed) =
|
|
1065 |
let val fs = add_term_tfree_names(t, []) \\ fixed;
|
|
1066 |
val ixns = add_term_tvar_ixns(t, []);
|
0
|
1067 |
val fmap = fs ~~ variantlist(fs, map #1 ixns)
|
256
|
1068 |
fun thaw(Type(a, Ts)) = Type(a, map thaw Ts)
|
0
|
1069 |
| thaw(T as TVar _) = T
|
256
|
1070 |
| thaw(T as TFree(a, S)) =
|
|
1071 |
(case assoc(fmap, a) of None => T | Some b => TVar((b, 0), S))
|
0
|
1072 |
in map_term_types thaw t end;
|
|
1073 |
|
|
1074 |
|
|
1075 |
end;
|
256
|
1076 |
|