Variants in the type checker #1847
Merged
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
18 tasks
Codecov Report
@@ Coverage Diff @@
## unstable #1847 +/- ##
============================================
+ Coverage 76.69% 76.76% +0.07%
============================================
Files 391 392 +1
Lines 12005 12038 +33
Branches 550 579 +29
============================================
+ Hits 9207 9241 +34
+ Misses 2798 2797 -1
Continue to review full report at Codecov.
|
shonfeder
reviewed
Jun 7, 2022
| @@ -110,6 +110,23 @@ class TestAnnotationParser extends AnyFunSuite with Checkers { | |||
| .map(r => fail("Expected a failure. Found: " + r)) | |||
| } | |||
|
|
|||
| test("parse variants in type aliases") { | |||
| val extractedText = | |||
| """MESSAGE =""" + "\n" + """ Req({ ask: Int }) """ + "\n" + """ | Ack({ success: Bool })""" | |||
There was a problem hiding this comment.
Seem like this could be a lot clearer using a multi-line string, no?
There was a problem hiding this comment.
For sure. The problem is that stripMargin is using | as a delimiter. So the tests were breaking. I could not find a better solution :(
There was a problem hiding this comment.
Oh I see! I think we can do
Suggested change
| """MESSAGE =""" + "\n" + """ Req({ ask: Int }) """ + "\n" + """ | Ack({ success: Bool })""" | |
| """#MESSAGE = | |
| #| Req({ ask: Int }) | |
| #| Ack({ success: Bool })""".stripMargin('#') |
Or using whatever char might be better in place of #.
I'd suggest making this change improves readability enough that it would be worth making the change here, but i won't block on it.
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
Outdated
Show resolved
Hide resolved
bugarela
approved these changes
Jun 7, 2022
tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <shon@informal.systems> Co-authored-by: Gabriela Moreira <gabrielamoreiramafra@gmail.com>
shonfeder
approved these changes
Jun 9, 2022
| @@ -156,6 +157,15 @@ class TestCommentPreprocessor extends AnyFunSuite with Checkers { | |||
| hasAnnotationsWhenNonEmpty("""(* aaa *)""") | |||
| } | |||
|
|
|||
| test("accept pipe") { | |||
| val extractedText = | |||
| """@typeAlias: MESSAGE = { tag: "req", ask: Int }""" + "\n" + """ | { tag: "ack", success: Bool };""" | |||
There was a problem hiding this comment.
Could also be cleaned up here using stripMargin
Merged
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 PR implements support for the variant type. On the way of implementing it, I have found the proposed syntax too inconvenient to work with, both at the user level and the implementation level. I have refactored it, similar to what was suggested earlier by @shonfeder. This will need an update to the ADRs in follow-up PRs. What is done here:
Variant1(Int) | Variant2({ value: Int, success: Bool}). SeeDefaultType1Parser.Variants.tla.SanyImporterto support the new API.ToEtcExpr, which implements the type checking rules.make fmt-fix(or had formatting run automatically on all files edited)