Add new HOLETYPES to TASTy format #17225
Closed
Conversation
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 was referenced Apr 11, 2023
nicolasstucki
force-pushed
the
add-tasty-hole-types
branch
from
68343c1 to
8204725
Compare
nicolasstucki
added
the
needs-minor-release
smarter
requested changes
Apr 11, 2023
| if targs.nonEmpty then | ||
| writeByte(HOLETYPES) | ||
| withLength { | ||
| targs.foreach(targ => pickleType(targ.tpe)) |
There was a problem hiding this comment.
Is there no position information in the targ that we're loosing by storing only the type?
| until(typesEnd)(readType()).map(TypeTree(_)) | ||
| else Nil | ||
| val args = until(end)(readTerm()) | ||
| TastyQuoteHole(true, idx, targs ::: args, TypeTree(tpe)).withType(tpe) |
There was a problem hiding this comment.
Is it useful to have the TypeTree parameter here if it's the same as the type of the tree?
There was a problem hiding this comment.
Maybe not. It is useful to have it in the TASTy HOLE. But we might be able to remove it from here.
There was a problem hiding this comment.
If we remove it, we don't have a way to retype the tree. I do not have another way to infer the type of hole. This is an issue when Ychecking the tree.
There was a problem hiding this comment.
The TreeChecker uses promote to retype trees with their existing type.
|
|
||
| HOLE Length idx_Nat tpe_Type (HOLETYPES Length targ_Type*)? arg_Tree* | ||
| -- Splice hole with index `idx`, the type of the hole `tpe`, type arguments of the hole `targ`s and term arguments of the hole `arg`s | ||
| -- Note: From 3.0 to 3.3 `args` could contain type arguments as well. This is no longer the case. |
There was a problem hiding this comment.
To be clear, args when you say "type arguments" here you mean TypeTrees, as opposed to the use of "type arguments" in the previous sentence where they are Types?
nicolasstucki
force-pushed
the
add-tasty-hole-types
branch
2 times, most recently
from
84d5293 to
e14f569
Compare
This is a new encoding of HOLE that differentiates between type and
term arguments of the hole.
```
Term = ...
HOLE Length idx_Nat tpe_Type HoleTypes? arg_Tree*
-- Splice hole with index `idx`, the type of the hole `tpe`,
type arguments of the hole `targ`s and term arguments
of the hole `arg`s
HoleTypes = HOLETYPES Length targ_Type*
```
nicolasstucki
force-pushed
the
add-tasty-hole-types
branch
from
e14f569 to
40cee6a
Compare
nicolasstucki
added a commit
that referenced
this pull request
Aug 8, 2023
This is a new encoding of HOLE that differentiates between type and term
arguments of the hole.
```
-- pickled quote trees: These trees can only appear in pickled quotes. They will never be in a TASTy file.
EXPLICITtpt tpt_Term
-- Tag for a type tree that in a context where it is not explicitly known that this tree is a type.
HOLE Length idx_Nat tpe_Type arg_Tree*
-- Splice hole with index `idx`, the type of the hole `tpe`, type and term arguments of the hole `arg`s
```
We will pickle type trees in `arg_Tree` using the `EXPLICITtpt` tag.
We will only have hole captured types if there is a type defined in a
quote and used in a nested quote. Most of the time we do not have those
types and therefore no overhead in the encoding compared to before this
change.
Alternative to #17225
Fixes #17137
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This is a new encoding of HOLE that differentiates between type and
term arguments of the hole.
We will only have hole
targsif there is a type defined in a quote and used in a nested quote. Most of the time we do not have those types and therefore no overhead in the encoding compared to before this change.Based on #17144