From 024e759538a9b9eb08f137ace7989ffa9039223c Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Fri, 16 Aug 2024 10:43:55 +0200
Subject: [PATCH] Rewrite for set membership of the powerset of a record where
 the record has infinite co-domains.

Simplified real-world scenario:
```tla
EXTENDS Integers

VARIABLE
  \* @type: Set({ p: (Int) });
  v

TypeOK ==
  v \in SUBSET [ p: Int ]

Init ==
  v = { [p |-> 42] }

Next ==
  UNCHANGED v
```

Apalache Error:
```sh
$ apalache-mc check --inv=TypeOK APARecSub.tla
[...]
Input error (see the manual): Found a set map over an infinite set of CellTFrom(Int). Not supported.
```

Rewrite:
```tla
S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T
```

Related commits, issues, PRs:
* 625a1645e75a910d43759c36ad8a06291ebc55b3
* 785e26925a45b077e14cf79f31f834e0c0919639

* https://github.com/apalache-mc/apalache/issues/723
* https://github.com/apalache-mc/apalache/issues/1627
* https://github.com/apalache-mc/apalache/issues/2762

* https://github.com/apalache-mc/apalache/pull/1453
* https://github.com/apalache-mc/apalache/pull/1629

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 .../scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala  | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
index 5f13923734..a577b66f48 100644
--- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
+++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
@@ -106,6 +106,10 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach {
     assert(expected == output)
   }
 
+  // An optimization for set membership of the powerset of a record where the record has infinite co-domains.
+  test("""S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T""") {
+  }
+
   // optimizations for set cardinalities
 
   test("""Cardinality(S) = 0 becomes S = {}""") {