Skip to content
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

Remove PostTypeChecker #1878

Merged
merged 8 commits into from
Jun 28, 2022
Merged

Remove PostTypeChecker #1878

merged 8 commits into from
Jun 28, 2022

Conversation

konnov
Copy link
Collaborator

@konnov konnov commented Jun 24, 2022

Blocked by #1880.

Extracted from #1870, as it requires more work on the integration tests.

Closes #1323. Removed the PostTypeChecker pass, as it was really stepping in the way, producing incomprehensible error messages. This started to happen in conjunction with row types, which can be quite tricky to understand when they contain a free variable. This feature should have been implemented in a separate PR, but it was too late. Here are the affected files:

  • deleted PostTypeCheckerPassImpl.scala

  • added MonotypeLanguagePred that ensures that all types are monotypes

  • placed an additional check with MonotypeLanguagePred in BoundedCheckerPassImpl

  • added/changed a few additional classes ReTLACombinedPredicate.scala, ReTLAToVMTModule.scala.

  • Ran make fmt-fix (or had formatting run automatically on all files edited)

  • Entries added to ./unreleased/ for any new functionality

@codecov-commenter
Copy link

codecov-commenter commented Jun 24, 2022

Codecov Report

Merging #1878 (fefec2d) into unstable (388d695) will decrease coverage by 0.08%.
The diff coverage is 0.00%.

@@             Coverage Diff              @@
##           unstable    #1878      +/-   ##
============================================
- Coverage     76.75%   76.67%   -0.09%     
============================================
  Files           400      401       +1     
  Lines         12305    12319      +14     
  Branches        574      575       +1     
============================================
  Hits           9445     9445              
- Misses         2860     2874      +14     
Impacted Files Coverage Δ
...syte/apalache/tla/bmcmt/config/CheckerModule.scala 0.00% <ø> (ø)
...ache/tla/bmcmt/config/ReTLACombinedPredicate.scala 0.00% <0.00%> (ø)
...e/apalache/tla/bmcmt/config/ReTLAToVMTModule.scala 0.00% <0.00%> (ø)
...ache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala 0.00% <0.00%> (ø)
...che/tla/lir/transformations/LanguageWatchdog.scala 50.00% <0.00%> (ø)
...ransformations/standard/MonotypeLanguagePred.scala 0.00% <0.00%> (ø)
...a/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala 97.36% <0.00%> (-2.64%) ⬇️
...he/io/annotations/parser/CommentPreprocessor.scala 97.80% <0.00%> (+1.09%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 388d695...fefec2d. Read the comment docs.

@konnov konnov added the blocked Issue blocked by another (for filtering) label Jun 24, 2022
@shonfeder
Copy link
Contributor

Thank you for factoring out for a smaller review.

I'll wait to review here until the integration tests are passing.

@Kukovec Kukovec removed the blocked Issue blocked by another (for filtering) label Jun 28, 2022
@konnov
Copy link
Collaborator Author

konnov commented Jun 28, 2022

This PR has passing tests. @Kukovec, @shonfeder, do you have free cycles to review this PR?

@konnov konnov merged commit 306eb3f into unstable Jun 28, 2022
@konnov konnov deleted the ik/monotypes2 branch June 28, 2022 15:32
This was referenced Jul 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[FEATURE] Ensure post type checking is optional
4 participants