[BUG] Desugaring the general case of EXCEPT #647
Comments
konnov
added a commit
that referenced
this issue
Mar 18, 2021
4 tasks
konnov
added a commit
that referenced
this issue
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 issue
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 issue
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
This was referenced Mar 29, 2021
Closed
Merged
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Desugarer is incorrectly pre-processing the general case of
[f EXCEPT !a_1 = e_1, ..., !a_n = e_n]. We should use the general semantics from the book and give up on parallel assignment semantics, as it is impossible to achieve when the accessorsa_1, ...,a_ncontain multiple indices.The text was updated successfully, but these errors were encountered: