Use type information to simplify membership tests

[thpani]

Addresses #723

Uses type information to simplify membership tests such as x \in BOOLEAN, x \in Int, x \in STRING, x \in Seq(...) when we know that x has the appropriate type.

[codecov-commenter]

Codecov Report

Merging #1406 (ec3c4de) into unstable (f679966) will increase coverage by 0.01%.
The diff coverage is 91.30%.

❗ Current head ec3c4de differs from pull request most recent head 02d4634. Consider uploading reports for the commit 02d4634 to get more accurate results

@@             Coverage Diff              @@
##           unstable    #1406      +/-   ##
============================================
+ Coverage     76.07%   76.08%   +0.01%     
============================================
  Files           338      339       +1     
  Lines         10962    10985      +23     
  Branches        546      542       -4     
============================================
+ Hits           8339     8358      +19     
- Misses         2623     2627       +4     

Impacted Files	Coverage Δ
...t/forsyte/apalache/tla/pp/passes/OptPassImpl.scala	0.00% <0.00%> (ø)
...syte/apalache/tla/pp/SetMembershipSimplifier.scala	95.00% <95.00%> (ø)
...in/scala/at/forsyte/apalache/tla/lir/Builder.scala	99.07% <100.00%> (+<0.01%)	⬆️
...ala/at/forsyte/apalache/tla/lir/TypedPredefs.scala	77.27% <100.00%> (+0.52%)	⬆️
...he/io/annotations/parser/CommentPreprocessor.scala	92.77% <0.00%> (-2.41%)	⬇️

---

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 f679966...02d4634. Read the comment docs.

[Kukovec]

I'll sign off, since this was the only blocking issue I had, but I'd like to hear @konnov and @shonfeder 's thoughts on #1406 (comment).

[shonfeder]

LGTM!

[thpani]

Well here we go... there was a bug in the abstraction (membership test with Nat), and we missed it in code review. It was obvious in the original exhaustive enumeration. PTAL.

@Kukovec @shonfeder Do you think this is easier to read and maintain than my original solution?

[Kukovec]

I don't know how we missed Nat, but rather than omitting it, why not just translate it to x >= 0?

[thpani]

I don't know how we missed Nat, but rather than omitting it, why not just translate it to x >= 0?

At least the OOPSLA encoding already does this, is there any benefit to doing it early?

[konnov]

I don't know how we missed Nat, but rather than omitting it, why not just translate it to x >= 0?

At least the OOPSLA encoding already does this, is there any benefit to doing it early?

I don't remember the details, but we probably do it only for state variables. You can write something like this in TLA+

\E i \in Int:
  i \in Nat => ...

[Kukovec]

LGTM, though I think you could get away with not doing any checks on the type tags. It's not wrong to check, in any case, but if you ever wanted to write

VARIABLE
  \* @type: Int;
  x
...
TypeOK == x \in BOOLEAN

Snowcat would reject that outright, since \in has type constraints.

[konnov]

Great! This PR transforms basic types. How about seq \in Seq(Int) and fun \in [Int -> Int]. Perhaps, something could be done about records and tuples too. Having the type information, we can do a lot of interesting simplifications.

[thpani]

LGTM, though I think you could get away with not doing any checks on the type tags.

Right, I was wondering about it, but was unsure if me might use this in a different context where Snowcat isn't run first.

[thpani]

Great! This PR transforms basic types. How about seq \in Seq(Int) and fun \in [Int -> Int]. Perhaps, something could be done about records and tuples too.

@konnov This already does seq \in Seq(_) as well! I've recorded the other ideas in #723, we can keep expanding the list there.

[konnov]

Added one more comment.