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.
6 * MLton is released under a BSD-style license.
7 * See the file MLton-LICENSE for details.
10 functor Interface (S: INTERFACE_STRUCTS): INTERFACE =
23 seq [str "[", l, str "]"]
29 structure Longstrid = Longstrid
30 structure Longtycon = Longtycon
31 structure Record = SortedRecord
32 structure Strid = Strid
36 structure Etycon = EnvTycon
37 structure EtypeStr = EnvTypeStr
39 structure Set = DisjointSet
43 datatype t = Con | Exn | Var
45 val layout: t -> Layout.t
46 val toString: t -> string
49 datatype t = Con | Exn | Var
56 val layout = Layout.str o toString
59 (* only needed for debugging *)
60 structure TyconId = IntUniqueId ()
66 val layoutRef: (t -> Layout.t) ref = ref (fn _ => Layout.empty)
67 fun layout d = (!layoutRef) d
75 val current: unit -> t
76 val layout: t -> Layout.t
85 val layout = Int.layout
89 val currentTime: int ref = ref 0
91 fun current () = !currentTime
95 val n = 1 + !currentTime
96 val _ = currentTime := n
102 structure FlexibleTycon =
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".
109 datatype t = T of {admitsEquality: AdmitsEquality.t ref,
111 creationTime: Time.t,
116 plist: PropertyList.t,
117 prettyDefault: string,
118 specs: Region.t AppendList.t ref} Set.t
119 withtype copy = t option ref
121 fun fields (T s) = Set.! s
124 fun make f = f o fields
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
138 val layoutPrettyDefault = Layout.str o prettyDefault
142 val {admitsEquality, hasCons, kind, prettyDefault, ...} =
145 {admitsEquality = !admitsEquality,
148 prettyDefault = prettyDefault}
151 val equals = fn (T s, T s') => Set.equals (s, s')
156 val {admitsEquality, creationTime, defn, hasCons, id, kind, prettyDefault, ...} = fields fc
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)]
167 val copies: copy list ref = ref []
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,
174 creationTime = Time.current (),
179 plist = PropertyList.new (),
180 prettyDefault = prettyDefault,
183 fun pushSpec (fc, region) =
185 val specsRef = specsRef fc
187 specsRef := AppendList.snoc (!specsRef, region)
194 Flexible of FlexibleTycon.t
197 val fromEnv: Etycon.t -> t = Rigid
199 fun admitsEquality c =
201 Flexible f => FlexibleTycon.admitsEquality f
202 | Rigid c => Etycon.admitsEquality c
204 val arrow = fromEnv Etycon.arrow
207 fn (Flexible f, Flexible f') => FlexibleTycon.equals (f, f')
208 | (Rigid c, Rigid c') => Etycon.equals (c, c')
211 val exn = Rigid Etycon.exn
214 fn Flexible f => FlexibleTycon.kind f
215 | Rigid c => Etycon.kind c
218 fn Flexible f => FlexibleTycon.layout f
219 | Rigid c => Etycon.layout c
221 val tuple = Rigid Etycon.tuple
223 fun layoutAppPretty (c, ts, {layoutPrettyEnvTycon, layoutPrettyFlexTycon}) =
226 EnvTycon.layoutAppPrettyNormal
227 (layoutPrettyFlexTycon f, ts)
229 EnvTycon.layoutAppPretty
230 (c, ts, {layoutPretty = layoutPrettyEnvTycon})
236 Con of Tycon.t * t vector
237 | Record of t Record.t
240 fun arrow (t1, t2) = Con (Tycon.arrow, Vector.new2 (t1, t2))
244 fun deArrowOpt (t: t): (t * t) option =
247 if Tycon.equals (c, Tycon.arrow)
248 then SOME (Vector.sub (ts, 0), Vector.sub (ts, 1))
254 NONE => Error.bug "Interface.Type.deArrow"
257 fun deEta (t: t, tyvars: Tyvar.t vector): Tycon.t option =
260 if Vector.length ts = Vector.length tyvars
261 andalso Vector.foralli (ts, fn (i, t) =>
265 (a, Vector.sub (tyvars, i))
271 val exn = Con (Tycon.exn, Vector.new0 ())
273 fun hom (t, {con, record, var}) =
276 fn Con (c, ts) => con (c, Vector.map (ts, loop))
277 | Record r => record (Record.map (r, loop))
289 paren (align [seq [str "Con ", Tycon.layout c],
290 Vector.layout layout ts])
292 Record.layout {record = r,
295 layoutTuple = Vector.layout layout,
297 | Var a => paren (seq [str "Var ", Tyvar.layout a])
302 fun substitute (t: t, sub: (Tyvar.t * t) vector): t =
305 case Vector.peek (sub, fn (a', _) => Tyvar.equals (a, a')) of
306 NONE => Error.bug "Interface.Type.substitute"
317 structure Scheme = GenericScheme (structure Type = Type
318 structure Tyvar = Tyvar)
324 fun kind (T {tyvars, ...}) =
325 Kind.Arity (Vector.length tyvars)
327 fun make (tyvars, ty) = T {ty = ty, tyvars = tyvars}
329 fun fromTycon tycon =
331 val kind = Tycon.kind tycon
334 Kind.Arity arity => arity
335 | Kind.Nary => Error.bug "Interface.Scheme.fromTycon: Kind.Nary"
339 Tyvar.makeNoname {equality = false})
341 make (tyvars, Type.con (tycon, Vector.map (tyvars, Type.var)))
348 val dest: t -> {name: Ast.Con.t,
349 scheme: Scheme.t} vector
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,
358 -> {scheme: Scheme.t}) -> t
361 datatype t = T of {name: Ast.Con.t,
362 scheme: Scheme.t} vector
366 val fromSortedVector = T
369 (fromSortedVector o QuickSort.sortVector)
370 (v, fn ({name = name1, ...}, {name = name2, ...}) =>
371 case Ast.Con.compare (name1, name2) of
376 val empty = T (Vector.new0 ())
380 (v, fn elt as {name, ...} =>
390 Vector.layout (fn {name, scheme} =>
394 seq [Ast.Con.layout name,
396 Scheme.layout scheme]
404 Datatype of {tycon: Tycon.t,
408 | Tycon of {eq: bool,
416 Datatype {tycon, ...} => Tycon.kind tycon
417 | Scheme s => Scheme.kind s
418 | Tycon {tycon, ...} => Tycon.kind tycon
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} =>
433 record [("eq", Bool.layout eq),
434 ("tycon", Tycon.layout tycon)]]
437 fun apply (t: t, tys: Type.t vector): Type.t =
439 Datatype {tycon, ...} => Type.con (tycon, tys)
440 | Scheme s => Scheme.apply (s, tys)
441 | Tycon {tycon, ...} => Type.con (tycon, tys)
444 Trace.trace ("Interface.TypeStr.apply", Layout.tuple2 (layout, Vector.layout Type.layout), Type.layout)
449 Datatype {cons, ...} => cons
452 fun data (tycon, cons, repl) =
453 Datatype {tycon = tycon, cons = cons, repl = repl}
457 fun tycon (tycon, eq) =
458 Tycon {eq = eq, tycon = tycon}
461 fun tyconAsScheme c =
462 def (Scheme.fromTycon c)
466 Datatype {tycon, cons, ...} => data (tycon, cons, true)
468 | Tycon {tycon, ...} => tyconAsScheme tycon
472 Datatype {tycon, ...} => tyconAsScheme tycon
474 | Tycon {tycon, ...} => tyconAsScheme tycon
483 Realized of EtypeStr.t
484 | TypeStr of TypeStr.t
489 val realized = U o Realized
490 val typeStr = U o TypeStr
491 val undefined = U Undefined
493 fun dest (d: t): dest =
496 | _ => Error.bug "Interface.Defn.dest"
505 Realized s => seq [str "Realized ", EtypeStr.layout s]
506 | TypeStr s => seq [str "TypeStr ", TypeStr.layout s]
507 | Undefined => str "Undefined"
511 (* expandTy expands all type definitions in ty *)
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,
526 val expandTy = expandTy
533 fun layoutPretty (ty, {expand, layoutPrettyEnvTycon, layoutPrettyFlexTycon, layoutPrettyTyvar}) =
536 Tycon.layoutAppPretty
537 (c, ts, {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
538 layoutPrettyFlexTycon = layoutPrettyFlexTycon})
540 case Record.detupleOpt r of
542 (LayoutPretty.simple o seq)
545 (Layout.separateRight
547 (Record.toVector r, fn (f, (t, _)) =>
548 seq [Record.Field.layout f, str ": ", t]),
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
555 Type.hom (ty, {con = con,
560 fun explainDoesNotAdmitEquality (ty, {layoutPrettyEnvTycon, layoutPrettyFlexTycon}) =
562 val layoutAppPretty = fn (c, ls) =>
563 Tycon.layoutAppPretty
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)
571 case Tycon.admitsEquality c of
572 AdmitsEquality.Always => NONE
573 | AdmitsEquality.Sometimes =>
574 if Vector.forall (los, Option.isNone)
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))
582 case Record.detupleOpt r of
585 val v = Record.toVector r
588 (v, ([], false), fn ((f, lo), (fls, extra)) =>
591 | SOME l => ((f,l)::fls, extra))
595 else (SOME o LayoutPretty.simple o seq)
598 (Layout.separateRight
600 (fls, fn (f, (l, _)) =>
601 seq [Record.Field.layout f,
608 | SOME los => con (Tycon.tuple, los)
611 val res = Type.hom (ty, {con = con,
623 fun toTyconOpt (s, {expand}) =
625 val s = if expand then abs s else s
628 Datatype {tycon, ...} => SOME tycon
631 val Scheme.T {tyvars, ty} = s
632 val ty = if expand then expandTy ty else ty
634 case Type.deEta (ty, tyvars) of
637 if Tycon.equals (c, Tycon.arrow)
638 orelse Tycon.equals (c, Tycon.tuple)
642 | Tycon {tycon, ...} => SOME tycon
646 fun copyCons cons: Cons.t =
647 Cons.map (cons, fn {scheme, ...} =>
648 {scheme = copyScheme scheme})
649 and copyDefn (d: Defn.t): Defn.t =
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
660 | TypeStr s => Defn.typeStr (copyTypeStr s)
661 | Undefined => Defn.undefined
663 and copyFlexibleTycon (fc: FlexibleTycon.t): FlexibleTycon.t =
666 val {admitsEquality, copy, defn, hasCons,
667 kind, prettyDefault, specs, ...} =
673 val fc' = make {admitsEquality = !admitsEquality,
674 defn = copyDefn (!defn),
677 prettyDefault = prettyDefault,
679 val _ = List.push (copies, copy)
680 val _ = copy := SOME fc'
686 and copyTycon (t: Tycon.t): Tycon.t =
691 Flexible c => Flexible (copyFlexibleTycon c)
694 and copyType (t: Type.t): Type.t =
698 hom (t, {con = fn (c, ts) => Con (copyTycon c, ts),
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 =
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)
714 structure AdmitsEquality =
718 fun fromBool b = if b then Sometimes else Never
721 fun flexibleTyconAdmitsEquality (fc: FlexibleTycon.t): AdmitsEquality.t =
723 val {admitsEquality, defn, ...} = FlexibleTycon.fields fc
724 datatype z = datatype Defn.dest
726 case Defn.dest (!defn) of
727 Realized _ => !admitsEquality
728 | TypeStr s => typeStrAdmitsEquality s
729 | Undefined => !admitsEquality
731 and schemeAdmitsEquality (s: Scheme.t): bool =
735 datatype z = datatype AdmitsEquality.t
737 case Tycon.admitsEquality c of
740 | Sometimes => Vector.forall (bs, fn b => b)
743 Type.hom (expandTy (Scheme.ty s),
745 record = fn r => Record.forall (r, fn b => b),
748 and tyconAdmitsEquality (t: Tycon.t): AdmitsEquality.t =
750 datatype z = datatype Tycon.t
753 Flexible c => flexibleTyconAdmitsEquality c
754 | Rigid e => Etycon.admitsEquality e
756 and typeStrAdmitsEquality (s: TypeStr.t): AdmitsEquality.t =
758 datatype z = datatype TypeStr.node
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
766 structure FlexibleTycon =
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,
778 prettyDefault = prettyDefault,
779 specs = AppendList.single region}
781 fun realize (fc, typeStr) =
783 val defn = defnRef fc
785 case Defn.dest (!defn) of
786 Defn.Undefined => defn := Defn.realized typeStr
787 | _ => Error.bug "Interface.FlexibleTycon.realize"
790 fun share (fc1 as T s1, fc2 as T s2, sharingSpec) =
792 val {admitsEquality = ae1, creationTime = t1,
793 hasCons = hc1, specs = ss1,
794 id, kind, plist, prettyDefault, ...} =
796 val {admitsEquality = ae2, creationTime = t2,
797 hasCons = hc2, specs = ss2, ...} =
799 val _ = Set.union (s1, s2)
802 (if Ref.equals (ss1, ss2)
804 else AppendList.append (!ss1, !ss2),
808 (s1, {admitsEquality = ref (AdmitsEquality.or (!ae1, !ae2)),
810 creationTime = Time.min (t1, t2),
811 defn = ref Defn.undefined,
813 hasCons = hc1 orelse hc2,
817 prettyDefault = prettyDefault})
822 type typeStr = TypeStr.t
824 datatype realization =
825 ETypeStr of EnvTypeStr.t
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
839 val admitsEquality = schemeAdmitsEquality
841 val copy = copyScheme
848 val admitsEquality = typeStrAdmitsEquality
850 val copy = copyTypeStr
852 fun specs (s, first) =
855 case toTyconOpt (s, {expand = false}) of
856 NONE => AppendList.empty
857 | SOME c => loopTycon c
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
870 (List.rev o AppendList.fold)
871 (loop s, [], fn (r, rs) =>
872 if List.contains (first::rs, r, Region.equals)
877 fun pushSpec (s, region) =
878 case TypeStr.toTyconOpt (s, {expand = false}) of
880 | SOME (Tycon.Flexible flex) =>
881 FlexibleTycon.pushSpec (flex, region)
882 | SOME (Tycon.Rigid _) => ()
884 fun getFlex {layoutPrettyEnvTycon,
885 layoutPrettyFlexTycon,
888 ty = {name: unit -> Layout.t,
891 tyStr: t}}: FlexibleTycon.t option =
895 val isEmpty = Layout.isEmpty
896 val tuple = Layout.tuple
897 val {layoutPretty = layoutPrettyTyvar,
898 localInit = localInitLayoutPrettyTyvar, ...} =
899 Tyvar.makeLayoutPretty ()
902 Kind.Arity arity => arity
903 | _ => Error.bug "Interface.TypeStr.getFlex: Kind.Nary"
907 Tyvar.makeNoname {equality = false})
908 val () = localInitLayoutPrettyTyvar tyvars
909 val tyargs = Vector.map (tyvars, Type.var)
910 val tyvars = Vector.map (tyvars, layoutPrettyTyvar)
912 case Vector.length tyvars of
914 | 1 => Vector.first tyvars
915 | _ => tuple (Vector.toList tyvars)
917 case TypeStr.node tyStr of
918 TypeStr.Datatype _ =>
920 seq [str "... (* = datatype ", l, str " *)"])
921 | TypeStr.Scheme _ =>
925 val defn = TypeStr.apply (tyStr, tyargs)
929 seq [str "type cannot be ", str oper,
930 str " (", str what, str "): ",
933 ((seq [str "type spec: ",
936 if isEmpty tyvars then empty else str " ",
938 mkRest ((#1 o Type.layoutPretty)
939 (defn, {expand = true,
940 layoutPrettyEnvTycon = layoutPrettyEnvTycon,
941 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
942 layoutPrettyTyvar = layoutPrettyTyvar}))])::
944 (specs (tyStr, spec), fn r =>
945 seq [str "spec at: ", Region.layout r]))))
950 case toTyconOpt (tyStr, {expand = true}) of
951 NONE => error "defined"
956 val {creationTime, defn, ...} = FlexibleTycon.fields c
958 case Defn.dest (!defn) of
960 Error.bug "Interface.TypeStr.getFlex: Realized"
962 Error.bug "Interface.TypeStr.getFlex: TypeStr"
964 if Time.< (creationTime, time)
965 then error "not local"
968 | Tycon.Rigid _ => error "defined")
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
983 | (SOME flex1, SOME flex2) =>
984 if Kind.equals (FlexibleTycon.kind flex1, FlexibleTycon.kind flex2)
985 then FlexibleTycon.share (flex1, flex2, region)
987 fun msg {name, region = _, spec, tyStr} =
989 val (keyword, rest) =
991 Datatype _ => ("datatype", str " = ...")
992 | Scheme _ => ("type", str " = ...")
995 then ("eqtype", empty)
999 Kind.Arity arity => arity
1000 | _ => Error.bug "Interface.TypeStr.share.msg: arity"
1004 Tyvar.makeNoname {equality = false})
1005 val {layoutPretty = layoutPrettyTyvar,
1006 localInit = localInitLayoutPrettyTyvar, ...} =
1007 Tyvar.makeLayoutPretty ()
1008 val () = localInitLayoutPrettyTyvar tyvars
1010 case Vector.length tyvars of
1012 | 1 => layoutPrettyTyvar (Vector.first tyvars)
1013 | _ => Layout.tuple (Vector.toListMap (tyvars, layoutPrettyTyvar))
1015 (seq [str "type spec: ",
1017 str " [", tyvars, str "] ",
1021 (specs (tyStr, spec), fn r =>
1022 seq [str "spec at: ", Region.layout r]))
1027 seq [str "types cannot be shared (arity): ",
1028 name1 (), str ", ", name2 ()],
1029 align ((msg ty1) @ (msg ty2)))
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))])],
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,
1048 case getFlex {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1049 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
1050 oper = "realized", time = time, ty = ty} of
1054 val error: (Layout.t list * Layout.t * Layout.t) option ref = ref NONE
1055 val addError = fn (msg, tyError, rlError) =>
1060 | SOME (msgs, _, _) => (str msg)::msgs
1062 error := SOME (msgs, tyError, rlError)
1065 val {layoutPretty = layoutPrettyTyvar,
1066 localInit = localInitLayoutPrettyTyvar, ...} =
1067 Tyvar.makeLayoutPretty ()
1068 fun layoutPrettyType t =
1071 layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1072 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
1073 layoutPrettyTyvar = layoutPrettyTyvar})
1075 val tyKind = TypeStr.kind tyStr
1078 Kind.Arity tyArity => tyArity
1079 | _ => Error.bug "Interface.TypeStr.wheree: tyArity"
1080 val rlKind = TypeStr.kind realization
1083 Kind.Arity rlArity => rlArity
1084 | _ => Error.bug "Interface.TypeStr.wheree: rlArity"
1088 (Int.max (tyArity, rlArity), fn _ =>
1089 Tyvar.makeNoname {equality = false})
1090 val () = localInitLayoutPrettyTyvar tyvars
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)
1097 fun layoutTyvars tyvars =
1101 case Vector.length tyvars of
1103 | 1 => layoutPrettyTyvar (Vector.first tyvars)
1104 | _ => tuple (Vector.toListMap (tyvars, layoutPrettyTyvar))
1106 if tyArity = rlArity
1112 else seq [str " ", tyvars, str " "]
1115 fun tyMsg (b, rest) =
1117 val empty = Layout.empty
1122 | SOME rest => rest]
1124 case TypeStr.node tyStr of
1125 Datatype _ => ("datatype", defn)
1126 | Scheme _ => ("type", defn)
1127 | Tycon {eq, ...} =>
1130 (if eq then "eqtype" else "type",
1135 seq [if b then bracket (str kw) else str kw,
1136 layoutTyvars tyTyvars,
1140 fun rlMsg (b, rest) =
1146 | SOME rest => rest]
1149 seq [if b then bracket (str kw) else str kw,
1150 layoutTyvars rlTyvars,
1156 if Kind.equals (tyKind, rlKind)
1158 else addError ("arity",
1159 tyMsg (false, NONE),
1160 rlMsg (false, NONE))
1162 if FlexibleTycon.hasCons flex
1164 Option.isNone (TypeStr.toTyconOpt
1165 (realization, {expand = true}))
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 ())
1176 (SOME o bracket o #1 o layoutPrettyType)
1177 (TypeStr.apply (realization, rlTyargs))
1179 addError ("type structure",
1180 tyMsg (tyKwErr, tyDefn),
1181 rlMsg (false, rlDefn))
1184 val tyAdmitsEquality = admitsEquality (#tyStr ty)
1185 val rlAdmitsEquality = admitsEquality realization
1187 if AdmitsEquality.<= (tyAdmitsEquality, rlAdmitsEquality)
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, ...} =>
1200 else (false, tyDefn ())
1202 Type.explainDoesNotAdmitEquality
1203 (TypeStr.apply (realization, rlTyargs),
1204 {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1205 layoutPrettyFlexTycon = layoutPrettyFlexTycon})
1207 addError ("admits equality",
1208 tyMsg (tyKwErr, tyDefn),
1209 rlMsg (false, rlDefn))
1215 (FlexibleTycon.defnRef flex := Defn.typeStr realization
1216 ; FlexibleTycon.pushSpec (flex, region)
1217 ; pushSpec (realization, region))
1218 | SOME (msgs, tyError, rlError) =>
1221 seq [str "type cannot be realized (",
1222 (seq o List.separate) (List.rev msgs, str ", "),
1225 align ((seq [str "type spec: ", tyError]) ::
1227 (specs (tyStr, spec), fn r =>
1228 seq [str "spec at: ", Region.layout r])) @
1229 [seq [str "type defn: ", rlError]]))
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))])],
1242 structure UniqueId = IntUniqueId ()
1244 structure TyconMap =
1246 datatype 'a t = T of {strs: (Strid.t * 'a t) array,
1247 types: (Ast.Tycon.t * 'a) array}
1249 fun layout layoutA =
1252 fun loop (T {strs, types}) =
1254 Array.layout (Layout.tuple2 (Strid.layout, loop)) strs),
1256 Array.layout (Layout.tuple2 (Ast.Tycon.layout, layoutA))
1262 fun empty (): 'a t = T {strs = Array.new0 (),
1263 types = Array.new0 ()}
1265 fun isEmpty (T {strs, types}) =
1266 0 = Array.length strs andalso 0 = Array.length types
1268 fun peekStrid (T {strs, ...}, strid) =
1269 Array.peekMap (strs, fn (strid', z) =>
1270 if Strid.equals (strid, strid')
1274 fun peekTycon (T {types, ...}, tycon) =
1275 Array.peekMap (types, fn (tycon', z) =>
1276 if Ast.Tycon.equals (tycon, tycon')
1282 (*---------------------------------------------------*)
1284 (*---------------------------------------------------*)
1286 datatype t = T of {copy: copy,
1287 flexible: FlexibleTycon.t TyconMap.t option ref,
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
1297 fun dest (T s) = Set.! s
1300 fun make f = f o dest
1302 val plist = make #plist
1306 case #original (dest I) of
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 (),
1318 uniqueId = UniqueId.new (),
1321 val empty = new {isClosed = true,
1323 strs = Array.new0 (),
1324 types = Array.new0 (),
1325 vals = Array.new0 ()}
1332 val {strs, types, uniqueId = u, vals, ...} = Set.! s
1334 record [("uniqueId", UniqueId.layout u),
1336 Array.layout (Layout.tuple2 (Strid.layout, layout)) strs),
1338 Array.layout (Layout.tuple2 (Ast.Tycon.layout, TypeStr.layout))
1341 Array.layout (Layout.tuple2 (Vid.layout,
1342 Layout.tuple2 (Status.layout,
1348 fun equals (T s, T s') = Set.equals (s, s')
1351 Trace.trace2 ("Interface.equals", layout, layout, Bool.layout) equals
1353 fun sameShape (I, I') =
1354 case (#original (dest I), #original (dest I')) of
1355 (SOME I, SOME I') => equals (I, I')
1358 fun peekStrid (T s, strid: Strid.t): t option =
1360 val {strs, ...} = Set.! s
1362 Array.peekMap (strs, fn (strid', I) =>
1363 if Strid.equals (strid, strid')
1368 datatype 'a peekResult =
1370 | UndefinedStructure of Strid.t list
1372 fun peekStrids (I: t, strids: Strid.t list): t peekResult =
1374 fun loop (I, strids, ac) =
1377 | strid :: strids =>
1378 case peekStrid (I, strid) of
1379 NONE => UndefinedStructure (rev (strid :: ac))
1380 | SOME I => loop (I, strids, strid :: ac)
1382 loop (I, strids, [])
1385 fun peekTycon (T s, tycon: Ast.Tycon.t): (Ast.Tycon.t * TypeStr.t) option =
1387 val {types, ...} = Set.! s
1389 Array.peekMap (types, fn (name, typeStr) =>
1390 if Ast.Tycon.equals (tycon, name)
1391 then SOME (name, typeStr)
1395 fun unbound (r: Region.t, className, x: Layout.t): unit =
1399 in seq [str "undefined ", str className, str " ", x]
1403 fun layoutStrids (ss: Strid.t list): Layout.t =
1404 Layout.str (concat (List.separate (List.map (ss, Strid.toString), ".")))
1406 fun lookupLongtycon (I: t, long: Longtycon.t, r: Region.t,
1407 {prefix: Strid.t list}) =
1409 val (ss, c) = Longtycon.split long
1411 case peekStrids (I, ss) of
1413 (case peekTycon (I, c) of
1415 (unbound (r, "type",
1416 Longtycon.layout (Longtycon.long (prefix @ ss, c)))
1418 | SOME (name, s) => SOME (name, s))
1419 | UndefinedStructure ss =>
1420 (unbound (r, "structure", layoutStrids (prefix @ ss))
1424 fun lookupLongstrid (I: t, long: Longstrid.t, r: Region.t,
1425 {prefix: Strid.t list}) =
1427 val (ss, s) = Longstrid.split long
1429 case peekStrids (I, ss) of
1431 (case peekStrid (I, s) of
1433 (unbound (r, "structure",
1434 Longstrid.layout (Longstrid.long (prefix @ ss, s)))
1437 | UndefinedStructure ss =>
1438 (unbound (r, "structure", layoutStrids (prefix @ ss))
1442 fun share {layoutPrettyEnvTycon, layoutPrettyFlexTycon,
1443 I1: t, long1: Longstrid.t, I2: t, long2: Longstrid.t,
1444 time, region}: unit =
1446 fun mkTy (s, long, strids, name) =
1448 val spec = Ast.Tycon.region name
1449 val region = Longstrid.region long
1452 val (ss, s) = Longstrid.split long
1454 Ast.Longtycon.layout
1455 (Ast.Longtycon.long (List.concat [ss, [s], rev strids],
1464 fun ensureFlexible (I: t, strids): unit =
1466 val {get: t -> bool ref, destroy, ...} =
1467 Property.destGet (plist, Property.initFun (fn _ => ref false))
1468 fun loop (I: t, strids): unit =
1478 val {strs, types, ...} = Set.! s
1481 (strs, fn (strid, I) =>
1482 ensureFlexible (I, strid :: strids))
1485 (types, fn (name, s) =>
1486 (ignore o TypeStr.getFlex)
1487 {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1488 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
1491 ty = mkTy (s, long1, strids, name)})
1496 val () = loop (I, strids)
1501 fun share (I1, I2, strids): unit =
1503 then ensureFlexible (I1, strids)
1504 else if sameShape (I1, I2)
1507 fun loop (T s1, T s2, strids): unit =
1509 val {isClosed, strs = strs1, types = types1, ...} = Set.! s1
1510 val {strs = strs2, types = types2, ...} = Set.! s2
1513 (types1, types2, fn ((name, s1), (_, s2)) =>
1515 {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1516 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
1519 ty1 = mkTy (s1, long1, strids, name),
1520 ty2 = mkTy (s2, long2, strids, name)})
1523 (strs1, strs2, fn ((name, I1), (_, I2)) =>
1524 loop (I1, I2, name :: strids))
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
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.
1540 then Set.union (s1, s2)
1546 loop (I1, I2, strids)
1548 else (* different shapes -- need to share pointwise *)
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) =
1556 val n1 = Array.length a1
1557 val n2 = Array.length a2
1559 if i1 < n1 andalso i2 < n2
1560 then compare (i1, Array.sub (a1, i1),
1561 i2, Array.sub (a2, i2))
1563 and compare (i1, (name1, z1), i2, (name2, z2)) =
1564 case compareNames (name1, name2) of
1570 then compare (i1, (name1, z1),
1571 i2, Array.sub (a2, i2))
1574 | EQUAL => (f (z1, z2, name1)
1575 ; both (i1 + 1, i2 + 1))
1581 then compare (i1, Array.sub (a1, i1),
1589 walk2 (strs1, strs2, Strid.compare,
1590 fn (I1, I2, name) => share (I1, I2, name :: strids))
1592 walk2 (types1, types2, Ast.Tycon.compare,
1593 fn (s1, s2, name) =>
1595 {layoutPrettyEnvTycon = layoutPrettyEnvTycon,
1596 layoutPrettyFlexTycon = layoutPrettyFlexTycon,
1599 ty1 = mkTy (s1, long1, strids, name),
1600 ty2 = mkTy (s2, long2, strids, name)})
1611 fn {I1, I2, time, ...} =>
1612 Layout.tuple [layout I1, layout I2, Time.layout time],
1616 fun copy (I: t): t =
1618 (* Keep track of all nodes that have forward pointers to copies, so
1619 * that we can gc them when done.
1621 val copies: copy list ref = ref []
1622 fun loop (I as T s): t =
1624 val r as {copy, ...} = Set.! s
1629 val {isClosed, original, strs, types, vals, ...} = r
1631 Array.map (types, fn (name, typeStr) =>
1632 (name, TypeStr.copy typeStr))
1634 Array.map (vals, fn (name, (status, scheme)) =>
1635 (name, (status, Scheme.copy scheme)))
1637 Array.map (strs, fn (name, I) => (name, loop I))
1639 SOME (case original of
1642 val I = T (Set.singleton {copy = ref NONE,
1643 flexible = ref NONE,
1644 isClosed = isClosed,
1645 original = original,
1646 plist = PropertyList.new (),
1649 uniqueId = UniqueId.new (),
1651 val _ = List.push (copies, copy)
1652 val _ = copy := SOME 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 := []
1667 val copy = Trace.trace ("Interface.copy", layout, layout) copy
1669 fun flexibleTycons (I: t): FlexibleTycon.t TyconMap.t =
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,
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 =
1683 val r = interfaceShortest I
1685 if isSome (!r) andalso length >= valOf (!r)
1686 then TyconMap.empty ()
1689 val _ = r := SOME length
1690 val {strs, types, ...} = dest I
1691 fun setTycon (tycon, isDatatype, isEqtype) =
1693 Tycon.Flexible fc =>
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
1702 case Defn.dest (!defn) of
1705 val r = tyconShortest fc
1708 andalso not isDatatype)
1711 andalso not isEqtype)
1713 (isSome (#length (!r))
1714 andalso length >= valOf (#length (!r)))
1717 val _ = #flex (!r) := NONE
1718 val flex = ref (SOME fc)
1719 val _ = r := {flex = flex,
1720 length = SOME length}
1730 (types, fn (tycon, typeStr) =>
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)
1741 (s, loop (I, 1 + length)))
1743 TyconMap.T {strs = strs, types = types}
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 =
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) =>
1758 if TyconMap.isEmpty m
1763 TyconMap.T {strs = strs, types = types}
1769 val flexibleTycons =
1772 val {flexible, ...} = Set.! s
1777 val f = flexibleTycons I
1778 val _ = flexible := SOME f
1785 val flexibleTycons =
1786 Trace.trace ("Interface.flexibleTycons", layout,
1787 TyconMap.layout FlexibleTycon.layout)
1792 val {strs, types, vals, ...} = Set.! s