Skip to content

Commit 1ace71d

Browse files
authored
Merge pull request #5730 from dotty-staging/realizability-cleanup-doc
Realizability: fixes and cleanups of docs
2 parents a98b901 + b0c8e68 commit 1ace71d

20 files changed

+75
-39
lines changed

compiler/src/dotty/tools/dotc/ast/TreeInfo.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -400,11 +400,11 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
400400
def isKnownPureOp(sym: Symbol) =
401401
sym.owner.isPrimitiveValueClass || sym.owner == defn.StringClass
402402
if (tree.tpe.isInstanceOf[ConstantType] && isKnownPureOp(tree.symbol) // A constant expression with pure arguments is pure.
403-
|| (fn.symbol.isStable && !fn.symbol.is(Lazy))
403+
|| (fn.symbol.isStableMember && !fn.symbol.is(Lazy))
404404
|| fn.symbol.isPrimaryConstructor && fn.symbol.owner.isNoInitsClass) // TODO: include in isStable?
405405
minOf(exprPurity(fn), args.map(exprPurity)) `min` Pure
406406
else if (fn.symbol.is(Erased)) Pure
407-
else if (fn.symbol.isStable /* && fn.symbol.is(Lazy) */)
407+
else if (fn.symbol.isStableMember /* && fn.symbol.is(Lazy) */)
408408
minOf(exprPurity(fn), args.map(exprPurity)) `min` Idempotent
409409
else Impure
410410
case Typed(expr, _) =>
@@ -439,7 +439,7 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
439439
val sym = tree.symbol
440440
if (!tree.hasType) Impure
441441
else if (!tree.tpe.widen.isParameterless || sym.isEffectivelyErased) SimplyPure
442-
else if (!sym.isStable) Impure
442+
else if (!sym.isStableMember) Impure
443443
else if (sym.is(Module))
444444
if (sym.moduleClass.isNoInitsClass) Pure else Idempotent
445445
else if (sym.is(Lazy)) Idempotent
@@ -521,7 +521,7 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
521521
case tpe: PolyType => maybeGetterType(tpe.resultType)
522522
case _ => false
523523
}
524-
sym.owner.isClass && !sym.isStable && maybeGetterType(sym.info)
524+
sym.owner.isClass && !sym.isStableMember && maybeGetterType(sym.info)
525525
}
526526

527527
/** Is tree a reference to a mutable variable, or to a potential getter

compiler/src/dotty/tools/dotc/core/CheckRealizable.scala

Lines changed: 28 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import collection.mutable
1010
/** Realizability status */
1111
object CheckRealizable {
1212

13-
abstract class Realizability(val msg: String) {
13+
sealed abstract class Realizability(val msg: String) {
1414
def andAlso(other: => Realizability): Realizability =
1515
if (this == Realizable) other else this
1616
def mapError(f: Realizability => Realizability): Realizability =
@@ -47,10 +47,18 @@ object CheckRealizable {
4747
def boundsRealizability(tp: Type)(implicit ctx: Context): Realizability =
4848
new CheckRealizable().boundsRealizability(tp)
4949

50-
private val LateInitialized = Lazy | Erased,
50+
private val LateInitialized = Lazy | Erased
5151
}
5252

53-
/** Compute realizability status */
53+
/** Compute realizability status.
54+
*
55+
* A type T is realizable iff it is inhabited by non-null values. This ensures that its type members have good bounds
56+
* (in the sense from DOT papers). A type projection T#L is legal if T is realizable, and can be understood as
57+
* Scala 2's `v.L forSome { val v: T }`.
58+
*
59+
* In general, a realizable type can have multiple inhabitants, hence it need not be stable (in the sense of
60+
* Type.isStable).
61+
*/
5462
class CheckRealizable(implicit ctx: Context) {
5563
import CheckRealizable._
5664

@@ -66,13 +74,22 @@ class CheckRealizable(implicit ctx: Context) {
6674

6775
/** The realizability status of given type `tp`*/
6876
def realizability(tp: Type): Realizability = tp.dealias match {
77+
/*
78+
* A `TermRef` for a path `p` is realizable if
79+
* - `p`'s type is stable and realizable, or
80+
* - its underlying path is idempotent (that is, *stable*), total, and not null.
81+
* We don't check yet the "not null" clause: that will require null-safety checking.
82+
*
83+
* We assume that stability of tp.prefix is checked elsewhere, since that's necessary for the path to be legal in
84+
* the first place.
85+
*/
6986
case tp: TermRef =>
7087
val sym = tp.symbol
7188
lazy val tpInfoRealizable = realizability(tp.info)
72-
if (sym.is(Stable)) realizability(tp.prefix)
89+
if (sym.is(StableRealizable)) realizability(tp.prefix)
7390
else {
7491
val r =
75-
if (sym.isStable && !isLateInitialized(sym))
92+
if (sym.isStableMember && !isLateInitialized(sym))
7693
// it's realizable because we know that a value of type `tp` has been created at run-time
7794
Realizable
7895
else if (!sym.isEffectivelyFinal)
@@ -83,10 +100,14 @@ class CheckRealizable(implicit ctx: Context) {
83100
// roughly: it's realizable if the info does not have bad bounds
84101
tpInfoRealizable.mapError(r => new ProblemInUnderlying(tp, r))
85102
r andAlso {
86-
if (sym.isStable) sym.setFlag(Stable) // it's known to be stable and realizable
103+
if (sym.isStableMember) sym.setFlag(StableRealizable) // it's known to be stable and realizable
87104
realizability(tp.prefix)
88105
} mapError { r =>
89-
if (tp.info.isStable && tpInfoRealizable == Realizable) Realizable else r
106+
// A mutable path is in fact stable and realizable if it has a realizable singleton type.
107+
if (tp.info.isStable && tpInfoRealizable == Realizable) {
108+
sym.setFlag(StableRealizable)
109+
Realizable
110+
} else r
90111
}
91112
}
92113
case _: SingletonType | NoPrefix =>

compiler/src/dotty/tools/dotc/core/Flags.scala

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -329,7 +329,7 @@ object Flags {
329329
final val Abstract: FlagSet = commonFlag(23, "abstract")
330330

331331
/** Lazy val or method is known or assumed to be stable and realizable */
332-
final val Stable: FlagSet = termFlag(24, "<stable>")
332+
final val StableRealizable: FlagSet = termFlag(24, "<stable>")
333333

334334
/** A case parameter accessor */
335335
final val CaseAccessor: FlagSet = termFlag(25, "<caseaccessor>")
@@ -509,7 +509,7 @@ object Flags {
509509
final val RetainedTypeArgFlags: FlagSet = VarianceFlags | Protected | Local
510510

511511
/** Modules always have these flags set */
512-
final val ModuleValCreationFlags: FlagSet = ModuleVal | Lazy | Final | Stable
512+
final val ModuleValCreationFlags: FlagSet = ModuleVal | Lazy | Final | StableRealizable
513513

514514
/** Module classes always have these flags set */
515515
final val ModuleClassCreationFlags: FlagSet = ModuleClass | Final
@@ -540,7 +540,7 @@ object Flags {
540540
/** Flags that can apply to a module val */
541541
final val RetainedModuleValFlags: FlagSet = RetainedModuleValAndClassFlags |
542542
Override | Final | Method | Implicit | Lazy |
543-
Accessor | AbsOverride | Stable | Captured | Synchronized | Erased
543+
Accessor | AbsOverride | StableRealizable | Captured | Synchronized | Erased
544544

545545
/** Flags that can apply to a module class */
546546
final val RetainedModuleClassFlags: FlagSet = RetainedModuleValAndClassFlags |
@@ -585,7 +585,7 @@ object Flags {
585585
final val InlineOrProxy: FlagSet = Inline | InlineProxy
586586

587587
/** Assumed to be pure */
588-
final val StableOrErased: FlagSet = Stable | Erased
588+
final val StableOrErased: FlagSet = StableRealizable | Erased
589589

590590
/** Labeled `private`, `final`, or `inline` */
591591
final val EffectivelyFinal: FlagSet = Private | Final | Inline
@@ -678,7 +678,7 @@ object Flags {
678678
final val JavaEnumTrait: FlagConjunction = allOf(JavaDefined, Enum)
679679

680680
/** A Java enum value */
681-
final val JavaEnumValue: FlagConjunction = allOf(Stable, JavaStatic, JavaDefined, Enum)
681+
final val JavaEnumValue: FlagConjunction = allOf(StableRealizable, JavaStatic, JavaDefined, Enum)
682682

683683
/** Labeled private[this] */
684684
final val PrivateLocal: FlagConjunction = allOf(Private, Local)
@@ -687,7 +687,7 @@ object Flags {
687687
final val PrivateLocalParamAccessor: FlagConjunction = allOf(Private, Local, ParamAccessor)
688688

689689
/** A parameter forwarder */
690-
final val ParamForwarder: FlagConjunction = allOf(Method, Stable, ParamAccessor)
690+
final val ParamForwarder: FlagConjunction = allOf(Method, StableRealizable, ParamAccessor)
691691

692692
/** A private[this] parameter */
693693
final val PrivateLocalParam: FlagConjunction = allOf(Private, Local, Param)

compiler/src/dotty/tools/dotc/core/SymDenotations.scala

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -608,10 +608,19 @@ object SymDenotations {
608608
}
609609
)
610610

611-
/** Is this a denotation of a stable term (or an arbitrary type)? */
612-
final def isStable(implicit ctx: Context): Boolean = {
611+
/** Is this a denotation of a stable term (or an arbitrary type)?
612+
* Terms are stable if they are idempotent (as in TreeInfo.Idempotent): that is, they always return the same value,
613+
* if any.
614+
*
615+
* A *member* is stable, basically, if it behaves like a field projection: that is, it projects a constant result
616+
* out of its owner.
617+
*
618+
* However, a stable member might not yet be initialized (if it is an object or anyhow lazy).
619+
* So the first call to a stable member might fail and/or produce side effects.
620+
*/
621+
final def isStableMember(implicit ctx: Context): Boolean = {
613622
def isUnstableValue = is(UnstableValue) || info.isInstanceOf[ExprType]
614-
isType || is(Stable) || !isUnstableValue
623+
isType || is(StableRealizable) || !isUnstableValue
615624
}
616625

617626
/** Is this a denotation of a class that does not have - either direct or inherited -

compiler/src/dotty/tools/dotc/core/Types.scala

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -147,9 +147,13 @@ object Types {
147147
/** Is this a value type or a wildcard? */
148148
final def isValueTypeOrWildcard: Boolean = isValueType || this.isInstanceOf[WildcardType]
149149

150-
/** Does this type denote a stable reference (i.e. singleton type)? */
150+
/** Does this type denote a stable reference (i.e. singleton type)?
151+
*
152+
* Like in isStableMember, "stability" means idempotence.
153+
* Rationale: If an expression has a stable type, the expression must be idempotent, so stable types
154+
* must be singleton types of stable expressions. */
151155
final def isStable(implicit ctx: Context): Boolean = stripTypeVar match {
152-
case tp: TermRef => tp.symbol.isStable && tp.prefix.isStable || tp.info.isStable
156+
case tp: TermRef => tp.symbol.isStableMember && tp.prefix.isStable || tp.info.isStable
153157
case _: SingletonType | NoPrefix => true
154158
case tp: RefinedOrRecType => tp.parent.isStable
155159
case tp: ExprType => tp.resultType.isStable
@@ -542,7 +546,7 @@ object Types {
542546
case tp: TermRef =>
543547
go (tp.underlying match {
544548
case mt: MethodType
545-
if mt.paramInfos.isEmpty && (tp.symbol is Stable) => mt.resultType
549+
if mt.paramInfos.isEmpty && (tp.symbol is StableRealizable) => mt.resultType
546550
case tp1 => tp1
547551
})
548552
case tp: TypeRef =>
@@ -1005,7 +1009,7 @@ object Types {
10051009
/** Widen type if it is unstable (i.e. an ExprType, or TermRef to unstable symbol */
10061010
final def widenIfUnstable(implicit ctx: Context): Type = stripTypeVar match {
10071011
case tp: ExprType => tp.resultType.widenIfUnstable
1008-
case tp: TermRef if !tp.symbol.isStable => tp.underlying.widenIfUnstable
1012+
case tp: TermRef if !tp.symbol.isStableMember => tp.underlying.widenIfUnstable
10091013
case _ => this
10101014
}
10111015

@@ -2200,6 +2204,8 @@ object Types {
22002204
def underlyingRef: TermRef
22012205
}
22022206

2207+
/** The singleton type for path prefix#myDesignator.
2208+
*/
22032209
abstract case class TermRef(override val prefix: Type,
22042210
private var myDesignator: Designator)
22052211
extends NamedType with SingletonType with ImplicitRef {

compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -653,7 +653,7 @@ class TreePickler(pickler: TastyPickler) {
653653
if (flags is Accessor) writeByte(FIELDaccessor)
654654
if (flags is CaseAccessor) writeByte(CASEaccessor)
655655
if (flags is DefaultParameterized) writeByte(DEFAULTparameterized)
656-
if (flags is Stable) writeByte(STABLE)
656+
if (flags is StableRealizable) writeByte(STABLE)
657657
if (flags is Extension) writeByte(EXTENSION)
658658
if (flags is ParamAccessor) writeByte(PARAMsetter)
659659
assert(!(flags is Label))

compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -626,7 +626,7 @@ class TreeUnpickler(reader: TastyReader,
626626
case CONTRAVARIANT => addFlag(Contravariant)
627627
case SCALA2X => addFlag(Scala2x)
628628
case DEFAULTparameterized => addFlag(DefaultParameterized)
629-
case STABLE => addFlag(Stable)
629+
case STABLE => addFlag(StableRealizable)
630630
case EXTENSION => addFlag(Extension)
631631
case PARAMsetter =>
632632
addFlag(ParamAccessor)

compiler/src/dotty/tools/dotc/core/unpickleScala2/PickleBuffer.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@ object PickleBuffer {
218218
LOCAL -> Local,
219219
JAVA -> JavaDefined,
220220
SYNTHETIC -> Synthetic,
221-
STABLE -> Stable,
221+
STABLE -> StableRealizable,
222222
STATIC -> JavaStatic,
223223
CASEACCESSOR -> CaseAccessor,
224224
DEFAULTPARAM -> (DefaultParameterized, Trait),

compiler/src/dotty/tools/dotc/interactive/Completion.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ object Completion {
260260
!sym.is(Artifact) &&
261261
(
262262
(mode.is(Mode.Term) && sym.isTerm)
263-
|| (mode.is(Mode.Type) && (sym.isType || sym.isStable))
263+
|| (mode.is(Mode.Type) && (sym.isType || sym.isStableMember))
264264
)
265265

266266
/**

compiler/src/dotty/tools/dotc/parsing/JavaParsers.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -858,7 +858,7 @@ object JavaParsers {
858858
skipAhead()
859859
accept(RBRACE)
860860
}
861-
ValDef(name.toTermName, enumType, unimplementedExpr).withMods(Modifiers(Flags.JavaEnum | Flags.Stable | Flags.JavaDefined | Flags.JavaStatic))
861+
ValDef(name.toTermName, enumType, unimplementedExpr).withMods(Modifiers(Flags.JavaEnum | Flags.StableRealizable | Flags.JavaDefined | Flags.JavaStatic))
862862
}
863863
}
864864

0 commit comments

Comments
 (0)