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