Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Copyright (C) 2009,2015,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 Interface (S: INTERFACE_STRUCTS): INTERFACE = | |
11 | struct | |
12 | ||
13 | open S | |
14 | ||
15 | local | |
16 | open Layout | |
17 | in | |
18 | val align = align | |
19 | val empty = empty | |
20 | val seq = seq | |
21 | val str = str | |
22 | val bracket = fn l => | |
23 | seq [str "[", l, str "]"] | |
24 | end | |
25 | ||
26 | local | |
27 | open Ast | |
28 | in | |
29 | structure Longstrid = Longstrid | |
30 | structure Longtycon = Longtycon | |
31 | structure Record = SortedRecord | |
32 | structure Strid = Strid | |
33 | structure Vid = Vid | |
34 | end | |
35 | ||
36 | structure Etycon = EnvTycon | |
37 | structure EtypeStr = EnvTypeStr | |
38 | ||
39 | structure Set = DisjointSet | |
40 | ||
41 | structure Status: | |
42 | sig | |
43 | datatype t = Con | Exn | Var | |
44 | ||
45 | val layout: t -> Layout.t | |
46 | val toString: t -> string | |
47 | end = | |
48 | struct | |
49 | datatype t = Con | Exn | Var | |
50 | ||
51 | val toString = | |
52 | fn Con => "Con" | |
53 | | Exn => "Exn" | |
54 | | Var => "Var" | |
55 | ||
56 | val layout = Layout.str o toString | |
57 | end | |
58 | ||
59 | (* only needed for debugging *) | |
60 | structure TyconId = IntUniqueId () | |
61 | ||
62 | structure Defn = | |
63 | struct | |
64 | type t = exn | |
65 | ||
66 | val layoutRef: (t -> Layout.t) ref = ref (fn _ => Layout.empty) | |
67 | fun layout d = (!layoutRef) d | |
68 | end | |
69 | ||
70 | structure Time:> | |
71 | sig | |
72 | type t | |
73 | ||
74 | val < : t * t -> bool | |
75 | val current: unit -> t | |
76 | val layout: t -> Layout.t | |
77 | val min: t * t -> t | |
78 | val tick: unit -> t | |
79 | end = | |
80 | struct | |
81 | type t = int | |
82 | ||
83 | val op < = Int.< | |
84 | ||
85 | val layout = Int.layout | |
86 | ||
87 | val min = Int.min | |
88 | ||
89 | val currentTime: int ref = ref 0 | |
90 | ||
91 | fun current () = !currentTime | |
92 | ||
93 | fun tick () = | |
94 | let | |
95 | val n = 1 + !currentTime | |
96 | val _ = currentTime := n | |
97 | in | |
98 | n | |
99 | end | |
100 | end | |
101 | ||
102 | structure FlexibleTycon = | |
103 | struct | |
104 | (* hasCons is true if this tycon occurs in any type structure where the | |
105 | * cons are nonempty. This allows us to do a quick check of the side | |
106 | * condition on rule 64 that requires all type structures to be well-formed | |
107 | * when implementing "where type". | |
108 | *) | |
109 | datatype t = T of {admitsEquality: AdmitsEquality.t ref, | |
110 | copy: copy, | |
111 | creationTime: Time.t, | |
112 | defn: exn ref, | |
113 | hasCons: bool, | |
114 | id: TyconId.t, | |
115 | kind: Kind.t, | |
116 | plist: PropertyList.t, | |
117 | prettyDefault: string, | |
118 | specs: Region.t AppendList.t ref} Set.t | |
119 | withtype copy = t option ref | |
120 | ||
121 | fun fields (T s) = Set.! s | |
122 | ||
123 | local | |
124 | fun make f = f o fields | |
125 | in | |
126 | val admitsEquality = ! o make #admitsEquality | |
127 | val defnRef = make #defn | |
128 | val defn = ! o defnRef | |
129 | val hasCons = make #hasCons | |
130 | val kind = make #kind | |
131 | val plist = make #plist | |
132 | val prettyDefault = make #prettyDefault | |
133 | fun setAdmitsEquality (f, ae) = | |
134 | (make #admitsEquality f) := ae | |
135 | val specsRef = make #specs | |
136 | val specs = ! o specsRef | |
137 | end | |
138 | val layoutPrettyDefault = Layout.str o prettyDefault | |
139 | ||
140 | fun dest fc = | |
141 | let | |
142 | val {admitsEquality, hasCons, kind, prettyDefault, ...} = | |
143 | fields fc | |
144 | in | |
145 | {admitsEquality = !admitsEquality, | |
146 | hasCons = hasCons, | |
147 | kind = kind, | |
148 | prettyDefault = prettyDefault} | |
149 | end | |
150 | ||
151 | val equals = fn (T s, T s') => Set.equals (s, s') | |
152 | ||
153 | fun layout fc = | |
154 | let | |
155 | open Layout | |
156 | val {admitsEquality, creationTime, defn, hasCons, id, kind, prettyDefault, ...} = fields fc | |
157 | in | |
158 | record [("admitsEquality", AdmitsEquality.layout (!admitsEquality)), | |
159 | ("creationTime", Time.layout creationTime), | |
160 | ("defn", Defn.layout (!defn)), | |
161 | ("hasCons", Bool.layout hasCons), | |
162 | ("id", TyconId.layout id), | |
163 | ("kind", Kind.layout kind), | |
164 | ("prettyDefault", String.layout prettyDefault)] | |
165 | end | |
166 | ||
167 | val copies: copy list ref = ref [] | |
168 | ||
169 | fun make {admitsEquality: AdmitsEquality.t, defn: Defn.t, | |
170 | hasCons: bool, kind: Kind.t, prettyDefault: string, | |
171 | specs: Region.t AppendList.t}: t = | |
172 | T (Set.singleton {admitsEquality = ref admitsEquality, | |
173 | copy = ref NONE, | |
174 | creationTime = Time.current (), | |
175 | defn = ref defn, | |
176 | hasCons = hasCons, | |
177 | id = TyconId.new (), | |
178 | kind = kind, | |
179 | plist = PropertyList.new (), | |
180 | prettyDefault = prettyDefault, | |
181 | specs = ref specs}) | |
182 | ||
183 | fun pushSpec (fc, region) = | |
184 | let | |
185 | val specsRef = specsRef fc | |
186 | in | |
187 | specsRef := AppendList.snoc (!specsRef, region) | |
188 | end | |
189 | end | |
190 | ||
191 | structure Tycon = | |
192 | struct | |
193 | datatype t = | |
194 | Flexible of FlexibleTycon.t | |
195 | | Rigid of Etycon.t | |
196 | ||
197 | val fromEnv: Etycon.t -> t = Rigid | |
198 | ||
199 | fun admitsEquality c = | |
200 | case c of | |
201 | Flexible f => FlexibleTycon.admitsEquality f | |
202 | | Rigid c => Etycon.admitsEquality c | |
203 | ||
204 | val arrow = fromEnv Etycon.arrow | |
205 | ||
206 | val equals = | |
207 | fn (Flexible f, Flexible f') => FlexibleTycon.equals (f, f') | |
208 | | (Rigid c, Rigid c') => Etycon.equals (c, c') | |
209 | | _ => false | |
210 | ||
211 | val exn = Rigid Etycon.exn | |
212 | ||
213 | val kind = | |
214 | fn Flexible f => FlexibleTycon.kind f | |
215 | | Rigid c => Etycon.kind c | |
216 | ||
217 | val layout = | |
218 | fn Flexible f => FlexibleTycon.layout f | |
219 | | Rigid c => Etycon.layout c | |
220 | ||
221 | val tuple = Rigid Etycon.tuple | |
222 | ||
223 | fun layoutAppPretty (c, ts, {layoutPrettyEnvTycon, layoutPrettyFlexTycon}) = | |
224 | case c of | |
225 | Flexible f => | |
226 | EnvTycon.layoutAppPrettyNormal | |
227 | (layoutPrettyFlexTycon f, ts) | |
228 | | Rigid c => | |
229 | EnvTycon.layoutAppPretty | |
230 | (c, ts, {layoutPretty = layoutPrettyEnvTycon}) | |
231 | end | |
232 | ||
233 | structure Type = | |
234 | struct | |
235 | datatype t = | |
236 | Con of Tycon.t * t vector | |
237 | | Record of t Record.t | |
238 | | Var of Tyvar.t | |
239 | ||
240 | fun arrow (t1, t2) = Con (Tycon.arrow, Vector.new2 (t1, t2)) | |
241 | ||
242 | val con = Con | |
243 | ||
244 | fun deArrowOpt (t: t): (t * t) option = | |
245 | case t of | |
246 | Con (c, ts) => | |
247 | if Tycon.equals (c, Tycon.arrow) | |
248 | then SOME (Vector.sub (ts, 0), Vector.sub (ts, 1)) | |
249 | else NONE | |
250 | | _ => NONE | |
251 | ||
252 | fun deArrow t = | |
253 | case deArrowOpt t of | |
254 | NONE => Error.bug "Interface.Type.deArrow" | |
255 | | SOME z => z | |
256 | ||
257 | fun deEta (t: t, tyvars: Tyvar.t vector): Tycon.t option = | |
258 | case t of | |
259 | Con (c, ts) => | |
260 | if Vector.length ts = Vector.length tyvars | |
261 | andalso Vector.foralli (ts, fn (i, t) => | |
262 | case t of | |
263 | Var a => | |
264 | Tyvar.equals | |
265 | (a, Vector.sub (tyvars, i)) | |
266 | | _ => false) | |
267 | then SOME c | |
268 | else NONE | |
269 | | _ => NONE | |
270 | ||
271 | val exn = Con (Tycon.exn, Vector.new0 ()) | |
272 | ||
273 | fun hom (t, {con, record, var}) = | |
274 | let | |
275 | val rec loop = | |
276 | fn Con (c, ts) => con (c, Vector.map (ts, loop)) | |
277 | | Record r => record (Record.map (r, loop)) | |
278 | | Var a => var a | |
279 | in | |
280 | loop t | |
281 | end | |
282 | ||
283 | local | |
284 | open Layout | |
285 | in | |
286 | fun layout t = | |
287 | case t of | |
288 | Con (c, ts) => | |
289 | paren (align [seq [str "Con ", Tycon.layout c], | |
290 | Vector.layout layout ts]) | |
291 | | Record r => | |
292 | Record.layout {record = r, | |
293 | separator = ": ", | |
294 | extra = "", | |
295 | layoutTuple = Vector.layout layout, | |
296 | layoutElt = layout} | |
297 | | Var a => paren (seq [str "Var ", Tyvar.layout a]) | |
298 | end | |
299 | ||
300 | val record = Record | |
301 | ||
302 | fun substitute (t: t, sub: (Tyvar.t * t) vector): t = | |
303 | let | |
304 | fun var a = | |
305 | case Vector.peek (sub, fn (a', _) => Tyvar.equals (a, a')) of | |
306 | NONE => Error.bug "Interface.Type.substitute" | |
307 | | SOME (_, t) => t | |
308 | in | |
309 | hom (t, {con = Con, | |
310 | record = Record, | |
311 | var = var}) | |
312 | end | |
313 | ||
314 | val var = Var | |
315 | end | |
316 | ||
317 | structure Scheme = GenericScheme (structure Type = Type | |
318 | structure Tyvar = Tyvar) | |
319 | ||
320 | structure Scheme = | |
321 | struct | |
322 | open Scheme | |
323 | ||
324 | fun kind (T {tyvars, ...}) = | |
325 | Kind.Arity (Vector.length tyvars) | |
326 | ||
327 | fun make (tyvars, ty) = T {ty = ty, tyvars = tyvars} | |
328 | ||
329 | fun fromTycon tycon = | |
330 | let | |
331 | val kind = Tycon.kind tycon | |
332 | val arity = | |
333 | case kind of | |
334 | Kind.Arity arity => arity | |
335 | | Kind.Nary => Error.bug "Interface.Scheme.fromTycon: Kind.Nary" | |
336 | val tyvars = | |
337 | Vector.tabulate | |
338 | (arity, fn _ => | |
339 | Tyvar.makeNoname {equality = false}) | |
340 | in | |
341 | make (tyvars, Type.con (tycon, Vector.map (tyvars, Type.var))) | |
342 | end | |
343 | end | |
344 | ||
345 | structure Cons : | |
346 | sig | |
347 | type t | |
348 | val dest: t -> {name: Ast.Con.t, | |
349 | scheme: Scheme.t} vector | |
350 | val empty: t | |
351 | val fromSortedVector: {name: Ast.Con.t, | |
352 | scheme: Scheme.t} vector -> t | |
353 | val fromVector: {name: Ast.Con.t, | |
354 | scheme: Scheme.t} vector -> t | |
355 | val layout: t -> Layout.t | |
356 | val map: t * ({name: Ast.Con.t, | |
357 | scheme: Scheme.t} | |
358 | -> {scheme: Scheme.t}) -> t | |
359 | end = | |
360 | struct | |
361 | datatype t = T of {name: Ast.Con.t, | |
362 | scheme: Scheme.t} vector | |
363 | ||
364 | fun dest (T v) = v | |
365 | ||
366 | val fromSortedVector = T | |
367 | ||
368 | fun fromVector v = | |
369 | (fromSortedVector o QuickSort.sortVector) | |
370 | (v, fn ({name = name1, ...}, {name = name2, ...}) => | |
371 | case Ast.Con.compare (name1, name2) of | |
372 | LESS => true | |
373 | | EQUAL => true | |
374 | | GREATER => false) | |
375 | ||
376 | val empty = T (Vector.new0 ()) | |
377 | ||
378 | fun map (T v, f) = | |
379 | (T o Vector.map) | |
380 | (v, fn elt as {name, ...} => | |
381 | let | |
382 | val {scheme} = | |
383 | f elt | |
384 | in | |
385 | {name = name, | |
386 | scheme = scheme} | |
387 | end) | |
388 | ||
389 | fun layout (T v) = | |
390 | Vector.layout (fn {name, scheme} => | |
391 | let | |
392 | open Layout | |
393 | in | |
394 | seq [Ast.Con.layout name, | |
395 | str ": ", | |
396 | Scheme.layout scheme] | |
397 | end) | |
398 | v | |
399 | end | |
400 | ||
401 | structure TypeStr = | |
402 | struct | |
403 | datatype node = | |
404 | Datatype of {tycon: Tycon.t, | |
405 | cons: Cons.t, | |
406 | repl: bool} | |
407 | | Scheme of Scheme.t | |
408 | | Tycon of {eq: bool, | |
409 | tycon: Tycon.t} | |
410 | type t = node | |
411 | ||
412 | val node = fn s => s | |
413 | ||
414 | fun kind s = | |
415 | case node s of | |
416 | Datatype {tycon, ...} => Tycon.kind tycon | |
417 | | Scheme s => Scheme.kind s | |
418 | | Tycon {tycon, ...} => Tycon.kind tycon | |
419 | ||
420 | fun layout t = | |
421 | let | |
422 | open Layout | |
423 | in | |
424 | case node t of | |
425 | Datatype {tycon, cons, repl} => | |
426 | seq [str "Datatype ", | |
427 | record [("tycon", Tycon.layout tycon), | |
428 | ("cons", Cons.layout cons), | |
429 | ("repl", Bool.layout repl)]] | |
430 | | Scheme s => Scheme.layout s | |
431 | | Tycon {eq, tycon} => | |
432 | seq [str "Tycon ", | |
433 | record [("eq", Bool.layout eq), | |
434 | ("tycon", Tycon.layout tycon)]] | |
435 | end | |
436 | ||
437 | fun apply (t: t, tys: Type.t vector): Type.t = | |
438 | case node t of | |
439 | Datatype {tycon, ...} => Type.con (tycon, tys) | |
440 | | Scheme s => Scheme.apply (s, tys) | |
441 | | Tycon {tycon, ...} => Type.con (tycon, tys) | |
442 | ||
443 | val apply = | |
444 | Trace.trace ("Interface.TypeStr.apply", Layout.tuple2 (layout, Vector.layout Type.layout), Type.layout) | |
445 | apply | |
446 | ||
447 | fun cons t = | |
448 | case node t of | |
449 | Datatype {cons, ...} => cons | |
450 | | _ => Cons.empty | |
451 | ||
452 | fun data (tycon, cons, repl) = | |
453 | Datatype {tycon = tycon, cons = cons, repl = repl} | |
454 | ||
455 | val def = Scheme | |
456 | ||
457 | fun tycon (tycon, eq) = | |
458 | Tycon {eq = eq, tycon = tycon} | |
459 | ||
460 | local | |
461 | fun tyconAsScheme c = | |
462 | def (Scheme.fromTycon c) | |
463 | in | |
464 | fun repl (t: t) = | |
465 | case node t of | |
466 | Datatype {tycon, cons, ...} => data (tycon, cons, true) | |
467 | | Scheme _ => t | |
468 | | Tycon {tycon, ...} => tyconAsScheme tycon | |
469 | ||
470 | fun abs (t: t) = | |
471 | case node t of | |
472 | Datatype {tycon, ...} => tyconAsScheme tycon | |
473 | | Scheme _ => t | |
474 | | Tycon {tycon, ...} => tyconAsScheme tycon | |
475 | end | |
476 | end | |
477 | ||
478 | structure Defn = | |
479 | struct | |
480 | open Defn | |
481 | ||
482 | datatype dest = | |
483 | Realized of EtypeStr.t | |
484 | | TypeStr of TypeStr.t | |
485 | | Undefined | |
486 | ||
487 | exception U of dest | |
488 | ||
489 | val realized = U o Realized | |
490 | val typeStr = U o TypeStr | |
491 | val undefined = U Undefined | |
492 | ||
493 | fun dest (d: t): dest = | |
494 | case d of | |
495 | U u => u | |
496 | | _ => Error.bug "Interface.Defn.dest" | |
497 | ||
498 | val () = | |
499 | layoutRef := | |
500 | (fn d => | |
501 | let | |
502 | open Layout | |
503 | in | |
504 | case dest d of | |
505 | Realized s => seq [str "Realized ", EtypeStr.layout s] | |
506 | | TypeStr s => seq [str "TypeStr ", TypeStr.layout s] | |
507 | | Undefined => str "Undefined" | |
508 | end) | |
509 | end | |
510 | ||
511 | (* expandTy expands all type definitions in ty *) | |
512 | local | |
513 | fun con (c, ts) = | |
514 | case c of | |
515 | Tycon.Flexible f => | |
516 | (case Defn.dest (FlexibleTycon.defn f) of | |
517 | Defn.Realized _ => Error.bug "Interface.expandTy: Realized" | |
518 | | Defn.TypeStr s => expandTy (TypeStr.apply (s, ts)) | |
519 | | Defn.Undefined => Type.Con (c, ts)) | |
520 | | Tycon.Rigid _ => Type.Con (c, ts) | |
521 | and expandTy (ty: Type.t): Type.t = | |
522 | Type.hom (ty, {con = con, | |
523 | record = Type.Record, | |
524 | var = Type.Var}) | |
525 | in | |
526 | val expandTy = expandTy | |
527 | end | |
528 | ||
529 | structure Type = | |
530 | struct | |
531 | open Type | |
532 | ||
533 | fun layoutPretty (ty, {expand, layoutPrettyEnvTycon, layoutPrettyFlexTycon, layoutPrettyTyvar}) = | |
534 | let | |
535 | fun con (c, ts) = | |
536 | Tycon.layoutAppPretty | |
537 | (c, ts, {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
538 | layoutPrettyFlexTycon = layoutPrettyFlexTycon}) | |
539 | fun record r = | |
540 | case Record.detupleOpt r of | |
541 | NONE => | |
542 | (LayoutPretty.simple o seq) | |
543 | [str "{", | |
544 | Layout.mayAlign | |
545 | (Layout.separateRight | |
546 | (Vector.toListMap | |
547 | (Record.toVector r, fn (f, (t, _)) => | |
548 | seq [Record.Field.layout f, str ": ", t]), | |
549 | ",")), | |
550 | str "}"] | |
551 | | SOME ts => con (Tycon.tuple, ts) | |
552 | fun var a = LayoutPretty.simple (layoutPrettyTyvar a) | |
553 | val ty = if expand then expandTy ty else ty | |
554 | in | |
555 | Type.hom (ty, {con = con, | |
556 | record = record, | |
557 | var = var}) | |
558 | end | |
559 | ||
560 | fun explainDoesNotAdmitEquality (ty, {layoutPrettyEnvTycon, layoutPrettyFlexTycon}) = | |
561 | let | |
562 | val layoutAppPretty = fn (c, ls) => | |
563 | Tycon.layoutAppPretty | |
564 | (c, ls, | |
565 | {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
566 | layoutPrettyFlexTycon = layoutPrettyFlexTycon}) | |
567 | val bracket = LayoutPretty.bracket | |
568 | val dontCare = LayoutPretty.dontCare | |
569 | fun getLay lo = Option.fold (lo, dontCare, #1) | |
570 | fun con (c, los) = | |
571 | case Tycon.admitsEquality c of | |
572 | AdmitsEquality.Always => NONE | |
573 | | AdmitsEquality.Sometimes => | |
574 | if Vector.forall (los, Option.isNone) | |
575 | then NONE | |
576 | else (SOME o layoutAppPretty) | |
577 | (c, Vector.map (los, getLay)) | |
578 | | AdmitsEquality.Never => | |
579 | (SOME o bracket o layoutAppPretty) | |
580 | (c, Vector.map (los, fn _ => dontCare)) | |
581 | fun record r = | |
582 | case Record.detupleOpt r of | |
583 | NONE => | |
584 | let | |
585 | val v = Record.toVector r | |
586 | val (fls, extra) = | |
587 | Vector.fold | |
588 | (v, ([], false), fn ((f, lo), (fls, extra)) => | |
589 | case lo of | |
590 | NONE => (fls, true) | |
591 | | SOME l => ((f,l)::fls, extra)) | |
592 | in | |
593 | if List.isEmpty fls | |
594 | then NONE | |
595 | else (SOME o LayoutPretty.simple o seq) | |
596 | [str "{", | |
597 | Layout.mayAlign | |
598 | (Layout.separateRight | |
599 | (List.revMap | |
600 | (fls, fn (f, (l, _)) => | |
601 | seq [Record.Field.layout f, | |
602 | str ": ", l]), | |
603 | ",")), | |
604 | if extra | |
605 | then str ", ...}" | |
606 | else str "}"] | |
607 | end | |
608 | | SOME los => con (Tycon.tuple, los) | |
609 | fun var _ = NONE | |
610 | val ty = expandTy ty | |
611 | val res = Type.hom (ty, {con = con, | |
612 | record = record, | |
613 | var = var}) | |
614 | in | |
615 | Option.map (res, #1) | |
616 | end | |
617 | end | |
618 | ||
619 | structure TypeStr = | |
620 | struct | |
621 | open TypeStr | |
622 | ||
623 | fun toTyconOpt (s, {expand}) = | |
624 | let | |
625 | val s = if expand then abs s else s | |
626 | in | |
627 | case node s of | |
628 | Datatype {tycon, ...} => SOME tycon | |
629 | | Scheme s => | |
630 | let | |
631 | val Scheme.T {tyvars, ty} = s | |
632 | val ty = if expand then expandTy ty else ty | |
633 | in | |
634 | case Type.deEta (ty, tyvars) of | |
635 | NONE => NONE | |
636 | | SOME c => | |
637 | if Tycon.equals (c, Tycon.arrow) | |
638 | orelse Tycon.equals (c, Tycon.tuple) | |
639 | then NONE | |
640 | else SOME c | |
641 | end | |
642 | | Tycon {tycon, ...} => SOME tycon | |
643 | end | |
644 | end | |
645 | ||
646 | fun copyCons cons: Cons.t = | |
647 | Cons.map (cons, fn {scheme, ...} => | |
648 | {scheme = copyScheme scheme}) | |
649 | and copyDefn (d: Defn.t): Defn.t = | |
650 | let | |
651 | open Defn | |
652 | in | |
653 | case dest d of | |
654 | Realized _ => | |
655 | (* This will never happen in a type-correct program, but it may | |
656 | * in a type-incorrect one. So, we return d to avoid terminating | |
657 | * MLton. | |
658 | *) | |
659 | d | |
660 | | TypeStr s => Defn.typeStr (copyTypeStr s) | |
661 | | Undefined => Defn.undefined | |
662 | end | |
663 | and copyFlexibleTycon (fc: FlexibleTycon.t): FlexibleTycon.t = | |
664 | let | |
665 | open FlexibleTycon | |
666 | val {admitsEquality, copy, defn, hasCons, | |
667 | kind, prettyDefault, specs, ...} = | |
668 | fields fc | |
669 | in | |
670 | case !copy of | |
671 | NONE => | |
672 | let | |
673 | val fc' = make {admitsEquality = !admitsEquality, | |
674 | defn = copyDefn (!defn), | |
675 | hasCons = hasCons, | |
676 | kind = kind, | |
677 | prettyDefault = prettyDefault, | |
678 | specs = !specs} | |
679 | val _ = List.push (copies, copy) | |
680 | val _ = copy := SOME fc' | |
681 | in | |
682 | fc' | |
683 | end | |
684 | | SOME fc' => fc' | |
685 | end | |
686 | and copyTycon (t: Tycon.t): Tycon.t = | |
687 | let | |
688 | open Tycon | |
689 | in | |
690 | case t of | |
691 | Flexible c => Flexible (copyFlexibleTycon c) | |
692 | | Rigid _ => t | |
693 | end | |
694 | and copyType (t: Type.t): Type.t = | |
695 | let | |
696 | open Type | |
697 | in | |
698 | hom (t, {con = fn (c, ts) => Con (copyTycon c, ts), | |
699 | record = Record, | |
700 | var = Var}) | |
701 | end | |
702 | and copyScheme (Scheme.T {tyvars, ty}): Scheme.t = | |
703 | Scheme.T {ty = copyType ty, tyvars = tyvars} | |
704 | and copyTypeStr (s: TypeStr.t): TypeStr.t = | |
705 | let | |
706 | open TypeStr | |
707 | in | |
708 | case node s of | |
709 | Datatype {cons, tycon, repl} => data (copyTycon tycon, copyCons cons, repl) | |
710 | | Scheme s => def (copyScheme s) | |
711 | | Tycon {eq, tycon = c} => tycon (copyTycon c, eq) | |
712 | end | |
713 | ||
714 | structure AdmitsEquality = | |
715 | struct | |
716 | open AdmitsEquality | |
717 | ||
718 | fun fromBool b = if b then Sometimes else Never | |
719 | end | |
720 | ||
721 | fun flexibleTyconAdmitsEquality (fc: FlexibleTycon.t): AdmitsEquality.t = | |
722 | let | |
723 | val {admitsEquality, defn, ...} = FlexibleTycon.fields fc | |
724 | datatype z = datatype Defn.dest | |
725 | in | |
726 | case Defn.dest (!defn) of | |
727 | Realized _ => !admitsEquality | |
728 | | TypeStr s => typeStrAdmitsEquality s | |
729 | | Undefined => !admitsEquality | |
730 | end | |
731 | and schemeAdmitsEquality (s: Scheme.t): bool = | |
732 | let | |
733 | fun con (c, bs) = | |
734 | let | |
735 | datatype z = datatype AdmitsEquality.t | |
736 | in | |
737 | case Tycon.admitsEquality c of | |
738 | Always => true | |
739 | | Never => false | |
740 | | Sometimes => Vector.forall (bs, fn b => b) | |
741 | end | |
742 | in | |
743 | Type.hom (expandTy (Scheme.ty s), | |
744 | {con = con, | |
745 | record = fn r => Record.forall (r, fn b => b), | |
746 | var = fn _ => true}) | |
747 | end | |
748 | and tyconAdmitsEquality (t: Tycon.t): AdmitsEquality.t = | |
749 | let | |
750 | datatype z = datatype Tycon.t | |
751 | in | |
752 | case t of | |
753 | Flexible c => flexibleTyconAdmitsEquality c | |
754 | | Rigid e => Etycon.admitsEquality e | |
755 | end | |
756 | and typeStrAdmitsEquality (s: TypeStr.t): AdmitsEquality.t = | |
757 | let | |
758 | datatype z = datatype TypeStr.node | |
759 | in | |
760 | case TypeStr.node s of | |
761 | Datatype {tycon = c, ...} => tyconAdmitsEquality c | |
762 | | Scheme s => AdmitsEquality.fromBool (schemeAdmitsEquality s) | |
763 | | Tycon {tycon = c, ...} => tyconAdmitsEquality c | |
764 | end | |
765 | ||
766 | structure FlexibleTycon = | |
767 | struct | |
768 | open FlexibleTycon | |
769 | ||
770 | fun new {admitsEquality: AdmitsEquality.t, | |
771 | hasCons: bool, kind: Kind.t, | |
772 | prettyDefault: string, | |
773 | region: Region.t}: t = | |
774 | make {admitsEquality = admitsEquality, | |
775 | defn = Defn.undefined, | |
776 | hasCons = hasCons, | |
777 | kind = kind, | |
778 | prettyDefault = prettyDefault, | |
779 | specs = AppendList.single region} | |
780 | ||
781 | fun realize (fc, typeStr) = | |
782 | let | |
783 | val defn = defnRef fc | |
784 | in | |
785 | case Defn.dest (!defn) of | |
786 | Defn.Undefined => defn := Defn.realized typeStr | |
787 | | _ => Error.bug "Interface.FlexibleTycon.realize" | |
788 | end | |
789 | ||
790 | fun share (fc1 as T s1, fc2 as T s2, sharingSpec) = | |
791 | let | |
792 | val {admitsEquality = ae1, creationTime = t1, | |
793 | hasCons = hc1, specs = ss1, | |
794 | id, kind, plist, prettyDefault, ...} = | |
795 | fields fc1 | |
796 | val {admitsEquality = ae2, creationTime = t2, | |
797 | hasCons = hc2, specs = ss2, ...} = | |
798 | fields fc2 | |
799 | val _ = Set.union (s1, s2) | |
800 | val specs = | |
801 | AppendList.snoc | |
802 | (if Ref.equals (ss1, ss2) | |
803 | then !ss1 | |
804 | else AppendList.append (!ss1, !ss2), | |
805 | sharingSpec) | |
806 | val _ = | |
807 | Set.:= | |
808 | (s1, {admitsEquality = ref (AdmitsEquality.or (!ae1, !ae2)), | |
809 | copy = ref NONE, | |
810 | creationTime = Time.min (t1, t2), | |
811 | defn = ref Defn.undefined, | |
812 | specs = ref specs, | |
813 | hasCons = hc1 orelse hc2, | |
814 | id = id, | |
815 | kind = kind, | |
816 | plist = plist, | |
817 | prettyDefault = prettyDefault}) | |
818 | in | |
819 | () | |
820 | end | |
821 | ||
822 | type typeStr = TypeStr.t | |
823 | ||
824 | datatype realization = | |
825 | ETypeStr of EnvTypeStr.t | |
826 | | TypeStr of typeStr | |
827 | ||
828 | fun realization (f: t): realization option = | |
829 | case Defn.dest (defn f) of | |
830 | Defn.Realized s => SOME (ETypeStr s) | |
831 | | Defn.TypeStr s => SOME (TypeStr s) | |
832 | | Defn.Undefined => NONE | |
833 | end | |
834 | ||
835 | structure Scheme = | |
836 | struct | |
837 | open Scheme | |
838 | ||
839 | val admitsEquality = schemeAdmitsEquality | |
840 | ||
841 | val copy = copyScheme | |
842 | end | |
843 | ||
844 | structure TypeStr = | |
845 | struct | |
846 | open TypeStr | |
847 | ||
848 | val admitsEquality = typeStrAdmitsEquality | |
849 | ||
850 | val copy = copyTypeStr | |
851 | ||
852 | fun specs (s, first) = | |
853 | let | |
854 | fun loop s = | |
855 | case toTyconOpt (s, {expand = false}) of | |
856 | NONE => AppendList.empty | |
857 | | SOME c => loopTycon c | |
858 | and loopTycon c = | |
859 | case c of | |
860 | Tycon.Flexible fc => | |
861 | AppendList.append | |
862 | (FlexibleTycon.specs fc, | |
863 | case Defn.dest (FlexibleTycon.defn fc) of | |
864 | Defn.Realized _ => AppendList.empty | |
865 | | Defn.TypeStr s => loop s | |
866 | | Defn.Undefined => AppendList.empty) | |
867 | | Tycon.Rigid _ => AppendList.empty | |
868 | in | |
869 | first :: | |
870 | (List.rev o AppendList.fold) | |
871 | (loop s, [], fn (r, rs) => | |
872 | if List.contains (first::rs, r, Region.equals) | |
873 | then rs | |
874 | else r :: rs) | |
875 | end | |
876 | ||
877 | fun pushSpec (s, region) = | |
878 | case TypeStr.toTyconOpt (s, {expand = false}) of | |
879 | NONE => () | |
880 | | SOME (Tycon.Flexible flex) => | |
881 | FlexibleTycon.pushSpec (flex, region) | |
882 | | SOME (Tycon.Rigid _) => () | |
883 | ||
884 | fun getFlex {layoutPrettyEnvTycon, | |
885 | layoutPrettyFlexTycon, | |
886 | oper: string, | |
887 | time: Time.t, | |
888 | ty = {name: unit -> Layout.t, | |
889 | region: Region.t, | |
890 | spec: Region.t, | |
891 | tyStr: t}}: FlexibleTycon.t option = | |
892 | let | |
893 | fun error what = | |
894 | let | |
895 | val isEmpty = Layout.isEmpty | |
896 | val tuple = Layout.tuple | |
897 | val {layoutPretty = layoutPrettyTyvar, | |
898 | localInit = localInitLayoutPrettyTyvar, ...} = | |
899 | Tyvar.makeLayoutPretty () | |
900 | val arity = | |
901 | case kind tyStr of | |
902 | Kind.Arity arity => arity | |
903 | | _ => Error.bug "Interface.TypeStr.getFlex: Kind.Nary" | |
904 | val tyvars = | |
905 | Vector.tabulate | |
906 | (arity, fn _ => | |
907 | Tyvar.makeNoname {equality = false}) | |
908 | val () = localInitLayoutPrettyTyvar tyvars | |
909 | val tyargs = Vector.map (tyvars, Type.var) | |
910 | val tyvars = Vector.map (tyvars, layoutPrettyTyvar) | |
911 | val tyvars = | |
912 | case Vector.length tyvars of | |
913 | 0 => empty | |
914 | | 1 => Vector.first tyvars | |
915 | | _ => tuple (Vector.toList tyvars) | |
916 | val (kw, mkRest) = | |
917 | case TypeStr.node tyStr of | |
918 | TypeStr.Datatype _ => | |
919 | ("datatype", fn l => | |
920 | seq [str "... (* = datatype ", l, str " *)"]) | |
921 | | TypeStr.Scheme _ => | |
922 | ("type", fn l => l) | |
923 | | TypeStr.Tycon _ => | |
924 | ("type", fn l => l) | |
925 | val defn = TypeStr.apply (tyStr, tyargs) | |
926 | val () = | |
927 | Control.error | |
928 | (region, | |
929 | seq [str "type cannot be ", str oper, | |
930 | str " (", str what, str "): ", | |
931 | name ()], | |
932 | align | |
933 | ((seq [str "type spec: ", | |
934 | str kw, str " ", | |
935 | tyvars, | |
936 | if isEmpty tyvars then empty else str " ", | |
937 | name (), str " = ", | |
938 | mkRest ((#1 o Type.layoutPretty) | |
939 | (defn, {expand = true, | |
940 | layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
941 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
942 | layoutPrettyTyvar = layoutPrettyTyvar}))]):: | |
943 | (List.map | |
944 | (specs (tyStr, spec), fn r => | |
945 | seq [str "spec at: ", Region.layout r])))) | |
946 | in | |
947 | NONE | |
948 | end | |
949 | in | |
950 | case toTyconOpt (tyStr, {expand = true}) of | |
951 | NONE => error "defined" | |
952 | | SOME c => | |
953 | (case c of | |
954 | Tycon.Flexible c => | |
955 | let | |
956 | val {creationTime, defn, ...} = FlexibleTycon.fields c | |
957 | in | |
958 | case Defn.dest (!defn) of | |
959 | Defn.Realized _ => | |
960 | Error.bug "Interface.TypeStr.getFlex: Realized" | |
961 | | Defn.TypeStr _ => | |
962 | Error.bug "Interface.TypeStr.getFlex: TypeStr" | |
963 | | Defn.Undefined => | |
964 | if Time.< (creationTime, time) | |
965 | then error "not local" | |
966 | else SOME c | |
967 | end | |
968 | | Tycon.Rigid _ => error "defined") | |
969 | end | |
970 | ||
971 | fun share {layoutPrettyEnvTycon, layoutPrettyFlexTycon, | |
972 | region: Region.t, time: Time.t, | |
973 | ty1 as {name = name1, ...}, | |
974 | ty2 as {name = name2, ...}} = | |
975 | case (getFlex {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
976 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
977 | oper = "shared", time = time, ty = ty1}, | |
978 | getFlex {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
979 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
980 | oper = "shared", time = time, ty = ty2}) of | |
981 | (NONE, _) => () | |
982 | | (_, NONE) => () | |
983 | | (SOME flex1, SOME flex2) => | |
984 | if Kind.equals (FlexibleTycon.kind flex1, FlexibleTycon.kind flex2) | |
985 | then FlexibleTycon.share (flex1, flex2, region) | |
986 | else let | |
987 | fun msg {name, region = _, spec, tyStr} = | |
988 | let | |
989 | val (keyword, rest) = | |
990 | case node tyStr of | |
991 | Datatype _ => ("datatype", str " = ...") | |
992 | | Scheme _ => ("type", str " = ...") | |
993 | | Tycon {eq, ...} => | |
994 | if eq | |
995 | then ("eqtype", empty) | |
996 | else ("type", empty) | |
997 | val arity = | |
998 | case kind tyStr of | |
999 | Kind.Arity arity => arity | |
1000 | | _ => Error.bug "Interface.TypeStr.share.msg: arity" | |
1001 | val tyvars = | |
1002 | Vector.tabulate | |
1003 | (arity, fn _ => | |
1004 | Tyvar.makeNoname {equality = false}) | |
1005 | val {layoutPretty = layoutPrettyTyvar, | |
1006 | localInit = localInitLayoutPrettyTyvar, ...} = | |
1007 | Tyvar.makeLayoutPretty () | |
1008 | val () = localInitLayoutPrettyTyvar tyvars | |
1009 | val tyvars = | |
1010 | case Vector.length tyvars of | |
1011 | 0 => empty | |
1012 | | 1 => layoutPrettyTyvar (Vector.first tyvars) | |
1013 | | _ => Layout.tuple (Vector.toListMap (tyvars, layoutPrettyTyvar)) | |
1014 | in | |
1015 | (seq [str "type spec: ", | |
1016 | str keyword, | |
1017 | str " [", tyvars, str "] ", | |
1018 | name (), | |
1019 | rest]):: | |
1020 | (List.map | |
1021 | (specs (tyStr, spec), fn r => | |
1022 | seq [str "spec at: ", Region.layout r])) | |
1023 | end | |
1024 | in | |
1025 | Control.error | |
1026 | (region, | |
1027 | seq [str "types cannot be shared (arity): ", | |
1028 | name1 (), str ", ", name2 ()], | |
1029 | align ((msg ty1) @ (msg ty2))) | |
1030 | end | |
1031 | ||
1032 | val share = | |
1033 | Trace.trace | |
1034 | ("Interface.TypeStr.share", | |
1035 | fn {time, ty1, ty2, ...} => | |
1036 | Layout.record [("time", Time.layout time), | |
1037 | ("ty1", Layout.record [("tyStr", layout (#tyStr ty1))]), | |
1038 | ("ty2", Layout.record [("tyStr", layout (#tyStr ty2))])], | |
1039 | Unit.layout) | |
1040 | share | |
1041 | ||
1042 | fun wheree {layoutPrettyEnvTycon, layoutPrettyFlexTycon, | |
1043 | region: Region.t, realization: t, time: Time.t, | |
1044 | ty as {name: unit -> Layout.t, | |
1045 | region = _: Region.t, | |
1046 | spec: Region.t, | |
1047 | tyStr: t}}: unit = | |
1048 | case getFlex {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1049 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
1050 | oper = "realized", time = time, ty = ty} of | |
1051 | NONE => () | |
1052 | | SOME flex => | |
1053 | let | |
1054 | val error: (Layout.t list * Layout.t * Layout.t) option ref = ref NONE | |
1055 | val addError = fn (msg, tyError, rlError) => | |
1056 | let | |
1057 | val msgs = | |
1058 | case !error of | |
1059 | NONE => [str msg] | |
1060 | | SOME (msgs, _, _) => (str msg)::msgs | |
1061 | in | |
1062 | error := SOME (msgs, tyError, rlError) | |
1063 | end | |
1064 | ||
1065 | val {layoutPretty = layoutPrettyTyvar, | |
1066 | localInit = localInitLayoutPrettyTyvar, ...} = | |
1067 | Tyvar.makeLayoutPretty () | |
1068 | fun layoutPrettyType t = | |
1069 | Type.layoutPretty | |
1070 | (t, {expand = true, | |
1071 | layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1072 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
1073 | layoutPrettyTyvar = layoutPrettyTyvar}) | |
1074 | ||
1075 | val tyKind = TypeStr.kind tyStr | |
1076 | val tyArity = | |
1077 | case tyKind of | |
1078 | Kind.Arity tyArity => tyArity | |
1079 | | _ => Error.bug "Interface.TypeStr.wheree: tyArity" | |
1080 | val rlKind = TypeStr.kind realization | |
1081 | val rlArity = | |
1082 | case rlKind of | |
1083 | Kind.Arity rlArity => rlArity | |
1084 | | _ => Error.bug "Interface.TypeStr.wheree: rlArity" | |
1085 | local | |
1086 | val tyvars = | |
1087 | Vector.tabulate | |
1088 | (Int.max (tyArity, rlArity), fn _ => | |
1089 | Tyvar.makeNoname {equality = false}) | |
1090 | val () = localInitLayoutPrettyTyvar tyvars | |
1091 | in | |
1092 | val tyTyvars = Vector.prefix (tyvars, tyArity) | |
1093 | val tyTyargs = Vector.map (tyTyvars, Type.var) | |
1094 | val rlTyvars = Vector.prefix (tyvars, rlArity) | |
1095 | val rlTyargs = Vector.map (rlTyvars, Type.var) | |
1096 | end | |
1097 | fun layoutTyvars tyvars = | |
1098 | let | |
1099 | open Layout | |
1100 | val tyvars = | |
1101 | case Vector.length tyvars of | |
1102 | 0 => empty | |
1103 | | 1 => layoutPrettyTyvar (Vector.first tyvars) | |
1104 | | _ => tuple (Vector.toListMap (tyvars, layoutPrettyTyvar)) | |
1105 | val tyvars = | |
1106 | if tyArity = rlArity | |
1107 | then tyvars | |
1108 | else bracket tyvars | |
1109 | in | |
1110 | if isEmpty tyvars | |
1111 | then str " " | |
1112 | else seq [str " ", tyvars, str " "] | |
1113 | end | |
1114 | ||
1115 | fun tyMsg (b, rest) = | |
1116 | let | |
1117 | val empty = Layout.empty | |
1118 | val defn = | |
1119 | seq [str " = ", | |
1120 | case rest of | |
1121 | NONE => str "..." | |
1122 | | SOME rest => rest] | |
1123 | val (kw, defn) = | |
1124 | case TypeStr.node tyStr of | |
1125 | Datatype _ => ("datatype", defn) | |
1126 | | Scheme _ => ("type", defn) | |
1127 | | Tycon {eq, ...} => | |
1128 | (case rest of | |
1129 | NONE => | |
1130 | (if eq then "eqtype" else "type", | |
1131 | empty) | |
1132 | | SOME _ => | |
1133 | ("type", defn)) | |
1134 | in | |
1135 | seq [if b then bracket (str kw) else str kw, | |
1136 | layoutTyvars tyTyvars, | |
1137 | name (), | |
1138 | defn] | |
1139 | end | |
1140 | fun rlMsg (b, rest) = | |
1141 | let | |
1142 | val defn = | |
1143 | seq [str " = ", | |
1144 | case rest of | |
1145 | NONE => str "..." | |
1146 | | SOME rest => rest] | |
1147 | val kw = "type" | |
1148 | in | |
1149 | seq [if b then bracket (str kw) else str kw, | |
1150 | layoutTyvars rlTyvars, | |
1151 | name (), | |
1152 | defn] | |
1153 | end | |
1154 | ||
1155 | val () = | |
1156 | if Kind.equals (tyKind, rlKind) | |
1157 | then () | |
1158 | else addError ("arity", | |
1159 | tyMsg (false, NONE), | |
1160 | rlMsg (false, NONE)) | |
1161 | val () = | |
1162 | if FlexibleTycon.hasCons flex | |
1163 | andalso | |
1164 | Option.isNone (TypeStr.toTyconOpt | |
1165 | (realization, {expand = true})) | |
1166 | then let | |
1167 | fun tyDefn () = | |
1168 | (SOME o bracket o #1 o layoutPrettyType) | |
1169 | (TypeStr.apply (tyStr, tyTyargs)) | |
1170 | val (tyKwErr, tyDefn) = | |
1171 | case TypeStr.node tyStr of | |
1172 | Datatype _ => (true, NONE) | |
1173 | | Scheme _ => (false, tyDefn ()) | |
1174 | | Tycon _ => (false, tyDefn ()) | |
1175 | val rlDefn = | |
1176 | (SOME o bracket o #1 o layoutPrettyType) | |
1177 | (TypeStr.apply (realization, rlTyargs)) | |
1178 | in | |
1179 | addError ("type structure", | |
1180 | tyMsg (tyKwErr, tyDefn), | |
1181 | rlMsg (false, rlDefn)) | |
1182 | end | |
1183 | else let | |
1184 | val tyAdmitsEquality = admitsEquality (#tyStr ty) | |
1185 | val rlAdmitsEquality = admitsEquality realization | |
1186 | in | |
1187 | if AdmitsEquality.<= (tyAdmitsEquality, rlAdmitsEquality) | |
1188 | then () | |
1189 | else let | |
1190 | fun tyDefn () = | |
1191 | (SOME o bracket o #1 o layoutPrettyType) | |
1192 | (TypeStr.apply (tyStr, tyTyargs)) | |
1193 | val (tyKwErr, tyDefn) = | |
1194 | case TypeStr.node tyStr of | |
1195 | Datatype _ => (false, NONE) | |
1196 | | Scheme _ => (false, tyDefn ()) | |
1197 | | Tycon {eq, ...} => | |
1198 | if eq | |
1199 | then (true, NONE) | |
1200 | else (false, tyDefn ()) | |
1201 | val rlDefn = | |
1202 | Type.explainDoesNotAdmitEquality | |
1203 | (TypeStr.apply (realization, rlTyargs), | |
1204 | {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1205 | layoutPrettyFlexTycon = layoutPrettyFlexTycon}) | |
1206 | in | |
1207 | addError ("admits equality", | |
1208 | tyMsg (tyKwErr, tyDefn), | |
1209 | rlMsg (false, rlDefn)) | |
1210 | end | |
1211 | end | |
1212 | in | |
1213 | case !error of | |
1214 | NONE => | |
1215 | (FlexibleTycon.defnRef flex := Defn.typeStr realization | |
1216 | ; FlexibleTycon.pushSpec (flex, region) | |
1217 | ; pushSpec (realization, region)) | |
1218 | | SOME (msgs, tyError, rlError) => | |
1219 | Control.error | |
1220 | (region, | |
1221 | seq [str "type cannot be realized (", | |
1222 | (seq o List.separate) (List.rev msgs, str ", "), | |
1223 | str "): ", | |
1224 | name ()], | |
1225 | align ((seq [str "type spec: ", tyError]) :: | |
1226 | (List.map | |
1227 | (specs (tyStr, spec), fn r => | |
1228 | seq [str "spec at: ", Region.layout r])) @ | |
1229 | [seq [str "type defn: ", rlError]])) | |
1230 | end | |
1231 | ||
1232 | val wheree = | |
1233 | Trace.trace ("Interface.TypeStr.wheree", | |
1234 | fn {realization, time, ty, ...} => | |
1235 | Layout.record [("realization", layout realization), | |
1236 | ("time", Time.layout time), | |
1237 | ("ty", Layout.record [("tyStr", layout (#tyStr ty))])], | |
1238 | Unit.layout) | |
1239 | wheree | |
1240 | end | |
1241 | ||
1242 | structure UniqueId = IntUniqueId () | |
1243 | ||
1244 | structure TyconMap = | |
1245 | struct | |
1246 | datatype 'a t = T of {strs: (Strid.t * 'a t) array, | |
1247 | types: (Ast.Tycon.t * 'a) array} | |
1248 | ||
1249 | fun layout layoutA = | |
1250 | let | |
1251 | open Layout | |
1252 | fun loop (T {strs, types}) = | |
1253 | record [("strs", | |
1254 | Array.layout (Layout.tuple2 (Strid.layout, loop)) strs), | |
1255 | ("types", | |
1256 | Array.layout (Layout.tuple2 (Ast.Tycon.layout, layoutA)) | |
1257 | types)] | |
1258 | in | |
1259 | loop | |
1260 | end | |
1261 | ||
1262 | fun empty (): 'a t = T {strs = Array.new0 (), | |
1263 | types = Array.new0 ()} | |
1264 | ||
1265 | fun isEmpty (T {strs, types}) = | |
1266 | 0 = Array.length strs andalso 0 = Array.length types | |
1267 | ||
1268 | fun peekStrid (T {strs, ...}, strid) = | |
1269 | Array.peekMap (strs, fn (strid', z) => | |
1270 | if Strid.equals (strid, strid') | |
1271 | then SOME z | |
1272 | else NONE) | |
1273 | ||
1274 | fun peekTycon (T {types, ...}, tycon) = | |
1275 | Array.peekMap (types, fn (tycon', z) => | |
1276 | if Ast.Tycon.equals (tycon, tycon') | |
1277 | then SOME z | |
1278 | else NONE) | |
1279 | ||
1280 | end | |
1281 | ||
1282 | (*---------------------------------------------------*) | |
1283 | (* Main Datatype *) | |
1284 | (*---------------------------------------------------*) | |
1285 | ||
1286 | datatype t = T of {copy: copy, | |
1287 | flexible: FlexibleTycon.t TyconMap.t option ref, | |
1288 | isClosed: bool, | |
1289 | original: t option, | |
1290 | plist: PropertyList.t, | |
1291 | strs: (Strid.t * t) array, | |
1292 | types: (Ast.Tycon.t * TypeStr.t) array, | |
1293 | uniqueId: UniqueId.t, | |
1294 | vals: (Ast.Vid.t * (Status.t * Scheme.t)) array} Set.t | |
1295 | withtype copy = t option ref | |
1296 | ||
1297 | fun dest (T s) = Set.! s | |
1298 | ||
1299 | local | |
1300 | fun make f = f o dest | |
1301 | in | |
1302 | val plist = make #plist | |
1303 | end | |
1304 | ||
1305 | fun original I = | |
1306 | case #original (dest I) of | |
1307 | NONE => I | |
1308 | | SOME I => I | |
1309 | ||
1310 | fun new {isClosed, original, strs, types, vals} = | |
1311 | T (Set.singleton {copy = ref NONE, | |
1312 | flexible = ref NONE, | |
1313 | isClosed = isClosed, | |
1314 | original = original, | |
1315 | plist = PropertyList.new (), | |
1316 | strs = strs, | |
1317 | types = types, | |
1318 | uniqueId = UniqueId.new (), | |
1319 | vals = vals}) | |
1320 | ||
1321 | val empty = new {isClosed = true, | |
1322 | original = NONE, | |
1323 | strs = Array.new0 (), | |
1324 | types = Array.new0 (), | |
1325 | vals = Array.new0 ()} | |
1326 | ||
1327 | local | |
1328 | open Layout | |
1329 | in | |
1330 | fun layout (T s) = | |
1331 | let | |
1332 | val {strs, types, uniqueId = u, vals, ...} = Set.! s | |
1333 | in | |
1334 | record [("uniqueId", UniqueId.layout u), | |
1335 | ("strs", | |
1336 | Array.layout (Layout.tuple2 (Strid.layout, layout)) strs), | |
1337 | ("types", | |
1338 | Array.layout (Layout.tuple2 (Ast.Tycon.layout, TypeStr.layout)) | |
1339 | types), | |
1340 | ("vals", | |
1341 | Array.layout (Layout.tuple2 (Vid.layout, | |
1342 | Layout.tuple2 (Status.layout, | |
1343 | Scheme.layout))) | |
1344 | vals)] | |
1345 | end | |
1346 | end | |
1347 | ||
1348 | fun equals (T s, T s') = Set.equals (s, s') | |
1349 | ||
1350 | val equals = | |
1351 | Trace.trace2 ("Interface.equals", layout, layout, Bool.layout) equals | |
1352 | ||
1353 | fun sameShape (I, I') = | |
1354 | case (#original (dest I), #original (dest I')) of | |
1355 | (SOME I, SOME I') => equals (I, I') | |
1356 | | _ => false | |
1357 | ||
1358 | fun peekStrid (T s, strid: Strid.t): t option = | |
1359 | let | |
1360 | val {strs, ...} = Set.! s | |
1361 | in | |
1362 | Array.peekMap (strs, fn (strid', I) => | |
1363 | if Strid.equals (strid, strid') | |
1364 | then SOME I | |
1365 | else NONE) | |
1366 | end | |
1367 | ||
1368 | datatype 'a peekResult = | |
1369 | Found of 'a | |
1370 | | UndefinedStructure of Strid.t list | |
1371 | ||
1372 | fun peekStrids (I: t, strids: Strid.t list): t peekResult = | |
1373 | let | |
1374 | fun loop (I, strids, ac) = | |
1375 | case strids of | |
1376 | [] => Found I | |
1377 | | strid :: strids => | |
1378 | case peekStrid (I, strid) of | |
1379 | NONE => UndefinedStructure (rev (strid :: ac)) | |
1380 | | SOME I => loop (I, strids, strid :: ac) | |
1381 | in | |
1382 | loop (I, strids, []) | |
1383 | end | |
1384 | ||
1385 | fun peekTycon (T s, tycon: Ast.Tycon.t): (Ast.Tycon.t * TypeStr.t) option = | |
1386 | let | |
1387 | val {types, ...} = Set.! s | |
1388 | in | |
1389 | Array.peekMap (types, fn (name, typeStr) => | |
1390 | if Ast.Tycon.equals (tycon, name) | |
1391 | then SOME (name, typeStr) | |
1392 | else NONE) | |
1393 | end | |
1394 | ||
1395 | fun unbound (r: Region.t, className, x: Layout.t): unit = | |
1396 | Control.error | |
1397 | (r, | |
1398 | let open Layout | |
1399 | in seq [str "undefined ", str className, str " ", x] | |
1400 | end, | |
1401 | Layout.empty) | |
1402 | ||
1403 | fun layoutStrids (ss: Strid.t list): Layout.t = | |
1404 | Layout.str (concat (List.separate (List.map (ss, Strid.toString), "."))) | |
1405 | ||
1406 | fun lookupLongtycon (I: t, long: Longtycon.t, r: Region.t, | |
1407 | {prefix: Strid.t list}) = | |
1408 | let | |
1409 | val (ss, c) = Longtycon.split long | |
1410 | in | |
1411 | case peekStrids (I, ss) of | |
1412 | Found I => | |
1413 | (case peekTycon (I, c) of | |
1414 | NONE => | |
1415 | (unbound (r, "type", | |
1416 | Longtycon.layout (Longtycon.long (prefix @ ss, c))) | |
1417 | ; NONE) | |
1418 | | SOME (name, s) => SOME (name, s)) | |
1419 | | UndefinedStructure ss => | |
1420 | (unbound (r, "structure", layoutStrids (prefix @ ss)) | |
1421 | ; NONE) | |
1422 | end | |
1423 | ||
1424 | fun lookupLongstrid (I: t, long: Longstrid.t, r: Region.t, | |
1425 | {prefix: Strid.t list}) = | |
1426 | let | |
1427 | val (ss, s) = Longstrid.split long | |
1428 | in | |
1429 | case peekStrids (I, ss) of | |
1430 | Found I => | |
1431 | (case peekStrid (I, s) of | |
1432 | NONE => | |
1433 | (unbound (r, "structure", | |
1434 | Longstrid.layout (Longstrid.long (prefix @ ss, s))) | |
1435 | ; NONE) | |
1436 | | SOME I => SOME I) | |
1437 | | UndefinedStructure ss => | |
1438 | (unbound (r, "structure", layoutStrids (prefix @ ss)) | |
1439 | ; NONE) | |
1440 | end | |
1441 | ||
1442 | fun share {layoutPrettyEnvTycon, layoutPrettyFlexTycon, | |
1443 | I1: t, long1: Longstrid.t, I2: t, long2: Longstrid.t, | |
1444 | time, region}: unit = | |
1445 | let | |
1446 | fun mkTy (s, long, strids, name) = | |
1447 | let | |
1448 | val spec = Ast.Tycon.region name | |
1449 | val region = Longstrid.region long | |
1450 | val name = fn () => | |
1451 | let | |
1452 | val (ss, s) = Longstrid.split long | |
1453 | in | |
1454 | Ast.Longtycon.layout | |
1455 | (Ast.Longtycon.long (List.concat [ss, [s], rev strids], | |
1456 | name)) | |
1457 | end | |
1458 | in | |
1459 | {name = name, | |
1460 | region = region, | |
1461 | spec = spec, | |
1462 | tyStr = s} | |
1463 | end | |
1464 | fun ensureFlexible (I: t, strids): unit = | |
1465 | let | |
1466 | val {get: t -> bool ref, destroy, ...} = | |
1467 | Property.destGet (plist, Property.initFun (fn _ => ref false)) | |
1468 | fun loop (I: t, strids): unit = | |
1469 | let | |
1470 | val r = get I | |
1471 | in | |
1472 | if !r | |
1473 | then () | |
1474 | else | |
1475 | let | |
1476 | val _ = r := true | |
1477 | val T s = I | |
1478 | val {strs, types, ...} = Set.! s | |
1479 | val _ = | |
1480 | Array.foreach | |
1481 | (strs, fn (strid, I) => | |
1482 | ensureFlexible (I, strid :: strids)) | |
1483 | val _ = | |
1484 | Array.foreach | |
1485 | (types, fn (name, s) => | |
1486 | (ignore o TypeStr.getFlex) | |
1487 | {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1488 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
1489 | oper = "shared", | |
1490 | time = time, | |
1491 | ty = mkTy (s, long1, strids, name)}) | |
1492 | in | |
1493 | () | |
1494 | end | |
1495 | end | |
1496 | val () = loop (I, strids) | |
1497 | val _ = destroy () | |
1498 | in | |
1499 | () | |
1500 | end | |
1501 | fun share (I1, I2, strids): unit = | |
1502 | if equals (I1, I2) | |
1503 | then ensureFlexible (I1, strids) | |
1504 | else if sameShape (I1, I2) | |
1505 | then | |
1506 | let | |
1507 | fun loop (T s1, T s2, strids): unit = | |
1508 | let | |
1509 | val {isClosed, strs = strs1, types = types1, ...} = Set.! s1 | |
1510 | val {strs = strs2, types = types2, ...} = Set.! s2 | |
1511 | val _ = | |
1512 | Array.foreach2 | |
1513 | (types1, types2, fn ((name, s1), (_, s2)) => | |
1514 | TypeStr.share | |
1515 | {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1516 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
1517 | region = region, | |
1518 | time = time, | |
1519 | ty1 = mkTy (s1, long1, strids, name), | |
1520 | ty2 = mkTy (s2, long2, strids, name)}) | |
1521 | val _ = | |
1522 | Array.foreach2 | |
1523 | (strs1, strs2, fn ((name, I1), (_, I2)) => | |
1524 | loop (I1, I2, name :: strids)) | |
1525 | val _ = | |
1526 | (* Can't always union here. I1 and I2 may have | |
1527 | * exactly the same shape, but may have free | |
1528 | * flxible tycons defined in other signatures that | |
1529 | * are different. | |
1530 | * However, if the interface is closed, that is, if | |
1531 | * all of the flexible tycons that appear in it are | |
1532 | * also defined in it, then sharing the structures | |
1533 | * implies that the structures are identical. This | |
1534 | * also relies on the fact that the structures have | |
1535 | * the same shape, which means that they are copies | |
1536 | * of the same interface. That is sufficient to | |
1537 | * guarantee that all rigid tycons are identical. | |
1538 | *) | |
1539 | if isClosed | |
1540 | then Set.union (s1, s2) | |
1541 | else () | |
1542 | in | |
1543 | () | |
1544 | end | |
1545 | in | |
1546 | loop (I1, I2, strids) | |
1547 | end | |
1548 | else (* different shapes -- need to share pointwise *) | |
1549 | let | |
1550 | val T s1 = I1 | |
1551 | val T s2 = I2 | |
1552 | val {strs = strs1, types = types1, ...} = Set.! s1 | |
1553 | val {strs = strs2, types = types2, ...} = Set.! s2 | |
1554 | fun walk2 (a1, a2, compareNames, f: 'a * 'a * 'b -> unit) = | |
1555 | let | |
1556 | val n1 = Array.length a1 | |
1557 | val n2 = Array.length a2 | |
1558 | fun both (i1, i2) = | |
1559 | if i1 < n1 andalso i2 < n2 | |
1560 | then compare (i1, Array.sub (a1, i1), | |
1561 | i2, Array.sub (a2, i2)) | |
1562 | else () | |
1563 | and compare (i1, (name1, z1), i2, (name2, z2)) = | |
1564 | case compareNames (name1, name2) of | |
1565 | GREATER => | |
1566 | let | |
1567 | val i2 = i2 + 1 | |
1568 | in | |
1569 | if i2 < n2 | |
1570 | then compare (i1, (name1, z1), | |
1571 | i2, Array.sub (a2, i2)) | |
1572 | else () | |
1573 | end | |
1574 | | EQUAL => (f (z1, z2, name1) | |
1575 | ; both (i1 + 1, i2 + 1)) | |
1576 | | LESS => | |
1577 | let | |
1578 | val i1 = i1 + 1 | |
1579 | in | |
1580 | if i1 < n1 | |
1581 | then compare (i1, Array.sub (a1, i1), | |
1582 | i2, (name2, z2)) | |
1583 | else () | |
1584 | end | |
1585 | in | |
1586 | both (0, 0) | |
1587 | end | |
1588 | val _ = | |
1589 | walk2 (strs1, strs2, Strid.compare, | |
1590 | fn (I1, I2, name) => share (I1, I2, name :: strids)) | |
1591 | val _ = | |
1592 | walk2 (types1, types2, Ast.Tycon.compare, | |
1593 | fn (s1, s2, name) => | |
1594 | TypeStr.share | |
1595 | {layoutPrettyEnvTycon = layoutPrettyEnvTycon, | |
1596 | layoutPrettyFlexTycon = layoutPrettyFlexTycon, | |
1597 | region = region, | |
1598 | time = time, | |
1599 | ty1 = mkTy (s1, long1, strids, name), | |
1600 | ty2 = mkTy (s2, long2, strids, name)}) | |
1601 | in | |
1602 | () | |
1603 | end | |
1604 | in | |
1605 | share (I1, I2, []) | |
1606 | end | |
1607 | ||
1608 | val share = | |
1609 | Trace.trace | |
1610 | ("Interface.share", | |
1611 | fn {I1, I2, time, ...} => | |
1612 | Layout.tuple [layout I1, layout I2, Time.layout time], | |
1613 | Unit.layout) | |
1614 | share | |
1615 | ||
1616 | fun copy (I: t): t = | |
1617 | let | |
1618 | (* Keep track of all nodes that have forward pointers to copies, so | |
1619 | * that we can gc them when done. | |
1620 | *) | |
1621 | val copies: copy list ref = ref [] | |
1622 | fun loop (I as T s): t = | |
1623 | let | |
1624 | val r as {copy, ...} = Set.! s | |
1625 | in | |
1626 | case !copy of | |
1627 | NONE => | |
1628 | let | |
1629 | val {isClosed, original, strs, types, vals, ...} = r | |
1630 | val types = | |
1631 | Array.map (types, fn (name, typeStr) => | |
1632 | (name, TypeStr.copy typeStr)) | |
1633 | val vals = | |
1634 | Array.map (vals, fn (name, (status, scheme)) => | |
1635 | (name, (status, Scheme.copy scheme))) | |
1636 | val strs = | |
1637 | Array.map (strs, fn (name, I) => (name, loop I)) | |
1638 | val original = | |
1639 | SOME (case original of | |
1640 | NONE => I | |
1641 | | SOME I => I) | |
1642 | val I = T (Set.singleton {copy = ref NONE, | |
1643 | flexible = ref NONE, | |
1644 | isClosed = isClosed, | |
1645 | original = original, | |
1646 | plist = PropertyList.new (), | |
1647 | strs = strs, | |
1648 | types = types, | |
1649 | uniqueId = UniqueId.new (), | |
1650 | vals = vals}) | |
1651 | val _ = List.push (copies, copy) | |
1652 | val _ = copy := SOME I | |
1653 | in | |
1654 | I | |
1655 | end | |
1656 | | SOME I => I | |
1657 | end | |
1658 | val I = loop I | |
1659 | fun clear copies = List.foreach (!copies, fn copy => copy := NONE) | |
1660 | val _ = clear copies | |
1661 | val _ = clear FlexibleTycon.copies | |
1662 | val _ = FlexibleTycon.copies := [] | |
1663 | in | |
1664 | I | |
1665 | end | |
1666 | ||
1667 | val copy = Trace.trace ("Interface.copy", layout, layout) copy | |
1668 | ||
1669 | fun flexibleTycons (I: t): FlexibleTycon.t TyconMap.t = | |
1670 | let | |
1671 | val {destroy = destroy1, | |
1672 | get = tyconShortest: (FlexibleTycon.t | |
1673 | -> {flex: FlexibleTycon.t option ref, | |
1674 | length: int option} ref), ...} = | |
1675 | Property.destGet (FlexibleTycon.plist, | |
1676 | Property.initFun (fn _ => ref {flex = ref NONE, | |
1677 | length = NONE})) | |
1678 | val {destroy = destroy2, | |
1679 | get = interfaceShortest: t -> int option ref, ...} = | |
1680 | Property.destGet (plist, Property.initFun (fn _ => ref NONE)) | |
1681 | fun loop (I: t, length: int): FlexibleTycon.t option ref TyconMap.t = | |
1682 | let | |
1683 | val r = interfaceShortest I | |
1684 | in | |
1685 | if isSome (!r) andalso length >= valOf (!r) | |
1686 | then TyconMap.empty () | |
1687 | else | |
1688 | let | |
1689 | val _ = r := SOME length | |
1690 | val {strs, types, ...} = dest I | |
1691 | fun setTycon (tycon, isDatatype, isEqtype) = | |
1692 | case tycon of | |
1693 | Tycon.Flexible fc => | |
1694 | let | |
1695 | val {admitsEquality, defn, hasCons, ...} = FlexibleTycon.fields fc | |
1696 | val admitsEquality = | |
1697 | case !admitsEquality of | |
1698 | AdmitsEquality.Always => true | |
1699 | | AdmitsEquality.Never => false | |
1700 | | AdmitsEquality.Sometimes => true | |
1701 | in | |
1702 | case Defn.dest (!defn) of | |
1703 | Defn.Undefined => | |
1704 | let | |
1705 | val r = tyconShortest fc | |
1706 | in | |
1707 | if (hasCons | |
1708 | andalso not isDatatype) | |
1709 | orelse | |
1710 | (admitsEquality | |
1711 | andalso not isEqtype) | |
1712 | orelse | |
1713 | (isSome (#length (!r)) | |
1714 | andalso length >= valOf (#length (!r))) | |
1715 | then ref NONE | |
1716 | else let | |
1717 | val _ = #flex (!r) := NONE | |
1718 | val flex = ref (SOME fc) | |
1719 | val _ = r := {flex = flex, | |
1720 | length = SOME length} | |
1721 | in | |
1722 | flex | |
1723 | end | |
1724 | end | |
1725 | | _ => ref NONE | |
1726 | end | |
1727 | | _ => ref NONE | |
1728 | val types = | |
1729 | Array.map | |
1730 | (types, fn (tycon, typeStr) => | |
1731 | (tycon, | |
1732 | case TypeStr.node typeStr of | |
1733 | TypeStr.Datatype {tycon, repl, ...} => | |
1734 | setTycon (tycon, not repl, true) | |
1735 | | TypeStr.Tycon {eq, tycon, ...} => | |
1736 | setTycon (tycon, false, eq) | |
1737 | | _ => ref NONE)) | |
1738 | val strs = | |
1739 | Array.map | |
1740 | (strs, fn (s, I) => | |
1741 | (s, loop (I, 1 + length))) | |
1742 | in | |
1743 | TyconMap.T {strs = strs, types = types} | |
1744 | end | |
1745 | end | |
1746 | val tm = loop (I, 0) | |
1747 | val _ = (destroy1 (); destroy2 ()) | |
1748 | fun collapse (tm: FlexibleTycon.t option ref TyconMap.t) | |
1749 | : FlexibleTycon.t TyconMap.t = | |
1750 | let | |
1751 | val TyconMap.T {strs, types} = tm | |
1752 | val types = Array.keepAllMap (types, fn (c, r) => | |
1753 | Option.map (!r, fn f => (c, f))) | |
1754 | val strs = Array.keepAllMap (strs, fn (s, m) => | |
1755 | let | |
1756 | val m = collapse m | |
1757 | in | |
1758 | if TyconMap.isEmpty m | |
1759 | then NONE | |
1760 | else SOME (s, m) | |
1761 | end) | |
1762 | in | |
1763 | TyconMap.T {strs = strs, types = types} | |
1764 | end | |
1765 | in | |
1766 | collapse tm | |
1767 | end | |
1768 | ||
1769 | val flexibleTycons = | |
1770 | fn I as T s => | |
1771 | let | |
1772 | val {flexible, ...} = Set.! s | |
1773 | in | |
1774 | case !flexible of | |
1775 | NONE => | |
1776 | let | |
1777 | val f = flexibleTycons I | |
1778 | val _ = flexible := SOME f | |
1779 | in | |
1780 | f | |
1781 | end | |
1782 | | SOME f => f | |
1783 | end | |
1784 | ||
1785 | val flexibleTycons = | |
1786 | Trace.trace ("Interface.flexibleTycons", layout, | |
1787 | TyconMap.layout FlexibleTycon.layout) | |
1788 | flexibleTycons | |
1789 | ||
1790 | fun dest (T s) = | |
1791 | let | |
1792 | val {strs, types, vals, ...} = Set.! s | |
1793 | in | |
1794 | {strs = strs, | |
1795 | types = types, | |
1796 | vals = vals} | |
1797 | end | |
1798 | ||
1799 | end |