-
Notifications
You must be signed in to change notification settings - Fork 1.1k
CC: Drop idempotent type maps #22910
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
29 commits
Select commit
Hold shift + click to select a range
d72e5ea
Fix override checking of alias vs abstract types
odersky 19dcfa2
Refactor: Drop isSubType parameter for override checking
odersky e9cdf94
More targeted handling of overriding checks against CapSet^
odersky cd2b7e6
Fix pathRoot
odersky 58162ff
Simplify levelOK check for of Result(...) instances
odersky 9105cf3
Reject ParamRefs in capture sets that are not in the result type of t…
odersky f6e5bc6
Harden checkApply duplicate error detection
odersky fc06af6
Under 3.8 solve all capture sets in types of vals and defs
odersky 67446d2
Solve all capture sets in types of vals and defs by default
odersky ccf9867
Simplify setup
odersky 1611183
Fix to interpolation
odersky 90cee43
Redo handling of closures without relying on pre-existing maps
odersky c662bc3
Re-use `NamerOps.methodType when computing initial types of methods
odersky 50b0b4d
Drop some BiTypeMaps
odersky dbd6f8f
Fuse successive SubstBindings maps and filters
odersky f33058c
Add tests that failed in CI before
odersky f43d24b
Drop IdempotentCaptRefMap and Mapped sets
odersky d8a8084
Unify existentials when matching function types
odersky 6d9dbf6
Tighten subsumption checking of Fresh instances
odersky 56de8df
Fix isPartOf
odersky 09e05f0
Fix SubstBindings BiTypeMap logic
odersky 58d052e
Variations on a test case
odersky bd0533a
Make captureSetofInfo cache in CaptureRefs depend on iteration count
odersky bb51ba0
Redo capture checks if necessary
odersky 99f5628
Revert "Split posCC from pos tests"
odersky d674405
Drop healTypeParam
odersky 3dd4f10
Refactor: move ccConfig into separate file
odersky 053341d
Refactor: Move CCState to separate file and make it more class based
odersky 86970ef
Refactor: Move previously @sharable data to ccState
odersky File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,165 @@ | ||
package dotty.tools | ||
package dotc | ||
package cc | ||
|
||
import core.* | ||
import CaptureSet.{CompareResult, CompareFailure, VarState} | ||
import collection.mutable | ||
import reporting.Message | ||
import Contexts.Context | ||
import Types.MethodType | ||
import Symbols.Symbol | ||
|
||
/** Capture checking state, which is known to other capture checking components */ | ||
class CCState: | ||
import CCState.* | ||
|
||
// ------ Error diagnostics ----------------------------- | ||
|
||
/** Error reprting notes produces since the last call to `test` */ | ||
var notes: List[ErrorNote] = Nil | ||
|
||
def addNote(note: ErrorNote): Unit = | ||
if !notes.exists(_.getClass == note.getClass) then | ||
notes = note :: notes | ||
|
||
def test(op: => CompareResult): CompareResult = | ||
val saved = notes | ||
notes = Nil | ||
try op match | ||
case res: CompareFailure => res.withNotes(notes) | ||
case res => res | ||
finally notes = saved | ||
|
||
def testOK(op: => Boolean): CompareResult = | ||
test(if op then CompareResult.OK else CompareResult.Fail(Nil)) | ||
|
||
/** Warnings relating to upper approximations of capture sets with | ||
* existentially bound variables. | ||
*/ | ||
val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer() | ||
|
||
// ------ Level handling --------------------------- | ||
|
||
private var curLevel: Level = outermostLevel | ||
|
||
/** The level of the current environment. Levels start at 0 and increase for | ||
* each nested function or class. -1 means the level is undefined. | ||
*/ | ||
def currentLevel(using Context): Level = curLevel | ||
|
||
/** Perform `op` in the next inner level */ | ||
inline def inNestedLevel[T](inline op: T)(using Context): T = | ||
val saved = curLevel | ||
curLevel = curLevel.nextInner | ||
try op finally curLevel = saved | ||
|
||
/** Perform `op` in the next inner level unless `p` holds. */ | ||
inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T = | ||
val saved = curLevel | ||
if !p then curLevel = curLevel.nextInner | ||
try op finally curLevel = saved | ||
|
||
/** A map recording the level of a symbol */ | ||
private val mySymLevel: mutable.Map[Symbol, Level] = mutable.Map() | ||
|
||
def symLevel(sym: Symbol): Level = mySymLevel.getOrElse(sym, undefinedLevel) | ||
|
||
def recordLevel(sym: Symbol)(using Context): Unit = mySymLevel(sym) = curLevel | ||
|
||
// ------ BiTypeMap adjustment ----------------------- | ||
|
||
private var myMapFutureElems = true | ||
|
||
/** When mapping a capture set with a BiTypeMap, should we create a BiMapped set | ||
* so that future elements can also be mapped, and elements added to the BiMapped | ||
* are back-propagated? Turned off when creating capture set variables for the | ||
* first time, since we then do not want to change the binder to the original type | ||
* without capture sets when back propagating. Error case where this shows: | ||
* pos-customargs/captures/lists.scala, method m2c. | ||
*/ | ||
def mapFutureElems(using Context) = myMapFutureElems | ||
|
||
/** Don't map future elements in this `op` */ | ||
inline def withoutMappedFutureElems[T](op: => T)(using Context): T = | ||
val saved = mapFutureElems | ||
myMapFutureElems = false | ||
try op finally myMapFutureElems = saved | ||
|
||
// ------ Iteration count of capture checking run | ||
|
||
private var iterCount = 1 | ||
|
||
def iterationId = iterCount | ||
|
||
def nextIteration[T](op: => T): T = | ||
iterCount += 1 | ||
try op finally iterCount -= 1 | ||
|
||
// ------ Global counters ----------------------- | ||
|
||
/** Next CaptureSet.Var id */ | ||
var varId = 0 | ||
|
||
/** Next root id */ | ||
var rootId = 0 | ||
|
||
// ------ VarState singleton objects ------------ | ||
// See CaptureSet.VarState creation methods for documentation | ||
|
||
object Separate extends VarState.Separating | ||
object HardSeparate extends VarState.Separating | ||
object Unrecorded extends VarState.Unrecorded | ||
object ClosedUnrecorded extends VarState.ClosedUnrecorded | ||
|
||
// ------ Context info accessed from companion object when isCaptureCheckingOrSetup is true | ||
|
||
private var openExistentialScopes: List[MethodType] = Nil | ||
|
||
private var capIsRoot: Boolean = false | ||
|
||
object CCState: | ||
|
||
opaque type Level = Int | ||
|
||
val undefinedLevel: Level = -1 | ||
|
||
val outermostLevel: Level = 0 | ||
|
||
extension (x: Level) | ||
def isDefined: Boolean = x >= 0 | ||
def <= (y: Level) = (x: Int) <= y | ||
def nextInner: Level = if isDefined then x + 1 else x | ||
|
||
/** If we are currently in capture checking or setup, and `mt` is a method | ||
* type that is not a prefix of a curried method, perform `op` assuming | ||
* a fresh enclosing existential scope `mt`, otherwise perform `op` directly. | ||
*/ | ||
inline def inNewExistentialScope[T](mt: MethodType)(op: => T)(using Context): T = | ||
if isCaptureCheckingOrSetup then | ||
val ccs = ccState | ||
val saved = ccs.openExistentialScopes | ||
if mt.marksExistentialScope then ccs.openExistentialScopes = mt :: ccs.openExistentialScopes | ||
try op finally ccs.openExistentialScopes = saved | ||
else | ||
op | ||
|
||
/** The currently opened existential scopes */ | ||
def openExistentialScopes(using Context): List[MethodType] = ccState.openExistentialScopes | ||
|
||
/** Run `op` under the assumption that `cap` can subsume all other capabilties | ||
* except Result capabilities. Every use of this method should be scrutinized | ||
* for whether it introduces an unsoundness hole. | ||
*/ | ||
inline def withCapAsRoot[T](op: => T)(using Context): T = | ||
if isCaptureCheckingOrSetup then | ||
val ccs = ccState | ||
val saved = ccs.capIsRoot | ||
ccs.capIsRoot = true | ||
try op finally ccs.capIsRoot = saved | ||
else op | ||
|
||
/** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */ | ||
def capIsRoot(using Context): Boolean = ccState.capIsRoot | ||
|
||
end CCState |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just wondering, do you know the highest number the counter goes when running the tests?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there should be at most one extra iteration. I believe that's the case always, but I am not sure about that.