Parse ASSUME declarations names #2808

fan-tom · 2024-01-20T00:14:54Z

Tests added for any new code
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entries added to ./unreleased/ for any new functionality

tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala

tla-io/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithTypes.scala

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala

fan-tom · 2024-01-20T00:39:41Z

tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala

@@ -348,7 +348,7 @@ trait IrGenerators extends TlaType1Gen {
    for {
      ex <- exGen
      tt <- genTypeTag
-    } yield TlaAssumeDecl(ex).withTag(tt)
+    } yield TlaAssumeDecl(None, ex).withTag(tt)


Should we generate named version?

Ah, let's not worry about it for now. We can allow add that in a follow up. The generators are do for an overhaul at some point any how.

.unreleased/features/01.md

codecov-commenter · 2024-01-20T02:25:17Z

Codecov Report

Attention: 3 lines in your changes are missing coverage. Please review.

Comparison is base (99fb4d2) 78.82% compared to head (880d1c3) 78.90%.

Files	Patch %	Lines
...ansformations/standard/ModuleByExTransformer.scala	0.00%	2 Missing ⚠️
...he/tla/lir/transformations/standard/DeepCopy.scala	66.66%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #2808      +/-   ##
==========================================
+ Coverage   78.82%   78.90%   +0.08%     
==========================================
  Files         467      467              
  Lines       15932    15942      +10     
  Branches     2588     2589       +1     
==========================================
+ Hits        12558    12579      +21     
+ Misses       3374     3363      -11

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

fan-tom · 2024-01-21T17:25:54Z

I added additional tests to increase code coverage based on the Codecov report, but these tests look ad-hoc, @shonfeder please advise whether I should preserve them or replace with something else, or just drop and ignore Codecov warnings

shonfeder

Awesome work! It was a pleasure to review. Thanks so much for picking this up :)

I have a few small change requests, and a suggestion or two, but they are all minor nits.

tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala

tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintIR.scala

tla-io/src/main/scala/at/forsyte/apalache/tla/imp/AssumeTranslator.scala

tla-io/src/test/scala/at/forsyte/apalache/io/TestPrettyWriterWithTypes.scala

tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala

tla-typechecker/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExprDecls.scala

tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala

shonfeder · 2024-01-22T19:14:23Z

I added additional tests to increase code coverage based on the Codecov report, but these tests look ad-hoc, @shonfeder please advise whether I should preserve them or replace with something else, or just drop and ignore Codecov warnings

I think the tests look OK :) In the future, if you don't think a test is meaningful, no need to add it just to get the coverage metrics, but since they are already here, let's keep 'em.

bugarela

Thanks for taking care of this!