diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index b451242d410d..2f5b7eb96a13 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -441,11 +441,13 @@ object Capabilities: /** An exclusive capability is a capability that derives * indirectly from a maximal capability without going through * a read-only capability or a capability classified as SharedCapability first. + * @param required if true, exclusivity can be obtained by setting the mutability + * status of some capture set variable from Ignored to Writer. */ - final def isExclusive(using Context): Boolean = + final def isExclusive(required: Boolean = false)(using Context): Boolean = !isReadOnly && !classifier.derivesFrom(defn.Caps_SharedCapability) - && (isTerminalCapability || captureSetOfInfo.isExclusive) + && (isTerminalCapability || captureSetOfInfo.isExclusive(required)) /** Similar to isExlusive, but also includes capabilties with capture * set variables in their info whose status is still open. @@ -564,8 +566,9 @@ object Capabilities: case _ => false def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability) - def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable) + def derivesFromStateful(using Context): Boolean = derivesFromCapTrait(defn.Caps_Stateful) def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability) + def derivesFromUnscoped(using Context): Boolean = derivesFromCapTrait(defn.Caps_Unscoped) /** The capture set consisting of exactly this reference */ def singletonCaptureSet(using Context): CaptureSet.Const = @@ -924,7 +927,7 @@ object Capabilities: * Unclassified : No set exists since some parts of tcs are not classified * ClassifiedAs(clss: All parts of tcss are classified with classes in clss */ - enum Classifiers: + enum Classifiers derives CanEqual: case UnknownClassifier case Unclassified case ClassifiedAs(clss: List[ClassSymbol]) @@ -965,7 +968,7 @@ object Capabilities: /** The place of - and cause for - creating a fresh capability. Used for * error diagnostics */ - enum Origin: + enum Origin derives CanEqual: case InDecl(sym: Symbol) case TypeArg(tp: Type) case UnsafeAssumePure diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index fd6451a01e37..c98f4392eea5 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -13,7 +13,7 @@ import tpd.* import Annotations.Annotation import CaptureSet.VarState import Capabilities.* -import Mutability.isMutableType +import Mutability.isStatefulType import StdNames.nme import config.Feature import NameKinds.TryOwnerName @@ -395,9 +395,9 @@ extension (tp: Type) false def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability) - def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable) + def derivesFromStateful(using Context): Boolean = derivesFromCapTrait(defn.Caps_Stateful) def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability) - def derivesFromExclusive(using Context): Boolean = derivesFromCapTrait(defn.Caps_ExclusiveCapability) + def derivesFromUnscoped(using Context): Boolean = derivesFromCapTrait(defn.Caps_Unscoped) /** Drop @retains annotations everywhere */ def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling @@ -531,7 +531,11 @@ extension (cls: ClassSymbol) else defn.AnyClass def isSeparate(using Context): Boolean = - cls.typeRef.isMutableType + cls.derivesFrom(defn.Caps_Separate) + || cls.typeRef.isStatefulType + || cls.paramGetters.exists: getter => + !getter.is(Private) // Setup makes sure that getters with capture sets are not private + && getter.hasAnnotation(defn.ConsumeAnnot) extension (sym: Symbol) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 903553214936..ee94d9bf1d31 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -59,15 +59,15 @@ sealed abstract class CaptureSet extends Showable: def mutability_=(x: Mutability): Unit = myMut = x - /** Mark this capture set as belonging to a Mutable type. Called when a new + /** Mark this capture set as belonging to a Stateful type. Called when a new * CapturingType is formed. This is different from the setter `mutability_=` - * in that it be defined with different behaviors: + * in that it can be defined with different behaviors: * - * - set mutability to Mutable (for normal Vars) + * - set mutability to Writer (for normal Vars) * - take mutability from the set's sources (for DerivedVars) * - compute mutability on demand based on mutability of elements (for Consts) */ - def associateWithMutable()(using Context): CaptureSet + def associateWithStateful()(using Context): CaptureSet /** Is this capture set constant (i.e. not an unsolved capture variable)? * Solved capture variables count as constant. @@ -148,15 +148,27 @@ sealed abstract class CaptureSet extends Showable: final def isAlwaysReadOnly(using Context): Boolean = isConst && isReadOnly - final def isExclusive(using Context): Boolean = - elems.exists(_.isExclusive) + /** Is capture set exclusive? If `required` is true, a variable capture set + * is forced to Writer mutability which makes it exclusive. Otherwise a set + * is exclusive if one of its elements is exclusive. + * Possible issue: If required is true, and the set is a constant, with + * multiple elements that each have a variable capture set, then we make + * the set exclusive by updating the first such variable capture set with + * Ignore mutability to have Write mutability. That makes the effect + * order dependent. + */ + def isExclusive(required: Boolean = false)(using Context): Boolean = + if required && !isConst && mutability == Ignored then + mutability = Writer + mutability == Writer + || elems.exists(_.isExclusive(required)) /** Similar to isExclusive, but also includes capture set variables * with unknown status. */ final def maybeExclusive(using Context): Boolean = reporting.trace(i"mabe exclusive $this"): if isConst then elems.exists(_.maybeExclusive) - else mutability != ReadOnly + else mutability != Reader final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance] @@ -191,7 +203,7 @@ sealed abstract class CaptureSet extends Showable: newElems.forall(tryInclude(_, origin)) protected def mutableToReader(origin: CaptureSet)(using Context): Boolean = - if mutability == Mutable then toReader() else true + if mutability == Writer then toReader() else true /** Add an element to this capture set, assuming it is not already accounted for, * and omitting any mapping or filtering. @@ -315,8 +327,8 @@ sealed abstract class CaptureSet extends Showable: def adaptMutability(that: CaptureSet)(using Context): CaptureSet | Null = val m1 = this.mutability val m2 = that.mutability - if m1 == Mutable && m2 == Reader then this.readOnly - else if m1 == Reader && m2 == Mutable then + if m1 == Writer && m2 == Reader then this.readOnly + else if m1 == Reader && m2 == Writer then if that.toReader() then this else null else this @@ -541,14 +553,14 @@ object CaptureSet: type Vars = SimpleIdentitySet[Var] type Deps = SimpleIdentitySet[CaptureSet] - enum Mutability: - case Mutable, Reader, Ignored + enum Mutability derives CanEqual: + case Writer, Reader, Ignored def | (that: Mutability): Mutability = if this == that then this else if this == Ignored || that == Ignored then Ignored else if this == Reader || that == Reader then Reader - else Mutable + else Writer def & (that: Mutability): Mutability = if this == that then this @@ -569,9 +581,9 @@ object CaptureSet: @sharable // sharable since the set is empty, so mutability won't be set val empty: CaptureSet.Const = Const(emptyRefs) - /** The empty capture set `{}` of a Mutable type, with Reader status */ - @sharable // sharable since the set is empty, so mutability won't be set - val emptyOfMutable: CaptureSet.Const = + /** The empty capture set `{}` of a Stateful type, with Reader status */ + @sharable // sharable since the set is empty, so mutability won't be re-set + val emptyOfStateful: CaptureSet.Const = val cs = Const(emptyRefs) cs.mutability = Mutability.Reader cs @@ -630,15 +642,15 @@ object CaptureSet: private var isComplete = true - def associateWithMutable()(using Context): CaptureSet = - if elems.isEmpty then emptyOfMutable + def associateWithStateful()(using Context): CaptureSet = + if elems.isEmpty then emptyOfStateful else isComplete = false // delay computation of Mutability status this override def mutability(using Context): Mutability = if !isComplete then - myMut = if maybeExclusive then Mutable else Reader + myMut = if maybeExclusive then Writer else Reader isComplete = true myMut @@ -652,7 +664,7 @@ object CaptureSet: else "" private def capImpliedByCapability(parent: Type)(using Context): Capability = - if parent.derivesFromMutable then GlobalCap.readOnly else GlobalCap + if parent.derivesFromStateful then GlobalCap.readOnly else GlobalCap /* The same as {cap} but generated implicitly for references of Capability subtypes. */ @@ -665,13 +677,14 @@ object CaptureSet: * nulls, this provides more lenient checking against compilation units that * were not yet compiled with capture checking on. */ - @sharable // sharable since the set is empty, so setMutable is a no-op + @sharable object Fluid extends Const(emptyRefs): override def isAlwaysEmpty(using Context) = false override def addThisElem(elem: Capability)(using Context, VarState) = true override def toReader()(using Context) = true override def accountsFor(x: Capability)(using Context)(using VarState): Boolean = true override def mightAccountFor(x: Capability)(using Context): Boolean = true + override def mutability_=(x: Mutability): Unit = () override def toString = "" end Fluid @@ -727,8 +740,8 @@ object CaptureSet: */ var deps: Deps = SimpleIdentitySet.empty - def associateWithMutable()(using Context): CaptureSet = - mutability = Mutable + def associateWithStateful()(using Context): CaptureSet = + mutability = Writer this def isConst(using Context) = solved >= ccState.iterationId @@ -846,7 +859,7 @@ object CaptureSet: if isConst then failWith(MutAdaptFailure(this)) else mutability = Reader - TypeComparer.logUndoAction(() => mutability = Mutable) + TypeComparer.logUndoAction(() => mutability = Writer) deps.forall(_.mutableToReader(this)) private def isPartOf(binder: Type)(using Context): Boolean = @@ -933,7 +946,7 @@ object CaptureSet: def markSolved(provisional: Boolean)(using Context): Unit = solved = if provisional then ccState.iterationId else Int.MaxValue deps.foreach(_.propagateSolved(provisional)) - if mutability == Mutable && !maybeExclusive then mutability = Reader + if mutability == Writer && !maybeExclusive then mutability = Reader var skippedMaps: Set[TypeMap] = Set.empty @@ -1046,7 +1059,7 @@ object CaptureSet: addAsDependentTo(source) /** Mutability is same as in source, except for readOnly */ - override def associateWithMutable()(using Context): CaptureSet = this + override def associateWithStateful()(using Context): CaptureSet = this override def mutableToReader(origin: CaptureSet)(using Context): Boolean = super.mutableToReader(origin) @@ -1175,8 +1188,8 @@ object CaptureSet: super.mutableToReader(origin) && { if (origin eq cs1) || (origin eq cs2) then true - else if cs1.isConst && cs1.mutability == Mutable then cs2.mutableToReader(this) - else if cs2.isConst && cs2.mutability == Mutable then cs1.mutableToReader(this) + else if cs1.isConst && cs1.mutability == Writer then cs2.mutableToReader(this) + else if cs2.isConst && cs2.mutability == Writer then cs1.mutableToReader(this) else true } @@ -1403,7 +1416,7 @@ object CaptureSet: else i"$elem cannot be included in $cs" end IncludeFailure - /** Failure indicating that a read-only capture set of a mutable type cannot be + /** Failure indicating that a read-only capture set of a stateful type cannot be * widened to an exclusive set. * @param cs the exclusive set in question * @param lo the lower type of the orginal type comparison, or NoType if not known @@ -1412,7 +1425,7 @@ object CaptureSet: case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends Note: def render(using Context): String = - def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type" + def ofType(tp: Type) = if tp.exists then i"of the stateful type $tp" else "of a stateful type" i""" | |Note that $cs is an exclusive capture set ${ofType(hi)}, diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index 879ffc368280..be8bccdcdaf1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -41,7 +41,7 @@ object CapturingType: apply(parent1, refs ++ refs1, boxed) case _ => val refs1 = - if parent.derivesFromMutable then refs.associateWithMutable() else refs + if parent.derivesFromStateful then refs.associateWithStateful() else refs refs1.adoptClassifier(parent.inheritedClassifier) AnnotatedType(parent, CaptureAnnotation(refs1, boxed)(defn.RetainsAnnot)) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 9ddcb7cce332..92d32849da40 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -40,7 +40,7 @@ object CheckCaptures: val name: String = "cc" val description: String = "capture checking" - enum EnvKind: + enum EnvKind derives CanEqual: case Regular // normal case case NestedInOwner // environment is a temporary one nested in the owner's environment, // and does not have a different actual owner symbol @@ -572,7 +572,7 @@ class CheckCaptures extends Recheck, SymTransformer: def checkReadOnlyMethod(included: CaptureSet, meth: Symbol): Unit = included.checkAddedElems: elem => - if elem.isExclusive then + if elem.isExclusive() then report.error( em"""Read-only $meth accesses exclusive capability $elem; |$meth should be declared an update method to allow this.""", @@ -597,7 +597,7 @@ class CheckCaptures extends Recheck, SymTransformer: if nextEnv != null && !nextEnv.owner.isStaticOwner then if nextEnv.owner != env.owner && env.owner.isReadOnlyMember - && env.owner.owner.derivesFrom(defn.Caps_Mutable) + && env.owner.owner.derivesFrom(defn.Caps_Stateful) then checkReadOnlyMethod(included, env.owner) recur(included, nextEnv, env) @@ -864,6 +864,7 @@ class CheckCaptures extends Recheck, SymTransformer: && !resultType.isBoxedCapturing && !tree.fun.symbol.isConstructor && !resultType.captureSet.containsResultCapability + && !resultType.captureSet.elems.exists(_.derivesFromUnscoped) && qualCaptures.mightSubcapture(refs) && argCaptures.forall(_.mightSubcapture(refs)) => val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _) @@ -961,7 +962,7 @@ class CheckCaptures extends Recheck, SymTransformer: /** The additional capture set implied by the capture sets of its fields. This * is either empty or, if some fields have a terminal capability in their span * capture sets, it consists of a single fresh cap that subsumes all these terminal - * capabiltities. Class parameters are not counted. If the type is a mutable type, + * capabiltities. Class parameters are not counted. If the type externds Separate, * we add a fresh cap in any case -- this is because we can currently hide * mutability in array vals, an example is neg-customargs/captures/matrix.scala. */ @@ -980,8 +981,6 @@ class CheckCaptures extends Recheck, SymTransformer: def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match case cls: ClassSymbol => var fieldClassifiers = knownFields(cls).flatMap(classifiersOfFreshInType) - if cls.typeRef.isMutableType then - fieldClassifiers = cls.classifier :: fieldClassifiers val parentClassifiers = cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) if fieldClassifiers.isEmpty && parentClassifiers.isEmpty @@ -1166,10 +1165,10 @@ class CheckCaptures extends Recheck, SymTransformer: tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) if ccConfig.noUnsafeMutableFields && sym.owner.isClass - && !sym.owner.derivesFrom(defn.Caps_Mutable) + && !sym.owner.derivesFrom(defn.Caps_Stateful) && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then report.error( - em"""Mutable $sym is defined in a class that does not extend `Mutable`. + em"""Mutable $sym is defined in a class that does not extend `Stateful`. |The variable needs to be annotated with `untrackedCaptures` to allow this.""", tree.namePos) @@ -1385,14 +1384,6 @@ class CheckCaptures extends Recheck, SymTransformer: * type arguments. Charge deep capture sets of type arguments to non-reserved typevars * to the environment. Other generic parents are represented as TypeApplys, where the * same check is already done in the TypeApply. - * 6. Consume parameters are only allowed for classes producing a fresh cap - * for their constructor, and they don't contribute to the capture set. Example: - * - * class A(consume val x: B^) extends caps.Separate - * val a = A(b) - * - * Here, `a` is of type A{val x: B^}^, and the outer `^` does not hide `b`. - * That's necessary since we would otherwise get consume/use conflicts on `b`. */ override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type = if Feature.enabled(Feature.separationChecking) then sepChecksEnabled = true @@ -1437,28 +1428,6 @@ class CheckCaptures extends Recheck, SymTransformer: markFreeTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_))) case _ => - // (6) Check that consume parameters are covered by an implied FreshCap - for getter <- cls.paramGetters do - if !getter.is(Private) // Setup makes sure that getters with capture sets are not private - && getter.hasAnnotation(defn.ConsumeAnnot) - then - val implied = captureSetImpliedByFields(cls, cls.appliedRef) - val getterCS = getter.info.captureSet - - val hasCoveringFresh = implied.elems.exists: - case fresh: FreshCap => - getterCS.elems.forall: elem => - given VarState = VarState.Unrecorded // make sure we don't add to fresh's hidden set - fresh.maxSubsumes(elem, canAddHidden = true) - case _ => - false - - if !hasCoveringFresh then - report.error( - em"""A consume parameter is only allowed for classes producing a `cap` in their constructor. - |This can be achieved by having the class extend caps.Separate.""", - getter.srcPos) - super.recheckClassDef(tree, impl, cls) finally completed += cls @@ -1867,7 +1836,7 @@ class CheckCaptures extends Recheck, SymTransformer: if needsAdaptation && !insertBox then // we are unboxing val criticalSet = // the set with which we unbox if covariant then - if expected.expectsReadOnly && actual.derivesFromMutable + if expected.expectsReadOnly && actual.derivesFromStateful then captures.readOnly else captures else expected.captureSet // contravarant: we unbox with captures of epected type @@ -2242,29 +2211,28 @@ class CheckCaptures extends Recheck, SymTransformer: end for end checkEscapingUses - /** Check all parent class constructors of classes extending Mutable - * either also extend Mutable or are read-only. + /** Check all parent class constructors of classes extending Stateful + * either also extend Stateful or are read-only. * * A parent class constructor is _read-only_ if the following conditions are met * 1. The class does not retain any exclusive capabilities from its environment. * 2. The constructor does not take arguments that retain exclusive capabilities. * 3. The class does not does not have fields that retain exclusive universal capabilities. */ - def checkMutableInheritance(cls: ClassSymbol, parents: List[Tree])(using Context): Unit = - if cls.derivesFrom(defn.Caps_Mutable) then + def checkStatefulInheritance(cls: ClassSymbol, parents: List[Tree])(using Context): Unit = + if cls.derivesFrom(defn.Caps_Stateful) then for parent <- parents do - if !parent.tpe.derivesFromMutable then + if !parent.tpe.derivesFromStateful then val pcls = parent.nuType.classSymbol val parentIsExclusive = if parent.isType then - capturedVars(pcls).isExclusive - || captureSetImpliedByFields(pcls.asClass, parent.nuType).isExclusive - - else parent.nuType.captureSet.isExclusive + capturedVars(pcls).isExclusive() + || captureSetImpliedByFields(pcls.asClass, parent.nuType).isExclusive() + else parent.nuType.captureSet.isExclusive() if parentIsExclusive then report.error( - em"""illegal inheritance: $cls which extends `Mutable` is not allowed to also extend $pcls - |since $pcls retains exclusive capabilities but does not extend `Mutable`.""", + em"""illegal inheritance: $cls which extends `Stateful` is not allowed to also extend $pcls + |since $pcls retains exclusive capabilities but does not extend `Stateful`.""", parent.srcPos) /** Checks to run after the rechecking pass: @@ -2272,8 +2240,8 @@ class CheckCaptures extends Recheck, SymTransformer: * - Check that no uses refer to reach capabilities of parameters of enclosing * methods or classes. * - Run the separation checker under language.experimental.separationChecking - * - Check that classes extending Mutable do not extend other classes that do - * not extend Mutable yet retain exclusive capabilities + * - Check that classes extending Stateful do not extend other classes that do + * not extend Stateful yet retain exclusive capabilities */ def postCheck(unit: tpd.Tree)(using Context): Unit = val checker = new TreeTraverser: @@ -2298,7 +2266,7 @@ class CheckCaptures extends Recheck, SymTransformer: args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol)) case _ => case TypeDef(_, impl: Template) => - checkMutableInheritance(tree.symbol.asClass, impl.parents) + checkStatefulInheritance(tree.symbol.asClass, impl.parents) case _ => end checker diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 200862e0668a..4869ced36c7c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -15,7 +15,7 @@ import typer.ProtoTypes.LhsProto object Mutability: /** Either OK, or a reason why capture set cannot be exclusive */ - private enum Exclusivity: + private enum Exclusivity derives CanEqual: case OK /** Enclosing symbol `sym` is a method of class `cls`, but not an update method */ @@ -48,13 +48,13 @@ object Mutability: extension (sym: Symbol) /** An update method is either a method marked with `update` or a setter - * of a field of a Mutable class that's not annotated with @uncheckedCaptures. - * `update` is implicit for `consume` methods of Mutable classes. + * of a field of a Stateful class that's not annotated with @uncheckedCaptures. + * `update` is implicit for `consume` methods of Stateful classes. */ def isUpdateMethod(using Context): Boolean = sym.isAllOf(Mutable | Method) && (if sym.isSetter then - sym.owner.derivesFrom(defn.Caps_Mutable) + sym.owner.derivesFrom(defn.Caps_Stateful) && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot) else true ) @@ -74,55 +74,59 @@ object Mutability: else sym.owner.inExclusivePartOf(cls) extension (tp: Type) - /** Is this a type extending `Mutable` that has non-private update methods + /** Is this a type extending `Stateful` that has non-private update methods * or mutable fields? */ - def isMutableType(using Context): Boolean = - tp.derivesFrom(defn.Caps_Mutable) + def isStatefulType(using Context): Boolean = + tp.derivesFrom(defn.Caps_Stateful) && tp.membersBasedOnFlags(Mutable, EmptyFlags).exists: mbr => if mbr.symbol.is(Method) then mbr.symbol.isUpdateMethod else !mbr.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) - /** OK, except if `tp` extends `Mutable` but `tp`'s capture set is non-exclusive */ - private def exclusivity(using Context): Exclusivity = - if tp.derivesFrom(defn.Caps_Mutable) then + /** OK, except if `tp` extends `Stateful` but `tp`'s capture set is non-exclusive + * @param required if true, exclusivity can be obtained by setting the mutability + * status of some capture set variable from Ignored to Writer. + */ + private def exclusivity(required: Boolean)(using Context): Exclusivity = + if tp.derivesFrom(defn.Caps_Stateful) then tp match - case tp: Capability if tp.isExclusive => Exclusivity.OK - case _ => tp.captureSet.exclusivity(tp) + case tp: Capability if tp.isExclusive(required) => Exclusivity.OK + case _ => + if tp.captureSet.isExclusive(required) then Exclusivity.OK + else Exclusivity.ReadOnly(tp) else Exclusivity.OK - /** Test conditions (1) and (2) listed in `adaptReadOnly` below */ - private def exclusivityInContext(using Context): Exclusivity = tp match + /** Test conditions (1) and (2) listed in `adaptReadOnly` below + * @param required if true, exclusivity can be obtained by setting the mutability + * status of some capture set variable from Ignored to Writer. + */ + private def exclusivityInContext(required: Boolean = false)(using Context): Exclusivity = tp match case tp: ThisType => - if tp.derivesFrom(defn.Caps_Mutable) + if tp.derivesFrom(defn.Caps_Stateful) then ctx.owner.inExclusivePartOf(tp.cls) else Exclusivity.OK case tp @ TermRef(prefix: Capability, _) => - prefix.exclusivityInContext.andAlso(tp.exclusivity) + prefix.exclusivityInContext(required).andAlso(tp.exclusivity(required)) case _ => - tp.exclusivity + tp.exclusivity(required) def expectsReadOnly(using Context): Boolean = tp match case tp: PathSelectionProto => tp.selector.isReadOnlyMember || tp.selector.isMutableVar && tp.pt != LhsProto case _ => tp.isValueType - && (!tp.isMutableType || tp.captureSet.mutability == CaptureSet.Mutability.Reader) - - extension (cs: CaptureSet) - private def exclusivity(tp: Type)(using Context): Exclusivity = - if cs.isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp) + && (!tp.isStatefulType || tp.captureSet.mutability == CaptureSet.Mutability.Reader) extension (ref: TermRef | ThisType) /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the * following is true: * - it appears in a non-exclusive context, - * - the expected type is a value type that is not a mutable type, + * - the expected type is a value type that is not a stateful type, * - the expected type is a read-only selection */ def adjustReadOnly(pt: Type)(using Context): Capability = { - if ref.derivesFromMutable - && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK) + if ref.derivesFromStateful + && (pt.expectsReadOnly || ref.exclusivityInContext() != Exclusivity.OK) then ref.readOnly else ref }.showing(i"Adjust RO $ref vs $pt = $result", capt) @@ -131,14 +135,14 @@ object Mutability: * of a field of `qualType`. */ def checkUpdate(qualType: Type, pos: SrcPos)(msg: => String)(using Context): Unit = - qualType.exclusivityInContext match + qualType.exclusivityInContext(required = true) match case Exclusivity.OK => case err => report.error(em"$msg\nsince ${err.description(qualType)}.", pos) /** Perform step (3) of adaptReadOnly below. * - * If actual is a capturing type T^C extending Mutable, and expected is an + * If actual is a capturing type T^C extending Stateful, and expected is an * unboxed non-singleton value type not extending mutable, widen the capture * set `C` to `ro(C).reader`. * The unboxed condition ensures that the expected type is not a type variable @@ -151,9 +155,9 @@ object Mutability: case actual @ CapturingType(parent, refs) => val parent1 = adaptReadOnlyToExpected(parent, expected) val refs1 = - if parent1.derivesFrom(defn.Caps_Mutable) + if parent1.derivesFrom(defn.Caps_Stateful) && expected.isValueType - && (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly) + && (!expected.derivesFromStateful || expected.captureSet.isAlwaysReadOnly) && !expected.isSingleton then refs.readOnly else refs @@ -223,23 +227,23 @@ object Mutability: /** Adapt type `actual` so that it represents a read-only access * if needed. `actual` is the widened version of original with capture - * set improved by the VAR rule. The conditions for adaptation are - * as follows (see modularity.md, section "Read-Only Accesses" for context) - * 1. The `original` reference is a `this` of a type extending Mutable and + * set improved by the VAR rule. One of the following conditions must hold for + * adaptions to be applied (see modularity.md, section "Read-Only Accesses" for context): + * 1. The `original` reference is a `this` of a type extending Stateful and * the access is not from an update method of the class of `this`. - * 2. The `original` reference refers to a type extending Mutable and is a path + * 2. The `original` reference refers to a type extending Stateful and is a path * where a prefix of that path has a read-only capture set. * 3. The expected type corresponding to some part of `actual` that refers - * to a type extending Mutable is a value type that is not a mutable type. + * to a type extending Stateful is a value type that is not a stateful type. * In that case this part is adapted to a read-only capture set. */ def adaptReadOnly(actual: Type, original: Type, expected: Type, tree: Tree)(using Context): Type = adaptReadOnlyToExpected(actual, expected) match case improved @ CapturingType(parent, refs) - if parent.derivesFrom(defn.Caps_Mutable) + if parent.derivesFrom(defn.Caps_Stateful) && expected.isValueType - && refs.isExclusive - && !original.exclusivityInContext.isOK => + && refs.isExclusive() + && !original.exclusivityInContext().isOK => improved.derivedCapturingType(parent, refs.readOnly) .showing(i"Adapted readonly $improved for $tree with original = $original in ${ctx.owner} --> $result", capt) case improved => diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 7442b44cf07f..092925b61378 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -31,7 +31,7 @@ import Capabilities.* object SepCheck: /** Enumerates kinds of captures encountered so far */ - enum Captures: + enum Captures derives CanEqual: case None case Explicit // one or more explicitly declared captures case Hidden // exacttly one hidden captures @@ -45,7 +45,7 @@ object SepCheck: end Captures /** The role in which a checked type appears, used for composing error messages */ - enum TypeRole: + enum TypeRole derives CanEqual: case Result(sym: Symbol, inferred: Boolean) case Argument(arg: Tree, meth: Symbol) case Qualifier(qual: Tree, meth: Symbol) @@ -260,7 +260,7 @@ object SepCheck: */ def common(refs1: Refs, refs2: Refs) = refs1.filter: ref => - ref.isExclusive && refs2.exists(_.stripReadOnly.covers(ref)) + ref.isExclusive() && refs2.exists(_.stripReadOnly.covers(ref)) ++ refs1 .filter: diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 61956cd25ca7..5c8c581f729c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -954,8 +954,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: recur(cs1) case Nil => recur(cls.baseClasses.filter(_.isClassifiedCapabilityClass).distinct) - if cls.derivesFrom(defn.Caps_SharedCapability) && cls.derivesFrom(defn.Caps_Mutable) then - report.error(em"$cls cannot inheit from both SharedCapability and Mutable", cls.srcPos) + if cls.derivesFrom(defn.Caps_SharedCapability) && cls.derivesFrom(defn.Caps_Stateful) then + report.error(em"$cls cannot inherit from both SharedCapability and Stateful", cls.srcPos) // ------ Checks to run after main capture checking -------------------------- diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala index 4f8dd5ef86bb..5ea8b17d8aaf 100644 --- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala +++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala @@ -48,7 +48,7 @@ object ccConfig: */ inline val useSpanCapset = false - /** If true force all mutable fields to be in Mutable classes, unless they + /** If true force all mutable fields to be in Stateful classes, unless they * are annotated with @untrackedCaptures */ inline val noUnsafeMutableFields = false diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 28a22091b219..028cfd0a5ffc 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1012,9 +1012,11 @@ class Definitions { @tu lazy val Caps_SharedCapability: ClassSymbol = requiredClass("scala.caps.SharedCapability") @tu lazy val Caps_ExclusiveCapability: ClassSymbol = requiredClass("scala.caps.ExclusiveCapability") @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control") + @tu lazy val Caps_Stateful: ClassSymbol = requiredClass("scala.caps.Stateful") + @tu lazy val Caps_Separate: ClassSymbol = requiredClass("scala.caps.Separate") + @tu lazy val Caps_Unscoped: ClassSymbol = requiredClass("scala.caps.Unscoped") @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable") @tu lazy val Caps_Read: ClassSymbol = requiredClass("scala.caps.Read") - @tu lazy val Caps_Unscoped: ClassSymbol = requiredClass("scala.caps.Unscoped") @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet") @tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal") @tu lazy val Caps_erasedValue: Symbol = CapsInternalModule.requiredMethod("erasedValue") @@ -2092,7 +2094,7 @@ class Definitions { @tu lazy val ccExperimental: Set[Symbol] = Set( CapsModule, CapsModule.moduleClass, PureClass, /* Caps_Classifier, Caps_SharedCapability, Caps_Control, -- already stable */ - Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, Caps_Unscoped, + Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, Caps_Unscoped, Caps_Stateful, Caps_Separate, RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, ConsumeAnnot, UseAnnot, ReserveAnnot, diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 09bce2358582..6a7e4733f9d9 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2896,7 +2896,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling throw ex /** - * - Compare capture sets using subCaptures. If the lower type derives from Mutable and the + * - Compare capture sets using subCaptures. If the lower type derives from Stateful and the * upper type does not, make the lower set read-only. * - Test whether the boxing status of tp1 and tp2 the same, or alternatively, * whether the capture set `refs1` of `tp1` is subcapture of the empty set? @@ -2904,7 +2904,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling */ protected def compareCaptures(tp1: Type, refs1: CaptureSet, tp2: Type, refs2: CaptureSet): Boolean = val refs1Adapted = - if tp1.derivesFromMutable && !tp2.derivesFromMutable + if tp1.derivesFromStateful && !tp2.derivesFromStateful then refs1.readOnly else refs1 val subc = subCaptures(refs1Adapted, refs2) diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index ef18a09cf28b..abf4d6209380 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -288,7 +288,7 @@ class PlainPrinter(_ctx: Context) extends Printer { if elideCapabilityCaps && parent.derivesFromCapability && refs.containsTerminalCapability - && (!parent.derivesFromExclusive || refs.isReadOnly) + && (!parent.derivesFromStateful || refs.isReadOnly) then toText(parent) else toTextCapturing(parent, refs, boxText) case tp @ RetainingType(parent, refSet) => diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala index 7f52c871f9de..d5f0971745fe 100644 --- a/compiler/src/dotty/tools/dotc/typer/Checking.scala +++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala @@ -696,8 +696,8 @@ object Checking { } if sym.isWrappedToplevelDef && !sym.isType && sym.flags.is(Infix, butNot = Extension) then fail(ModifierNotAllowedForDefinition(Flags.Infix, s"A top-level ${sym.showKind} cannot be infix.")) - if sym.isUpdateMethod && !sym.owner.derivesFrom(defn.Caps_Mutable) then - fail(em"Update method ${sym.name} must be declared in a class extending the `Mutable` trait.") + if sym.isUpdateMethod && !sym.owner.derivesFrom(defn.Caps_Stateful) then + fail(em"Update method ${sym.name} must be declared in a class extending the `Stateful` trait.") if sym.is(Erased) then checkErasedOK(sym) checkCombination(Final, Open) checkCombination(Sealed, Open) diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala index 1207914fbcd1..81404fc40e88 100644 --- a/compiler/src/dotty/tools/dotc/typer/Namer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala @@ -1001,7 +1001,7 @@ class Namer { typer: Typer => private def normalizeFlags(denot: SymDenotation)(using Context): Unit = if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) - && denot.owner.derivesFrom(defn.Caps_Mutable) + && denot.owner.derivesFrom(defn.Caps_Stateful) then denot.setFlag(Mutable) diff --git a/docs/_docs/reference/experimental/capture-checking/classifiers.md b/docs/_docs/reference/experimental/capture-checking/classifiers.md index 0799d2ebc6a3..38e460ba9967 100644 --- a/docs/_docs/reference/experimental/capture-checking/classifiers.md +++ b/docs/_docs/reference/experimental/capture-checking/classifiers.md @@ -46,7 +46,8 @@ trait SharedCapability extends Capability Classifier trait Control extends SharedCapability, Classifier trait ExclusiveCapability extends Capability -trait Unscoped extends ExclusiveCapability, Classifier +trait Stateful extends ExclusiveCapability +trait Unscoped extends Stateful, Classifier ``` Here is a graph showing the hierarchy of predefined capability traits. Classifier traits are underlined. ``` @@ -58,7 +59,7 @@ Here is a graph showing the hierarchy of predefined capability traits. Classifie SharedCapability ExclusiveCapability ---------------- | | | - | | + | Stateful | | | | Control Unscoped @@ -77,27 +78,6 @@ exclusive capabilities can have shared capabilities in their capture set but not These are all expressed by having their capability classes extend `Control`. -### The Unscoped Classifier - -Capabilities classified as `Unscoped` can escape their environment. For instance, the following -is permitted: -```scala -class Ref[T](init: T) extends Unscoped - -class File: - def read(): String = ... - -def withFile[T](op: (f: File^) => T): T = - op(new File) - -withFile: f => - val r: Ref^ = Ref(f.read()) - r -``` -Here, `r` is a fresh reference that escapes the scope of `withFile`. That's OK only since -`Ref` is classified as `Unscoped`. Since `Unscoped` is a classifier it means that `Ref` cannot -possible capture `f`, which as a `File` is not classified as unscoped. So returning a `Ref` -from a `withFile` does not affect the lifetime of `f`. ### Classifier Restriction diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 177dc7e18a23..3d32b89a2315 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -1,15 +1,17 @@ --- layout: doc-page -title: "Mutability" +title: "Stateful Capabilities" nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/mutability.html --- ## Introduction -An important class of effects represents accesses to mutable variables and mutable data structures. Here we distinguish two kinds of accesses: write access and read-only access. This is reflected by the kinds of capabilities permitting these effects. -A write capability to a mutable data structure `x` is just `x`. The corresponding read-only capability is written `x.rd`. +An important class of effects represents accesses to mutable variables and mutable data structures. This is intimately tied with the concept of _program state_. Stateful capabilities are capabilities that allow to consult and change the program state. -Mutable data structures are expressed with the marker trait `caps.Mutable`. +We distinguish two kinds of accesses: full access that allows state changes and read-only access that allows to observe the state but not to change it. This is reflected by the kinds of capabilities permitting these effects. A regular capability representing a stateful object `x` is just `x`. The corresponding read-only capability is written `x.rd`. + +A common kind of stateful capabilities represent mutable variables that can be read and written. +These mutable data structures are expressed with the marker trait `caps.Mutable`. For instance, consider a simple reference cell: ```scala import caps.Mutable @@ -21,19 +23,23 @@ val r: Ref[Int]^ = Ref(22) ``` A function `() => r.fld += 1` has type `() ->{r} Unit` since it writes to the field `fld` of `r`. By contrast, a function `() => r.fld` has type `() ->{r.rd} Int` since it only reads the contents of `r` but does not update it. +In fact, `Mutable` instances combine several properties that each are represented as separate traits. +In the following, we present these traits and their associated capabilities. + ## Capability Kinds A capability is called - _shared_ if it is [classified](classifiers.md) as a `SharedCapability` - _exclusive_ otherwise. -## The Mutable Trait +## The `Stateful` Trait -We introduce a new trait +In the `scala.caps` object we define a new trait ```scala -trait Mutable +trait Stateful extends ExclusiveCapability ``` -It is used as a marker trait for types that define mutable variables and/or _update methods_. +It is used as a marker trait for classes that can consult and change the global program state. +These classes typically contain mutable variables and/or _update methods_. ## Update Methods @@ -41,70 +47,68 @@ Update methods are declared using a new soft modifier `update`. **Example:** ```scala -class Ref(init: Int) extends Mutable: - private var current = init - def get: Int = current - update def set(x: Int): Unit = current = x +class Counter extends Stateful: + private var count = 0 + def value: Int = count + update def incr(x: Int): Unit = current = x ``` -`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined in the method itself or passed to it in parameters. +`update` can only be used in classes or objects extending `Stateful`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Stateful` may access exclusive capabilities only if they are defined in the method itself or passed to it in parameters. -In class `Ref`, the `set` method should be declared as an update method since it accesses `this` as an exclusive write capability by writing to the variable `this.current` in its environment. +In class `Counter`, the `incr` method should be declared as an update method since it accesses `this` as an exclusive write capability by writing to the variable `this.count` in its environment. -`update` can also be used on an inner class of a class or object extending `Mutable`. It gives all code in the class the right -to access exclusive capabilities in the class environment. Normal classes +`update` can also be used on an inner class of a class or object extending `Stateful`. It gives all code in the inner class the right to access exclusive capabilities in the outer class environment. Normal classes can only access exclusive capabilities defined in the class or passed to it in parameters. +For instance, we can also define counter objects that update a shared variable that is external to the object: + ```scala -object Registry extends Mutable: - var count = 0 - update class Counter: +object Registry extends Stateful: + var sharedCount = 0 + update class CounterX: update def next: Int = - count += 1 - count + sharedCount += 1 + sharedCount ``` -Normal method members of `Mutable` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller. +Normal method members of `Stateful` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller. An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as `toString` or `==` inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method. -The `apply` method of a function type is also a normal method, hence `Mutable` classes may not implement a function type using an update method as the `apply` method. +The `apply` method of a function type is also a normal method, hence `Stateful` classes may not implement a function type using an update method as the `apply` method. -## Mutable Types +## Stateful Types -A type is called a _mutable_ if it extends `Mutable` and it has a mutable variable or +A _type_ is called a _stateful_ if it extends `Stateful` and it has a mutable variable or an update method or an update class as non-private member or constructor. -When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`. -**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced) +**Restriction:** A non-stateful type cannot be downcast by a pattern match to a stateful type. (Note: This is currently not enforced) **Definition:** A parent class constructor is _read-only_ if the following conditions are met: 1. The class does not retain any exclusive capabilities from its environment. 2. The constructor does not take arguments that retain exclusive capabilities. - 3. The class does not does not have fields that retain exclusive universal capabilities. + 3. The class does not have fields that retain exclusive universal capabilities. -**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only. +**Restriction:** If a class or trait extends `Stateful` all its parent classes or traits must either extend `Stateful` or be read-only. -The idea is that when we upcast a reference to a type extending `Mutable` to a type that does not extend `Mutable`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented +The idea is that when we upcast a reference to a type extending `Stateful` to a type that does not extend `Stateful`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented in the class can access exclusive capabilities on its own. And we also cannot override any of the methods of this class with a method accessing exclusive capabilities, since such a method would have to be an update method and update methods are not allowed to override regular methods. - - **Example:** -Consider trait `IterableOnce` from the standard library. +Consider the trait `IterableOnce` from the standard library. ```scala -trait IterableOnce[+T] extends Mutable: +trait IterableOnce[+T] extends Stateful: def iterator: Iterator[T]^{this} update def foreach(op: T => Unit): Unit update def exists(op: T => Boolean): Boolean ... ``` -The trait is a mutable type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`. +The trait is a stateful type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`. ```scala trait Iterator[T] extends IterableOnce[T]: def iterator = this @@ -114,7 +118,7 @@ trait Iterator[T] extends IterableOnce[T]: update def exists(op; T => Boolean): Boolean = ... ... ``` -But there are other implementations of `IterableOnce` that are not mutable types (even though they do indirectly extend the `Mutable` trait). Notably, collection classes implement `IterableOnce` by creating a fresh +But there are other implementations of `IterableOnce` that are not stateful types (even though they do indirectly extend the `Stateful` trait). Notably, collection classes implement `IterableOnce` by creating a fresh `iterator` each time one is required. The mutation via `next()` is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each `update` method in `IterableOnce` by a normal method without the `update` modifier. ```scala @@ -123,24 +127,125 @@ trait Iterable[T] extends IterableOnce[T]: def foreach(op: T => Unit) = iterator.foreach(op) def exists(op: T => Boolean) = iterator.exists(op) ``` -Here, `Iterable` is not a mutable type since it has no update method as member. +Here, `Iterable` is not a stateful type since it has no update method as member. All inherited update methods are (re-)implemented by normal methods. -**Note:** One might think that we don't need a base trait `Mutable` since in any case -a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of `Mutable` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Mutable`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Mutable`. But `apply` may well be implemented by -a method that accesses exclusive capabilities. +**Note:** One might think that we don't need a base trait `Stateful` since in any case +a stateful type is defined by the presence of update methods, not by what it extends. In fact the importance of `Stateful` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Stateful`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Stateful`. But `apply` may well be implemented by a method that accesses exclusive capabilities. -## Read-only Capabilities +A mutable class such as a reference cell or a mutable array or matrix is clearly a stateful type. +But it also has two other properties that are explained in the following. + +## Separate Classes + +Each time one creates a value of a mutable type one gets a separate fresh object that can be updated independently +of other objects. This property is expressed by extending the `Separate` trait in the `scala.caps` object: +```scala +trait Separate extends Stateful +``` +If a value of a type extending Separate is created, a fresh `cap` is automatically +added to the value's capture set: +```scala +class S extends Separate +val s = S() // s: S^ +``` -If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix. +Whether or not a class should be `Separate` is a design question. For instance here is a +design of `Iterator` with a `map` method that is `Stateful` but not `Separate`: -A read-only capability can be seen as a [classified](classifiers.md) capability -using a classifier trait `Read`. I.e. -`x.rd` is a shorthand for `x.only[Read]`. +```scala +class Iterator[T] extends Stateful: + def hasNext: Boolean + update def next: T + update def map[U](f: T => U): Iterator[U]^{this, f} = new Iterator: + def hasNext = Iterator.this.hasNext + update def next: Iterator.this.next + +def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator: + var current = xs + def hasNext = current.nonEmpty + def next = try current.head finally current = current.tail +``` + +Here, `listIterator` returns a fresh iterator with separate state, whereas `map` returns an iterator capturing the current iterator `this` and the passed function `f`, without representing a separate state. + +One could also decide to make iterator a `Separate` class: + +```scala +class SepIterator[T] extends Stateful, Separate: + def hasNext: Boolean + update def next: T + consume def map[U](consume f: T => U) = new SepIterator: + def hasNext = Iterator.this.hasNext + update def next: Iterator.this.next +``` +`SepIterator`'s `map` method returns a fresh iterator of type `SepIterator[U]^`. We lose the knowledge that this iterator captures `this` and `f`. So this second version of iterators might seem less useful than the first. However, we can check aliasing conditions using [separation checking](./separation-checking.md). Separation checking +would inform us that creating a mapped iterator invalidates any future accesses to the original iterator or the passed function `f`. This is expressed by the `consume` modifiers on the `map` method and it parameter. The `consume` modifier will be explained in detail in the section on separation checking. + +## The Unscoped Classifier + +Usually, capabilities have bounded lifetimes. For instance, consider again the withFile method: +```scala +class File: + def read(): String = ... + def close(): Unit = ... + +def withFile[T](op: (f: File^) => T): T = + op(new File) +``` +Here, we need to enforce that the return type of `op` cannot possibly capture the +`File` parameter `f`. This is achieved by preventing `op` from returning new capabilities +that are not already known outside the call to `withFile`. But this scheme can be too restrictive. +For instance, we might want to read the file's contents into a `Separate` capability such as +a `Ref` cell. That `Ref` cell would not hold on to the file, but it would not be a pure type either, +since the cell itself is a capability. + +We can make this compile by declaring `Ref` cells to be `Unscoped`. +Capabilities classified as `Unscoped` can escape their environment. For instance, the following +is permitted: +```scala +class Ref[T](init: T) extends Separate, Unscoped + +withFile: f => + val r: Ref[String]^ = Ref(f.read()) + r +``` +Here, `r` is a fresh reference of type `Ref[String]` that escapes the scope of `withFile`. That's OK only since +`Ref` is classified as `Unscoped`. Since `Unscoped` is a [classifier](./classifiers.md) it means that `Ref` cannot possibly capture `f`, which as a `File` is not classified as `Unscoped`. So returning a `Ref` +from a `withFile` does not affect the lifetime of `f`. + +## Mutable Classes + +Classes such as ref-cells, arrays, or matrices are stateful, unscoped, and their instances represent fresh capabilities. This common combination is expressed by the `Mutable` trait in the `scala.caps` object. + +```scala +trait Mutable extends Stateful, Separate, Unscoped +``` + +Examples: + +```scala +class Ref[T](init: T) extends Mutable: + private var current = init + def get: T = current + update def set(x: T): Unit = current = x + +class Arr[T](n: Int) extends Mutable: + private val elems = new Array[T](n) + def apply(i: Int): T = elems(i) + update def update(i: Int, x: T) = elems(i) = x +``` + +An example of a `Stateful` and `Unscoped` capability that is _not_ `Separate` would be a +facade class that reveals some part of an underlying `Mutable` capability. + +## Read-only Capabilities + +If `x` is an exclusive capability of a type extending `Stateful`, `x.rd` is its associated _read-only_ capability. **Implicitly added capture sets** -A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from other capability traits which implicitly add `{cap}`. +A reference to a type extending trait `Stateful` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from other capability traits which implicitly add `{cap}`. For instance, consider: ```scala @@ -151,13 +256,13 @@ Here, `from` is implicitly read-only, and `to`'s type has capture set `cap`. I.e ```scala def addContents(from: Ref[Int]^{cap.rd}, to: Ref[Int]^{cap}): Unit ``` -In other words, the explicit `^` indicates where write effects can happen. +In other words, the explicit `^` indicates where state changes can happen. ## Read-Only Accesses -An access `p.m` to an update method or class `m` in a mutable type is permitted only if the type `M` of the prefix `p` retains exclusive capabilities. If `M` is pure or its capture set has only shared and read-only capabilities then the access is not permitted. +An access `p.m` to an update method or class `m` in a stateful type is permitted only if the type `S` of the prefix `p` retains exclusive capabilities. If `S` is pure or its capture set has only shared and read-only capabilities then the access is not permitted. -A _read-only access_ is a reference to a type extending `Mutable` where one of the following conditions holds: +A _read-only access_ is a reference to a type extending `Stateful` where one of the following conditions hold: 1. The reference is `this` and the access is not from an update method of the class of `this`. For instance: ```scala @@ -177,8 +282,8 @@ A _read-only access_ is a reference to a type extending `Mutable` where one of t val c: RefContainer = RefContainer() def get = c.r.get // read-only access to `c.r` ``` - In the last example, `c.r` is a read-only access since the prefix `c` is a read-only reference. Note that `^{cap.rd}` was implicitly added to `c: RefContainer` since `RefContainer` is a `Mutable` class. - 3. The expected type of the reference is a value type that is not a mutable type. For instance: + In the last example, `c.r` is a read-only access since the prefix `c` is a read-only reference. Note that `^{cap.rd}` was implicitly added to `c: RefContainer` since `RefContainer` is a `Stateful` capability class. + 3. The expected type of the reference is a value type that is not a stateful type. For instance: ```scala val r: Ref[Int]^ = Ref(22) val x: Object = r // read-only access to `r` @@ -190,7 +295,7 @@ A _read-only access_ is a reference to a type extending `Mutable` where one of t ``` The first two conditions represent safety conditions: we _must_ declare the access a read-only access since the context of the access does not permit updates. The last two conditions are opportunistic: we _are allowed_ to declare the access a read-only access since the context -of the access does not require write capabilities. +of the access does not require full capabilities. A read-only access charges the read-only capability `x.rd` to its environment. Other accesses charge the full capability `x`. @@ -207,16 +312,16 @@ val g = () => x.set(1) // g: () ->{x} Unit `f` accesses a regular method, so it charges only `x.rd` to its environment which shows up in its capture set. By contrast, `g` accesses an update method of `x`, so its capture set is `{x}`. -A reference to a mutable type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK: +A reference to a stateful type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK: ```scala -val a: Ref^ = Ref(1) -val b1: Ref^{a.rd} = a -val b2: Ref^{cap.rd} = a +val a: Ref[Int]^ = Ref(1) +val b1: Ref[Int]^{a.rd} = a +val b2: Ref[Int]^{cap.rd} = a ``` ## Lazy Vals and Read-Only Restrictions -Lazy val initializers in `Mutable` classes are subject to read-only restrictions similar to those for normal methods. Specifically, a lazy val initializer in a `Mutable` class cannot call update methods or refer to non-local exclusive capabilities, i.e., capabilities defined outside the lazy val's scope. +Lazy val initializers in `Stateful` classes are subject to read-only restrictions similar to those for normal methods. Specifically, a lazy val initializer in a `Stateful` class cannot call update methods or refer to non-local exclusive capabilities, i.e., capabilities defined outside the lazy val's scope. For example, when a lazy val is declared in a local method's scope, its initializer may freely use capabilities from the surrounding environment: ```scala @@ -226,9 +331,9 @@ def example(r: Ref[Int]^) = r.set(100 * i) // ok: can call update method () => r.get() + i ``` -However, within a `Mutable` class, a lazy val declaration has only read access to non-local exclusive capabilities: +However, within a `Stateful` class, a lazy val declaration has only read access to non-local exclusive capabilities: ```scala -class Wrapper(val r: Ref[Int]^) extends Mutable: +class Wrapper(val r: Ref[Int]^) extends Stateful: lazy val badInit: () ->{r} Int = r.set(100) // error: call to update method () => r.set(r.get() * 2); r.get() // error: call to update method @@ -254,8 +359,8 @@ class Example: Here, `local` is created within the lazy val's initializer, so it counts as a local capability. The initializer can call update methods on it. -This makes lazy vals behave like normal methods in `Mutable` classes: they can read from their environment but cannot update it unless explicitly marked. -Unlike for methods, there's currently no `update` modifier for lazy vals in `Mutable` classes, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might +This makes lazy vals behave like normal methods in `Stateful` classes: they can read from their environment but cannot update it unless explicitly marked. +Unlike for methods, there's currently no `update` modifier for lazy vals in `Stateful` classes, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might support `update lazy val` if there are compelling use cases and there is sufficient community demand. ## Update Restrictions @@ -281,7 +386,6 @@ val ro: Ref[Int] = r ro.set(22) // disallowed, since `ro` is read-only access ``` - ## Untracked Vars Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance: @@ -297,15 +401,15 @@ class Cache[T](eval: () -> T): known = true x ``` -Note that, even though `Cache` has mutable variables, it is not declared as a `Mutable` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`. +Note that, even though `Cache` has mutable variables, it is not declared as a `Stateful` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`. We can avoid the need for update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable field are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer to use `@untrackedCaptures` responsibly so that it does not hide visible side effects on mutable state. -Note that at the moment an assignment to a variable is restricted _only_ if the variable is a field of a `Mutable` class. Fields of other classes and local variables are currently not checked. So the `Cache` class above would in fact +Note that at the moment an assignment to a variable is restricted _only_ if the variable is a field of a `Stateful` class. Fields of other classes and local variables are currently not checked. So the `Cache` class above would in fact currently compile without the addition of `@untrackedCaptures`. -But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` can be declared only in classes extending `Mutable`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `@untrackedCapture`s would become essential as an escape hatch. +But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` can be declared only in classes extending `Stateful`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `@untrackedCapture`s would become essential as an escape hatch. By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables. @@ -319,23 +423,24 @@ The contradiction can be explained by noting that we use a capture set in two di First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it. -But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref^`, we can access all its methods, but if we have a `Ref^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a mutable type with exclusive capabilities lets you do more than a mutable type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities. +But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref[T]^`, we can access all its methods, but if we have a `Ref[T]^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a stateful type with exclusive capabilities lets you do more than a stateful type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities. -The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `RD`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source. -We add an implicit read-only qualifier `RD` to all capture sets on mutable types that consist only of shared or read-only capabilities. +The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `reader`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source. +We add an implicit read-only qualifier `reader` to all capture sets on stateful types that consist only of shared or read-only capabilities. So when we write ```scala -val b1: Ref^{a.rd} = a +val b1: Ref[A]^{a.rd} = a ``` we really mean ```scala -val b1: Ref^{a.rd}.RD = a +val b1: Ref[A]^{a.rd}.reader = a ``` +The current implementation shows the implicit `reader` qualifier under the `-Ycc-verbose` setting. + The subcapturing theory for sets is then as before, with the following additional rules: - - `C <: C.RD` - - `C₁.RD <: C₂.RD` if `C₍ <: C₂` - - `{x, ...}.RD = {x.rd, ...}.RD` + - `C <: C.reader` + - `C₁.reader <: C₂.reader` if `C₍ <: C₂` + - `{x, ...}.reader = {x.rd, ...}.reader` - `{x.rd, ...} <: {x, ...}` - diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index a04a5690df7d..188e476c849b 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -78,20 +78,31 @@ type Exclusive = ExclusiveCapability */ trait Control extends SharedCapability, Classifier -/** Marker trait for classes with methods that require an exclusive reference. */ +/** Marker trait for classes that can consult and change the global program state. + * These classes typically contain mutable variables and/or update methods. + */ +@experimental +trait Stateful extends ExclusiveCapability + +/** Marker trait for classes that produce fresh capabilities with their values. If a value of a type + * extending Separate is created, a fresh `cap` is automatically added to the value's capture set. + */ @experimental -trait Mutable extends ExclusiveCapability +trait Separate extends Stateful + +/** Marker trait for classes that are not subject to scoping restrictions of captured capabilities. + */ +@experimental +trait Unscoped extends Stateful, Classifier + +@experimental +trait Mutable extends Stateful, Separate, Unscoped /** Marker trait for classes with reader methods, typically extended by Mutable classes */ @experimental @deprecated trait Read extends Mutable -/** Marker trait for classes that are not subject to scoping restrictions - * of captured capabilities. - */ -@experimental -trait Unscoped extends ExclusiveCapability, Classifier /** Carrier trait for capture set type parameters */ @experimental diff --git a/tests/neg-custom-args/captures/check-inferred.check b/tests/neg-custom-args/captures/check-inferred.check index 968aa9dfe244..4fb0b030f7c3 100644 --- a/tests/neg-custom-args/captures/check-inferred.check +++ b/tests/neg-custom-args/captures/check-inferred.check @@ -58,4 +58,4 @@ | Fields capturing a root capability need to be given an explicit type unless the capability is already | subsumed by the computed capability of the enclosing class. | - | where: ^ refers to a fresh root capability in the type of value count + | where: ^ refers to a fresh root capability classified as Unscoped in the type of value count diff --git a/tests/neg-custom-args/captures/classified-inheritance2.check b/tests/neg-custom-args/captures/classified-inheritance2.check index 87455916c072..3d608ff53bff 100644 --- a/tests/neg-custom-args/captures/classified-inheritance2.check +++ b/tests/neg-custom-args/captures/classified-inheritance2.check @@ -1,7 +1,7 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance2.scala:4:6 --------------------------------------------- -4 |class Logger extends SharedCapability, Mutable: // error (1) does this make sense? +4 |class Logger extends SharedCapability, Stateful: // error (1) does this make sense? | ^ - | class Logger cannot inheit from both SharedCapability and Mutable + | class Logger cannot inherit from both SharedCapability and Stateful -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classified-inheritance2.scala:12:27 ---------------------- 12 | val t: Logger^{} = Logger() // error | ^^^^^^^^ diff --git a/tests/neg-custom-args/captures/classified-inheritance2.scala b/tests/neg-custom-args/captures/classified-inheritance2.scala index 301fb9fb473d..a3921dba948e 100644 --- a/tests/neg-custom-args/captures/classified-inheritance2.scala +++ b/tests/neg-custom-args/captures/classified-inheritance2.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import language.experimental.separationChecking import caps.* -class Logger extends SharedCapability, Mutable: // error (1) does this make sense? +class Logger extends SharedCapability, Stateful: // error (1) does this make sense? private var _state: Int = 0 update def log(msg: String): Unit = () diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check index d684517a1d9c..4937bf7fc6e4 100644 --- a/tests/neg-custom-args/captures/consume-in-constructor.check +++ b/tests/neg-custom-args/captures/consume-in-constructor.check @@ -1,8 +1,3 @@ --- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:11:21 -------------------------------------------- -11 |class A3(consume val b: B^) // error - | ^ - | A consume parameter is only allowed for classes producing a `cap` in their constructor. - | This can be achieved by having the class extend caps.Separate. -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 -------------------------------------------- 20 | println(b) // error | ^ diff --git a/tests/neg-custom-args/captures/consume-in-constructor.scala b/tests/neg-custom-args/captures/consume-in-constructor.scala index 0786a4c2def0..3a087c41cfbb 100644 --- a/tests/neg-custom-args/captures/consume-in-constructor.scala +++ b/tests/neg-custom-args/captures/consume-in-constructor.scala @@ -1,4 +1,4 @@ -import caps.{cap, Mutable} +import caps.{cap, Stateful} class B @@ -8,8 +8,8 @@ class A1(val b: B^): class A2(consume val b: B^): val bb: B^ = B() -class A3(consume val b: B^) // error -class A4(consume val b: B^) extends Mutable { var x: Int = 1 } // ok +class A3(consume val b: B^) // was error now ok +class A4(consume val b: B^) extends Stateful { var x: Int = 1 } // ok def Test = val b: B^ = B() val a1 = A1(b) diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check index 0a5aa5b8137e..ee59c309e370 100644 --- a/tests/neg-custom-args/captures/i23726.check +++ b/tests/neg-custom-args/captures/i23726.check @@ -13,8 +13,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:16:5 ------------------------------------------------------------- 16 | f3(b) // error | ^ @@ -30,8 +30,8 @@ | Footprint set of function result : {op, b} | The two sets overlap at : {b} | - |where: ^ refers to a fresh root capability in the type of value b - | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value b + | ^² refers to a fresh root capability classified as Unscoped created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:24:5 ------------------------------------------------------------- 24 | f7(a) // error | ^ @@ -47,5 +47,5 @@ | Footprint set of function prefix : {f7*, a, b} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test1 when checking argument to parameter x of method apply diff --git a/tests/neg-custom-args/captures/i24310.scala b/tests/neg-custom-args/captures/i24310.scala index 741ce05b8e5c..e9b1ba03d27f 100644 --- a/tests/neg-custom-args/captures/i24310.scala +++ b/tests/neg-custom-args/captures/i24310.scala @@ -5,7 +5,7 @@ class Ref extends Mutable: def get(): Int = value update def set(v: Int): Unit = value = v -class Matrix(val f: () => Int) extends Mutable: +class Matrix(val f: () => Int) extends Stateful: self: Matrix^ => def run() = f() // error <- note the missing update update def add(): Unit = () diff --git a/tests/neg-custom-args/captures/i24335.check b/tests/neg-custom-args/captures/i24335.check index 9a01057fda12..b70624a44460 100644 --- a/tests/neg-custom-args/captures/i24335.check +++ b/tests/neg-custom-args/captures/i24335.check @@ -14,4 +14,4 @@ | Fields capturing a root capability need to be given an explicit type unless the capability is already | subsumed by the computed capability of the enclosing class. | - | where: ^ refers to a fresh root capability in the type of value r + | where: ^ refers to a fresh root capability classified as Unscoped in the type of value r diff --git a/tests/neg-custom-args/captures/i24373.scala b/tests/neg-custom-args/captures/i24373.scala index 16f6d7258692..8c70b878620b 100644 --- a/tests/neg-custom-args/captures/i24373.scala +++ b/tests/neg-custom-args/captures/i24373.scala @@ -1,10 +1,10 @@ trait Foo: consume def sink1: Unit = () -trait Bar extends Foo, caps.Mutable: +trait Bar extends Foo, caps.Stateful: consume def sink2: Unit = () -class C extends caps.Mutable: +class C extends caps.Stateful: def sink4(consume x: Foo^) = () object Foo: diff --git a/tests/neg-custom-args/captures/i24373a.scala b/tests/neg-custom-args/captures/i24373a.scala index ea739fb9c436..5fdf95acfea9 100644 --- a/tests/neg-custom-args/captures/i24373a.scala +++ b/tests/neg-custom-args/captures/i24373a.scala @@ -1,5 +1,5 @@ trait Foo -trait Bar extends Foo, caps.Mutable +trait Bar extends Foo, caps.Stateful def Test = diff --git a/tests/neg-custom-args/captures/implied-ro.scala b/tests/neg-custom-args/captures/implied-ro.scala index d1bf81519054..765b85af502b 100644 --- a/tests/neg-custom-args/captures/implied-ro.scala +++ b/tests/neg-custom-args/captures/implied-ro.scala @@ -1,5 +1,5 @@ import caps.* -class Ref extends Mutable, Unscoped +class Ref extends Stateful, Unscoped class C: val r: Ref = Ref() diff --git a/tests/neg-custom-args/captures/lazyvals-sep.check b/tests/neg-custom-args/captures/lazyvals-sep.check index e859829e1f3b..7140b2015f7e 100644 --- a/tests/neg-custom-args/captures/lazyvals-sep.check +++ b/tests/neg-custom-args/captures/lazyvals-sep.check @@ -29,10 +29,10 @@ |Found: Ref^{TestClass.this.r.rd} |Required: Ref^ | - |Note that {cap} is an exclusive capture set of the mutable type Ref^, - |it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}. + |Note that {cap} is an exclusive capture set of the stateful type Ref^, + |it cannot subsume a read-only capture set of the stateful type Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability classified as Unscoped created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 --------------------------------- @@ -41,10 +41,10 @@ |Found: Ref^{TestClass.this.r.rd} |Required: Ref^ | - |Note that {cap} is an exclusive capture set of the mutable type Ref^, - |it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}. + |Note that {cap} is an exclusive capture set of the stateful type Ref^, + |it cannot subsume a read-only capture set of the stateful type Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability classified as Unscoped created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 ------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/lazyvals-sep.scala b/tests/neg-custom-args/captures/lazyvals-sep.scala index 50fcf472d824..e9a60cfa84b5 100644 --- a/tests/neg-custom-args/captures/lazyvals-sep.scala +++ b/tests/neg-custom-args/captures/lazyvals-sep.scala @@ -8,14 +8,14 @@ class Ref(x: Int) extends Mutable: update def set(newValue: Int): Unit = value = newValue // For testing types other than functions -class Wrapper(val ref: Ref^) extends Mutable: +class Wrapper(val ref: Ref^) extends Stateful: def compute(): Int = ref.get() update def mutate(x: Int): Unit = ref.set(x) class WrapperRd(val ref: Ref^{cap.rd}): def compute(): Int = ref.get() -class TestClass extends Mutable: +class TestClass extends Stateful: val r: Ref^ = Ref(0) val r2: Ref^ = Ref(42) @@ -118,6 +118,6 @@ def test = lazy val lazyVal2: () ->{r.rd} Int = val current = r2.get() - r.set(current * 100) // ok, lazy vals outside Mutable can access exclusive capabilities + r.set(current * 100) // ok, lazy vals outside Stateful can access exclusive capabilities () => r.get() diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index ae70cb3aa249..6a3853770f4e 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -4,32 +4,32 @@ | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append | on line 11 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter buf + | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- 20 | val buf3 = buf1.append(4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 18 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- 28 | val buf3 = buf1.append(4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 25 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- 38 | val buf3 = buf1.append(4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append |on line 33 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot | be used as a prefix to consume method append. | - | where: ^ refers to a fresh root capability in the type of parameter buf + | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 97d0409e55ed..225792af4189 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -1,13 +1,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 --------------------------------- 7 | def bar: BadBuffer[T]^ = this // error // error separation | ^^^^ - | Found: BadBuffer[T]^{BadBuffer.this.rd} - | Required: BadBuffer[T]^ + | Found: BadBuffer[T]^{BadBuffer.this.rd} + | Required: BadBuffer[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^, - | it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type BadBuffer[T]^, + | it cannot subsume a read-only capture set of the stateful type BadBuffer[T]^{BadBuffer.this.rd}. | - | where: ^ and cap refer to a fresh root capability in the result type of method bar + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the result type of method bar | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:27 ------------------------------------------------------ @@ -23,11 +23,11 @@ -- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:29 ----------------------------------------------------- 10 | def bar: BadBuffer[T]^ = this // error // error | ^^^^ - | Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition - | of method append with result type BadBuffer[T]^. - | This type hides capabilities {BadBuffer.this} + | Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition + | of method append with result type BadBuffer[T]^. + | This type hides capabilities {BadBuffer.this} | - | where: ^ refers to a fresh root capability in the result type of method append + | where: ^ refers to a fresh root capability classified as Unscoped in the result type of method append -- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:13 ----------------------------------------------------- 10 | def bar: BadBuffer[T]^ = this // error // error | ^^^^^^^^^^^^^ @@ -39,35 +39,35 @@ |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app |on line 21 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of parameter buf + |where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 ----------------------------------------------------- 30 | val buf3 = app(buf1, 4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 28 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 ----------------------------------------------------- 38 | val buf3 = app(buf1, 4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 35 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 ----------------------------------------------------- 48 | val buf3 = app(buf1, 4) // error | ^^^^ |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app |on line 43 and therefore is no longer available. | - |where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------ 52 | app(buf, 1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot | be passed as a consume parameter to method app. | - | where: ^ refers to a fresh root capability in the type of parameter buf + | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 ----------------------------------------------------- 62 | val c3 = contents(buf) // error | ^^^ diff --git a/tests/neg-custom-args/captures/matrix.check b/tests/neg-custom-args/captures/matrix.check index 6a58b62dc2a3..6345f34802f8 100644 --- a/tests/neg-custom-args/captures/matrix.check +++ b/tests/neg-custom-args/captures/matrix.check @@ -13,7 +13,7 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul + |where: cap is a fresh root capability classified as Unscoped created in method Test when checking argument to parameter y of method mul -- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------ 30 | mul1(m1, m2, m2) // error: will fail separation checking | ^^ @@ -29,4 +29,4 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1 + |where: cap is a fresh root capability classified as Unscoped created in method Test when checking argument to parameter y of method mul1 diff --git a/tests/neg-custom-args/captures/mut-iterator.scala b/tests/neg-custom-args/captures/mut-iterator.scala index a6e022ead7fe..ee38f11600f1 100644 --- a/tests/neg-custom-args/captures/mut-iterator.scala +++ b/tests/neg-custom-args/captures/mut-iterator.scala @@ -1,6 +1,6 @@ -import caps.{cap, Mutable, SharedCapability} +import caps.{cap, Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean def next(): T diff --git a/tests/neg-custom-args/captures/mut-iterator1.scala b/tests/neg-custom-args/captures/mut-iterator1.scala index c51575c4b2f7..4ba6fdf06a67 100644 --- a/tests/neg-custom-args/captures/mut-iterator1.scala +++ b/tests/neg-custom-args/captures/mut-iterator1.scala @@ -1,6 +1,6 @@ -import caps.{Mutable, SharedCapability} +import caps.{Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean def next(): T diff --git a/tests/neg-custom-args/captures/mut-iterator2.scala b/tests/neg-custom-args/captures/mut-iterator2.scala index 9a2b76018dba..807bf81eff37 100644 --- a/tests/neg-custom-args/captures/mut-iterator2.scala +++ b/tests/neg-custom-args/captures/mut-iterator2.scala @@ -1,6 +1,6 @@ -import caps.{Mutable, SharedCapability} +import caps.{Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean update def next(): T diff --git a/tests/neg-custom-args/captures/mut-iterator3.scala b/tests/neg-custom-args/captures/mut-iterator3.scala index 5170cebe6f03..350818bf1d9f 100644 --- a/tests/neg-custom-args/captures/mut-iterator3.scala +++ b/tests/neg-custom-args/captures/mut-iterator3.scala @@ -1,6 +1,6 @@ -import caps.{cap, Mutable, SharedCapability} +import caps.{cap, Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean update def next(): T diff --git a/tests/neg-custom-args/captures/mut-iterator4.scala b/tests/neg-custom-args/captures/mut-iterator4.scala index 114c08af2001..72c60d26edfc 100644 --- a/tests/neg-custom-args/captures/mut-iterator4.scala +++ b/tests/neg-custom-args/captures/mut-iterator4.scala @@ -1,6 +1,6 @@ -import caps.{cap, Mutable, SharedCapability} +import caps.{cap, Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean update def next(): T diff --git a/tests/neg-custom-args/captures/mut-iterator5.scala b/tests/neg-custom-args/captures/mut-iterator5.scala index a2af33c2e1f4..65af100c2853 100644 --- a/tests/neg-custom-args/captures/mut-iterator5.scala +++ b/tests/neg-custom-args/captures/mut-iterator5.scala @@ -1,6 +1,6 @@ -import caps.{cap, Mutable, SharedCapability} +import caps.{cap, Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean update def next(): T diff --git a/tests/neg-custom-args/captures/mut-outside-mutable.check b/tests/neg-custom-args/captures/mut-outside-mutable.check index b0ff82884ebe..b81b53b9fd4b 100644 --- a/tests/neg-custom-args/captures/mut-outside-mutable.check +++ b/tests/neg-custom-args/captures/mut-outside-mutable.check @@ -1,8 +1,12 @@ -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:5:13 ------------------------------------------------ 5 | update def foreach(op: T => Unit): Unit // error | ^ - | Update method foreach must be declared in a class extending the `Mutable` trait. + | Update method foreach must be declared in a class extending the `Stateful` trait. -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:9:15 ------------------------------------------------ 9 | update def baz() = 1 // error | ^ - | Update method baz must be declared in a class extending the `Mutable` trait. + | Update method baz must be declared in a class extending the `Stateful` trait. +-- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:14:15 ----------------------------------------------- +14 | update def baz() = 1 // error + | ^ + | Update method baz must be declared in a class extending the `Stateful` trait. diff --git a/tests/neg-custom-args/captures/mut-outside-mutable.scala b/tests/neg-custom-args/captures/mut-outside-mutable.scala index 12c47334a422..abf9dd8fb3ae 100644 --- a/tests/neg-custom-args/captures/mut-outside-mutable.scala +++ b/tests/neg-custom-args/captures/mut-outside-mutable.scala @@ -1,10 +1,14 @@ -import caps.Mutable +import caps.Stateful trait IterableOnce[T]: def iterator: Iterator[T]^{this} update def foreach(op: T => Unit): Unit // error -trait Foo extends Mutable: +trait Foo extends Stateful: def bar = update def baz() = 1 // error baz() + +trait Bar extends Stateful: + class Baz: + update def baz() = 1 // error diff --git a/tests/neg-custom-args/captures/mut-override.scala b/tests/neg-custom-args/captures/mut-override.scala index aa2913645e43..19f21ff69829 100644 --- a/tests/neg-custom-args/captures/mut-override.scala +++ b/tests/neg-custom-args/captures/mut-override.scala @@ -1,6 +1,6 @@ -import caps.Mutable +import caps.Stateful -trait IterableOnce[T] extends Mutable: +trait IterableOnce[T] extends Stateful: def iterator: Iterator[T]^{this} update def foreach(op: T => Unit): Unit diff --git a/tests/neg-custom-args/captures/mut-widen-empty.check b/tests/neg-custom-args/captures/mut-widen-empty.check index 70a5622af1e6..b3ab5df59979 100644 --- a/tests/neg-custom-args/captures/mut-widen-empty.check +++ b/tests/neg-custom-args/captures/mut-widen-empty.check @@ -1,12 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:12:24 ------------------------------ 12 | val c: Arr[String]^ = b // error | ^ - | Found: (b : Arr[String]^{}) - | Required: Arr[String]^ + | Found: (b : Arr[String]^{}) + | Required: Arr[String]^ | - | Note that {cap} is an exclusive capture set of the mutable type Arr[String]^, - | it cannot subsume a read-only capture set of the mutable type Arr[String]^{}. + | Note that {cap} is an exclusive capture set of the stateful type Arr[String]^, + | it cannot subsume a read-only capture set of the stateful type Arr[String]^{}. | - | where: ^ and cap refer to a fresh root capability in the type of value c + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check index 2b498c823f57..0ab347f2ec48 100644 --- a/tests/neg-custom-args/captures/mutability.check +++ b/tests/neg-custom-args/captures/mutability.check @@ -11,13 +11,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:10:25 ----------------------------------- 10 | val self2: Ref[T]^ = this // error // error separation | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability in the type of value self2 + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:11:13 -------------------------------------------------------- @@ -26,23 +26,23 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability in the type of class Ref + | where: ^ refers to a fresh root capability classified as Unscoped in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:14:12 -------------------------------------------------------- 14 | self3().set(x) // error | ^^^^^^^^^^^ - | Cannot call update method set of Ref[T^{}]^{self3} - | since its capture set {self3} is read-only. + | Cannot call update method set of Ref[T^{}]^{Ref.this.rd} + | since its capture set {Ref.this.rd} of value self3 is read-only. -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:15:31 ----------------------------------- 15 | val self4: () => Ref[T]^ = () => this // error | ^^^^^^^^^^ - | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} - | Required: () => Ref[T]^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T^'s1]^{Ref.this.rd}. | - | where: => refers to a fresh root capability in the type of value self4 - | ^ and cap refer to a fresh root capability in the type of value self4 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability classified as Unscoped in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:16:15 -------------------------------------------------------- @@ -51,7 +51,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability in the type of class Ref + | where: ^ refers to a fresh root capability classified as Unscoped in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:19:12 -------------------------------------------------------- 19 | self5().set(x) // error | ^^^^^^^^^^^ @@ -60,13 +60,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:20:27 ----------------------------------- 20 | def self6(): Ref[T]^ = this // error // error separation | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability in the result type of method self6 + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:21:15 -------------------------------------------------------- @@ -75,7 +75,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability in the type of class Ref + | where: ^ refers to a fresh root capability classified as Unscoped in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:25:25 -------------------------------------------------------- 25 | def set(x: T) = this.x.set(x) // error | ^^^^^^^^^^ @@ -91,24 +91,24 @@ | ^^^^^^^^ | Cannot call update method set of r3.x | since the capture set {r3} of its prefix (r3 : Ref2[Int]) is read-only. --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:42:29 ----------------------------------- -42 | val r5: () => Ref2[Int]^ = () => ref2 // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:43:29 ----------------------------------- +43 | val r5: () => Ref2[Int]^ = () => ref2 // error | ^^^^^^^^^^ - | Found: () ->{ref2.rd} Ref2[Int]^{ref2} - | Required: () => Ref2[Int]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, - | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | Note that {cap} is an exclusive capture set of the stateful type Ref2[Int]^, + | it cannot subsume a read-only capture set of the stateful type Ref2[Int]^{ref2}. | - | where: => refers to a fresh root capability in the type of value r5 - | ^ and cap refer to a fresh root capability in the type of value r5 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability classified as Unscoped in the type of value r5 | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/mutability.scala:45:9 --------------------------------------------------------- -45 | r6().x.set(33) // error +-- Error: tests/neg-custom-args/captures/mutability.scala:46:9 --------------------------------------------------------- +46 | r6().x.set(33) // error | ^^^^^^^^^^ - | Cannot call update method set of Ref[Int]^{r6*.rd} - | since its capture set {r6*.rd} is read-only. + | Cannot call update method set of Ref[Int]^{cap.rd} + | since its capture set {cap.rd} is read-only. -- Error: tests/neg-custom-args/captures/mutability.scala:10:15 -------------------------------------------------------- 10 | val self2: Ref[T]^ = this // error // error separation | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/mutability.scala b/tests/neg-custom-args/captures/mutability.scala index cc419241982c..d4d4002f9e22 100644 --- a/tests/neg-custom-args/captures/mutability.scala +++ b/tests/neg-custom-args/captures/mutability.scala @@ -37,6 +37,7 @@ def test = r3.x.set(33) // error val r4 = () => Ref2(22) + val r4x = r4().x r4().x.set(33) // ok val ref2: Ref2[Int] = Ref2(22) val r5: () => Ref2[Int]^ = () => ref2 // error diff --git a/tests/neg-custom-args/captures/mutable-inheritance.check b/tests/neg-custom-args/captures/mutable-inheritance.check index 84d69eb2824c..0027dd0523a2 100644 --- a/tests/neg-custom-args/captures/mutable-inheritance.check +++ b/tests/neg-custom-args/captures/mutable-inheritance.check @@ -1,15 +1,15 @@ -- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:7:16 ------------------------------------------------ -7 |class C extends B(??? : Int => Int), caps.Mutable // error +7 |class C extends B(??? : Int => Int), caps.Stateful // error | ^^^^^^^^^^^^^^^^^^^ - | illegal inheritance: class C which extends `Mutable` is not allowed to also extend class B - | since class B retains exclusive capabilities but does not extend `Mutable`. + | illegal inheritance: class C which extends `Stateful` is not allowed to also extend class B + | since class B retains exclusive capabilities but does not extend `Stateful`. -- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:18:16 ----------------------------------------------- -18 |class H extends G, caps.Mutable // error +18 |class H extends G, caps.Stateful // error | ^ - | illegal inheritance: class H which extends `Mutable` is not allowed to also extend class G - | since class G retains exclusive capabilities but does not extend `Mutable`. + | illegal inheritance: class H which extends `Stateful` is not allowed to also extend class G + | since class G retains exclusive capabilities but does not extend `Stateful`. -- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:4:18 ------------------------------------------------ -4 | class A extends E, caps.Mutable // error +4 | class A extends E, caps.Stateful // error | ^ - | illegal inheritance: class A which extends `Mutable` is not allowed to also extend class E - | since class E retains exclusive capabilities but does not extend `Mutable`. + | illegal inheritance: class A which extends `Stateful` is not allowed to also extend class E + | since class E retains exclusive capabilities but does not extend `Stateful`. diff --git a/tests/neg-custom-args/captures/mutable-inheritance.scala b/tests/neg-custom-args/captures/mutable-inheritance.scala index 6637fbb0ea7b..40837914b8c5 100644 --- a/tests/neg-custom-args/captures/mutable-inheritance.scala +++ b/tests/neg-custom-args/captures/mutable-inheritance.scala @@ -1,20 +1,20 @@ def test(c: Object^) = class E: def f = println(c) - class A extends E, caps.Mutable // error + class A extends E, caps.Stateful // error class B(x: Int => Int) -class C extends B(??? : Int => Int), caps.Mutable // error +class C extends B(??? : Int => Int), caps.Stateful // error -class D extends caps.Mutable: +class D extends caps.Stateful: var x: Int = 0 -class F extends D, caps.Mutable // ok +class F extends D, caps.Stateful // ok -class Ref extends caps.Mutable +class Ref extends caps.Stateful class G: val r: Ref^ = Ref() -class H extends G, caps.Mutable // error +class H extends G, caps.Stateful // error diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check index 7f7a1ee83681..169059d9bc61 100644 --- a/tests/neg-custom-args/captures/mutvars.check +++ b/tests/neg-custom-args/captures/mutvars.check @@ -11,31 +11,31 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:9:25 --------------------------------------- 9 | val self2: Ref[T]^ = this // error // error separation | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability in the type of value self2 + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:13:16 ----------------------------------------------------------- 13 | self3().fld = x // error | ^^^^^^^^^^^^^^^ - | Cannot assign to field fld of Ref[T^{}]^{self3} - | since its capture set {self3} is read-only. + | Cannot assign to field fld of Ref[T^{}]^{Ref.this.rd} + | since its capture set {Ref.this.rd} of value self3 is read-only. -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:14:31 -------------------------------------- 14 | val self4: () => Ref[T]^ = () => this // error | ^^^^^^^^^^ - | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} - | Required: () => Ref[T]^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T^'s1]^{Ref.this.rd}. | - | where: => refers to a fresh root capability in the type of value self4 - | ^ and cap refer to a fresh root capability in the type of value self4 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability classified as Unscoped in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:18:16 ----------------------------------------------------------- @@ -46,13 +46,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:19:27 -------------------------------------- 19 | def self6(): Ref[T]^ = this // error // error separation | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the stateful type Ref[T]^, + | it cannot subsume a read-only capture set of the stateful type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability in the result type of method self6 + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:24:29 ----------------------------------------------------------- @@ -73,21 +73,21 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:41:29 -------------------------------------- 41 | val r5: () => Ref2[Int]^ = () => ref2 // error | ^^^^^^^^^^ - | Found: () ->{ref2.rd} Ref2[Int]^{ref2} - | Required: () => Ref2[Int]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, - | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | Note that {cap} is an exclusive capture set of the stateful type Ref2[Int]^, + | it cannot subsume a read-only capture set of the stateful type Ref2[Int]^{ref2}. | - | where: => refers to a fresh root capability in the type of value r5 - | ^ and cap refer to a fresh root capability in the type of value r5 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability classified as Unscoped in the type of value r5 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 ----------------------------------------------------------- 44 | r6().x.fld = 33 // error | ^^^^^^^^^^^^^^^ - | Cannot assign to field fld of Ref[Int]^{r6*.rd} - | since its capture set {r6*.rd} is read-only. + | Cannot assign to field fld of Ref[Int]^{cap.rd} + | since its capture set {cap.rd} is read-only. -- Error: tests/neg-custom-args/captures/mutvars.scala:9:15 ------------------------------------------------------------ 9 | val self2: Ref[T]^ = this // error // error separation | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/paths-complex-consume.scala b/tests/neg-custom-args/captures/paths-complex-consume.scala index 05b0592c6c3e..9c1deb031387 100644 --- a/tests/neg-custom-args/captures/paths-complex-consume.scala +++ b/tests/neg-custom-args/captures/paths-complex-consume.scala @@ -1,13 +1,13 @@ import language.experimental.captureChecking import language.experimental.separationChecking import caps.cap -import scala.caps.Mutable +import scala.caps.Stateful // Create a deeper nesting structure class D() class C(val d: D^) class B(val c: C^) -class A(consume val b: B^) extends Mutable: +class A(consume val b: B^) extends Stateful: update def use() = println("Using A") // Test 1: Accessing nested fields through a consumed path @@ -23,11 +23,11 @@ def testNestedFieldsAfterConsume = println(a.b.c.d) // OK - deeper nesting through consumed path // Test 2: Non-trivial prefix accessing a consumed field -class Container(consume val a: A^) extends Mutable: +class Container(consume val a: A^) extends Stateful: val other: A^ = A(B(C(D()))) update def operate() = other.use() -class Outer(consume val container: Container^) extends Mutable: +class Outer(consume val container: Container^) extends Stateful: update def execute() = container.operate() def testComplexPrefix = @@ -49,7 +49,7 @@ def testComplexPrefix = println(a1) // error // Test 3: Multiple consume parameters with nested access -class Multi(consume val b1: B^, consume val b2: B^) extends Mutable: +class Multi(consume val b1: B^, consume val b2: B^) extends Stateful: val b3: B^ = B(C(D())) update def combine() = () @@ -71,7 +71,7 @@ def testMultipleConsume = println(b2) // error // Test 4: Consume at multiple levels with complex paths -class Top(consume val outer: Outer^) extends Mutable: +class Top(consume val outer: Outer^) extends Stateful: update def topAction() = outer.execute() def testMultiLevelConsume = diff --git a/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala b/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala index 004443505324..9320fd6d932a 100644 --- a/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala +++ b/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala @@ -7,15 +7,15 @@ class Foo extends ExclusiveCapability, Classifier // Testing with various DerivedCapabilities class D class C(val d: D) -class B(val c: C) extends Foo, Mutable: +class B(val c: C) extends Foo, Stateful: update def foo() = println("foo") -class A(consume val b: B^) extends Mutable: +class A(consume val b: B^) extends Stateful: update def bar() = b.foo() -class A2(consume val b: B^) extends Mutable: +class A2(consume val b: B^) extends Stateful: update def bar() = b.foo() -class A3(consume var b: B^) extends Mutable: +class A3(consume var b: B^) extends Stateful: update def bar() = b.foo() -class A4(consume val b: A2^{cap.only[Foo]}) extends Mutable: // FIXME needs to be classified as Foo, too +class A4(consume val b: A2^{cap.only[Foo]}) extends Stateful: // FIXME needs to be classified as Foo, too update def bar() = b.b.foo() // Test: Access nested fields (suffix paths) after consume diff --git a/tests/neg-custom-args/captures/ref-with-file.check b/tests/neg-custom-args/captures/ref-with-file.check new file mode 100644 index 000000000000..0e3ebf764e3d --- /dev/null +++ b/tests/neg-custom-args/captures/ref-with-file.check @@ -0,0 +1,46 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:18:12 -------------------------------- +18 | withFile: f => // error + | ^ + |Found: (f: File^'s1) ->'s2 Ref[File^'s3]^ + |Required: (f: File^²) => Ref[File^'s4]^'s5 + | + |Note that capability cap cannot be included in capture set {} of value r. + | + |where: => refers to a fresh root capability created in method Test when checking argument to parameter op of method withFile + | ^ refers to a fresh root capability classified as Unscoped in the type of value r + | ^² refers to the universal root capability + | cap is a fresh root capability created in anonymous function of type (f: File^'s1): Ref[File^'s3]^ of parameter parameter f² of method $anonfun +19 | val r = Ref(f) +20 | r + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:21:12 -------------------------------- +21 | withFile: f => // error + | ^ + |Found: (f: File^'s6) ->'s7 (??? : -> Nothing) + |Required: (f: File^) => Nothing + | + |Note that capability cap cannot be included in capture set {} of value r. + | + |where: => refers to a fresh root capability created in method Test when checking argument to parameter op of method withFile + | ^ refers to the universal root capability + | cap is a fresh root capability created in anonymous function of type (f: File^'s6): (??? : -> Nothing) of parameter parameter f² of method $anonfun +22 | val r = Ref(f) +23 | ??? + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ref-with-file.scala:25:18 -------------------------------- +25 | withFileAndRef: (f, r: Ref[String]^) => // error + | ^ + |Capability cap outlives its scope: it leaks into outer capture set 's8 which is owned by method Test. + |The leakage occurred when trying to match the following types: + | + |Found: (f: File^'s9, r: Ref[String]^) ->'s10 Ref[String]^ + |Required: (f: File^, r: Ref[String]^) => Ref[String]^'s8 + | + |where: => refers to a fresh root capability created in method Test when checking argument to parameter op of method withFileAndRef + | ^ and cap refer to the universal root capability +26 | r.put(f.read()) +27 | r + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/ref-with-file.scala b/tests/neg-custom-args/captures/ref-with-file.scala new file mode 100644 index 000000000000..927e4a289aa7 --- /dev/null +++ b/tests/neg-custom-args/captures/ref-with-file.scala @@ -0,0 +1,28 @@ +import caps.* + +class Ref[T](init: T) extends Stateful, Unscoped: + var x = init + def get: T = x + update def put(y: T): Unit = x = y + +class File: + def read(): String = ??? + +def withFile[T](op: (f: File^) => T): T = + op(new File) + +def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T = + op(File(), Ref("")) + +def Test = + withFile: f => // error + val r = Ref(f) + r + withFile: f => // error + val r = Ref(f) + ??? + + withFileAndRef: (f, r: Ref[String]^) => // error + r.put(f.read()) + r + diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 3434539b10a4..c4ab6f6b5e3e 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -6,16 +6,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- 12 | val t: Ref^{cap} = a // error // error separation | ^ - | Found: (a : Ref) - | Required: Ref^ + | Found: (a : Ref) + | Required: Ref^ | - | Note that {cap} is an exclusive capture set of the mutable type Ref^, - | it cannot subsume a read-only capture set of the mutable type (a : Ref). + | Note that {cap} is an exclusive capture set of the stateful type Ref^, + | it cannot subsume a read-only capture set of the stateful type (a : Ref). | - | Note that capability cap².rd is not included in capture set {cap}. + | Note that capability cap².rd is not included in capture set {cap}. | - | where: ^ and cap refer to a fresh root capability in the type of value t - | cap² is a fresh root capability in the type of parameter a + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value t + | cap² is a fresh root capability classified as Unscoped in the type of parameter a | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:9 ------------------------------------------------- diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala index a2dfeed491b4..e6a851f9f4c5 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.scala +++ b/tests/neg-custom-args/captures/scope-extrude-mut.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -class A extends caps.Mutable: +class A extends caps.Stateful: var x = 0 class B: diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check index 54ab518926cc..548284898742 100644 --- a/tests/neg-custom-args/captures/sep-box.check +++ b/tests/neg-custom-args/captures/sep-box.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability classified as Unscoped created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 5854c52cd84b..68b893b12d33 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -4,14 +4,14 @@ | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad | on line 18 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter x + | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- 21 | par(rx, () => x.put(42)) // error | ^ | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad | on line 18 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter x + | where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index 3f98e6cd686a..aa751eba09b0 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -1,12 +1,12 @@ -- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 ------------------------------------------------------- 12 | def mkCounter(): Pair[Ref^, Ref^] = // error | ^^^^^^^^^^^^^^^^ - | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {c, cap, cap²}. - | Another part, Ref^², captures capabilities {c}. - | The two sets overlap at {c}. + |Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. + |One part, Ref^, hides capabilities {c, cap, cap²}. + |Another part, Ref^², captures capabilities {c}. + |The two sets overlap at {c}. | - | where: ^ refers to a fresh root capability in the result type of method mkCounter - | ^² refers to a fresh root capability in the result type of method mkCounter - | cap is a fresh root capability in the type of value c - | cap² is a fresh root capability created in value c when constructing instance Ref + |where: ^ refers to a fresh root capability classified as Unscoped in the result type of method mkCounter + | ^² refers to a fresh root capability classified as Unscoped in the result type of method mkCounter + | cap is a fresh root capability classified as Unscoped in the type of value c + | cap² is a fresh root capability classified as Unscoped created in value c when constructing instance Ref diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index ea32ef208b88..232144c1ebaf 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -24,8 +24,8 @@ | Footprint set of second argument : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test0 when checking argument to parameter x of method foo + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test0 when checking argument to parameter x of method foo -- Error: tests/neg-custom-args/captures/sep-curried.scala:22:44 ------------------------------------------------------- 22 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error | ^ @@ -41,8 +41,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in value f when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in value f when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:29:6 -------------------------------------------------------- 29 | foo(a)(a) // error | ^ @@ -58,8 +58,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test2 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test2 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:35:9 -------------------------------------------------------- 35 | foo(a)(a) // error | ^ @@ -75,8 +75,8 @@ | Footprint set of function prefix : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test3 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test3 when checking argument to parameter y of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:42:4 -------------------------------------------------------- 42 | f(a) // error | ^ @@ -92,5 +92,5 @@ | Footprint set of function prefix : {f, a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability in the type of value a - | ^² refers to a fresh root capability created in method test4 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value a + | ^² refers to a fresh root capability classified as Unscoped created in method test4 when checking argument to parameter y of method apply diff --git a/tests/neg-custom-args/captures/sep-list.check b/tests/neg-custom-args/captures/sep-list.check index 5ecde5d6d2bd..7b5b6bd69fa7 100644 --- a/tests/neg-custom-args/captures/sep-list.check +++ b/tests/neg-custom-args/captures/sep-list.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {h2, xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability classified as Unscoped created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check index ff0d2237dd2d..7dd80ba80a15 100644 --- a/tests/neg-custom-args/captures/sep-pairs-unboxed.check +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -13,8 +13,8 @@ | Footprint set of second argument : {x} | The two sets overlap at : {x} | - |where: ^ refers to a fresh root capability in the type of parameter x - | ^² refers to a fresh root capability created in method mkPair when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability classified as Unscoped in the type of parameter x + | ^² refers to a fresh root capability classified as Unscoped created in method mkPair when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 ------------------------------------------------- 35 | val twoCopy = Pair(two.fst, two.fst) // error | ^^^^^^^ @@ -30,8 +30,8 @@ | Footprint set of second argument : {two.fst} | The two sets overlap at : {two.fst} | - |where: ^ refers to a fresh root capability in the type of value fst - | ^² refers to a fresh root capability created in value twoCopy when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value fst + | ^² refers to a fresh root capability classified as Unscoped created in value twoCopy when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 ------------------------------------------------- 41 | val twisted = PairPair(two.fst, two) // error | ^^^^^^^ @@ -39,7 +39,7 @@ |to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair |corresponds to capture-polymorphic formal parameter fst of type Ref^² |and hides capabilities {two.fst}. - |Some of these overlap with the captures of the second argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. + |Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). | | Hidden set of current argument : {two.fst} | Hidden footprint of current argument : {two.fst} @@ -47,8 +47,8 @@ | Footprint set of second argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability in the type of value fst - | ^² refers to a fresh root capability created in value twisted when checking argument to parameter fst of constructor PairPair + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value fst + | ^² refers to a fresh root capability classified as Unscoped created in value twisted when checking argument to parameter fst of constructor PairPair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:33 ------------------------------------------------- 47 | val twisted = swapped(two, two.snd) // error | ^^^^^^^ @@ -56,7 +56,7 @@ |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^ |corresponds to capture-polymorphic formal parameter y of type Ref^² |and hides capabilities {two.snd}. - |Some of these overlap with the captures of the first argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. + |Some of these overlap with the captures of the first argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). | | Hidden set of current argument : {two.snd} | Hidden footprint of current argument : {two.snd} @@ -64,8 +64,8 @@ | Footprint set of first argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability in the type of value snd - | ^² refers to a fresh root capability created in value twisted when checking argument to parameter y of method swapped + |where: ^ refers to a fresh root capability classified as Unscoped in the type of value snd + | ^² refers to a fresh root capability classified as Unscoped created in value twisted when checking argument to parameter y of method swapped -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 ------------------------------------------------- 58 | val twoOther = Pair(two.fst, two.snd) // error // error | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index 6005eb1a49e6..9b6cb295d8e8 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -6,27 +6,27 @@ | Another part, Ref^², captures capabilities {r0}. | The two sets overlap at {r0}. | - | where: ^ refers to a fresh root capability in the type of value r1 - | ^² refers to a fresh root capability in the type of value r1 + | where: ^ refers to a fresh root capability classified as Unscoped in the type of value r1 + | ^² refers to a fresh root capability classified as Unscoped in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:13:9 ---------------------------------------------------------- 13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0 | ^^^^^^^^^^^^^^^^ - | Separation failure in method bad's result type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {r1*, cap, cap², r0}. - | Another part, Ref^², captures capabilities {r1*, r0}. - | The two sets overlap at {r1*, r0}. + | Separation failure in method bad's result type Pair[Ref^, Ref^²]. + | One part, Ref^, hides capabilities {r1*, cap, cap², r0}. + | Another part, Ref^², captures capabilities {r1*, r0}. + | The two sets overlap at {r1*, r0}. | - | where: ^ refers to a fresh root capability in the result type of method bad - | ^² refers to a fresh root capability in the result type of method bad - | cap is a fresh root capability in the type of value r1 - | cap² is a fresh root capability in the type of value r1 + | where: ^ refers to a fresh root capability classified as Unscoped in the result type of method bad + | ^² refers to a fresh root capability classified as Unscoped in the result type of method bad + | cap is a fresh root capability classified as Unscoped in the type of value r1 + | cap² is a fresh root capability classified as Unscoped in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:43:18 --------------------------------------------------------- 43 | val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error | ^^^^^^^^^^^^^^^^ - | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {fstSame}. - | Another part, Ref^², captures capabilities {sndSame, same.snd*}. - | The two sets overlap at {cap of value same}. + | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. + | One part, Ref^, hides capabilities {fstSame}. + | Another part, Ref^², captures capabilities {sndSame, same.snd*}. + | The two sets overlap at {cap of value same}. | - | where: ^ refers to a fresh root capability in the type of value sameToPair - | ^² refers to a fresh root capability in the type of value sameToPair + | where: ^ refers to a fresh root capability classified as Unscoped in the type of value sameToPair + | ^² refers to a fresh root capability classified as Unscoped in the type of value sameToPair diff --git a/tests/neg-custom-args/captures/unscoped-classifier.check b/tests/neg-custom-args/captures/unscoped-classifier.check index c14a151105e5..b891c64907bd 100644 --- a/tests/neg-custom-args/captures/unscoped-classifier.check +++ b/tests/neg-custom-args/captures/unscoped-classifier.check @@ -13,9 +13,10 @@ -- Error: tests/neg-custom-args/captures/unscoped-classifier.scala:17:15 ----------------------------------------------- 17 | def gg() = g() // error but msg could be better | ^ - | reference (g : () => Unit) is not included in the allowed capture set {cap} of the self type of class E + | Read-only method gg accesses exclusive capability (g : () => Unit); + | method gg should be declared an update method to allow this. | - | where: cap is a fresh root capability classified as Unscoped in the type of class E + | where: => refers to a fresh root capability in the type of parameter g -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unscoped-classifier.scala:19:11 -------------------------- 19 | val b = B() // error but msg could be better | ^^^ diff --git a/tests/neg-custom-args/captures/update-call.scala b/tests/neg-custom-args/captures/update-call.scala index aa2913645e43..19f21ff69829 100644 --- a/tests/neg-custom-args/captures/update-call.scala +++ b/tests/neg-custom-args/captures/update-call.scala @@ -1,6 +1,6 @@ -import caps.Mutable +import caps.Stateful -trait IterableOnce[T] extends Mutable: +trait IterableOnce[T] extends Stateful: def iterator: Iterator[T]^{this} update def foreach(op: T => Unit): Unit diff --git a/tests/new/test.scala b/tests/new/test.scala index 00174769a0f0..4541893e0ffb 100644 --- a/tests/new/test.scala +++ b/tests/new/test.scala @@ -1 +1,27 @@ -object Test +import caps.* + +class Ref[T](init: T) extends caps.Stateful, Unscoped: + var x = init + def get: T = x + update def put(y: T): Unit = x = y + +class File: + def read(): String = ??? + +def withFile[T](op: (f: File^) => T): T = + op(new File) + +def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T = + op(File(), Ref("")) + +def Test = +/* + withFileAndRef: (f, r: Ref[String]^) => + r.put(f.read()) +*/ + + withFileAndRef: (f, r) => + r.put(f.read()) + + + diff --git a/tests/pos-custom-args/captures/i23422.scala b/tests/pos-custom-args/captures/i23422.scala index f014473f3f2d..72bf3158a702 100644 --- a/tests/pos-custom-args/captures/i23422.scala +++ b/tests/pos-custom-args/captures/i23422.scala @@ -3,7 +3,7 @@ import caps.* trait Cap class Inv[T] extends SharedCapability class Inv2[T] -class Inv3[T] extends Mutable +class Inv3[T] extends Stateful def test(c: Cap^): Unit = val t1: Inv[() ->{c} Unit] = Inv() // error val t2: Inv2[() ->{c} Unit] = Inv2() // ok diff --git a/tests/pos-custom-args/captures/i24373b.scala b/tests/pos-custom-args/captures/i24373b.scala index 342f48d36f76..23f9fbc25c66 100644 --- a/tests/pos-custom-args/captures/i24373b.scala +++ b/tests/pos-custom-args/captures/i24373b.scala @@ -1,13 +1,13 @@ trait Foo extends caps.ExclusiveCapability -trait Bar extends Foo, caps.Mutable +trait Bar extends Foo, caps.Stateful def Test = def f(self: Foo^): Unit = () val x: Bar^ = new Bar {} - val g = () => f(x) // `Foo` is not Mutable so `x.rd` is charged here + val g = () => f(x) // `Foo` is not Stateful so `x.rd` is charged here val _: () ->{x.rd} Unit = g // surprising, but correct diff --git a/tests/pos-custom-args/captures/mark-free-ro.scala b/tests/pos-custom-args/captures/mark-free-ro.scala index 625b6ba7813c..698155fae410 100644 --- a/tests/pos-custom-args/captures/mark-free-ro.scala +++ b/tests/pos-custom-args/captures/mark-free-ro.scala @@ -1,10 +1,10 @@ -import caps.{cap, Mutable} +import caps.{cap, Stateful} import caps.unsafe.untrackedCaptures -class Test extends Mutable: +class Test extends Stateful: var ctxStack: Array[FreshCtx^] = new Array(10) - class FreshCtx(level: Int) extends Mutable: + class FreshCtx(level: Int) extends Stateful: this: FreshCtx^ => def detached: Boolean = val c: FreshCtx^{cap.rd} = ctxStack(level) diff --git a/tests/pos-custom-args/captures/mut-iterator.scala b/tests/pos-custom-args/captures/mut-iterator.scala index c019f0cc95ff..a07bc205cfc1 100644 --- a/tests/pos-custom-args/captures/mut-iterator.scala +++ b/tests/pos-custom-args/captures/mut-iterator.scala @@ -1,6 +1,6 @@ -import caps.{cap, Mutable, SharedCapability} +import caps.{cap, Stateful, SharedCapability} -trait Iterator[T] extends Mutable: +trait Iterator[T] extends Stateful: def hasNext: Boolean update def next(): T diff --git a/tests/pos-custom-args/captures/mutable-capturing-sharable.scala b/tests/pos-custom-args/captures/mutable-capturing-sharable.scala index d3b6650f90bc..ec63d1ada2b0 100644 --- a/tests/pos-custom-args/captures/mutable-capturing-sharable.scala +++ b/tests/pos-custom-args/captures/mutable-capturing-sharable.scala @@ -3,7 +3,7 @@ import language.experimental.separationChecking import caps.* class Logger extends SharedCapability: def log(msg: String): Unit = () -class TracedRef(logger: Logger^{cap.only[SharedCapability]}) extends Mutable: +class TracedRef(logger: Logger^{cap.only[SharedCapability]}) extends Stateful: private var _data: Int = 0 update def set(newValue: Int): Unit = logger.log("set") @@ -12,7 +12,7 @@ class TracedRef(logger: Logger^{cap.only[SharedCapability]}) extends Mutable: logger.log("get") // error, but should it be allowed? _data -class TracedRef2(logger: Logger) extends Mutable: +class TracedRef2(logger: Logger) extends Stateful: private var _data: Int = 0 update def set(newValue: Int): Unit = logger.log("set") diff --git a/tests/pos-custom-args/captures/mutable-hiding-shared.scala b/tests/pos-custom-args/captures/mutable-hiding-shared.scala index fad7bbe0389c..daf46e583305 100644 --- a/tests/pos-custom-args/captures/mutable-hiding-shared.scala +++ b/tests/pos-custom-args/captures/mutable-hiding-shared.scala @@ -3,7 +3,7 @@ import caps.* class Logger extends SharedCapability: def log(msg: String): Unit = println(msg) -class Ref(init: Int)(using l: Logger) extends Mutable: +class Ref(init: Int)(using l: Logger) extends Stateful: self: Ref^ => private var current = init def get(): Int = diff --git a/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala index 76573f0238b4..eee75b728bbe 100644 --- a/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala +++ b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala @@ -6,7 +6,7 @@ import caps.* class D class C(val d: D^) class B(val c: C^) -class A(consume val b: B^) extends Mutable { var x: Int = 0 } +class A(consume val b: B^) extends Separate // Test 1: Simple suffix paths after consume def test1 = diff --git a/tests/pos-custom-args/captures/ref-with-file.scala b/tests/pos-custom-args/captures/ref-with-file.scala index 1922a52f0c88..fbb28377fa2d 100644 --- a/tests/pos-custom-args/captures/ref-with-file.scala +++ b/tests/pos-custom-args/captures/ref-with-file.scala @@ -1,6 +1,6 @@ import caps.* -class Ref[T](init: T) extends Mutable, Unscoped: +class Ref[T](init: T) extends caps.Stateful, Unscoped: var x = init def get: T = x update def put(y: T): Unit = x = y @@ -11,9 +11,15 @@ class File: def withFile[T](op: (f: File^) => T): T = op(new File) +def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T = + op(File(), Ref("")) + def Test = withFile: f => val r = Ref(f.read()) r + withFileAndRef: (f, r: Ref[String]^) => + r.put(f.read()) + diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala index 002410e2afd4..bcc4aa1be1c5 100644 --- a/tests/pos-custom-args/captures/ro-array.scala +++ b/tests/pos-custom-args/captures/ro-array.scala @@ -1,7 +1,7 @@ import caps.* object Test -class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Mutable: +class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Stateful: private val arr: Array[T] = new Array[T](len) def get(i: Int): T = arr(i) update def set(i: Int, x: T): Unit = arr(i) = x diff --git a/tests/pos-custom-args/captures/unscoped-ref-result.scala b/tests/pos-custom-args/captures/unscoped-ref-result.scala new file mode 100644 index 000000000000..fa0601ddf08c --- /dev/null +++ b/tests/pos-custom-args/captures/unscoped-ref-result.scala @@ -0,0 +1,11 @@ +class Ref[T](init: T) extends caps.Mutable: + var x: T = init + update def set(x: T) = this.x = x + +class Ref2[T](init: T) extends caps.Mutable: + val x = Ref[T](init) + +def test = + val r4 = () => Ref2(22) + val _: Ref2[Int]^{r4*} = r4() + r4().x.set(33) // ok diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index 13b1c9f46fe2..b1e6e8321596 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -36,9 +36,11 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.Contains$.containsImpl", "scala.caps.Exists", "scala.caps.ExclusiveCapability", + "scala.caps.Stateful", + "scala.caps.Separate", + "scala.caps.Unscoped", "scala.caps.Mutable", "scala.caps.Read", - "scala.caps.Unscoped", "scala.caps.internal", "scala.caps.internal$", "scala.caps.cap",