Integrating types 9: a few bugfixes #671
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
shonfeder
approved these changes
Mar 23, 2021
tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Desugarer.scala
Outdated
Show resolved
Hide resolved
konnov
added a commit
that referenced
this pull request
Mar 23, 2021
* migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon
konnov
added a commit
that referenced
this pull request
Mar 23, 2021
* a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon
konnov
added a commit
that referenced
this pull request
Mar 23, 2021
* add a watchdog listener * close #647: Desugarer preprocesses the general case of EXCEPT * unrelease notes * type-aware test for Desugarer * made Desugarer type-aware! * fixed a type bug that was found by the type watchdog * propagating types in AssignmentOperatorIntroduction * made SkolemizationMarker type-aware * made ExpansionMarker type-aware * fixed TestSymbTransGenerator * moved the integration tests to test/tla * removed the Paxos tests, which is already in the integration tests * enabled snowcat by default, as the preprocessing is type-aware * Integrating types 7: victory over enthropy (#663) * a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon
konnov
added a commit
that referenced
this pull request
Mar 23, 2021
…type-aware (#657) * bugfix: translating labels * fixing types in Unroller and Inliner * moved and rewrote TestInlinerofUserOper, made it type-aware * made TestUnroller type-aware * made ParameterNormalizer type-aware * made TestUnroller and Unroller type-aware * running the type checker right after the parser * a reference to the closed issue * Integrating types 6: made Desugarer type aware (#658) * add a watchdog listener * close #647: Desugarer preprocesses the general case of EXCEPT * unrelease notes * type-aware test for Desugarer * made Desugarer type-aware! * fixed a type bug that was found by the type watchdog * propagating types in AssignmentOperatorIntroduction * made SkolemizationMarker type-aware * made ExpansionMarker type-aware * fixed TestSymbTransGenerator * moved the integration tests to test/tla * removed the Paxos tests, which is already in the integration tests * enabled snowcat by default, as the preprocessing is type-aware * Integrating types 7: victory over enthropy (#663) * a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon
konnov
added a commit
that referenced
this pull request
Mar 24, 2021
* annotated all tests and fixed some * Integrating types 5: made Inliner, Unroller, and ParameterNormalizer type-aware (#657) * bugfix: translating labels * fixing types in Unroller and Inliner * moved and rewrote TestInlinerofUserOper, made it type-aware * made TestUnroller type-aware * made ParameterNormalizer type-aware * made TestUnroller and Unroller type-aware * running the type checker right after the parser * a reference to the closed issue * Integrating types 6: made Desugarer type aware (#658) * add a watchdog listener * close #647: Desugarer preprocesses the general case of EXCEPT * unrelease notes * type-aware test for Desugarer * made Desugarer type-aware! * fixed a type bug that was found by the type watchdog * propagating types in AssignmentOperatorIntroduction * made SkolemizationMarker type-aware * made ExpansionMarker type-aware * fixed TestSymbTransGenerator * moved the integration tests to test/tla * removed the Paxos tests, which is already in the integration tests * enabled snowcat by default, as the preprocessing is type-aware * Integrating types 7: victory over enthropy (#663) * a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon * fixed the accidental bug introduced in refactoring
konnov
added a commit
that referenced
this pull request
Mar 24, 2021
…es type-aware (#650) * made Normalizer type-aware * Refactored Builder, introduced UntypedPredefs and TypedPredefs, removed several implicits * fix TestReplaceFixed * fix TestChangeListener * fix TestLetInExpander * fix TestIncrementalRenaming * fix TestBuilder * fix TestSourceStore * fix TestSanyImporter * fix Keramelizer and TestKeramelizer * fix TestDesugarer * fix TestExprOptimizer * fix TestOperAppToLetInDef * fix TestUnroller * fix TestAssignmentStrategyEncoder * fix TestSmtFreeSTE * fix TestSymbTransGenerator * fix TestRewriterKeraSet * fix TestExpansionMarker * fix TestSkolemizationMarker * fix TestSparseOracle * fix oracles * fix more tests * fix AbstractTestTransitionExecutorImpl * fox TestSymbStateRewriterSequence * fix TestSymbStateRewriterInt * a quick test for Normalizer and a bug fix in Normalizer * fixed the copy-pasted test * fix formatting * fixed after comments by Jure * changed two expressions to the IR form, for consistency * addressed the comments by Shon * Integrating types 4: migrated tests to Snowcat (#652) * annotated all tests and fixed some * Integrating types 5: made Inliner, Unroller, and ParameterNormalizer type-aware (#657) * bugfix: translating labels * fixing types in Unroller and Inliner * moved and rewrote TestInlinerofUserOper, made it type-aware * made TestUnroller type-aware * made ParameterNormalizer type-aware * made TestUnroller and Unroller type-aware * running the type checker right after the parser * a reference to the closed issue * Integrating types 6: made Desugarer type aware (#658) * add a watchdog listener * close #647: Desugarer preprocesses the general case of EXCEPT * unrelease notes * type-aware test for Desugarer * made Desugarer type-aware! * fixed a type bug that was found by the type watchdog * propagating types in AssignmentOperatorIntroduction * made SkolemizationMarker type-aware * made ExpansionMarker type-aware * fixed TestSymbTransGenerator * moved the integration tests to test/tla * removed the Paxos tests, which is already in the integration tests * enabled snowcat by default, as the preprocessing is type-aware * Integrating types 7: victory over enthropy (#663) * a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon * fixed the accidental bug introduced in refactoring
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 fixes a few bugs that I ran into while preparing a tutorial.
make fmt-fix(or had formatting run automatically on all files edited)Documentation added for any new functionalityEntry added to UNRELEASED.md for any new functionality