author | wenzelm |
Tue, 20 May 1997 19:29:50 +0200 | |
changeset 3257 | 4e3724e0659f |
parent 3175 | 02d32516bc92 |
child 3411 | 163f8f4a42d7 |
permissions | -rw-r--r-- |
256 | 1 |
(* Title: Pure/type.ML |
0 | 2 |
ID: $Id$ |
416 | 3 |
Author: Tobias Nipkow & Lawrence C Paulson |
0 | 4 |
|
2964 | 5 |
Type signatures, unification of types, interface to type inference. |
0 | 6 |
*) |
7 |
||
8 |
signature TYPE = |
|
2964 | 9 |
sig |
10 |
(*TFrees vs TVars*) |
|
621 | 11 |
val no_tvars: typ -> typ |
12 |
val varifyT: typ -> typ |
|
13 |
val unvarifyT: typ -> typ |
|
14 |
val varify: term * string list -> term |
|
2964 | 15 |
val freeze_vars: typ -> typ |
16 |
val thaw_vars: typ -> typ |
|
17 |
val freeze: term -> term |
|
18 |
||
19 |
(*type signatures*) |
|
0 | 20 |
type type_sig |
200 | 21 |
val rep_tsig: type_sig -> |
256 | 22 |
{classes: class list, |
2964 | 23 |
classrel: (class * class list) list, |
256 | 24 |
default: sort, |
963 | 25 |
tycons: (string * int) list, |
621 | 26 |
abbrs: (string * (string list * typ)) list, |
963 | 27 |
arities: (string * (class * sort list) list) list} |
0 | 28 |
val defaultS: type_sig -> sort |
2964 | 29 |
val logical_types: type_sig -> string list |
30 |
||
31 |
val subsort: type_sig -> sort * sort -> bool |
|
32 |
val eq_sort: type_sig -> sort * sort -> bool |
|
33 |
val norm_sort: type_sig -> sort -> sort |
|
34 |
val nonempty_sort: type_sig -> sort list -> sort -> bool |
|
35 |
val rem_sorts: typ -> typ |
|
36 |
||
416 | 37 |
val tsig0: type_sig |
621 | 38 |
val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig |
2964 | 39 |
val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig |
422 | 40 |
val ext_tsig_defsort: type_sig -> sort -> type_sig |
582 | 41 |
val ext_tsig_types: type_sig -> (string * int) list -> type_sig |
621 | 42 |
val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig |
963 | 43 |
val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig |
256 | 44 |
val merge_tsigs: type_sig * type_sig -> type_sig |
2964 | 45 |
|
46 |
val typ_errors: type_sig -> typ * string list -> string list |
|
256 | 47 |
val cert_typ: type_sig -> typ -> typ |
48 |
val norm_typ: type_sig -> typ -> typ |
|
2964 | 49 |
|
256 | 50 |
val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term |
2964 | 51 |
|
52 |
(*type matching*) |
|
53 |
exception TYPE_MATCH |
|
256 | 54 |
val typ_match: type_sig -> (indexname * typ) list * (typ * typ) |
55 |
-> (indexname * typ) list |
|
2964 | 56 |
val typ_instance: type_sig * typ * typ -> bool |
3175 | 57 |
val of_sort: type_sig -> typ * sort -> bool |
2964 | 58 |
|
59 |
(*type unification*) |
|
60 |
exception TUNIFY |
|
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1392
diff
changeset
|
61 |
val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ) |
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1392
diff
changeset
|
62 |
-> (indexname * typ) list * int |
450 | 63 |
val raw_unify: typ * typ -> bool |
0 | 64 |
|
2964 | 65 |
(*type inference*) |
66 |
val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list |
|
67 |
-> indexname -> sort |
|
68 |
val constrain: term -> typ -> term |
|
2979 | 69 |
val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T) |
70 |
-> type_sig -> (string -> typ option) -> (indexname -> typ option) |
|
71 |
-> (indexname -> sort option) -> string list -> bool -> typ list -> term list |
|
2964 | 72 |
-> term list * (indexname * typ) list |
73 |
end; |
|
74 |
||
75 |
structure Type: TYPE = |
|
0 | 76 |
struct |
77 |
||
2964 | 78 |
|
621 | 79 |
(*** TFrees vs TVars ***) |
80 |
||
81 |
(*disallow TVars*) |
|
82 |
fun no_tvars T = |
|
83 |
if null (typ_tvars T) then T |
|
84 |
else raise_type "Illegal schematic type variable(s)" [T] []; |
|
85 |
||
2964 | 86 |
(* varify, unvarify *) |
621 | 87 |
|
2964 | 88 |
val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S)); |
89 |
||
621 | 90 |
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts) |
91 |
| unvarifyT (TVar ((a, 0), S)) = TFree (a, S) |
|
92 |
| unvarifyT T = T; |
|
93 |
||
94 |
fun varify (t, fixed) = |
|
95 |
let |
|
96 |
val fs = add_term_tfree_names (t, []) \\ fixed; |
|
97 |
val ixns = add_term_tvar_ixns (t, []); |
|
98 |
val fmap = fs ~~ variantlist (fs, map #1 ixns) |
|
2964 | 99 |
fun thaw (f as (a, S)) = |
100 |
(case assoc (fmap, a) of |
|
101 |
None => TFree f |
|
102 |
| Some b => TVar ((b, 0), S)); |
|
103 |
in |
|
104 |
map_term_types (map_type_tfree thaw) t |
|
105 |
end; |
|
106 |
||
107 |
||
108 |
(* thaw, freeze *) |
|
621 | 109 |
|
2964 | 110 |
val thaw_vars = |
111 |
let |
|
112 |
fun thaw (f as (a, S)) = |
|
113 |
(case explode a of |
|
114 |
"?" :: "'" :: vn => |
|
115 |
let val ((b, i), _) = Syntax.scan_varname vn in |
|
116 |
TVar (("'" ^ b, i), S) |
|
117 |
end |
|
118 |
| _ => TFree f) |
|
119 |
in map_type_tfree thaw end; |
|
120 |
||
121 |
val freeze_vars = |
|
122 |
map_type_tvar (fn (v, S) => TFree (Syntax.string_of_vname v, S)); |
|
621 | 123 |
|
124 |
||
2964 | 125 |
local |
126 |
fun nextname (pref, c) = |
|
127 |
if c = "z" then (pref ^ "a", "a") |
|
128 |
else (pref, chr (ord c + 1)); |
|
416 | 129 |
|
2964 | 130 |
fun newtvars used = |
131 |
let |
|
132 |
fun new ([], _, vmap) = vmap |
|
133 |
| new (ixn :: ixns, p as (pref, c), vmap) = |
|
134 |
let val nm = pref ^ c in |
|
135 |
if nm mem_string used then new (ixn :: ixns, nextname p, vmap) |
|
136 |
else new (ixns, nextname p, (ixn, nm) :: vmap) |
|
137 |
end |
|
138 |
in new end; |
|
416 | 139 |
|
2964 | 140 |
(*Turn all TVars which satisfy p into new (if freeze then TFrees else TVars). |
141 |
Note that if t contains frozen TVars there is the possibility that a TVar is |
|
142 |
turned into one of those. This is sound but not complete.*) |
|
416 | 143 |
|
2964 | 144 |
fun convert used freeze p t = |
145 |
let |
|
146 |
val used = |
|
147 |
if freeze then add_term_tfree_names (t, used) |
|
148 |
else used union (map #1 (filter_out p (add_term_tvar_ixns (t, [])))); |
|
149 |
val ixns = filter p (add_term_tvar_ixns (t, [])); |
|
150 |
val vmap = newtvars used (ixns, ("'", "a"), []); |
|
151 |
fun conv (var as (ixn, S)) = |
|
152 |
(case assoc (vmap, ixn) of |
|
153 |
None => TVar(var) |
|
154 |
| Some a => if freeze then TFree (a, S) else TVar ((a, 0), S)); |
|
155 |
in |
|
156 |
map_term_types (map_type_tvar conv) t |
|
157 |
end; |
|
158 |
in |
|
159 |
fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t; |
|
160 |
end; |
|
256 | 161 |
|
162 |
||
163 |
||
416 | 164 |
(*** type signatures ***) |
256 | 165 |
|
2964 | 166 |
(* type type_sig *) |
167 |
||
256 | 168 |
(* |
169 |
classes: |
|
2964 | 170 |
list of all declared classes; |
0 | 171 |
|
2964 | 172 |
classrel: |
173 |
(see Pure/sorts.ML) |
|
256 | 174 |
|
175 |
default: |
|
2964 | 176 |
default sort attached to all unconstrained type vars; |
256 | 177 |
|
963 | 178 |
tycons: |
2964 | 179 |
association list of all declared types with the number of their |
256 | 180 |
arguments; |
181 |
||
182 |
abbrs: |
|
2964 | 183 |
association list of type abbreviations; |
256 | 184 |
|
963 | 185 |
arities: |
2964 | 186 |
(see Pure/sorts.ML) |
0 | 187 |
*) |
188 |
||
256 | 189 |
datatype type_sig = |
190 |
TySg of { |
|
191 |
classes: class list, |
|
2964 | 192 |
classrel: (class * class list) list, |
256 | 193 |
default: sort, |
963 | 194 |
tycons: (string * int) list, |
621 | 195 |
abbrs: (string * (string list * typ)) list, |
2964 | 196 |
arities: (string * (class * sort list) list) list}; |
256 | 197 |
|
189 | 198 |
fun rep_tsig (TySg comps) = comps; |
0 | 199 |
|
256 | 200 |
fun defaultS (TySg {default, ...}) = default; |
201 |
||
2964 | 202 |
fun logical_types (TySg {classrel, arities, tycons, ...}) = |
203 |
let |
|
204 |
fun log_class c = Sorts.class_le classrel (c, logicC); |
|
205 |
fun log_type t = exists (log_class o #1) (assocs arities t); |
|
206 |
in |
|
207 |
filter log_type (map #1 tycons) |
|
208 |
end; |
|
209 |
||
210 |
||
211 |
(* sorts *) |
|
212 |
||
213 |
(* FIXME declared!? *) |
|
214 |
||
215 |
fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel; |
|
216 |
fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel; |
|
217 |
fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel; |
|
218 |
||
219 |
fun nonempty_sort (tsig as TySg {classrel, arities, ...}) hyps S = |
|
220 |
Sorts.nonempty_sort classrel arities hyps S; |
|
221 |
||
222 |
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys) |
|
223 |
| rem_sorts (TFree (x, _)) = TFree (x, []) |
|
224 |
| rem_sorts (TVar (xi, _)) = TVar (xi, []); |
|
225 |
||
256 | 226 |
|
582 | 227 |
(* error messages *) |
256 | 228 |
|
416 | 229 |
fun undcl_class c = "Undeclared class " ^ quote c; |
2233
f919bdd5f9b6
Removed or eta-expanded some declarations that are illegal under value
paulson
parents:
2182
diff
changeset
|
230 |
fun err_undcl_class s = error (undcl_class s); |
0 | 231 |
|
422 | 232 |
fun err_dup_classes cs = |
233 |
error ("Duplicate declaration of class(es) " ^ commas_quote cs); |
|
416 | 234 |
|
235 |
fun undcl_type c = "Undeclared type constructor " ^ quote c; |
|
256 | 236 |
|
582 | 237 |
fun err_neg_args c = |
238 |
error ("Negative number of arguments of type constructor " ^ quote c); |
|
239 |
||
416 | 240 |
fun err_dup_tycon c = |
241 |
error ("Duplicate declaration of type constructor " ^ quote c); |
|
242 |
||
621 | 243 |
fun dup_tyabbrs ts = |
244 |
"Duplicate declaration of type abbreviation(s) " ^ commas_quote ts; |
|
416 | 245 |
|
246 |
fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c; |
|
0 | 247 |
|
248 |
||
2964 | 249 |
(* FIXME err_undcl_class! *) |
0 | 250 |
(* 'leq' checks the partial order on classes according to the |
2964 | 251 |
statements in the association list 'a' (i.e. 'classrel') |
0 | 252 |
*) |
253 |
||
256 | 254 |
fun less a (C, D) = case assoc (a, C) of |
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
255 |
Some ss => D mem_string ss |
621 | 256 |
| None => err_undcl_class C; |
0 | 257 |
|
256 | 258 |
fun leq a (C, D) = C = D orelse less a (C, D); |
0 | 259 |
|
260 |
||
261 |
||
2964 | 262 |
(* FIXME *) |
200 | 263 |
(*Instantiation of type variables in types*) |
264 |
(*Pre: instantiations obey restrictions! *) |
|
265 |
fun inst_typ tye = |
|
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
266 |
let fun inst(var as (v, _)) = case assoc(tye, v) of |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
267 |
Some U => inst_typ tye U |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
268 |
| None => TVar(var) |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
269 |
in map_type_tvar inst end; |
0 | 270 |
|
271 |
||
3175 | 272 |
|
273 |
fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort classrel arities; |
|
274 |
||
275 |
fun check_has_sort (tsig, T, S) = |
|
276 |
if of_sort tsig (T, S) then () |
|
2991 | 277 |
else raise_type ("Type not of sort " ^ Sorts.str_of_sort S) [T] []; |
0 | 278 |
|
279 |
||
280 |
(*Instantiation of type variables in types *) |
|
256 | 281 |
fun inst_typ_tvars(tsig, tye) = |
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
282 |
let fun inst(var as (v, S)) = case assoc(tye, v) of |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
283 |
Some U => (check_has_sort(tsig, U, S); U) |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
284 |
| None => TVar(var) |
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
285 |
in map_type_tvar inst end; |
0 | 286 |
|
287 |
(*Instantiation of type variables in terms *) |
|
2617 | 288 |
fun inst_term_tvars (_,[]) t = t |
289 |
| inst_term_tvars arg t = map_term_types (inst_typ_tvars arg) t; |
|
200 | 290 |
|
291 |
||
1484 | 292 |
(* norm_typ *) |
200 | 293 |
|
2991 | 294 |
(*expand abbreviations and normalize sorts*) |
295 |
fun norm_typ (tsig as TySg {abbrs, ...}) ty = |
|
256 | 296 |
let |
621 | 297 |
val idx = maxidx_of_typ ty + 1; |
298 |
||
2991 | 299 |
fun norm (Type (a, Ts)) = |
256 | 300 |
(case assoc (abbrs, a) of |
2991 | 301 |
Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U)) |
302 |
| None => Type (a, map norm Ts)) |
|
303 |
| norm (TFree (x, S)) = TFree (x, norm_sort tsig S) |
|
304 |
| norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S); |
|
256 | 305 |
in |
2991 | 306 |
norm ty |
256 | 307 |
end; |
308 |
||
309 |
||
310 |
||
311 |
||
312 |
||
313 |
(** build type signatures **) |
|
314 |
||
2964 | 315 |
fun make_tsig (classes, classrel, default, tycons, abbrs, arities) = |
316 |
TySg {classes = classes, classrel = classrel, default = default, |
|
963 | 317 |
tycons = tycons, abbrs = abbrs, arities = arities}; |
416 | 318 |
|
319 |
val tsig0 = make_tsig ([], [], [], [], [], []); |
|
256 | 320 |
|
0 | 321 |
|
1215
a206f722bef9
added nonempty_sort (a somewhat braindead version!);
wenzelm
parents:
963
diff
changeset
|
322 |
|
a206f722bef9
added nonempty_sort (a somewhat braindead version!);
wenzelm
parents:
963
diff
changeset
|
323 |
|
416 | 324 |
(* typ_errors *) |
256 | 325 |
|
416 | 326 |
(*check validity of (not necessarily normal) type; accumulate error messages*) |
256 | 327 |
|
416 | 328 |
fun typ_errors tsig (typ, errors) = |
256 | 329 |
let |
963 | 330 |
val TySg {classes, tycons, abbrs, ...} = tsig; |
416 | 331 |
|
332 |
fun class_err (errs, c) = |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
333 |
if c mem_string classes then errs |
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
334 |
else undcl_class c ins_string errs; |
256 | 335 |
|
336 |
val sort_err = foldl class_err; |
|
0 | 337 |
|
256 | 338 |
fun typ_errs (Type (c, Us), errs) = |
339 |
let |
|
340 |
val errs' = foldr typ_errs (Us, errs); |
|
341 |
fun nargs n = |
|
342 |
if n = length Us then errs' |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
343 |
else ("Wrong number of arguments: " ^ quote c) ins_string errs'; |
256 | 344 |
in |
963 | 345 |
(case assoc (tycons, c) of |
256 | 346 |
Some n => nargs n |
347 |
| None => |
|
348 |
(case assoc (abbrs, c) of |
|
349 |
Some (vs, _) => nargs (length vs) |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
350 |
| None => undcl_type c ins_string errs)) |
256 | 351 |
end |
352 |
| typ_errs (TFree (_, S), errs) = sort_err (errs, S) |
|
416 | 353 |
| typ_errs (TVar ((x, i), S), errs) = |
354 |
if i < 0 then |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
355 |
("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S) |
416 | 356 |
else sort_err (errs, S); |
256 | 357 |
in |
416 | 358 |
typ_errs (typ, errors) |
256 | 359 |
end; |
360 |
||
361 |
||
362 |
(* cert_typ *) |
|
363 |
||
2964 | 364 |
(*check and normalize typ wrt. tsig*) (*exception TYPE*) |
365 |
fun cert_typ tsig T = |
|
366 |
(case typ_errors tsig (T, []) of |
|
367 |
[] => norm_typ tsig T |
|
368 |
| errs => raise_type (cat_lines errs) [T] []); |
|
256 | 369 |
|
370 |
||
371 |
||
422 | 372 |
(** merge type signatures **) |
256 | 373 |
|
422 | 374 |
(*'assoc_union' merges two association lists if the contents associated |
375 |
the keys are lists*) |
|
0 | 376 |
|
422 | 377 |
fun assoc_union (as1, []) = as1 |
378 |
| assoc_union (as1, (key, l2) :: as2) = |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
379 |
(case assoc_string (as1, key) of |
2964 | 380 |
Some l1 => assoc_union |
381 |
(overwrite (as1, (key, l1 union_string l2)), as2) |
|
422 | 382 |
| None => assoc_union ((key, l2) :: as1, as2)); |
0 | 383 |
|
384 |
||
2964 | 385 |
(* merge classrel *) |
0 | 386 |
|
2964 | 387 |
fun merge_classrel (classrel1, classrel2) = |
388 |
let val classrel = transitive_closure (assoc_union (classrel1, classrel2)) |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
389 |
in |
2964 | 390 |
if exists (op mem_string) classrel then |
422 | 391 |
error ("Cyclic class structure!") (* FIXME improve msg, raise TERM *) |
2964 | 392 |
else classrel |
416 | 393 |
end; |
394 |
||
395 |
||
422 | 396 |
(* coregularity *) |
0 | 397 |
|
398 |
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) |
|
399 |
||
963 | 400 |
fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of |
0 | 401 |
Some(w1) => if w = w1 then () else |
256 | 402 |
error("There are two declarations\n" ^ |
2964 | 403 |
Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^ |
404 |
Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^ |
|
0 | 405 |
"with the same result class.") |
406 |
| None => (); |
|
407 |
||
963 | 408 |
(* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2 |
0 | 409 |
such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *) |
410 |
||
963 | 411 |
fun coreg_err(t, (C1,w1), (C2,w2)) = |
2964 | 412 |
error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and " |
413 |
^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict"); |
|
0 | 414 |
|
2964 | 415 |
fun coreg classrel (t, Cw1) = |
416 |
let |
|
417 |
fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) = |
|
418 |
if leq classrel (C1,C2) then |
|
419 |
if Sorts.sorts_le classrel (w1,w2) then () |
|
420 |
else coreg_err(t, Cw1, Cw2) |
|
421 |
else () |
|
422 |
fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1)) |
|
963 | 423 |
in seq check end; |
0 | 424 |
|
2964 | 425 |
fun add_arity classrel ars (tCw as (_,Cw)) = |
426 |
(is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars); |
|
0 | 427 |
|
256 | 428 |
fun varying_decls t = |
429 |
error ("Type constructor " ^ quote t ^ " has varying number of arguments"); |
|
0 | 430 |
|
431 |
||
963 | 432 |
(* 'merge_arities' builds the union of two 'arities' lists; |
422 | 433 |
it only checks the two restriction conditions and inserts afterwards |
434 |
all elements of the second list into the first one *) |
|
435 |
||
2964 | 436 |
fun merge_arities classrel = |
437 |
let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw); |
|
422 | 438 |
|
963 | 439 |
fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of |
440 |
Some(ars1) => |
|
441 |
let val ars = foldl (test_ar t) (ars1, ars2) |
|
442 |
in overwrite (arities1, (t,ars)) end |
|
443 |
| None => c::arities1 |
|
422 | 444 |
in foldl merge_c end; |
445 |
||
963 | 446 |
fun add_tycons (tycons, tn as (t,n)) = |
447 |
(case assoc (tycons, t) of |
|
448 |
Some m => if m = n then tycons else varying_decls t |
|
449 |
| None => tn :: tycons); |
|
422 | 450 |
|
451 |
fun merge_abbrs (abbrs1, abbrs2) = |
|
621 | 452 |
let val abbrs = abbrs1 union abbrs2 in |
453 |
(case gen_duplicates eq_fst abbrs of |
|
422 | 454 |
[] => abbrs |
621 | 455 |
| dups => raise_term (dup_tyabbrs (map fst dups)) []) |
422 | 456 |
end; |
457 |
||
458 |
||
459 |
(* 'merge_tsigs' takes the above declared functions to merge two type |
|
460 |
signatures *) |
|
461 |
||
2964 | 462 |
fun merge_tsigs(TySg{classes=classes1, default=default1, classrel=classrel1, |
963 | 463 |
tycons=tycons1, arities=arities1, abbrs=abbrs1}, |
2964 | 464 |
TySg{classes=classes2, default=default2, classrel=classrel2, |
963 | 465 |
tycons=tycons2, arities=arities2, abbrs=abbrs2}) = |
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
466 |
let val classes' = classes1 union_string classes2; |
2964 | 467 |
val classrel' = merge_classrel (classrel1, classrel2); |
963 | 468 |
val tycons' = foldl add_tycons (tycons1, tycons2) |
2964 | 469 |
val arities' = merge_arities classrel' (arities1, arities2); |
470 |
val default' = Sorts.norm_sort classrel' (default1 @ default2); |
|
422 | 471 |
val abbrs' = merge_abbrs(abbrs1, abbrs2); |
2964 | 472 |
in make_tsig(classes', classrel', default', tycons', abbrs', arities') end; |
422 | 473 |
|
474 |
||
475 |
||
476 |
(*** extend type signatures ***) |
|
477 |
||
2964 | 478 |
(** add classes and classrel relations **) |
422 | 479 |
|
480 |
fun add_classes classes cs = |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
481 |
(case cs inter_string classes of |
422 | 482 |
[] => cs @ classes |
483 |
| dups => err_dup_classes cs); |
|
484 |
||
485 |
||
2964 | 486 |
(*'add_classrel' adds a tuple consisting of a new class (the new class has |
422 | 487 |
already been inserted into the 'classes' list) and its superclasses (they |
2964 | 488 |
must be declared in 'classes' too) to the 'classrel' list of the given type |
422 | 489 |
signature; furthermore all inherited superclasses according to the |
490 |
superclasses brought with are inserted and there is a check that there are |
|
491 |
no cycles (i.e. C <= D <= C, with C <> D);*) |
|
492 |
||
2964 | 493 |
fun add_classrel classes (classrel, (s, ges)) = |
621 | 494 |
let |
2964 | 495 |
fun upd (classrel, s') = |
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
496 |
if s' mem_string classes then |
2964 | 497 |
let val ges' = the (assoc (classrel, s)) |
498 |
in case assoc (classrel, s') of |
|
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
499 |
Some sups => if s mem_string sups |
422 | 500 |
then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) |
2964 | 501 |
else overwrite |
502 |
(classrel, (s, sups union_string ges')) |
|
503 |
| None => classrel |
|
621 | 504 |
end |
505 |
else err_undcl_class s' |
|
2964 | 506 |
in foldl upd (classrel @ [(s, ges)], ges) end; |
422 | 507 |
|
508 |
||
509 |
(* 'extend_classes' inserts all new classes into the corresponding |
|
2964 | 510 |
lists ('classes', 'classrel') if possible *) |
422 | 511 |
|
2964 | 512 |
fun extend_classes (classes, classrel, new_classes) = |
621 | 513 |
let |
514 |
val classes' = add_classes classes (map fst new_classes); |
|
2964 | 515 |
val classrel' = foldl (add_classrel classes') (classrel, new_classes); |
516 |
in (classes', classrel') end; |
|
422 | 517 |
|
518 |
||
621 | 519 |
(* ext_tsig_classes *) |
520 |
||
521 |
fun ext_tsig_classes tsig new_classes = |
|
522 |
let |
|
2964 | 523 |
val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig; |
524 |
val (classes',classrel') = extend_classes (classes,classrel,new_classes); |
|
621 | 525 |
in |
2964 | 526 |
make_tsig (classes', classrel', default, tycons, abbrs, arities) |
621 | 527 |
end; |
528 |
||
529 |
||
2964 | 530 |
(* ext_tsig_classrel *) |
422 | 531 |
|
2964 | 532 |
fun ext_tsig_classrel tsig pairs = |
422 | 533 |
let |
2964 | 534 |
val TySg {classes, classrel, default, tycons, abbrs, arities} = tsig; |
422 | 535 |
|
536 |
(* FIXME clean! *) |
|
2964 | 537 |
val classrel' = |
538 |
merge_classrel (classrel, map (fn (c1, c2) => (c1, [c2])) pairs); |
|
422 | 539 |
in |
2964 | 540 |
make_tsig (classes, classrel', default, tycons, abbrs, arities) |
422 | 541 |
end; |
542 |
||
543 |
||
544 |
(* ext_tsig_defsort *) |
|
545 |
||
2964 | 546 |
fun ext_tsig_defsort(TySg{classes,classrel,tycons,abbrs,arities,...}) default = |
547 |
make_tsig (classes, classrel, default, tycons, abbrs, arities); |
|
422 | 548 |
|
549 |
||
550 |
||
621 | 551 |
(** add types **) |
582 | 552 |
|
2964 | 553 |
fun ext_tsig_types (TySg {classes, classrel, default, tycons, abbrs, arities}) ts = |
582 | 554 |
let |
555 |
fun check_type (c, n) = |
|
556 |
if n < 0 then err_neg_args c |
|
963 | 557 |
else if is_some (assoc (tycons, c)) then err_dup_tycon c |
2233
f919bdd5f9b6
Removed or eta-expanded some declarations that are illegal under value
paulson
parents:
2182
diff
changeset
|
558 |
else if is_some (assoc (abbrs, c)) then error (ty_confl c) |
582 | 559 |
else (); |
560 |
in |
|
561 |
seq check_type ts; |
|
2964 | 562 |
make_tsig (classes, classrel, default, ts @ tycons, abbrs, |
963 | 563 |
map (rpair [] o #1) ts @ arities) |
582 | 564 |
end; |
565 |
||
566 |
||
567 |
||
568 |
(** add type abbreviations **) |
|
569 |
||
570 |
fun abbr_errors tsig (a, (lhs_vs, rhs)) = |
|
571 |
let |
|
963 | 572 |
val TySg {tycons, abbrs, ...} = tsig; |
621 | 573 |
val rhs_vs = map (#1 o #1) (typ_tvars rhs); |
582 | 574 |
|
575 |
val dup_lhs_vars = |
|
576 |
(case duplicates lhs_vs of |
|
577 |
[] => [] |
|
621 | 578 |
| vs => ["Duplicate variables on lhs: " ^ commas_quote vs]); |
582 | 579 |
|
580 |
val extra_rhs_vars = |
|
581 |
(case gen_rems (op =) (rhs_vs, lhs_vs) of |
|
582 |
[] => [] |
|
621 | 583 |
| vs => ["Extra variables on rhs: " ^ commas_quote vs]); |
582 | 584 |
|
585 |
val tycon_confl = |
|
963 | 586 |
if is_none (assoc (tycons, a)) then [] |
582 | 587 |
else [ty_confl a]; |
588 |
||
589 |
val dup_abbr = |
|
590 |
if is_none (assoc (abbrs, a)) then [] |
|
591 |
else ["Duplicate declaration of abbreviation"]; |
|
592 |
in |
|
593 |
dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @ |
|
594 |
typ_errors tsig (rhs, []) |
|
595 |
end; |
|
596 |
||
621 | 597 |
fun prep_abbr tsig (a, vs, raw_rhs) = |
598 |
let |
|
599 |
fun err msgs = (seq writeln msgs; |
|
600 |
error ("The error(s) above occurred in type abbreviation " ^ quote a)); |
|
601 |
||
602 |
val rhs = rem_sorts (varifyT (no_tvars raw_rhs)) |
|
603 |
handle TYPE (msg, _, _) => err [msg]; |
|
604 |
val abbr = (a, (vs, rhs)); |
|
605 |
in |
|
582 | 606 |
(case abbr_errors tsig abbr of |
621 | 607 |
[] => abbr |
608 |
| msgs => err msgs) |
|
582 | 609 |
end; |
610 |
||
2964 | 611 |
fun add_abbr (tsig as TySg{classes,classrel,default,tycons,arities,abbrs}, |
963 | 612 |
abbr) = |
621 | 613 |
make_tsig |
2964 | 614 |
(classes,classrel,default,tycons, prep_abbr tsig abbr :: abbrs, arities); |
621 | 615 |
|
616 |
fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs); |
|
582 | 617 |
|
618 |
||
619 |
||
422 | 620 |
(** add arities **) |
621 |
||
0 | 622 |
(* 'coregular' checks |
963 | 623 |
- the two restrictions 'is_unique_decl' and 'coreg' |
256 | 624 |
- if the classes in the new type declarations are known in the |
0 | 625 |
given type signature |
626 |
- if one type constructor has always the same number of arguments; |
|
256 | 627 |
if one type declaration has passed all checks it is inserted into |
963 | 628 |
the 'arities' association list of the given type signatrure *) |
0 | 629 |
|
2964 | 630 |
fun coregular (classes, classrel, tycons) = |
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2148
diff
changeset
|
631 |
let fun ex C = if C mem_string classes then () else err_undcl_class(C); |
0 | 632 |
|
963 | 633 |
fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of |
0 | 634 |
Some(n) => if n <> length w then varying_decls(t) else |
963 | 635 |
((seq o seq) ex w; ex C; |
636 |
let val ars = the (assoc(arities, t)) |
|
2964 | 637 |
val ars' = add_arity classrel ars (t,(C,w)) |
963 | 638 |
in overwrite(arities, (t,ars')) end) |
2233
f919bdd5f9b6
Removed or eta-expanded some declarations that are illegal under value
paulson
parents:
2182
diff
changeset
|
639 |
| None => error (undcl_type t); |
0 | 640 |
|
963 | 641 |
in addar end; |
0 | 642 |
|
643 |
||
963 | 644 |
(* 'close' extends the 'arities' association list after all new type |
0 | 645 |
declarations have been inserted successfully: |
646 |
for every declaration t:(Ss)C , for all classses D with C <= D: |
|
647 |
if there is no declaration t:(Ss')C' with C < C' and C' <= D |
|
963 | 648 |
then insert the declaration t:(Ss)D into 'arities' |
0 | 649 |
this means, if there exists a declaration t:(Ss)C and there is |
650 |
no declaration t:(Ss')D with C <=D then the declaration holds |
|
256 | 651 |
for all range classes more general than C *) |
652 |
||
2964 | 653 |
fun close classrel arities = |
654 |
let fun check sl (l, (s, dom)) = case assoc (classrel, s) of |
|
621 | 655 |
Some sups => |
256 | 656 |
let fun close_sup (l, sup) = |
2964 | 657 |
if exists (fn s'' => less classrel (s, s'') andalso |
658 |
leq classrel (s'', sup)) sl |
|
0 | 659 |
then l |
256 | 660 |
else (sup, dom)::l |
661 |
in foldl close_sup (l, sups) end |
|
0 | 662 |
| None => l; |
256 | 663 |
fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l)); |
963 | 664 |
in map ext arities end; |
0 | 665 |
|
422 | 666 |
|
621 | 667 |
(* ext_tsig_arities *) |
256 | 668 |
|
2964 | 669 |
fun norm_domain classrel = |
670 |
let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran)) |
|
671 |
in map one_min end; |
|
672 |
||
621 | 673 |
fun ext_tsig_arities tsig sarities = |
416 | 674 |
let |
2964 | 675 |
val TySg {classes, classrel, default, tycons, arities, abbrs} = tsig; |
963 | 676 |
val arities1 = |
2964 | 677 |
List.concat |
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2617
diff
changeset
|
678 |
(map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities); |
2964 | 679 |
val arities2 = foldl (coregular (classes, classrel, tycons)) |
680 |
(arities, norm_domain classrel arities1) |
|
681 |
|> close classrel; |
|
416 | 682 |
in |
2964 | 683 |
make_tsig (classes, classrel, default, tycons, abbrs, arities2) |
416 | 684 |
end; |
0 | 685 |
|
686 |
||
416 | 687 |
|
2964 | 688 |
(*** type unification and friends ***) |
0 | 689 |
|
2964 | 690 |
(** matching **) |
0 | 691 |
|
2964 | 692 |
exception TYPE_MATCH; |
0 | 693 |
|
2964 | 694 |
fun typ_match tsig = |
695 |
let |
|
696 |
fun match (subs, (TVar (v, S), T)) = |
|
697 |
(case assoc (subs, v) of |
|
698 |
None => ((v, (check_has_sort (tsig, T, S); T)) :: subs |
|
699 |
handle TYPE _ => raise TYPE_MATCH) |
|
700 |
| Some U => if U = T then subs else raise TYPE_MATCH) |
|
701 |
| match (subs, (Type (a, Ts), Type (b, Us))) = |
|
702 |
if a <> b then raise TYPE_MATCH |
|
703 |
else foldl match (subs, Ts ~~ Us) |
|
704 |
| match (subs, (TFree x, TFree y)) = |
|
705 |
if x = y then subs else raise TYPE_MATCH |
|
706 |
| match _ = raise TYPE_MATCH; |
|
707 |
in match end; |
|
0 | 708 |
|
2964 | 709 |
fun typ_instance (tsig, T, U) = |
710 |
(typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false; |
|
711 |
||
0 | 712 |
|
2964 | 713 |
|
714 |
(** unification **) |
|
715 |
||
0 | 716 |
exception TUNIFY; |
717 |
||
718 |
||
2964 | 719 |
(* occurs check *) |
0 | 720 |
|
2964 | 721 |
fun occurs v tye = |
722 |
let |
|
723 |
fun occ (Type (_, Ts)) = exists occ Ts |
|
724 |
| occ (TFree _) = false |
|
725 |
| occ (TVar (w, _)) = |
|
726 |
eq_ix (v, w) orelse |
|
727 |
(case assoc (tye, w) of |
|
728 |
None => false |
|
729 |
| Some U => occ U); |
|
0 | 730 |
in occ end; |
731 |
||
2964 | 732 |
|
733 |
(* chase variable assignments *) |
|
734 |
||
735 |
(*if devar returns a type var then it must be unassigned*) |
|
736 |
fun devar (T as TVar (v, _), tye) = |
|
737 |
(case assoc (tye, v) of |
|
738 |
Some U => devar (U, tye) |
|
739 |
| None => T) |
|
256 | 740 |
| devar (T, tye) = T; |
0 | 741 |
|
1627 | 742 |
|
2964 | 743 |
(* add_env *) |
0 | 744 |
|
2964 | 745 |
(*avoids chains 'a |-> 'b |-> 'c ...*) |
746 |
fun add_env (p, []) = [p] |
|
747 |
| add_env (vT as (v, T), (xU as (x, TVar (w, S))) :: ps) = |
|
748 |
(if eq_ix (v, w) then (x, T) else xU) :: add_env (vT, ps) |
|
749 |
| add_env (v, x :: xs) = x :: add_env (v, xs); |
|
0 | 750 |
|
751 |
||
2964 | 752 |
(* unify *) |
753 |
||
754 |
fun unify (tsig as TySg {classrel, arities, ...}) maxidx tyenv TU = |
|
755 |
let |
|
756 |
val tyvar_count = ref maxidx; |
|
757 |
fun gen_tyvar S = TVar (("'a", inc tyvar_count), S); |
|
758 |
||
759 |
fun mg_domain a S = |
|
760 |
Sorts.mg_domain classrel arities a S handle TYPE _ => raise TUNIFY; |
|
761 |
||
762 |
fun meet ((_, []), tye) = tye |
|
763 |
| meet ((TVar (xi, S'), S), tye) = |
|
764 |
if Sorts.sort_le classrel (S', S) then tye |
|
765 |
else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye) |
|
766 |
| meet ((TFree (_, S'), S), tye) = |
|
767 |
if Sorts.sort_le classrel (S', S) then tye |
|
768 |
else raise TUNIFY |
|
769 |
| meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye) |
|
770 |
and meets (([], []), tye) = tye |
|
771 |
| meets ((T :: Ts, S :: Ss), tye) = |
|
772 |
meets ((Ts, Ss), meet ((devar (T, tye), S), tye)) |
|
773 |
| meets _ = sys_error "meets"; |
|
774 |
||
775 |
fun unif ((ty1, ty2), tye) = |
|
776 |
(case (devar (ty1, tye), devar (ty2, tye)) of |
|
777 |
(T as TVar (v, S1), U as TVar (w, S2)) => |
|
778 |
if eq_ix (v, w) then tye |
|
779 |
else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye) |
|
780 |
else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye) |
|
781 |
else |
|
782 |
let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in |
|
783 |
add_env ((v, S), add_env ((w, S), tye)) |
|
784 |
end |
|
785 |
| (TVar (v, S), T) => |
|
786 |
if occurs v tye T then raise TUNIFY |
|
787 |
else meet ((T, S), add_env ((v, T), tye)) |
|
788 |
| (T, TVar (v, S)) => |
|
789 |
if occurs v tye T then raise TUNIFY |
|
790 |
else meet ((T, S), add_env ((v, T), tye)) |
|
791 |
| (Type (a, Ts), Type (b, Us)) => |
|
792 |
if a <> b then raise TUNIFY |
|
793 |
else foldr unif (Ts ~~ Us, tye) |
|
794 |
| (T, U) => if T = U then tye else raise TUNIFY); |
|
795 |
in |
|
796 |
(unif (TU, tyenv), ! tyvar_count) |
|
797 |
end; |
|
0 | 798 |
|
799 |
||
2964 | 800 |
(* raw_unify *) |
0 | 801 |
|
2964 | 802 |
(*purely structural unification -- ignores sorts*) |
450 | 803 |
fun raw_unify (ty1, ty2) = |
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1392
diff
changeset
|
804 |
(unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true) |
450 | 805 |
handle TUNIFY => false; |
806 |
||
807 |
||
0 | 808 |
|
2964 | 809 |
(** type inference **) |
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1392
diff
changeset
|
810 |
|
2964 | 811 |
(* constraints *) |
2587 | 812 |
|
813 |
fun get_sort tsig def_sort env xi = |
|
814 |
(case (assoc (env, xi), def_sort xi) of |
|
815 |
(None, None) => defaultS tsig |
|
816 |
| (None, Some S) => S |
|
817 |
| (Some S, None) => S |
|
818 |
| (Some S, Some S') => |
|
819 |
if eq_sort tsig (S, S') then S |
|
820 |
else error ("Sort constraint inconsistent with default for type variable " ^ |
|
821 |
quote (Syntax.string_of_vname' xi))); |
|
822 |
||
2964 | 823 |
fun constrain t T = |
824 |
if T = dummyT then t |
|
825 |
else Const ("_type_constraint_", T) $ t; |
|
0 | 826 |
|
827 |
||
2964 | 828 |
(* decode_types *) |
0 | 829 |
|
2964 | 830 |
(*transform parse tree into raw term (idempotent)*) |
831 |
fun decode_types tsig is_const def_type def_sort tm = |
|
832 |
let |
|
833 |
fun get_type xi = if_none (def_type xi) dummyT; |
|
834 |
val sort_env = Syntax.raw_term_sorts (eq_sort tsig) tm; |
|
835 |
||
836 |
fun decodeT t = |
|
837 |
cert_typ tsig (Syntax.typ_of_term (get_sort tsig def_sort sort_env) t); |
|
0 | 838 |
|
2964 | 839 |
fun decode (Const ("_constrain", _) $ t $ typ) = |
840 |
constrain (decode t) (decodeT typ) |
|
841 |
| decode (Const ("_constrainAbs", _) $ (abs as Abs (x, T, t)) $ typ) = |
|
842 |
if T = dummyT then Abs (x, decodeT typ, decode t) |
|
843 |
else constrain abs (decodeT typ --> dummyT) |
|
844 |
| decode (Abs (x, T, t)) = Abs (x, T, decode t) |
|
845 |
| decode (t $ u) = decode t $ decode u |
|
846 |
| decode (t as Free (x, T)) = |
|
847 |
if is_const x then Const (x, T) |
|
848 |
else if T = dummyT then Free (x, get_type (x, ~1)) |
|
849 |
else constrain t (get_type (x, ~1)) |
|
850 |
| decode (t as Var (xi, T)) = |
|
851 |
if T = dummyT then Var (xi, get_type xi) |
|
852 |
else constrain t (get_type xi) |
|
853 |
| decode (t as Bound _) = t |
|
854 |
| decode (t as Const _) = t; |
|
855 |
in |
|
856 |
decode tm |
|
857 |
end; |
|
0 | 858 |
|
859 |
||
2964 | 860 |
(* infer_types *) |
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
861 |
|
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
862 |
(* |
2964 | 863 |
Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti |
864 |
unifies with Ti (for i=1,...,n). |
|
865 |
||
866 |
tsig: type signature |
|
867 |
const_type: term signature |
|
868 |
def_type: partial map from indexnames to types (constrains Frees, Vars) |
|
869 |
def_sort: partial map from indexnames to sorts (constrains TFrees, TVars) |
|
870 |
used: list of already used type variables |
|
871 |
freeze: if true then generated parameters are turned into TFrees, else TVars |
|
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
621
diff
changeset
|
872 |
*) |
0 | 873 |
|
2964 | 874 |
(*user-supplied inference parameters*) |
875 |
fun q_is_param (x, _) = |
|
876 |
(case explode x of |
|
877 |
"?" :: _ => true |
|
878 |
| _ => false); |
|
0 | 879 |
|
2979 | 880 |
fun infer_types prt prT tsig const_type def_type def_sort used freeze pat_Ts raw_ts = |
565 | 881 |
let |
2964 | 882 |
val TySg {classrel, arities, ...} = tsig; |
883 |
val pat_Ts' = map (cert_typ tsig) pat_Ts; |
|
884 |
val raw_ts' = |
|
885 |
map (decode_types tsig (is_some o const_type) def_type def_sort) raw_ts; |
|
886 |
val (ts, Ts, unifier) = |
|
2979 | 887 |
TypeInfer.infer_types prt prT const_type classrel arities used freeze |
2964 | 888 |
q_is_param raw_ts' pat_Ts'; |
565 | 889 |
in |
2964 | 890 |
(ts, unifier) |
565 | 891 |
end; |
0 | 892 |
|
893 |
end; |