Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Copyright (C) 2009-2010,2012,2017 Matthew Fluet. |
2 | * Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh | |
3 | * Jagannathan, and Stephen Weeks. | |
4 | * Copyright (C) 1997-2000 NEC Research Institute. | |
5 | * | |
6 | * MLton is released under a BSD-style license. | |
7 | * See the file MLton-LICENSE for details. | |
8 | *) | |
9 | ||
10 | functor TypeEnv (S: TYPE_ENV_STRUCTS): TYPE_ENV = | |
11 | struct | |
12 | ||
13 | open S | |
14 | ||
15 | structure Layout = | |
16 | struct | |
17 | open Layout | |
18 | val bracket = fn l => | |
19 | seq [str "[", l, str "]"] | |
20 | end | |
21 | local | |
22 | open Layout | |
23 | in | |
24 | val seq = seq | |
25 | val str = str | |
26 | end | |
27 | ||
28 | local | |
29 | open LayoutPretty | |
30 | in | |
31 | val bracket = bracket | |
32 | val dontCare = dontCare | |
33 | val simple = simple | |
34 | end | |
35 | ||
36 | local | |
37 | open Tycon | |
38 | in | |
39 | structure AdmitsEquality = AdmitsEquality | |
40 | structure Kind = Kind | |
41 | end | |
42 | structure Field = Record.Field | |
43 | structure Srecord = SortedRecord | |
44 | structure Set = DisjointSet | |
45 | ||
46 | (* | |
47 | * Keep a clock that the elaborator ticks for each declaration. Associate each | |
48 | * type with a time that indicates the earliest declaration at which the type | |
49 | * occurs. The time is used for several things. | |
50 | * | |
51 | * 1. When we need to generalize a type, we can tell which unknowns appear | |
52 | * only in the declaration under consideration, and can hence be generalized. | |
53 | * | |
54 | * 2. Similarly, for type variables, we can tell if they appear in an earlier | |
55 | * declaration than the one in which they are to be bound, and hence can | |
56 | * not be generalized. | |
57 | * | |
58 | * 3. For "FlexRecord" types, we can tell when it appears only in the declaration | |
59 | * under consideration, and can hence be converted to a "GenFlexRecord" type | |
60 | * which allows for generalization of fields not yet known to be in the | |
61 | * flexRecord. | |
62 | * | |
63 | * 4. For type constructors, we can tell if they are used outside of the scope | |
64 | * of their definition. This handles the side conditions on rules 4, 17, and | |
65 | * 19. | |
66 | *) | |
67 | ||
68 | structure Time:> | |
69 | sig | |
70 | type t | |
71 | ||
72 | val <= : t * t -> bool | |
73 | val equals: t * t -> bool | |
74 | val layout: t -> Layout.t | |
75 | val max: t * t -> t | |
76 | val min: t * t -> t | |
77 | val now: unit -> t | |
78 | val region: t -> Region.t | |
79 | val tick: {region: Region.t} -> unit | |
80 | val zero: t | |
81 | end = | |
82 | struct | |
83 | datatype t = T of {clock: int, | |
84 | region: Region.t} | |
85 | ||
86 | local | |
87 | fun make f (T r) = f r | |
88 | in | |
89 | val clock = make #clock | |
90 | val region = make #region | |
91 | end | |
92 | ||
93 | fun layout t = | |
94 | Layout.tuple [Int.layout (clock t), | |
95 | Region.layout (region t)] | |
96 | ||
97 | local | |
98 | fun make f (t, t') = f (clock t, clock t') | |
99 | in | |
100 | val equals = make Int.equals | |
101 | val op <= = make Int.<= | |
102 | end | |
103 | fun max (t, t') = if t <= t' then t' else t | |
104 | fun min (t, t') = if t <= t' then t else t' | |
105 | ||
106 | val zero = T {clock = 0, region = Region.bogus} | |
107 | ||
108 | local | |
109 | val current: t ref = ref zero | |
110 | in | |
111 | fun now () = !current | |
112 | fun tick {region} = | |
113 | current := T {clock = 1 + clock (!current), | |
114 | region = region} | |
115 | end | |
116 | ||
117 | val tick = Trace.trace ("TypeEnv.Time.tick", Layout.ignore, Unit.layout) tick | |
118 | end | |
119 | ||
120 | structure Tyvar = | |
121 | struct | |
122 | open Tyvar | |
123 | ||
124 | local | |
125 | val {get = info: Tyvar.t -> {isEquality: bool, | |
126 | time: Time.t}, | |
127 | set = setInfo, ...} = | |
128 | Property.getSet | |
129 | (Tyvar.plist, | |
130 | Property.initRaise ("TypeEnv.Tyvar.info", Tyvar.layout)) | |
131 | fun init (a, ie) = | |
132 | setInfo (a, {isEquality = ie, | |
133 | time = Time.now ()}) | |
134 | in | |
135 | local | |
136 | fun make f = f o info | |
137 | in | |
138 | val time = make #time | |
139 | val isEquality = make #isEquality | |
140 | end | |
141 | fun makeString (s, {equality}) = | |
142 | let | |
143 | val a = newString s | |
144 | val _ = init (a, equality) | |
145 | in | |
146 | a | |
147 | end | |
148 | fun makeNoname {equality} = | |
149 | let | |
150 | val a = newNoname () | |
151 | val _ = init (a, equality) | |
152 | in | |
153 | a | |
154 | end | |
155 | fun makeLike a = | |
156 | let | |
157 | val a' = new a | |
158 | val _ = init (a', isEquality a) | |
159 | in | |
160 | a' | |
161 | end | |
162 | end | |
163 | ||
164 | local | |
165 | fun makeLocalNames () = | |
166 | let | |
167 | val a = Char.toInt #"a" | |
168 | val z = Char.toInt #"z" | |
169 | val cnt = Counter.new a | |
170 | fun reset () = Counter.reset (cnt, a) | |
171 | fun next b = | |
172 | let | |
173 | val n = Counter.next cnt | |
174 | in | |
175 | Layout.str | |
176 | (concat [if isEquality b then "''" else "'", | |
177 | if n > z | |
178 | then concat ["a", Int.toString (n - z)] | |
179 | else Char.toString (Char.fromInt n)]) | |
180 | end | |
181 | in | |
182 | {next = next, | |
183 | reset = reset} | |
184 | end | |
185 | in | |
186 | fun makeLayoutPretty () = | |
187 | let | |
188 | val {destroy, get = layoutPretty, set = setLayoutPretty, ...} = | |
189 | Property.destGetSet (plist, Property.initFun Tyvar.layout) | |
190 | fun localInit bs = | |
191 | let | |
192 | val {next, ...} = makeLocalNames () | |
193 | in | |
194 | Vector.foreach | |
195 | (bs, fn b => setLayoutPretty (b, next b)) | |
196 | end | |
197 | in | |
198 | {destroy = destroy, | |
199 | layoutPretty = layoutPretty, | |
200 | localInit = localInit} | |
201 | end | |
202 | ||
203 | fun makeLayoutPrettyLocal () = | |
204 | let | |
205 | val {next, reset} = makeLocalNames () | |
206 | val {destroy, get = layoutPretty, ...} = | |
207 | Property.destGet (plist, Property.initFun next) | |
208 | in | |
209 | {destroy = destroy, | |
210 | layoutPretty = layoutPretty, | |
211 | reset = fn () => (reset (); destroy ())} | |
212 | end | |
213 | end | |
214 | end | |
215 | structure TyvarExt = Tyvar | |
216 | ||
217 | structure Tycon = | |
218 | struct | |
219 | open Tycon | |
220 | ||
221 | local | |
222 | val {get = info: t -> {admitsEquality: AdmitsEquality.t ref, | |
223 | kind: Kind.t, | |
224 | prettyDefault: string, | |
225 | region: Region.t, | |
226 | time: Time.t}, | |
227 | set = setInfo, ...} = | |
228 | Property.getSet | |
229 | (Tycon.plist, | |
230 | Property.initRaise ("TypeEnv.Tycon.info", Tycon.layout)) | |
231 | fun init (c, a, k, pd, r) = | |
232 | setInfo (c, {admitsEquality = ref a, | |
233 | kind = k, | |
234 | prettyDefault = pd, | |
235 | region = r, | |
236 | time = Time.now ()}) | |
237 | val _ = | |
238 | List.foreach | |
239 | (Tycon.prims, fn {tycon = c, admitsEquality = a, kind = k, name = lpd, ...} => | |
240 | init (c, a, k, lpd, Region.bogus)) | |
241 | val made: Tycon.t list ref = ref [] | |
242 | in | |
243 | local | |
244 | fun make f = f o info | |
245 | in | |
246 | val admitsEquality = ! o make #admitsEquality | |
247 | val kind = make #kind | |
248 | val prettyDefault = make #prettyDefault | |
249 | val region = make #region | |
250 | val time = make #time | |
251 | fun setAdmitsEquality (t, ae) = | |
252 | (make #admitsEquality t) := ae | |
253 | end | |
254 | val layoutPrettyDefault = Layout.str o prettyDefault | |
255 | fun make {admitsEquality, kind, name, | |
256 | prettyDefault, region} = | |
257 | let | |
258 | val tycon = Tycon.newString name | |
259 | val _ = init (tycon, admitsEquality, kind, | |
260 | prettyDefault, region) | |
261 | val _ = List.push (made, tycon) | |
262 | in | |
263 | tycon | |
264 | end | |
265 | fun makeLike c = | |
266 | make {admitsEquality = admitsEquality c, | |
267 | kind = kind c, | |
268 | name = originalName c, | |
269 | prettyDefault = prettyDefault c, | |
270 | region = region c} | |
271 | fun scopeNew th = | |
272 | let | |
273 | val oldMade = !made | |
274 | val () = made := [] | |
275 | val res = th () | |
276 | val newMade = !made | |
277 | val () = made := oldMade | |
278 | in | |
279 | (res, newMade) | |
280 | end | |
281 | end | |
282 | fun makeBogus {name, kind, region} = | |
283 | make {admitsEquality = AdmitsEquality.Sometimes, | |
284 | kind = kind, | |
285 | name = name, | |
286 | prettyDefault = concat ["<", name, ">"], | |
287 | region = Option.fold (region, Region.bogus, #1)} | |
288 | end | |
289 | ||
290 | structure Equality:> | |
291 | sig | |
292 | datatype t = False | True | Unknown | |
293 | ||
294 | val and2: t * t -> t | |
295 | val andL: 'a list * ('a -> t) -> t | |
296 | val andV: 'a vector * ('a -> t) -> t | |
297 | val applyTycon: Tycon.t * t vector -> t | |
298 | val fromBool: bool -> t | |
299 | val join: t * t -> t | |
300 | val layout: t -> Layout.t | |
301 | val or2: t * t -> t | |
302 | end = | |
303 | struct | |
304 | datatype t = False | True | Unknown | |
305 | ||
306 | fun layout e = | |
307 | case e of | |
308 | False => Layout.str "False" | |
309 | | True => Layout.str "True" | |
310 | | Unknown => Layout.str "Unknown" | |
311 | ||
312 | fun and2 (e1, e2) = | |
313 | case (e1, e2) of | |
314 | (False, _) => False | |
315 | | (_, False) => False | |
316 | | (True, _) => e2 | |
317 | | (_, True) => e1 | |
318 | | (Unknown, Unknown) => Unknown | |
319 | ||
320 | fun andL (xs, f) = List.fold (xs, True, fn (x, e) => and2 (f x, e)) | |
321 | fun andV (xs, f) = Vector.fold (xs, True, fn (x, e) => and2 (f x, e)) | |
322 | ||
323 | fun or2 (e1, e2) = | |
324 | case (e1, e2) of | |
325 | (False, _) => e2 | |
326 | | (_, False) => e1 | |
327 | | (True, _) => True | |
328 | | (_, True) => True | |
329 | | (Unknown, Unknown) => Unknown | |
330 | ||
331 | fun join (e1, e2) = | |
332 | case (e1, e2) of | |
333 | (Unknown, _) => e2 | |
334 | | (_, Unknown) => e1 | |
335 | | (False, False) => False | |
336 | | (True, True) => True | |
337 | | _ => Error.bug "TypeEnv.Equality.join" | |
338 | ||
339 | fun applyTycon (c, es) = | |
340 | let | |
341 | datatype z = datatype AdmitsEquality.t | |
342 | in | |
343 | case Tycon.admitsEquality c of | |
344 | Always => True | |
345 | | Sometimes => andV (es, fn e => e) | |
346 | | Never => False | |
347 | end | |
348 | ||
349 | fun fromBool b = if b then True else False | |
350 | end | |
351 | ||
352 | structure Unknown = | |
353 | struct | |
354 | datatype t = T of {canGeneralize: bool, | |
355 | id: int} | |
356 | ||
357 | local | |
358 | fun make f (T r) = f r | |
359 | in | |
360 | val id = make #id | |
361 | end | |
362 | ||
363 | fun layout (T {canGeneralize, id, ...}) = | |
364 | seq [str "Unknown ", | |
365 | Layout.record [("canGeneralize", Bool.layout canGeneralize), | |
366 | ("id", Int.layout id)]] | |
367 | ||
368 | fun layoutPretty _ = str "???" | |
369 | ||
370 | fun equals (u, u') = id u = id u' | |
371 | ||
372 | local | |
373 | val c = Counter.new 0 | |
374 | in | |
375 | val newId = fn () => Counter.next c | |
376 | end | |
377 | ||
378 | fun new {canGeneralize} = | |
379 | T {canGeneralize = canGeneralize, | |
380 | id = newId ()} | |
381 | ||
382 | fun join (T r, T r'): t = | |
383 | T {canGeneralize = #canGeneralize r andalso #canGeneralize r', | |
384 | id = newId ()} | |
385 | end | |
386 | ||
387 | (* Flexible record spine, i.e. a possibly extensible list of fields. *) | |
388 | structure Spine: | |
389 | sig | |
390 | type t | |
391 | ||
392 | val canAddFields: t -> bool | |
393 | val equals: t * t -> bool | |
394 | val fields: t -> Field.t list | |
395 | (* ensureField checks if field is there. If it is not, then ensureField | |
396 | * will add it unless no more fields are allowed in the spine. | |
397 | * It returns true iff it succeeds. | |
398 | *) | |
399 | val ensureField: t * Field.t -> bool | |
400 | val foldOverNew: t * (Field.t * 'a) list * 'b * (Field.t * 'b -> 'b) -> 'b | |
401 | val layout: t -> Layout.t | |
402 | val new: Field.t list -> t | |
403 | val noMoreFields: t -> unit | |
404 | val unify: t * t -> unit | |
405 | end = | |
406 | struct | |
407 | datatype t = T of {id: int, | |
408 | body: {fields: Field.t list ref, | |
409 | more: bool ref} Set.t} | |
410 | ||
411 | local | |
412 | val c = Counter.new 0 | |
413 | in | |
414 | val newId = fn () => Counter.next c | |
415 | end | |
416 | ||
417 | fun new fields = T {id = newId (), | |
418 | body = Set.singleton {fields = ref fields, | |
419 | more = ref true}} | |
420 | ||
421 | fun equals (T {id = id1,...}, T {id = id2,...}) = id1 = id2 | |
422 | ||
423 | fun layout (T {body = s,...}) = | |
424 | let | |
425 | val {fields, more} = Set.! s | |
426 | in | |
427 | Layout.record [("fields", List.layout Field.layout (!fields)), | |
428 | ("more", Bool.layout (!more))] | |
429 | end | |
430 | ||
431 | fun canAddFields (T {body = s,...}) = ! (#more (Set.! s)) | |
432 | fun fields (T {body = s,...}) = ! (#fields (Set.! s)) | |
433 | ||
434 | fun ensureFieldValue ({fields, more}, f) = | |
435 | List.contains (!fields, f, Field.equals) | |
436 | orelse (!more andalso (List.push (fields, f); true)) | |
437 | ||
438 | fun ensureField (T {body = s,...}, f) = ensureFieldValue (Set.! s, f) | |
439 | ||
440 | fun noMoreFields (T {body = s,...}) = #more (Set.! s) := false | |
441 | ||
442 | fun unify (T {body = s1,...}, T {body = s2,...}) = | |
443 | let | |
444 | val {fields = fs1, more = m1} = Set.! s1 | |
445 | val {fields = fs2, more = m2} = Set.! s2 | |
446 | val _ = Set.union (s1, s2) | |
447 | val fs = List.union (!fs1, !fs2, Field.equals) | |
448 | val m = !m1 andalso !m2 | |
449 | val _ = Set.:= (s1, {fields = ref fs, more = ref m}) | |
450 | in | |
451 | () | |
452 | end | |
453 | ||
454 | fun foldOverNew (spine: t, fs, ac, g) = | |
455 | List.fold | |
456 | (fields spine, ac, fn (f, ac) => | |
457 | if List.exists (fs, fn (f', _) => Field.equals (f, f')) | |
458 | then ac | |
459 | else g (f, ac)) | |
460 | end | |
461 | ||
462 | structure Type = | |
463 | struct | |
464 | structure Overload = | |
465 | struct | |
466 | datatype t = Char | Int | Real | Word | |
467 | ||
468 | val equals: t * t -> bool = op = | |
469 | ||
470 | val toString = | |
471 | fn Char => "Char" | |
472 | | Int => "Int" | |
473 | | Real => "Real" | |
474 | | Word => "Word" | |
475 | ||
476 | val layout = Layout.str o toString | |
477 | ||
478 | val matchesTycon: t * Tycon.t -> bool = | |
479 | fn (ov, c) => | |
480 | case ov of | |
481 | Char => Tycon.isCharX c | |
482 | | Int => Tycon.isIntX c | |
483 | | Real => Tycon.isRealX c | |
484 | | Word => Tycon.isWordX c | |
485 | ||
486 | val defaultTycon: t -> Tycon.t = | |
487 | fn Char => Tycon.defaultChar () | |
488 | | Int => Tycon.defaultInt () | |
489 | | Real => Tycon.defaultReal () | |
490 | | Word => Tycon.defaultWord () | |
491 | ||
492 | val admitsEquality: t -> Equality.t = | |
493 | fn Char => Equality.True | |
494 | | Int => Equality.True | |
495 | | Real => Equality.False | |
496 | | Word => Equality.True | |
497 | end | |
498 | ||
499 | (* Tuples of length <> 1 are always represented as records. | |
500 | * There will never be tuples of length one. | |
501 | *) | |
502 | datatype t = T of {equality: Equality.t ref, | |
503 | plist: PropertyList.t, | |
504 | time: Time.t ref, | |
505 | ty: ty} Set.t | |
506 | and ty = | |
507 | Con of Tycon.t * t vector | |
508 | | FlexRecord of {fields: fields, | |
509 | spine: Spine.t} | |
510 | (* GenFlexRecord only appears in type schemes. | |
511 | * It will never be unified. | |
512 | * The fields that are filled in after generalization are stored in | |
513 | * extra. | |
514 | *) | |
515 | | GenFlexRecord of genFlexRecord | |
516 | | Overload of Overload.t | |
517 | | Record of t Srecord.t | |
518 | | Unknown of Unknown.t | |
519 | | Var of Tyvar.t | |
520 | withtype fields = (Field.t * t) list | |
521 | and genFlexRecord = | |
522 | {extra: unit -> {field: Field.t, | |
523 | tyvar: Tyvar.t} list, | |
524 | fields: (Field.t * t) list, | |
525 | spine: Spine.t} | |
526 | ||
527 | local | |
528 | fun make f (T s) = f (Set.! s) | |
529 | in | |
530 | val equality = make #equality | |
531 | val plist: t -> PropertyList.t = make #plist | |
532 | val time: t -> Time.t ref = make #time | |
533 | val getTy: t -> ty = make #ty | |
534 | end | |
535 | ||
536 | local | |
537 | open Layout | |
538 | in | |
539 | fun layoutFields fs = | |
540 | List.layout (Layout.tuple2 (Field.layout, layout)) fs | |
541 | and layout (T s) = | |
542 | let | |
543 | val {equality, time, ty, ...} = Set.! s | |
544 | in | |
545 | record | |
546 | [("time", Time.layout (!time)), | |
547 | ("equality", Equality.layout (!equality)), | |
548 | ("ty", | |
549 | case ty of | |
550 | Con (c, ts) => | |
551 | paren (align [seq [str "Con ", Tycon.layout c], | |
552 | Vector.layout layout ts]) | |
553 | | FlexRecord {fields, spine} => | |
554 | seq [str "Flex ", | |
555 | record [("fields", layoutFields fields), | |
556 | ("spine", Spine.layout spine)]] | |
557 | | GenFlexRecord {extra, fields, spine} => | |
558 | seq [str "GenFlex ", | |
559 | record [("extra", | |
560 | List.layout | |
561 | (fn {field, tyvar} => | |
562 | record [("field", Field.layout field), | |
563 | ("tyvar", Tyvar.layout tyvar)]) | |
564 | (extra ())), | |
565 | ("fields", layoutFields fields), | |
566 | ("spine", Spine.layout spine)]] | |
567 | | Overload ov => Overload.layout ov | |
568 | | Record r => Srecord.layout {record = r, | |
569 | separator = ": ", | |
570 | extra = "", | |
571 | layoutTuple = Vector.layout layout, | |
572 | layoutElt = layout} | |
573 | | Unknown u => Unknown.layout u | |
574 | | Var a => paren (seq [str "Var ", Tyvar.layout a]))] | |
575 | end | |
576 | end | |
577 | end | |
578 | ||
579 | structure Tycon = | |
580 | struct | |
581 | open Tycon | |
582 | ||
583 | val {get = opaqueExpansion: t -> (Type.t vector -> Type.t) option, | |
584 | set = setOpaqueExpansion, ...} = | |
585 | Property.getSet (Tycon.plist, Property.initConst NONE) | |
586 | ||
587 | val opaqueExpansion = | |
588 | Trace.trace | |
589 | ("TypeEnv.Tycon.opaqueExpansion", Tycon.layout, Layout.ignore) | |
590 | opaqueExpansion | |
591 | ||
592 | val setOpaqueExpansion = fn (c, f) => | |
593 | setOpaqueExpansion (c, SOME f) | |
594 | end | |
595 | structure TyconExt = Tycon | |
596 | ||
597 | structure LayoutPretty = | |
598 | struct | |
599 | open LayoutPretty | |
600 | fun record (ds: (Field.t * bool * t) list, flexible: bool) = | |
601 | simple (case ds of | |
602 | [] => if flexible then str "{...}" else str "{}" | |
603 | | _ => | |
604 | seq [str "{", | |
605 | Layout.mayAlign | |
606 | (Layout.separateRight | |
607 | (List.map | |
608 | (QuickSort.sortList (ds, fn ((f, _, _), (f', _, _)) => | |
609 | Field.<= (f, f')), | |
610 | fn (f, b, (l, _)) => | |
611 | let | |
612 | val f = Field.layout f | |
613 | val row = seq [f, str ": ", l] | |
614 | val row = if b then Layout.bracket row else row | |
615 | in | |
616 | row | |
617 | end), | |
618 | ",")), | |
619 | str (if flexible | |
620 | then ", ...}" | |
621 | else "}")]) | |
622 | fun tuple (ls: t vector): t = | |
623 | Tycon.layoutAppPretty | |
624 | (Tycon.tuple, ls, | |
625 | {layoutPretty = fn _ => | |
626 | Error.bug "TypeEnv.LayoutPretty.tuple: layoutPretty"}) | |
627 | end | |
628 | ||
629 | structure Type = | |
630 | struct | |
631 | open Type | |
632 | ||
633 | fun makeHom {con, expandOpaque, flexRecord, genFlexRecord, | |
634 | guard, overload, record, recursive, unknown, var} = | |
635 | let | |
636 | datatype status = Processing | Seen | Unseen | |
637 | val {destroy = destroyStatus, get = status, ...} = | |
638 | Property.destGet (plist, Property.initFun (fn _ => ref Unseen)) | |
639 | val {get, destroy = destroyProp} = | |
640 | Property.destGet | |
641 | (plist, | |
642 | Property.initRec | |
643 | (fn (t, get) => | |
644 | let | |
645 | val r = status t | |
646 | in | |
647 | case !r of | |
648 | Seen => Error.bug "TypeEnv.Type.makeHom: impossible" | |
649 | | Processing => recursive t | |
650 | | Unseen => | |
651 | (case guard t of | |
652 | NONE => | |
653 | let | |
654 | val _ = r := Processing | |
655 | fun loopFields fields = | |
656 | List.revMap (fields, fn (f, t) => (f, get t)) | |
657 | val res = | |
658 | case getTy t of | |
659 | Con (c, ts) => | |
660 | let | |
661 | fun no () = | |
662 | con (t, c, Vector.map (ts, get)) | |
663 | fun yes () = | |
664 | (case Tycon.opaqueExpansion c of | |
665 | NONE => no () | |
666 | | SOME f => get (f ts)) | |
667 | in | |
668 | if expandOpaque then yes () else no () | |
669 | end | |
670 | | FlexRecord {fields, spine} => | |
671 | flexRecord | |
672 | (t, {fields = loopFields fields, | |
673 | spine = spine}) | |
674 | | GenFlexRecord {extra, fields, spine} => | |
675 | genFlexRecord | |
676 | (t, {extra = extra, | |
677 | fields = loopFields fields, | |
678 | spine = spine}) | |
679 | | Overload ov => overload (t, ov) | |
680 | | Record r => record (t, Srecord.map (r, get)) | |
681 | | Unknown u => unknown (t, u) | |
682 | | Var a => var (t, a) | |
683 | val _ = r := Seen | |
684 | in | |
685 | res | |
686 | end | |
687 | | SOME res => (r := Seen; res)) | |
688 | end)) | |
689 | fun destroy () = | |
690 | (destroyStatus () | |
691 | ; destroyProp ()) | |
692 | in | |
693 | {hom = get, destroy = destroy} | |
694 | end | |
695 | ||
696 | fun hom (ty, z) = | |
697 | let | |
698 | val {hom, destroy} = makeHom z | |
699 | in | |
700 | Exn.finally (fn () => hom ty, destroy) | |
701 | end | |
702 | ||
703 | fun makeLayoutPretty {expandOpaque, | |
704 | layoutPrettyTycon, | |
705 | layoutPrettyTyvar} : | |
706 | {destroy: unit -> unit, | |
707 | layoutPretty: t -> LayoutPretty.t} = | |
708 | let | |
709 | val layoutAppPretty = fn (c, ts) => | |
710 | Tycon.layoutAppPretty | |
711 | (c, ts, {layoutPretty = layoutPrettyTycon}) | |
712 | fun con (_, c, ts) = layoutAppPretty (c, ts) | |
713 | fun con0 c = layoutAppPretty (c, Vector.new0 ()) | |
714 | fun flexRecord (_, {fields, spine}) = | |
715 | LayoutPretty.record | |
716 | (List.fold | |
717 | (fields, | |
718 | Spine.foldOverNew (spine, fields, [], fn (f, ac) => | |
719 | (f, false, simple (str "#???")) | |
720 | :: ac), | |
721 | fn ((f, t), ac) => (f, false, t) :: ac), | |
722 | Spine.canAddFields spine) | |
723 | fun genFlexRecord (_, {extra, fields, spine}) = | |
724 | LayoutPretty.record | |
725 | (List.fold | |
726 | (fields, | |
727 | List.revMap (extra (), fn {field, tyvar} => | |
728 | (field, false, simple (layoutPrettyTyvar tyvar))), | |
729 | fn ((f, t), ac) => (f, false, t) :: ac), | |
730 | Spine.canAddFields spine) | |
731 | fun overload (_, ov) = con0 (Overload.defaultTycon ov) | |
732 | fun record (_, r) = | |
733 | case Srecord.detupleOpt r of | |
734 | NONE => | |
735 | LayoutPretty.record | |
736 | (Vector.toListMap | |
737 | (Srecord.toVector r, | |
738 | fn (f, t) => (f, false, t)), | |
739 | false) | |
740 | | SOME ts => LayoutPretty.tuple ts | |
741 | fun recursive _ = simple (str "<recur>") | |
742 | fun unknown (_, u) = simple (Unknown.layoutPretty u) | |
743 | fun var (_, a) = simple (layoutPrettyTyvar a) | |
744 | val {destroy, hom = layoutPretty} = | |
745 | makeHom {con = con, | |
746 | expandOpaque = expandOpaque, | |
747 | flexRecord = flexRecord, | |
748 | genFlexRecord = genFlexRecord, | |
749 | guard = fn _ => NONE, | |
750 | overload = overload, | |
751 | record = record, | |
752 | recursive = recursive, | |
753 | unknown = unknown, | |
754 | var = var} | |
755 | in | |
756 | {destroy = destroy, | |
757 | layoutPretty = layoutPretty} | |
758 | end | |
759 | ||
760 | fun layoutPretty (t, {expandOpaque, layoutPrettyTycon, layoutPrettyTyvar}) = | |
761 | let | |
762 | val {destroy, layoutPretty} = | |
763 | makeLayoutPretty {expandOpaque = expandOpaque, | |
764 | layoutPrettyTycon = layoutPrettyTycon, | |
765 | layoutPrettyTyvar = layoutPrettyTyvar} | |
766 | val res = layoutPretty t | |
767 | val () = destroy () | |
768 | in | |
769 | res | |
770 | end | |
771 | ||
772 | fun getEquality t = | |
773 | let | |
774 | (* guarded; only invoked if '!(Tycon.admitsEquality c) = Sometimes' *) | |
775 | fun con (_, c, es) = Equality.applyTycon (c, es) | |
776 | fun flexRecord (_, {fields: (Field.t * Equality.t) list, spine}) = | |
777 | if Spine.canAddFields spine | |
778 | then Equality.Unknown | |
779 | else Equality.andL (fields, #2) | |
780 | (* impossible; *) | |
781 | fun genFlexRecord _ = Error.bug "TypeEnv.Type.getEquality.genFlexRecord" | |
782 | (* guarded; an overload has known equality *) | |
783 | fun overload _ = Error.bug "TypeEnv.Type.getEquality.overload" | |
784 | fun record (_, r: Equality.t Srecord.t) = | |
785 | Equality.andV (Srecord.toVector r, #2) | |
786 | (* impossible *) | |
787 | fun recursive _ = Error.bug "TypeEnv.Type.getEquality.recursive" | |
788 | (* guarded; only invoked if '!(Type.equality t) = Unknown' *) | |
789 | fun unknown (_, _) = Equality.Unknown | |
790 | (* guarded; a tyvar has known equality *) | |
791 | fun var _ = Error.bug "TypeEnv.Type.getEquality.var" | |
792 | fun wrap (f, sel) arg = | |
793 | let | |
794 | val res = f arg | |
795 | val _ = equality (sel arg) := res | |
796 | in | |
797 | res | |
798 | end | |
799 | fun guard t = | |
800 | let | |
801 | val e = !(equality t) | |
802 | in | |
803 | case e of | |
804 | Equality.Unknown => NONE | |
805 | | _ => SOME e | |
806 | end | |
807 | in | |
808 | hom (t, {con = wrap (con, #1), | |
809 | expandOpaque = false, | |
810 | flexRecord = wrap (flexRecord, #1), | |
811 | genFlexRecord = genFlexRecord, | |
812 | guard = guard, | |
813 | overload = overload, | |
814 | record = wrap (record, #1), | |
815 | recursive = recursive, | |
816 | unknown = unknown, | |
817 | var = var}) | |
818 | end | |
819 | ||
820 | val getEquality = | |
821 | Trace.trace | |
822 | ("TypeEnv.Type.getEquality", layout, Equality.layout) | |
823 | getEquality | |
824 | val _ = getEquality | |
825 | ||
826 | fun deConOpt t = | |
827 | case getTy t of | |
828 | Con x => SOME x | |
829 | | _ => NONE | |
830 | ||
831 | fun deEta (t: t, tyvars: Tyvar.t vector): Tycon.t option = | |
832 | case deConOpt t of | |
833 | SOME (c, ts) => | |
834 | if Vector.length ts = Vector.length tyvars | |
835 | andalso Vector.foralli (ts, fn (i, t) => | |
836 | case getTy t of | |
837 | Var a => | |
838 | Tyvar.equals | |
839 | (a, Vector.sub (tyvars, i)) | |
840 | | _ => false) | |
841 | then SOME c | |
842 | else NONE | |
843 | | _ => NONE | |
844 | ||
845 | fun make {equality, time, ty}: t = | |
846 | T (Set.singleton {equality = ref equality, | |
847 | plist = PropertyList.new (), | |
848 | time = ref time, | |
849 | ty = ty}) | |
850 | ||
851 | fun newTy (ty: ty): t = | |
852 | let | |
853 | val (equality, time) = | |
854 | case ty of | |
855 | Con (c, ts) => | |
856 | (Equality.applyTycon | |
857 | (c, Vector.map (ts, ! o equality)), | |
858 | Vector.fold | |
859 | (ts, Tycon.time c, fn (t, t') => | |
860 | Time.max (!(time t), t'))) | |
861 | | GenFlexRecord _ => | |
862 | Error.bug "TypeEnv.Type.newTy: GenFlexRecord" | |
863 | | FlexRecord _ => | |
864 | (Equality.Unknown, | |
865 | Time.now ()) | |
866 | | Overload ov => | |
867 | (Overload.admitsEquality ov, | |
868 | Time.zero) | |
869 | | Record r => | |
870 | (Srecord.fold | |
871 | (r, Equality.True, fn (t, e') => | |
872 | Equality.and2 (!(equality t), e')), | |
873 | Srecord.fold | |
874 | (r, Time.zero, fn (t, t') => | |
875 | Time.max (!(time t), t'))) | |
876 | | Unknown _ => | |
877 | Error.bug "TypeEnv.Type.newTy: Unknown" | |
878 | | Var a => | |
879 | (Equality.fromBool (Tyvar.isEquality a), | |
880 | Tyvar.time a) | |
881 | in | |
882 | make {equality = equality, | |
883 | time = time, | |
884 | ty = ty} | |
885 | end | |
886 | ||
887 | fun setTy (T s, ty) = | |
888 | let | |
889 | val {equality, plist, time, ...} = Set.! s | |
890 | in | |
891 | Set.:= (s, {equality = equality, | |
892 | plist = plist, | |
893 | time = time, | |
894 | ty = ty}) | |
895 | end | |
896 | ||
897 | fun unknownAux {canGeneralize, equality, time} = | |
898 | let | |
899 | val u = Unknown.new {canGeneralize = canGeneralize} | |
900 | val t = make {equality = equality, | |
901 | time = time, | |
902 | ty = Unknown u} | |
903 | in | |
904 | (u, t) | |
905 | end | |
906 | val unknown = #2 o unknownAux | |
907 | ||
908 | fun new () = | |
909 | unknown | |
910 | {canGeneralize = true, | |
911 | equality = Equality.Unknown, | |
912 | time = Time.now ()} | |
913 | ||
914 | val new = Trace.trace ("TypeEnv.Type.new", Unit.layout, layout) new | |
915 | ||
916 | fun newFlex {fields, spine} = | |
917 | newTy (FlexRecord {fields = fields, spine = spine}) | |
918 | ||
919 | fun flexRecord record = | |
920 | let | |
921 | val v = Srecord.toVector record | |
922 | val spine = Spine.new (Vector.toListMap (v, #1)) | |
923 | fun isResolved (): bool = not (Spine.canAddFields spine) | |
924 | val t = newFlex {fields = Vector.toList v, | |
925 | spine = spine} | |
926 | in | |
927 | (t, isResolved) | |
928 | end | |
929 | ||
930 | fun record r = newTy (Record r) | |
931 | ||
932 | fun tuple ts = | |
933 | if 1 = Vector.length ts | |
934 | then Vector.first ts | |
935 | else newTy (Record (Srecord.tuple ts)) | |
936 | ||
937 | fun con (tycon, ts) = | |
938 | if Tycon.equals (tycon, Tycon.tuple) | |
939 | then tuple ts | |
940 | else newTy (Con (tycon, ts)) | |
941 | ||
942 | fun var a = newTy (Var a) | |
943 | end | |
944 | ||
945 | structure Ops = TypeOps (structure Tycon = Tycon | |
946 | open Type) | |
947 | ||
948 | structure UnifyResult = | |
949 | struct | |
950 | datatype ('a, 'b) t = | |
951 | NotUnifiable of 'a | |
952 | | Unified of 'b | |
953 | ||
954 | val layout = | |
955 | fn NotUnifiable _ => str "NotUnifiable" | |
956 | | Unified _ => str "Unified" | |
957 | end | |
958 | ||
959 | structure Type = | |
960 | struct | |
961 | (* Order is important, since want specialized definitions in Type to | |
962 | * override general definitions in Ops. | |
963 | *) | |
964 | open Ops Type | |
965 | ||
966 | val unit = tuple (Vector.new0 ()) | |
967 | ||
968 | fun isArrow t = | |
969 | case getTy t of | |
970 | Con (c, _) => Tycon.equals (c, Tycon.arrow) | |
971 | | _ => false | |
972 | ||
973 | fun isBool t = | |
974 | case getTy t of | |
975 | Con (c, _) => Tycon.isBool c | |
976 | | _ => false | |
977 | ||
978 | fun isCharX t = | |
979 | case getTy t of | |
980 | Con (c, _) => Tycon.isCharX c | |
981 | | Overload Overload.Char => true | |
982 | | _ => false | |
983 | ||
984 | fun isCPointer t = | |
985 | case getTy t of | |
986 | Con (c, _) => Tycon.isCPointer c | |
987 | | _ => false | |
988 | ||
989 | fun isInt t = | |
990 | case getTy t of | |
991 | Con (c, _) => Tycon.isIntX c | |
992 | | Overload Overload.Int => true | |
993 | | _ => false | |
994 | ||
995 | fun isUnit t = | |
996 | case getTy t of | |
997 | Record r => | |
998 | (case Srecord.detupleOpt r of | |
999 | NONE => false | |
1000 | | SOME v => Vector.isEmpty v) | |
1001 | | _ => false | |
1002 | ||
1003 | fun isUnknown t = | |
1004 | case getTy t of | |
1005 | Unknown _ => true | |
1006 | | _ => false | |
1007 | ||
1008 | local | |
1009 | fun make ov () = newTy (Overload ov) | |
1010 | datatype z = datatype Overload.t | |
1011 | in | |
1012 | val unresolvedChar = make Char | |
1013 | val unresolvedInt = make Int | |
1014 | val unresolvedReal = make Real | |
1015 | val unresolvedWord = make Word | |
1016 | end | |
1017 | ||
1018 | fun unresolvedString () = vector (unresolvedChar ()) | |
1019 | ||
1020 | val traceCanUnify = | |
1021 | Trace.trace2 | |
1022 | ("TypeEnv.Type.canUnify", layout, layout, Bool.layout) | |
1023 | ||
1024 | fun canUnify arg = | |
1025 | traceCanUnify | |
1026 | (fn (t, t') => | |
1027 | case (getTy t, getTy t') of | |
1028 | (Unknown _, _) => true | |
1029 | | (_, Unknown _) => true | |
1030 | | (Con (c, ts), t') => conAnd (c, ts, t') | |
1031 | | (t', Con (c, ts)) => conAnd (c, ts, t') | |
1032 | | (Overload o1, Overload o2) => Overload.equals (o1, o2) | |
1033 | | (Record r, Record r') => | |
1034 | let | |
1035 | val fs = Srecord.toVector r | |
1036 | val fs' = Srecord.toVector r' | |
1037 | in Vector.length fs = Vector.length fs' | |
1038 | andalso Vector.forall2 (fs, fs', fn ((f, t), (f', t')) => | |
1039 | Field.equals (f, f') | |
1040 | andalso canUnify (t, t')) | |
1041 | end | |
1042 | | (Var a, Var a') => Tyvar.equals (a, a') | |
1043 | | _ => false) arg | |
1044 | and conAnd (c, ts, t') = | |
1045 | case t' of | |
1046 | Con (c', ts') => | |
1047 | Tycon.equals (c, c') | |
1048 | andalso Vector.forall2 (ts, ts', canUnify) | |
1049 | | Overload ov => | |
1050 | Vector.isEmpty ts andalso Overload.matchesTycon (ov, c) | |
1051 | | _ => false | |
1052 | ||
1053 | (* checkEquality t checks that t is an equality type. If t is | |
1054 | * not an equality type, then checkEquality t returns: | |
1055 | * - a layout object highlighting violations in t | |
1056 | * - an alternate type, replacing violations in t with fresh | |
1057 | * equality unification variables and a layout object | |
1058 | * highlighting the fresh unification variables. | |
1059 | *) | |
1060 | fun checkEquality (t, {layoutPrettyTycon: Tycon.t -> Layout.t, | |
1061 | layoutPrettyTyvar: Tyvar.t -> Layout.t}) = | |
1062 | let | |
1063 | val layoutAppPretty = fn (c, ts) => | |
1064 | Tycon.layoutAppPretty | |
1065 | (c, ts, {layoutPretty = layoutPrettyTycon}) | |
1066 | type ll = LayoutPretty.t * LayoutPretty.t | |
1067 | local | |
1068 | fun getLay sel (llo: ll option, _) = | |
1069 | Option.fold (llo, dontCare, sel o #1) | |
1070 | in | |
1071 | val getLay1 = getLay #1 | |
1072 | val getLay2 = getLay #2 | |
1073 | end | |
1074 | fun getTy (_, ty) = ty | |
1075 | (* guarded; only invoked if 'Tycon.admitsEquality c = Sometimes' *) | |
1076 | fun con (_, c, rs) = | |
1077 | if Vector.forall (rs, Option.isNone o #1) | |
1078 | then NONE | |
1079 | else SOME (layoutAppPretty | |
1080 | (c, Vector.map (rs, getLay1)), | |
1081 | layoutAppPretty | |
1082 | (c, Vector.map (rs, getLay2)), | |
1083 | Type.con | |
1084 | (c, Vector.map (rs, getTy))) | |
1085 | fun doRecord (fls: (Field.t * ll) list, | |
1086 | extra: bool, mk: unit -> t) = | |
1087 | if List.isEmpty fls | |
1088 | then NONE | |
1089 | else let | |
1090 | fun doit sel = | |
1091 | LayoutPretty.record | |
1092 | (List.map | |
1093 | (fls, fn (f, lll) => | |
1094 | (f, false, sel lll)), | |
1095 | extra) | |
1096 | in | |
1097 | SOME (doit #1, doit #2, mk ()) | |
1098 | end | |
1099 | fun flexRecord (_, {fields, spine}) = | |
1100 | doRecord (List.keepAllMap | |
1101 | (fields, fn (f, r) => | |
1102 | Option.map (#1 r, fn ll => (f, ll))), | |
1103 | Spine.canAddFields spine, | |
1104 | fn () => | |
1105 | let | |
1106 | val fields = | |
1107 | List.map (fields, fn (f, r) => | |
1108 | (f, getTy r)) | |
1109 | in | |
1110 | Type.newFlex {fields = fields, | |
1111 | spine = spine} | |
1112 | end) | |
1113 | (* impossible *) | |
1114 | fun genFlexRecord _ = Error.bug "TypeEnv.Type.checkEquality.genFlexRecord" | |
1115 | (* guarded; an overload has known equality | |
1116 | * only invoked if '!(Type.equality t) = False' *) | |
1117 | fun overload (_, ov) = | |
1118 | case ov of | |
1119 | Overload.Real => | |
1120 | let | |
1121 | val ty = | |
1122 | Type.unknown {canGeneralize = true, | |
1123 | equality = Equality.True, | |
1124 | time = Time.now ()} | |
1125 | in | |
1126 | SOME (bracket (simple (str "real")), | |
1127 | bracket (simple (str "<equality>")), | |
1128 | ty) | |
1129 | end | |
1130 | | _ => Error.bug "TypeEnv.Type.checkEquality.overload" | |
1131 | fun record (_, r) = | |
1132 | case Srecord.detupleOpt r of | |
1133 | NONE => | |
1134 | let | |
1135 | val fields = Srecord.toVector r | |
1136 | val fields' = | |
1137 | Vector.keepAllMap | |
1138 | (fields, fn (f, r) => | |
1139 | Option.map (#1 r, fn ll => (f, ll))) | |
1140 | in | |
1141 | doRecord (Vector.toList fields', | |
1142 | not (Vector.length fields = Vector.length fields'), | |
1143 | fn () => | |
1144 | let | |
1145 | val fields = | |
1146 | Vector.map (fields, fn (f, r) => | |
1147 | (f, getTy r)) | |
1148 | val fields = Srecord.fromVector fields | |
1149 | in | |
1150 | Type.record fields | |
1151 | end) | |
1152 | end | |
1153 | | SOME rs => | |
1154 | if Vector.forall (rs, Option.isNone o #1) | |
1155 | then NONE | |
1156 | else SOME (LayoutPretty.tuple (Vector.map (rs, getLay1)), | |
1157 | LayoutPretty.tuple (Vector.map (rs, getLay2)), | |
1158 | Type.tuple (Vector.map (rs, getTy))) | |
1159 | (* impossible *) | |
1160 | fun recursive _ = Error.bug "TypeEnv.Type.checkEquality.recursive" | |
1161 | fun unknown (t, _) = | |
1162 | case !(equality t) of | |
1163 | Equality.False => | |
1164 | let | |
1165 | val ty = | |
1166 | Type.unknown {canGeneralize = true, | |
1167 | equality = Equality.True, | |
1168 | time = Time.now ()} | |
1169 | in | |
1170 | SOME (bracket (simple (str "<non-equality>")), | |
1171 | bracket (simple (str "<equality>")), | |
1172 | ty) | |
1173 | end | |
1174 | | Equality.True => NONE | |
1175 | | Equality.Unknown => NONE | |
1176 | (* guarded; a tyvar has known equality | |
1177 | * only invoked if '!(Type.equality t) = False' *) | |
1178 | fun var (_, a) = | |
1179 | if Tyvar.isEquality a | |
1180 | then Error.bug "TypeEnv.Type.checkEquality.var" | |
1181 | else let | |
1182 | val ty = | |
1183 | Type.unknown {canGeneralize = true, | |
1184 | equality = Equality.True, | |
1185 | time = Time.now ()} | |
1186 | in | |
1187 | SOME (bracket (simple (layoutPrettyTyvar a)), | |
1188 | bracket (simple (str "<equality>")), | |
1189 | ty) | |
1190 | end | |
1191 | fun wrap (f, sel) arg = | |
1192 | case f arg of | |
1193 | NONE => | |
1194 | let | |
1195 | val t = sel arg | |
1196 | in | |
1197 | equality t := Equality.True | |
1198 | ; (NONE, t) | |
1199 | end | |
1200 | | SOME (l1, l2, t) => | |
1201 | (SOME (l1, l2), t) | |
1202 | (* Need extra guarding of Con, because proceeding with | |
1203 | * hom/con would recursively force all Unknowns in type | |
1204 | * args to Equality.True, even if tycon is | |
1205 | * AdmitsEquality.Never. *) | |
1206 | fun guard t = | |
1207 | case !(equality t) of | |
1208 | Equality.True => SOME (NONE, t) | |
1209 | | _ => (case Type.getTy t of | |
1210 | Con (c, ts) => | |
1211 | (case Tycon.admitsEquality c of | |
1212 | AdmitsEquality.Always => SOME (NONE, t) | |
1213 | | AdmitsEquality.Sometimes => NONE | |
1214 | | AdmitsEquality.Never => | |
1215 | let | |
1216 | val ty = | |
1217 | Type.unknown {canGeneralize = true, | |
1218 | equality = Equality.True, | |
1219 | time = Time.now ()} | |
1220 | in | |
1221 | SOME (SOME ((bracket o layoutAppPretty) | |
1222 | (c, Vector.map (ts, fn _ => dontCare)), | |
1223 | bracket (simple (str "<equality>"))), | |
1224 | ty) | |
1225 | end) | |
1226 | | _ => NONE) | |
1227 | val res : ll option * t = | |
1228 | hom (t, {con = wrap (con, #1), | |
1229 | expandOpaque = false, | |
1230 | flexRecord = wrap (flexRecord, #1), | |
1231 | genFlexRecord = genFlexRecord, | |
1232 | guard = guard, | |
1233 | overload = wrap (overload, #1), | |
1234 | record = wrap (record, #1), | |
1235 | recursive = recursive, | |
1236 | unknown = wrap (unknown, #1), | |
1237 | var = wrap (var, #1)}) | |
1238 | in | |
1239 | case res of | |
1240 | (NONE, _) => NONE | |
1241 | | (SOME (l1, l2), t) => | |
1242 | SOME (l1, (t, l2)) | |
1243 | end | |
1244 | ||
1245 | (* checkTime (t, bound) checks that all components of t have | |
1246 | * times no larger than bound. If t has components with time | |
1247 | * larger than bound, then checkTime (t, bound) returns: | |
1248 | * - a layout object highlighting violations in t | |
1249 | * - an alternate type, replacing violations in t with fresh | |
1250 | * unification variables at time bound and a layout object | |
1251 | * highlighting the fresh unification variables. | |
1252 | * - a list of violating tycons | |
1253 | * - a list of violating tyvars | |
1254 | *) | |
1255 | fun makeCheckTime {layoutPrettyTycon: Tycon.t -> Layout.t, | |
1256 | layoutPrettyTyvar: Tyvar.t -> Layout.t} = | |
1257 | let | |
1258 | val layoutAppPretty = fn (c, ts) => | |
1259 | Tycon.layoutAppPretty | |
1260 | (c, ts, {layoutPretty = layoutPrettyTycon}) | |
1261 | val times: Time.t list ref = ref [] | |
1262 | val tycons: Tycon.t list ref = ref [] | |
1263 | val tyvars: Tyvar.t list ref = ref [] | |
1264 | type lll = LayoutPretty.t * LayoutPretty.t * LayoutPretty.t | |
1265 | local | |
1266 | fun getLay sel (lllo: lll option, _) = | |
1267 | Option.fold (lllo, dontCare, sel o #1) | |
1268 | in | |
1269 | val getLay1 = getLay #1 | |
1270 | val getLay2 = getLay #2 | |
1271 | val getLay3 = getLay #3 | |
1272 | end | |
1273 | fun getTy (_, ty) = ty | |
1274 | fun con bound (_, c, rs) = | |
1275 | if Time.<= (Tycon.time c, bound) | |
1276 | then if Vector.forall (rs, Option.isNone o #1) | |
1277 | then NONE | |
1278 | else SOME (layoutAppPretty | |
1279 | (c, Vector.map (rs, getLay1)), | |
1280 | layoutAppPretty | |
1281 | (c, Vector.map (rs, getLay2)), | |
1282 | layoutAppPretty | |
1283 | (c, Vector.map (rs, getLay3)), | |
1284 | Type.con | |
1285 | (c, Vector.map (rs, getTy))) | |
1286 | else let | |
1287 | val (u, ty) = | |
1288 | Type.unknownAux {canGeneralize = true, | |
1289 | equality = Equality.Unknown, | |
1290 | time = bound} | |
1291 | in | |
1292 | List.push (times, bound) | |
1293 | ; List.push (tycons, c) | |
1294 | ; SOME ((bracket o layoutAppPretty) | |
1295 | (c, Vector.map (rs, getLay2)), | |
1296 | layoutAppPretty | |
1297 | (c, Vector.map (rs, getLay2)), | |
1298 | bracket (simple (Unknown.layoutPretty u)), | |
1299 | ty) | |
1300 | end | |
1301 | fun doRecord (fls: (Field.t * lll) list, | |
1302 | extra: bool, mk: unit -> t) = | |
1303 | if List.isEmpty fls | |
1304 | then NONE | |
1305 | else let | |
1306 | fun doit sel = | |
1307 | LayoutPretty.record | |
1308 | (List.map | |
1309 | (fls, fn (f, lll) => | |
1310 | (f, false, sel lll)), | |
1311 | extra) | |
1312 | in | |
1313 | SOME (doit #1, doit #2, doit #3, mk ()) | |
1314 | end | |
1315 | fun flexRecord (_, {fields, spine}) = | |
1316 | doRecord (List.keepAllMap | |
1317 | (fields, fn (f, r) => | |
1318 | Option.map (#1 r, fn lll => (f, lll))), | |
1319 | Spine.canAddFields spine, | |
1320 | fn () => | |
1321 | let | |
1322 | val fields = | |
1323 | List.map (fields, fn (f, r) => | |
1324 | (f, getTy r)) | |
1325 | in | |
1326 | Type.newFlex {fields = fields, | |
1327 | spine = spine} | |
1328 | end) | |
1329 | fun record (_, r) = | |
1330 | case Srecord.detupleOpt r of | |
1331 | NONE => | |
1332 | let | |
1333 | val fields = Srecord.toVector r | |
1334 | val fields' = | |
1335 | Vector.keepAllMap | |
1336 | (fields, fn (f, r) => | |
1337 | Option.map (#1 r, fn lll => (f, lll))) | |
1338 | in | |
1339 | doRecord (Vector.toList fields', | |
1340 | not (Vector.length fields = Vector.length fields'), | |
1341 | fn () => | |
1342 | let | |
1343 | val fields = | |
1344 | Vector.map (fields, fn (f, r) => | |
1345 | (f, getTy r)) | |
1346 | val fields = Srecord.fromVector fields | |
1347 | in | |
1348 | Type.record fields | |
1349 | end) | |
1350 | end | |
1351 | | SOME rs => | |
1352 | if Vector.forall (rs, Option.isNone o #1) | |
1353 | then NONE | |
1354 | else SOME (LayoutPretty.tuple (Vector.map (rs, getLay1)), | |
1355 | LayoutPretty.tuple (Vector.map (rs, getLay2)), | |
1356 | LayoutPretty.tuple (Vector.map (rs, getLay3)), | |
1357 | Type.tuple (Vector.map (rs, getTy))) | |
1358 | fun var bound (_, a) = | |
1359 | if Time.<= (Tyvar.time a, bound) | |
1360 | then NONE | |
1361 | else let | |
1362 | val (u, ty) = | |
1363 | Type.unknownAux {canGeneralize = true, | |
1364 | equality = Equality.Unknown, | |
1365 | time = bound} | |
1366 | in | |
1367 | List.push (times, bound) | |
1368 | ; List.push (tyvars, a) | |
1369 | ; SOME (bracket (simple (layoutPrettyTyvar a)), | |
1370 | simple (layoutPrettyTyvar a), | |
1371 | bracket (simple (Unknown.layoutPretty u)), | |
1372 | ty) | |
1373 | end | |
1374 | fun genFlexRecord _ = Error.bug "TypeEnv.Type.checkTime.genFlexRecord" | |
1375 | fun recursive _ = Error.bug "TypeEnv.Type.checkTime.recursive" | |
1376 | fun checkTime (t, bound) = | |
1377 | if Time.<= (!(time t), bound) | |
1378 | then NONE | |
1379 | else let | |
1380 | fun wrap (f, sel) arg = | |
1381 | case f arg of | |
1382 | NONE => | |
1383 | let | |
1384 | val t = sel arg | |
1385 | in | |
1386 | time t := bound | |
1387 | ; (NONE, t) | |
1388 | end | |
1389 | | SOME (l1, l2, l3, t) => | |
1390 | (time t := bound | |
1391 | ; (SOME (l1, l2, l3), t)) | |
1392 | fun guard t = | |
1393 | if Time.<= (!(time t), bound) | |
1394 | then SOME (NONE, t) | |
1395 | else NONE | |
1396 | val res : lll option * t = | |
1397 | hom (t, {con = wrap (con bound, #1), | |
1398 | expandOpaque = false, | |
1399 | flexRecord = wrap (flexRecord, #1), | |
1400 | genFlexRecord = genFlexRecord, | |
1401 | guard = guard, | |
1402 | overload = wrap (fn _ => NONE, #1), | |
1403 | record = wrap (record, #1), | |
1404 | recursive = recursive, | |
1405 | unknown = wrap (fn _ => NONE, #1), | |
1406 | var = wrap (var bound, #1)}) | |
1407 | in | |
1408 | case res of | |
1409 | (NONE, _) => NONE | |
1410 | | (SOME (l1, _, l3), t) => | |
1411 | SOME (l1, (t, l3)) | |
1412 | end | |
1413 | fun finishCheckTime () = | |
1414 | {times = List.removeDuplicates (!times, Time.equals), | |
1415 | tycons = List.removeDuplicates (!tycons, Tycon.equals), | |
1416 | tyvars = List.removeDuplicates (!tyvars, Tyvar.equals)} | |
1417 | in | |
1418 | {checkTime = checkTime, | |
1419 | finishCheckTime = finishCheckTime} | |
1420 | end | |
1421 | ||
1422 | datatype z = datatype UnifyResult.t | |
1423 | ||
1424 | val traceUnify = | |
1425 | Trace.trace2 | |
1426 | ("TypeEnv.Type.unify", layout, layout, | |
1427 | UnifyResult.layout: | |
1428 | (LayoutPretty.t * LayoutPretty.t, unit) UnifyResult.t -> Layout.t) | |
1429 | ||
1430 | fun unify (t, t', | |
1431 | {layoutPretty: t -> LayoutPretty.t, | |
1432 | layoutPrettyTycon: Tycon.t -> Layout.t, | |
1433 | layoutPrettyTyvar: Tyvar.t -> Layout.t}) = | |
1434 | let | |
1435 | val layoutAppPretty = fn (c, ts) => | |
1436 | Tycon.layoutAppPretty | |
1437 | (c, ts, {layoutPretty = layoutPrettyTycon}) | |
1438 | val checkEquality = fn t => | |
1439 | checkEquality (t, {layoutPrettyTycon = layoutPrettyTycon, | |
1440 | layoutPrettyTyvar = layoutPrettyTyvar}) | |
1441 | val {checkTime, finishCheckTime} = | |
1442 | makeCheckTime {layoutPrettyTycon = layoutPrettyTycon, | |
1443 | layoutPrettyTyvar = layoutPrettyTyvar} | |
1444 | fun unify arg = | |
1445 | traceUnify | |
1446 | (fn (outer as T s, outer' as T s') => | |
1447 | if Set.equals (s, s') | |
1448 | then Unified () | |
1449 | else | |
1450 | let | |
1451 | fun notUnifiable (l: LayoutPretty.t, l': LayoutPretty.t) = | |
1452 | NotUnifiable (l, l') | |
1453 | fun notUnifiableBracket (l, l') = | |
1454 | notUnifiable (bracket l, bracket l') | |
1455 | fun flexToRecord (fields, spine) = | |
1456 | (Vector.fromList fields, | |
1457 | Spine.canAddFields spine) | |
1458 | fun rigidToRecord r = | |
1459 | (Srecord.toVector r, | |
1460 | false) | |
1461 | fun flexToFlexToRecord (fields, spine, equality, time, outer, spine') = | |
1462 | let | |
1463 | val () = | |
1464 | List.foreach | |
1465 | (Spine.fields spine', fn f' => | |
1466 | ignore (Spine.ensureField (spine, f'))) | |
1467 | val fields = | |
1468 | Spine.foldOverNew | |
1469 | (spine, fields, fields, fn (f, fields) => | |
1470 | let | |
1471 | val u = | |
1472 | Type.unknown | |
1473 | {canGeneralize = true, | |
1474 | equality = Equality.or2 (equality, Equality.Unknown), | |
1475 | time = time} | |
1476 | in | |
1477 | (f, u) :: fields | |
1478 | end) | |
1479 | val _ = setTy (outer, FlexRecord {fields = fields, spine = spine}) | |
1480 | in | |
1481 | flexToRecord (fields, spine) | |
1482 | end | |
1483 | fun flexToRigidToRecord (fields, spine, equality, time, outer, r') = | |
1484 | let | |
1485 | val () = | |
1486 | Vector.foreach | |
1487 | (Srecord.toVector r', fn (f', _) => | |
1488 | ignore (Spine.ensureField (spine, f'))) | |
1489 | val () = Spine.noMoreFields spine | |
1490 | val fields = | |
1491 | Spine.foldOverNew | |
1492 | (spine, fields, fields, fn (f, fields) => | |
1493 | let | |
1494 | val u = | |
1495 | Type.unknown | |
1496 | {canGeneralize = true, | |
1497 | equality = Equality.or2 (equality, Equality.Unknown), | |
1498 | time = time} | |
1499 | in | |
1500 | (f, u) :: fields | |
1501 | end) | |
1502 | val r = Srecord.fromVector (Vector.fromList fields) | |
1503 | val _ = setTy (outer, Record r) | |
1504 | in | |
1505 | rigidToRecord r | |
1506 | end | |
1507 | fun oneFlex ({fields, spine}, equality, time, outer, r', swap) = | |
1508 | unifyRecords | |
1509 | (flexToRigidToRecord (fields, spine, equality, time, outer, r'), | |
1510 | rigidToRecord r', | |
1511 | fn () => Unified (Record r'), | |
1512 | notUnifiable o (fn (l, l') => | |
1513 | if swap | |
1514 | then (l', l) | |
1515 | else (l, l'))) | |
1516 | fun genFlexError () = | |
1517 | Error.bug "TypeEnv.Type.unify: GenFlexRecord" | |
1518 | val {equality, time, ty = t, plist} = Set.! s | |
1519 | val {equality = equality', time = time', ty = t', ...} = Set.! s' | |
1520 | fun not () = | |
1521 | notUnifiableBracket (layoutPretty outer, | |
1522 | layoutPretty outer') | |
1523 | fun unifys (ts, ts', yes, no) = | |
1524 | let | |
1525 | val us = Vector.map2 (ts, ts', unify) | |
1526 | in | |
1527 | if Vector.forall | |
1528 | (us, fn Unified _ => true | _ => false) | |
1529 | then yes () | |
1530 | else | |
1531 | let | |
1532 | val (ls, ls') = | |
1533 | Vector.unzip | |
1534 | (Vector.map | |
1535 | (us, fn u => | |
1536 | case u of | |
1537 | Unified _ => (dontCare, dontCare) | |
1538 | | NotUnifiable (l, l') => (l, l'))) | |
1539 | in | |
1540 | no (ls, ls') | |
1541 | end | |
1542 | end | |
1543 | fun conAnd (c, ts, t, t', swap) = | |
1544 | let | |
1545 | fun maybe (z, z') = | |
1546 | if swap then (z', z) else (z, z') | |
1547 | in | |
1548 | case t of | |
1549 | Con (c', ts') => | |
1550 | if Tycon.equals (c, c') | |
1551 | then | |
1552 | if Vector.length ts <> Vector.length ts' | |
1553 | then | |
1554 | let | |
1555 | fun lay ts = | |
1556 | simple | |
1557 | (Layout.seq | |
1558 | [Layout.str | |
1559 | (concat ["<", | |
1560 | Int.toString | |
1561 | (Vector.length ts), | |
1562 | " args> "]), | |
1563 | Tycon.layout c]) | |
1564 | in | |
1565 | notUnifiableBracket | |
1566 | (maybe (lay ts, lay ts')) | |
1567 | end | |
1568 | else | |
1569 | unifys | |
1570 | (ts, ts', | |
1571 | fn () => Unified t, | |
1572 | fn (ls, ls') => | |
1573 | let | |
1574 | fun lay ls = layoutAppPretty (c, ls) | |
1575 | in | |
1576 | notUnifiable | |
1577 | (maybe (lay ls, lay ls')) | |
1578 | end) | |
1579 | else not () | |
1580 | | Overload ov => | |
1581 | if Vector.isEmpty ts | |
1582 | andalso Overload.matchesTycon (ov, c) | |
1583 | then Unified t' | |
1584 | else not () | |
1585 | | _ => not () | |
1586 | end | |
1587 | fun oneUnknown (u: Unknown.t, | |
1588 | equality: Equality.t, | |
1589 | time: Time.t, | |
1590 | outer: t, | |
1591 | t': Type.ty, | |
1592 | outer': Type.t, | |
1593 | swap: bool) = | |
1594 | let | |
1595 | (* This should fail if the unknown occurs in t. *) | |
1596 | fun con (_, _, ts) = | |
1597 | Vector.exists (ts, fn b => b) | |
1598 | fun doFields fields = | |
1599 | List.exists (fields, fn (_, b) => b) | |
1600 | fun flexRecord (_, {fields, spine = _}) = | |
1601 | doFields fields | |
1602 | fun record (_, r) = Srecord.exists (r, fn b => b) | |
1603 | fun unknown (_, u') = Unknown.equals (u, u') | |
1604 | fun no _ = false | |
1605 | val isCircular = | |
1606 | hom (outer', | |
1607 | {con = con, | |
1608 | expandOpaque = false, | |
1609 | flexRecord = flexRecord, | |
1610 | genFlexRecord = fn _ => | |
1611 | Error.bug "TypeEnv.Type.unify.oneUnknown: genFlexRecord", | |
1612 | guard = fn _ => NONE, | |
1613 | overload = no, | |
1614 | record = record, | |
1615 | recursive = fn _ => | |
1616 | Error.bug "TypeEnv.Type.unify.oneUnknown: recursive", | |
1617 | unknown = unknown, | |
1618 | var = no}) | |
1619 | in | |
1620 | if isCircular | |
1621 | then not () | |
1622 | else let | |
1623 | fun err (l, (t'', l'')) = | |
1624 | (setTy (outer, getTy t'') | |
1625 | ; notUnifiable | |
1626 | (if swap | |
1627 | then (l, l'') | |
1628 | else (l'', l))) | |
1629 | in | |
1630 | case equality of | |
1631 | Equality.True => | |
1632 | (case checkEquality outer' of | |
1633 | NONE => Unified t' | |
1634 | | SOME (l, (t'', l'')) => | |
1635 | err (l, (t'', l''))) | |
1636 | | _ => | |
1637 | (case checkTime (outer', time) of | |
1638 | NONE => Unified t' | |
1639 | | SOME (l, (t'', l'')) => | |
1640 | err (l, (t'', l''))) | |
1641 | end | |
1642 | end | |
1643 | val res = | |
1644 | case (t, t') of | |
1645 | (Unknown r, Unknown r') => | |
1646 | (case (!equality, !equality') of | |
1647 | (Equality.True, Equality.False) => | |
1648 | notUnifiableBracket | |
1649 | (simple (str "<equality>"), | |
1650 | simple (str "<non-equality>")) | |
1651 | | (Equality.False, Equality.True) => | |
1652 | notUnifiableBracket | |
1653 | (simple (str "<non-equality>"), | |
1654 | simple (str "<equality>")) | |
1655 | | _ => Unified (Unknown (Unknown.join (r, r')))) | |
1656 | | (Unknown u, _) => | |
1657 | oneUnknown (u, !equality, !time, outer, t', outer', false) | |
1658 | | (_, Unknown u') => | |
1659 | oneUnknown (u', !equality', !time', outer', t, outer, true) | |
1660 | | (Con (c, ts), _) => conAnd (c, ts, t', t, false) | |
1661 | | (_, Con (c, ts)) => conAnd (c, ts, t, t', true) | |
1662 | | (FlexRecord f, Record r') => | |
1663 | oneFlex (f, !equality, !time, outer, r', false) | |
1664 | | (Record r, FlexRecord f') => | |
1665 | oneFlex (f', !equality', !time', outer', r, true) | |
1666 | | (FlexRecord {fields = fields, spine = spine}, | |
1667 | FlexRecord {fields = fields', spine = spine'}) => | |
1668 | let | |
1669 | fun yes () = | |
1670 | let | |
1671 | val () = Spine.unify (spine, spine') | |
1672 | val fields = | |
1673 | List.fold | |
1674 | (fields, fields', fn ((f, t), ac) => | |
1675 | if List.exists (fields', fn (f', _) => | |
1676 | Field.equals (f, f')) | |
1677 | then ac | |
1678 | else (f, t) :: ac) | |
1679 | in | |
1680 | Unified (FlexRecord {fields = fields, | |
1681 | spine = spine}) | |
1682 | end | |
1683 | in | |
1684 | unifyRecords | |
1685 | (flexToFlexToRecord (fields, spine, !equality, !time, outer, spine'), | |
1686 | flexToFlexToRecord (fields', spine', !equality', !time', outer', spine), | |
1687 | yes, notUnifiable) | |
1688 | end | |
1689 | | (GenFlexRecord _, _) => genFlexError () | |
1690 | | (_, GenFlexRecord _) => genFlexError () | |
1691 | | (Overload ov1, Overload ov2) => | |
1692 | if Overload.equals (ov1, ov2) | |
1693 | then Unified t | |
1694 | else not () | |
1695 | | (Record r, Record r') => | |
1696 | (case (Srecord.detupleOpt r, | |
1697 | Srecord.detupleOpt r') of | |
1698 | (NONE, NONE) => | |
1699 | unifyRecords | |
1700 | (rigidToRecord r, rigidToRecord r', | |
1701 | fn () => Unified (Record r), | |
1702 | notUnifiable) | |
1703 | | (SOME ts, SOME ts') => | |
1704 | if Vector.length ts = Vector.length ts' | |
1705 | then unifys | |
1706 | (ts, ts', | |
1707 | fn () => Unified (Record r), | |
1708 | fn (ls, ls') => | |
1709 | notUnifiable | |
1710 | (LayoutPretty.tuple ls, | |
1711 | LayoutPretty.tuple ls')) | |
1712 | else not () | |
1713 | | _ => not ()) | |
1714 | | (Var a, Var a') => | |
1715 | if Tyvar.equals (a, a') | |
1716 | then Unified t | |
1717 | else not () | |
1718 | | _ => not () | |
1719 | val res = | |
1720 | case res of | |
1721 | NotUnifiable (l, l') => | |
1722 | NotUnifiable (l, l') | |
1723 | | Unified ty => | |
1724 | let | |
1725 | val () = Set.union (s, s') | |
1726 | val () = time := Time.min (!time, !time') | |
1727 | val () = equality := Equality.join (!equality, !equality') | |
1728 | val () = | |
1729 | Set.:= (s, {equality = equality, | |
1730 | plist = plist, | |
1731 | time = time, | |
1732 | ty = ty}) | |
1733 | in | |
1734 | Unified () | |
1735 | end | |
1736 | in | |
1737 | res | |
1738 | end) arg | |
1739 | and unifyRecords ((fields: (Field.t * t) vector, | |
1740 | dots: bool), | |
1741 | (fields': (Field.t * t) vector, | |
1742 | dots': bool), | |
1743 | yes, no) = | |
1744 | let | |
1745 | fun subset (fields, fields', | |
1746 | ac, dots, ac', dots', | |
1747 | skipBoth) = | |
1748 | Vector.fold | |
1749 | (fields, (ac, dots, ac', dots'), | |
1750 | fn ((f, t), (ac, dots, ac', dots')) => | |
1751 | case Vector.peek (fields', fn (f', _) => | |
1752 | Field.equals (f, f')) of | |
1753 | NONE => | |
1754 | ((f, true, dontCare) :: ac, dots, ac', dots') | |
1755 | | SOME (_, t') => | |
1756 | if skipBoth | |
1757 | then (ac, dots, ac', dots') | |
1758 | else | |
1759 | case unify (t, t') of | |
1760 | NotUnifiable (l, l') => | |
1761 | ((f, false, l) :: ac, dots, | |
1762 | (f, false, l') :: ac', dots') | |
1763 | | Unified _ => (ac, true, ac', true)) | |
1764 | val (ac, dots, ac', dots') = | |
1765 | subset (fields, fields', [], dots, [], dots', false) | |
1766 | val (ac', dots', ac, dots) = | |
1767 | subset (fields', fields, ac', dots', ac, dots, true) | |
1768 | in | |
1769 | case (ac, ac') of | |
1770 | ([], []) => yes () | |
1771 | | _ => no (LayoutPretty.record (ac, dots), | |
1772 | LayoutPretty.record (ac', dots')) | |
1773 | end | |
1774 | val res = unify (t, t') | |
1775 | in | |
1776 | case res of | |
1777 | NotUnifiable ((l, _), (l', _)) => | |
1778 | let | |
1779 | val {times, tycons, tyvars} = | |
1780 | finishCheckTime () | |
1781 | fun notes () = | |
1782 | if List.isEmpty tycons andalso List.isEmpty tyvars | |
1783 | then Layout.empty | |
1784 | else let | |
1785 | fun doit (xs, lay) = | |
1786 | List.insertionSort | |
1787 | (List.map (xs, fn x => (x, lay x)), | |
1788 | fn ((_, l1), (_, l2)) => | |
1789 | String.<= (Layout.toString l1, | |
1790 | Layout.toString l2)) | |
1791 | val tycons = doit (tycons, layoutPrettyTycon) | |
1792 | val tyvars = doit (tyvars, layoutPrettyTyvar) | |
1793 | val tys = | |
1794 | List.map (tycons, #2) | |
1795 | @ List.map (tyvars, #2) | |
1796 | in | |
1797 | Layout.align | |
1798 | [seq [str "note: ", | |
1799 | if List.length tys > 1 | |
1800 | then str "types would escape their scope: " | |
1801 | else str "type would escape its scope: ", | |
1802 | seq (Layout.separate (tys, ", "))], | |
1803 | (Layout.align o List.map) | |
1804 | (tycons, fn (c, _) => | |
1805 | seq [str "escape from: ", | |
1806 | Region.layout (Tycon.region c)]), | |
1807 | (Layout.align o List.map) | |
1808 | (times, fn t => | |
1809 | seq [str "escape to: ", | |
1810 | Region.layout (Time.region t)])] | |
1811 | end | |
1812 | in | |
1813 | NotUnifiable (l, l', | |
1814 | {notes = notes}) | |
1815 | end | |
1816 | | Unified () => Unified () | |
1817 | end | |
1818 | ||
1819 | local | |
1820 | val {get: Tycon.t -> (t * Tycon.t) option, set, ...} = | |
1821 | Property.getSetOnce (Tycon.plist, Property.initConst NONE) | |
1822 | in | |
1823 | fun setSynonym (c, c') = set (c, SOME (con (c, Vector.new0 ()), c')) | |
1824 | val synonym = get | |
1825 | end | |
1826 | ||
1827 | val () = | |
1828 | List.foreach | |
1829 | (CharSize.all, fn s => | |
1830 | setSynonym (Tycon.char s, | |
1831 | Tycon.word (WordSize.fromBits (CharSize.bits s)))) | |
1832 | ||
1833 | val () = | |
1834 | List.foreach | |
1835 | (IntSize.all, fn s => | |
1836 | setSynonym (Tycon.int s, | |
1837 | Tycon.word (WordSize.fromBits (IntSize.bits s)))) | |
1838 | ||
1839 | structure Overload = | |
1840 | struct | |
1841 | open Overload | |
1842 | ||
1843 | val defaultType = | |
1844 | fn Char => con (Tycon.defaultChar (), Vector.new0 ()) | |
1845 | | Int => con (Tycon.defaultInt (), Vector.new0 ()) | |
1846 | | Real => con (Tycon.defaultReal (), Vector.new0 ()) | |
1847 | | Word => con (Tycon.defaultWord (), Vector.new0 ()) | |
1848 | end | |
1849 | ||
1850 | fun 'a simpleHom {con: t * Tycon.t * 'a vector -> 'a, | |
1851 | expandOpaque: bool, | |
1852 | record: t * (Field.t * 'a) vector -> 'a, | |
1853 | replaceSynonyms: bool, | |
1854 | var: t * Tyvar.t -> 'a} = | |
1855 | let | |
1856 | val unit = con (unit, Tycon.tuple, Vector.new0 ()) | |
1857 | val unknown = unit | |
1858 | fun sortFields (fields: (Field.t * 'a) list) = | |
1859 | let | |
1860 | val a = Array.fromList fields | |
1861 | val () = | |
1862 | QuickSort.sortArray (a, fn ((f, _), (f', _)) => | |
1863 | Field.<= (f, f')) | |
1864 | in | |
1865 | Array.toVector a | |
1866 | end | |
1867 | fun unsorted (t, fields: (Field.t * 'a) list) = | |
1868 | let | |
1869 | val v = sortFields fields | |
1870 | in | |
1871 | record (t, v) | |
1872 | end | |
1873 | fun genFlexRecord (t, {extra, fields, spine = _}) = | |
1874 | unsorted (t, | |
1875 | List.fold | |
1876 | (extra (), fields, fn ({field, tyvar}, ac) => | |
1877 | (field, var (Type.var tyvar, tyvar)) :: ac)) | |
1878 | fun flexRecord (t, {fields, spine}) = | |
1879 | if Spine.canAddFields spine | |
1880 | then Error.bug "TypeEnv.Type.simpleHom: flexRecord" | |
1881 | else unsorted (t, | |
1882 | Spine.foldOverNew | |
1883 | (spine, fields, fields, fn (f, ac) => | |
1884 | (f, unit) :: ac)) | |
1885 | fun recursive _ = Error.bug "TypeEnv.Type.simpleHom.recursive" | |
1886 | val con = | |
1887 | if not replaceSynonyms | |
1888 | then con | |
1889 | else | |
1890 | fn (t, c, ts) => | |
1891 | let | |
1892 | val (t, c) = | |
1893 | case synonym c of | |
1894 | NONE => (t, c) | |
1895 | | SOME (t, c) => (t, c) | |
1896 | in | |
1897 | con (t, c, ts) | |
1898 | end | |
1899 | fun overload (t', ov) = | |
1900 | let | |
1901 | val t = Overload.defaultType ov | |
1902 | val _ = unify (t, t', | |
1903 | {layoutPretty = fn _ => | |
1904 | Error.bug "TypeEnv.Type.simpleHom.overload: layoutPretty", | |
1905 | layoutPrettyTycon = fn _ => | |
1906 | Error.bug "TypeEnv.Type.simpleHom.overload: layoutPrettyTycon", | |
1907 | layoutPrettyTyvar = fn _ => | |
1908 | Error.bug "TypeEnv.Type.simpleHom.overload: layoutPrettyTyvar"}) | |
1909 | in | |
1910 | con (t, Overload.defaultTycon ov, Vector.new0 ()) | |
1911 | end | |
1912 | in | |
1913 | makeHom {con = con, | |
1914 | expandOpaque = expandOpaque, | |
1915 | flexRecord = flexRecord, | |
1916 | genFlexRecord = genFlexRecord, | |
1917 | guard = fn _ => NONE, | |
1918 | overload = overload, | |
1919 | record = fn (t, r) => record (t, Srecord.toVector r), | |
1920 | recursive = recursive, | |
1921 | unknown = fn _ => unknown, | |
1922 | var = var} | |
1923 | end | |
1924 | end | |
1925 | ||
1926 | structure Scheme = | |
1927 | struct | |
1928 | datatype t = | |
1929 | General of {bound: unit -> Tyvar.t vector, | |
1930 | canGeneralize: bool, | |
1931 | flexes: Type.genFlexRecord list, | |
1932 | tyvars: Tyvar.t vector, | |
1933 | ty: Type.t} | |
1934 | | Mono of Type.t | |
1935 | ||
1936 | val ty = | |
1937 | fn General {ty, ...} => ty | |
1938 | | Mono ty => ty | |
1939 | ||
1940 | val dest = | |
1941 | fn General {bound, ty, ...} => (bound (), ty) | |
1942 | | Mono ty => (Vector.new0 (), ty) | |
1943 | ||
1944 | val kind = | |
1945 | fn General {bound, ...} => Kind.Arity (Vector.length (bound ())) | |
1946 | | Mono _ => Kind.Arity 0 | |
1947 | ||
1948 | fun layout s = | |
1949 | case s of | |
1950 | Mono t => Type.layout t | |
1951 | | General {canGeneralize, tyvars, ty, ...} => | |
1952 | Layout.record [("canGeneralize", Bool.layout canGeneralize), | |
1953 | ("tyvars", Vector.layout Tyvar.layout tyvars), | |
1954 | ("ty", Type.layout ty)] | |
1955 | ||
1956 | fun make {canGeneralize, tyvars, ty} = | |
1957 | if Vector.isEmpty tyvars | |
1958 | then Mono ty | |
1959 | else General {bound = fn () => tyvars, | |
1960 | canGeneralize = canGeneralize, | |
1961 | flexes = [], | |
1962 | tyvars = tyvars, | |
1963 | ty = ty} | |
1964 | ||
1965 | val fromType = Mono | |
1966 | ||
1967 | fun fromTycon (tycon: Tycon.t): t = | |
1968 | let | |
1969 | val kind = Tycon.kind tycon | |
1970 | val arity = | |
1971 | case kind of | |
1972 | Kind.Arity arity => arity | |
1973 | | Kind.Nary => Error.bug "TypeEnv.Scheme.fromTycon: Kind.Nary" | |
1974 | val tyvars = | |
1975 | Vector.tabulate | |
1976 | (arity, fn _ => | |
1977 | Tyvar.makeNoname {equality = false}) | |
1978 | in | |
1979 | make | |
1980 | {canGeneralize = true, | |
1981 | ty = Type.con (tycon, Vector.map (tyvars, Type.var)), | |
1982 | tyvars = tyvars} | |
1983 | end | |
1984 | ||
1985 | fun instantiateAux (t: t, subst) = | |
1986 | case t of | |
1987 | Mono ty => {args = fn () => Vector.new0 (), | |
1988 | instance = ty} | |
1989 | | General {canGeneralize, flexes, tyvars, ty, ...} => | |
1990 | (case Type.deEta (ty, tyvars) of | |
1991 | SOME tycon => | |
1992 | let | |
1993 | val types = | |
1994 | Vector.mapi | |
1995 | (tyvars, fn (i, a) => | |
1996 | subst {canGeneralize = canGeneralize, | |
1997 | equality = Tyvar.isEquality a, | |
1998 | index = i}) | |
1999 | in | |
2000 | {args = fn () => types, | |
2001 | instance = Type.con (tycon, types)} | |
2002 | end | |
2003 | | NONE => | |
2004 | let | |
2005 | open Type | |
2006 | val {destroy = destroyTyvarInst, | |
2007 | get = tyvarInst: Tyvar.t -> Type.t option, | |
2008 | set = setTyvarInst} = | |
2009 | Property.destGetSetOnce (Tyvar.plist, | |
2010 | Property.initConst NONE) | |
2011 | val types = | |
2012 | Vector.mapi | |
2013 | (tyvars, fn (i, a) => | |
2014 | let | |
2015 | val t = subst {canGeneralize = canGeneralize, | |
2016 | equality = Tyvar.isEquality a, | |
2017 | index = i} | |
2018 | val _ = setTyvarInst (a, SOME t) | |
2019 | in | |
2020 | t | |
2021 | end) | |
2022 | type z = {isNew: bool, ty: Type.t} | |
2023 | fun isNew {isNew = b, ty = _} = b | |
2024 | fun keep ty = {isNew = false, ty = ty} | |
2025 | fun con (ty, c, zs) = | |
2026 | if Vector.exists (zs, isNew) | |
2027 | then {isNew = true, | |
2028 | ty = Type.con (c, Vector.map (zs, #ty))} | |
2029 | else keep ty | |
2030 | val flexInsts = ref [] | |
2031 | fun genFlexRecord (_, {extra = _, fields, spine}) = | |
2032 | let | |
2033 | val fields = List.revMap (fields, fn (f, t: z) => | |
2034 | (f, #ty t)) | |
2035 | val flex = newFlex {fields = fields, | |
2036 | spine = spine} | |
2037 | val _ = List.push (flexInsts, {flex = flex, | |
2038 | spine = spine}) | |
2039 | in | |
2040 | {isNew = true, | |
2041 | ty = flex} | |
2042 | end | |
2043 | fun record (t, r) = | |
2044 | if Srecord.exists (r, isNew) | |
2045 | then {isNew = true, | |
2046 | ty = Type.record (Srecord.map (r, #ty))} | |
2047 | else keep t | |
2048 | fun recursive _ = | |
2049 | (* If we get here, there has already been a type error | |
2050 | * in the user's program, so we return a new type to avoid | |
2051 | * compounding the error. | |
2052 | *) | |
2053 | {isNew = true, | |
2054 | ty = Type.new ()} | |
2055 | fun var (ty, a) = | |
2056 | case tyvarInst a of | |
2057 | NONE => {isNew = false, ty = ty} | |
2058 | | SOME ty => {isNew = true, ty = ty} | |
2059 | val {ty: Type.t, ...} = | |
2060 | Type.hom (ty, {con = con, | |
2061 | expandOpaque = false, | |
2062 | flexRecord = keep o #1, | |
2063 | genFlexRecord = genFlexRecord, | |
2064 | guard = fn _ => NONE, | |
2065 | overload = keep o #1, | |
2066 | record = record, | |
2067 | recursive = recursive, | |
2068 | unknown = keep o #1, | |
2069 | var = var}) | |
2070 | val _ = destroyTyvarInst () | |
2071 | val flexInsts = !flexInsts | |
2072 | fun args (): Type.t vector = | |
2073 | Vector.fromList | |
2074 | (List.fold | |
2075 | (flexes, Vector.toList types, | |
2076 | fn ({fields, spine, ...}, ac) => | |
2077 | let | |
2078 | fun done peek = | |
2079 | Spine.foldOverNew | |
2080 | (spine, fields, ac, fn (f, ac) => | |
2081 | (case peek f of | |
2082 | NONE => Type.unit | |
2083 | | SOME t => t) :: ac) | |
2084 | in | |
2085 | case List.peek (flexInsts, | |
2086 | fn {spine = spine', ...} => | |
2087 | Spine.equals (spine, spine')) of | |
2088 | NONE => done (fn _ => NONE) | |
2089 | | SOME {flex, ...} => | |
2090 | let | |
2091 | fun peekFields (fields, f) = | |
2092 | Option.map | |
2093 | (List.peek (fields, fn (f', _) => | |
2094 | Field.equals (f, f')), | |
2095 | #2) | |
2096 | in | |
2097 | done | |
2098 | (case Type.getTy flex of | |
2099 | FlexRecord {fields, ...} => | |
2100 | (fn f => peekFields (fields, f)) | |
2101 | | GenFlexRecord {extra, fields, ...} => | |
2102 | (fn f => | |
2103 | case peekFields (fields, f) of | |
2104 | NONE => | |
2105 | Option.map | |
2106 | (List.peek | |
2107 | (extra (), | |
2108 | fn {field, ...} => | |
2109 | Field.equals (f, field)), | |
2110 | Type.var o #tyvar) | |
2111 | | SOME t => SOME t) | |
2112 | | Record r => | |
2113 | (fn f => Srecord.peek (r, f)) | |
2114 | | _ => Error.bug "TypeEnv.instantiate': General:strange flexInst") | |
2115 | end | |
2116 | end)) | |
2117 | in | |
2118 | {args = args, | |
2119 | instance = ty} | |
2120 | end) | |
2121 | ||
2122 | fun apply (s, ts) = | |
2123 | #instance (instantiateAux (s, fn {index, ...} => Vector.sub (ts, index))) | |
2124 | ||
2125 | fun instantiate s = | |
2126 | instantiateAux | |
2127 | (s, fn {canGeneralize, equality, ...} => | |
2128 | Type.unknown {canGeneralize = canGeneralize, | |
2129 | equality = if equality | |
2130 | then Equality.True | |
2131 | else Equality.Unknown, | |
2132 | time = Time.now ()}) | |
2133 | ||
2134 | val instantiate = | |
2135 | Trace.trace ("TypeEnv.Scheme.instantiate", layout, Type.layout o #instance) | |
2136 | instantiate | |
2137 | ||
2138 | fun fresh s = | |
2139 | let | |
2140 | val (tyvars, _) = dest s | |
2141 | val tyvars = Vector.map (tyvars, Tyvar.makeLike) | |
2142 | in | |
2143 | (tyvars, apply (s, (Vector.map (tyvars, Type.var)))) | |
2144 | end | |
2145 | ||
2146 | fun freshEq s = | |
2147 | let | |
2148 | val (tyvars, _) = dest s | |
2149 | val tyvars = Vector.map (tyvars, fn _ => Tyvar.makeNoname {equality = true}) | |
2150 | in | |
2151 | (tyvars, apply (s, (Vector.map (tyvars, Type.var)))) | |
2152 | end | |
2153 | ||
2154 | fun admitsEquality s = | |
2155 | let | |
2156 | val (_, ty) = freshEq s | |
2157 | in | |
2158 | case !(Type.equality ty) of | |
2159 | Equality.False => false | |
2160 | | Equality.True => true | |
2161 | | Equality.Unknown => Error.bug "TypeEnv.Scheme.admitsEquality: Unknown" | |
2162 | end | |
2163 | ||
2164 | val admitsEquality = | |
2165 | Trace.trace ("TypeEnv.Scheme.admitsEquality", layout, Bool.layout) | |
2166 | admitsEquality | |
2167 | ||
2168 | fun checkEquality (s, {layoutPrettyTycon}) = | |
2169 | let | |
2170 | fun layoutPrettyTyvar _ = | |
2171 | Error.bug "TypeEnv.Scheme.checkEquality.layoutPrettyTyvar" | |
2172 | val (_, ty) = freshEq s | |
2173 | in | |
2174 | Option.map | |
2175 | (Type.checkEquality | |
2176 | (ty, {layoutPrettyTycon = layoutPrettyTycon, | |
2177 | layoutPrettyTyvar = layoutPrettyTyvar}), | |
2178 | fn ((l, _), _) => l) | |
2179 | end | |
2180 | ||
2181 | fun haveUnknowns s: bool = | |
2182 | let | |
2183 | fun con (_, _, bs) = Vector.exists (bs, fn b => b) | |
2184 | fun no _ = false | |
2185 | val {destroy, hom} = | |
2186 | Type.makeHom | |
2187 | {con = con, | |
2188 | expandOpaque = false, | |
2189 | flexRecord = fn (_, {fields, ...}) => List.exists (fields, #2), | |
2190 | genFlexRecord = (fn (_, {fields, ...}) => | |
2191 | List.exists (fields, #2)), | |
2192 | guard = fn _ => NONE, | |
2193 | overload = no, | |
2194 | record = fn (_, r) => Srecord.exists (r, fn b => b), | |
2195 | recursive = no, | |
2196 | unknown = fn _ => true, | |
2197 | var = no} | |
2198 | val res = hom (ty s) | |
2199 | val _ = destroy () | |
2200 | in | |
2201 | res | |
2202 | end | |
2203 | end | |
2204 | ||
2205 | fun 'a close region = | |
2206 | let | |
2207 | val beforeGen = Time.now () | |
2208 | val () = Time.tick region | |
2209 | in | |
2210 | fn (ensure, | |
2211 | varTypes, | |
2212 | {error: 'a * Layout.t * Tyvar.t list -> unit, | |
2213 | layoutPrettyTycon, | |
2214 | layoutPrettyTyvar}) => | |
2215 | let | |
2216 | local | |
2217 | fun checkTime (t, bound) = | |
2218 | let | |
2219 | val {checkTime, finishCheckTime} = | |
2220 | Type.makeCheckTime {layoutPrettyTycon = layoutPrettyTycon, | |
2221 | layoutPrettyTyvar = layoutPrettyTyvar} | |
2222 | in | |
2223 | Option.map (checkTime (t, bound), fn z => | |
2224 | (z, finishCheckTime ())) | |
2225 | end | |
2226 | in | |
2227 | val varTypes = | |
2228 | Vector.map | |
2229 | (varTypes, fn ({isExpansive, ty, var}) => | |
2230 | if not isExpansive | |
2231 | then {isExpansive = false, | |
2232 | ty = ty} | |
2233 | else (case checkTime (ty, beforeGen) of | |
2234 | NONE => {isExpansive = true, | |
2235 | ty = ty} | |
2236 | | SOME (((l, _), _), {tyvars, ...}) => | |
2237 | (error (var, l, tyvars) | |
2238 | ; {isExpansive = false, | |
2239 | ty = ty}))) | |
2240 | end | |
2241 | val tyvars = Vector.toList ensure | |
2242 | (* Convert all the unknown types bound at this level into tyvars. | |
2243 | * Convert all the FlexRecords bound at this level into | |
2244 | * GenFlexRecords. | |
2245 | *) | |
2246 | val (flexes, tyvars) = | |
2247 | if Vector.forall | |
2248 | (varTypes, fn {ty, ...} => | |
2249 | Time.<= (!(Type.time ty), beforeGen)) | |
2250 | then ([], tyvars) | |
2251 | else let | |
2252 | val flexes = ref [] | |
2253 | val tyvars = ref tyvars | |
2254 | fun flexRecord (t, _) = | |
2255 | let | |
2256 | val (fields, spine) = | |
2257 | case Type.getTy t of | |
2258 | Type.FlexRecord {fields, spine} => | |
2259 | (fields, spine) | |
2260 | | _ => Error.bug "TypeEnv.close.flexRecord: not FlexRecord" | |
2261 | fun newField f = | |
2262 | {field = f, | |
2263 | tyvar = Tyvar.makeNoname {equality = false}} | |
2264 | val extra = | |
2265 | let | |
2266 | val all = ref [] | |
2267 | val fields = | |
2268 | List.map (fields, fn (f, _) => (f, ())) | |
2269 | in | |
2270 | fn () => | |
2271 | let | |
2272 | val old = !all | |
2273 | val fields = | |
2274 | List.fold | |
2275 | (old, fields, fn ({field, ...}, ac) => | |
2276 | (field, ()) :: ac) | |
2277 | val new = | |
2278 | Spine.foldOverNew | |
2279 | (spine, fields, old, fn (f, ac) => | |
2280 | (newField f) :: ac) | |
2281 | val () = all := new | |
2282 | in | |
2283 | new | |
2284 | end | |
2285 | end | |
2286 | val gfr = {extra = extra, | |
2287 | fields = fields, | |
2288 | spine = spine} | |
2289 | val _ = List.push (flexes, gfr) | |
2290 | in | |
2291 | Type.setTy | |
2292 | (t, Type.GenFlexRecord gfr) | |
2293 | end | |
2294 | fun unknown (t, Unknown.T {canGeneralize, ...}) = | |
2295 | if not canGeneralize | |
2296 | then () | |
2297 | else let | |
2298 | val equality = Type.equality t | |
2299 | val a = | |
2300 | Tyvar.makeNoname | |
2301 | {equality = | |
2302 | case !equality of | |
2303 | Equality.False => false | |
2304 | | Equality.True => true | |
2305 | | Equality.Unknown => | |
2306 | (equality := Equality.False | |
2307 | ; false)} | |
2308 | val _ = List.push (tyvars, a) | |
2309 | in | |
2310 | Type.setTy | |
2311 | (t, Type.Var a) | |
2312 | end | |
2313 | fun guard t = | |
2314 | if Time.<= (!(Type.time t), beforeGen) | |
2315 | then SOME () | |
2316 | else NONE | |
2317 | val {destroy, hom} = | |
2318 | Type.makeHom | |
2319 | {con = fn _ => (), | |
2320 | expandOpaque = false, | |
2321 | flexRecord = flexRecord, | |
2322 | genFlexRecord = fn _ => (), | |
2323 | guard = guard, | |
2324 | overload = fn _ => (), | |
2325 | record = fn _ => (), | |
2326 | recursive = fn _ => (), | |
2327 | unknown = unknown, | |
2328 | var = fn _ => ()} | |
2329 | val _ = Vector.foreach (varTypes, hom o #ty) | |
2330 | val _ = destroy () | |
2331 | in | |
2332 | (!flexes, !tyvars) | |
2333 | end | |
2334 | (* For all fields that were added to the generalized flex records, | |
2335 | * add a type variable. | |
2336 | *) | |
2337 | fun bound () = | |
2338 | Vector.fromList | |
2339 | (List.fold | |
2340 | (flexes, tyvars, fn ({extra, fields, spine}, ac) => | |
2341 | let | |
2342 | val extra = extra () | |
2343 | in | |
2344 | Spine.foldOverNew | |
2345 | (spine, fields, ac, fn (f, ac) => | |
2346 | case List.peek (extra, fn {field, ...} => | |
2347 | Field.equals (f, field)) of | |
2348 | NONE => Error.bug "TypeEnv.close.bound: GenFlex missing field" | |
2349 | | SOME {tyvar, ...} => tyvar :: ac) | |
2350 | end)) | |
2351 | val schemes = | |
2352 | Vector.map | |
2353 | (varTypes, fn {isExpansive, ty} => | |
2354 | if isExpansive | |
2355 | then Scheme.Mono ty | |
2356 | else Scheme.General {bound = bound, | |
2357 | canGeneralize = true, | |
2358 | flexes = flexes, | |
2359 | tyvars = Vector.fromList tyvars, | |
2360 | ty = ty}) | |
2361 | in | |
2362 | {bound = bound, | |
2363 | schemes = schemes} | |
2364 | end | |
2365 | end | |
2366 | ||
2367 | structure Type = | |
2368 | struct | |
2369 | open Type | |
2370 | ||
2371 | fun homConVar {con, expandOpaque, var} = | |
2372 | let | |
2373 | fun tuple (t, ts) = | |
2374 | if 1 = Vector.length ts | |
2375 | then Vector.first ts | |
2376 | else con (t, Tycon.tuple, ts) | |
2377 | in | |
2378 | simpleHom {con = con, | |
2379 | expandOpaque = expandOpaque, | |
2380 | record = fn (t, fs) => tuple (t, Vector.map (fs, #2)), | |
2381 | replaceSynonyms = true, | |
2382 | var = var} | |
2383 | end | |
2384 | ||
2385 | fun makeHom {con, expandOpaque, var} = | |
2386 | homConVar {con = fn (_, c, ts) => con (c, ts), | |
2387 | expandOpaque = expandOpaque, | |
2388 | var = fn (_, a) => var a} | |
2389 | ||
2390 | fun deRecord t = | |
2391 | let | |
2392 | val {hom, destroy} = | |
2393 | simpleHom | |
2394 | {con = fn (t, _, _) => (t, NONE), | |
2395 | expandOpaque = false, | |
2396 | record = fn (t, fs) => (t, | |
2397 | SOME (Vector.map (fs, fn (f, (t, _)) => | |
2398 | (f, t)))), | |
2399 | replaceSynonyms = true, | |
2400 | var = fn (t, _) => (t, NONE)} | |
2401 | val res = | |
2402 | case #2 (hom t) of | |
2403 | NONE => Error.bug "TypeEnv.Type.deRecord" | |
2404 | | SOME fs => fs | |
2405 | val _ = destroy () | |
2406 | in | |
2407 | res | |
2408 | end | |
2409 | ||
2410 | fun deTupleOpt t = | |
2411 | let | |
2412 | val {destroy, hom} = | |
2413 | homConVar | |
2414 | {con = fn (t, c, ts) => (t, | |
2415 | if Tycon.equals (c, Tycon.tuple) | |
2416 | then SOME (Vector.map (ts, #1)) | |
2417 | else NONE), | |
2418 | expandOpaque = false, | |
2419 | var = fn (t, _) => (t, NONE)} | |
2420 | val res = #2 (hom t) | |
2421 | val _ = destroy () | |
2422 | in | |
2423 | res | |
2424 | end | |
2425 | ||
2426 | val deTupleOpt = | |
2427 | Trace.trace ("TypeEnv.Type.deTupleOpt", layout, | |
2428 | Option.layout (Vector.layout layout)) | |
2429 | deTupleOpt | |
2430 | ||
2431 | fun hom (t, {con, expandOpaque = e, record, replaceSynonyms = r, | |
2432 | var}) = | |
2433 | let | |
2434 | val {hom, destroy} = | |
2435 | simpleHom {con = fn (_, c, v) => con (c, v), | |
2436 | expandOpaque = e, | |
2437 | record = fn (_, fs) => record (Srecord.fromVector fs), | |
2438 | replaceSynonyms = r, | |
2439 | var = fn (_, a) => var a} | |
2440 | val res = hom t | |
2441 | val _ = destroy () | |
2442 | in | |
2443 | res | |
2444 | end | |
2445 | ||
2446 | fun copy t = | |
2447 | hom (t, {con = Type.con, | |
2448 | expandOpaque = false, | |
2449 | record = Type.record, | |
2450 | replaceSynonyms = false, | |
2451 | var = Type.var}) | |
2452 | ||
2453 | val unify = | |
2454 | fn (t1, t2, {error, layoutPretty, layoutPrettyTycon, layoutPrettyTyvar}) => | |
2455 | case unify (t1, t2, {layoutPretty = layoutPretty, | |
2456 | layoutPrettyTycon = layoutPrettyTycon, | |
2457 | layoutPrettyTyvar = layoutPrettyTyvar}) of | |
2458 | NotUnifiable (l1, l2, extra) => error (l1, l2, extra) | |
2459 | | Unified () => () | |
2460 | ||
2461 | val checkTime = | |
2462 | fn (t, bound, {layoutPrettyTycon, layoutPrettyTyvar}) => | |
2463 | let | |
2464 | val {checkTime, finishCheckTime} = | |
2465 | makeCheckTime {layoutPrettyTycon = layoutPrettyTycon, | |
2466 | layoutPrettyTyvar = layoutPrettyTyvar} | |
2467 | in | |
2468 | Option.map | |
2469 | (checkTime (t, bound), fn ((l, _), (ty, _)) => | |
2470 | (l, ty, let val {tycons, tyvars, ...} = finishCheckTime () | |
2471 | in {tycons = tycons, tyvars = tyvars} | |
2472 | end)) | |
2473 | end | |
2474 | end | |
2475 | ||
2476 | end |