Import Upstream version 20180207
[hcoop/debian/mlton.git] / mlton / elaborate / interface.fun
CommitLineData
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
10functor Interface (S: INTERFACE_STRUCTS): INTERFACE =
11struct
12
13open S
14
15local
16 open Layout
17in
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 "]"]
24end
25
26local
27 open Ast
28in
29 structure Longstrid = Longstrid
30 structure Longtycon = Longtycon
31 structure Record = SortedRecord
32 structure Strid = Strid
33 structure Vid = Vid
34end
35
36structure Etycon = EnvTycon
37structure EtypeStr = EnvTypeStr
38
39structure Set = DisjointSet
40
41structure 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 *)
60structure TyconId = IntUniqueId ()
61
62structure 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
70structure 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
102structure 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
191structure 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
233structure 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
317structure Scheme = GenericScheme (structure Type = Type
318 structure Tyvar = Tyvar)
319
320structure 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
345structure 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
401structure 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
478structure 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 *)
512local
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})
525in
526 val expandTy = expandTy
527end
528
529structure 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
619structure 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
646fun copyCons cons: Cons.t =
647 Cons.map (cons, fn {scheme, ...} =>
648 {scheme = copyScheme scheme})
649and 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
663and 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
686and 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
694and 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
702and copyScheme (Scheme.T {tyvars, ty}): Scheme.t =
703 Scheme.T {ty = copyType ty, tyvars = tyvars}
704and 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
714structure AdmitsEquality =
715 struct
716 open AdmitsEquality
717
718 fun fromBool b = if b then Sometimes else Never
719 end
720
721fun 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
731and 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
748and 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
756and 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
766structure 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
835structure Scheme =
836 struct
837 open Scheme
838
839 val admitsEquality = schemeAdmitsEquality
840
841 val copy = copyScheme
842 end
843
844structure 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
1242structure 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
1286datatype 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
1295withtype copy = t option ref
1296
1297fun dest (T s) = Set.! s
1298
1299local
1300 fun make f = f o dest
1301in
1302 val plist = make #plist
1303end
1304
1305fun original I =
1306 case #original (dest I) of
1307 NONE => I
1308 | SOME I => I
1309
1310fun 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
1321val empty = new {isClosed = true,
1322 original = NONE,
1323 strs = Array.new0 (),
1324 types = Array.new0 (),
1325 vals = Array.new0 ()}
1326
1327local
1328 open Layout
1329in
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
1346end
1347
1348fun equals (T s, T s') = Set.equals (s, s')
1349
1350val equals =
1351 Trace.trace2 ("Interface.equals", layout, layout, Bool.layout) equals
1352
1353fun sameShape (I, I') =
1354 case (#original (dest I), #original (dest I')) of
1355 (SOME I, SOME I') => equals (I, I')
1356 | _ => false
1357
1358fun 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
1368datatype 'a peekResult =
1369 Found of 'a
1370 | UndefinedStructure of Strid.t list
1371
1372fun 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
1385fun 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
1395fun 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
1403fun layoutStrids (ss: Strid.t list): Layout.t =
1404 Layout.str (concat (List.separate (List.map (ss, Strid.toString), ".")))
1405
1406fun 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
1424fun 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
1442fun 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
1608val 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
1616fun 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
1667val copy = Trace.trace ("Interface.copy", layout, layout) copy
1668
1669fun 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
1769val 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
1785val flexibleTycons =
1786 Trace.trace ("Interface.flexibleTycons", layout,
1787 TyconMap.layout FlexibleTycon.layout)
1788 flexibleTycons
1789
1790fun 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
1799end