Merge branch 'unstable' into ik/sequences1486-2

UNRELEASED.md

@@ -19,6 +19,7 @@
  * Look up modules in the same directory, see #1491
  * Support for the community module `SequencesExt`, see  #1539
  * Support for the community module `BagsExt`, see #1555
+ * Support for the community module `Folds`, see #1558
 
 ### Improvements
 

build.sbt

@@ -269,6 +269,8 @@ lazy val root = (project in file("."))
                   "tla2sany/StandardModules/__rewire_finite_sets_ext_in_apalache.tla",
                 (src_dir / "__rewire_sequences_ext_in_apalache.tla") ->
                   "tla2sany/StandardModules/__rewire_sequences_ext_in_apalache.tla",
+                (src_dir / "__rewire_folds_in_apalache.tla") ->
+                  "tla2sany/StandardModules/__rewire_folds_in_apalache.tla",
             ),
         )
       },

src/tla/__rewire_folds_in_apalache.tla

@@ -0,0 +1,39 @@
+--------------------------- MODULE Folds -----------------------------------
+\*------ MODULE __rewire_folds_in_apalache -----------------------
+(**
+ * ^^^^^^^^^^^^^^^^^^^^^^ We have to call this module Folds in any
+ * case, otherwise, SANY complains.
+ *
+ * This file contains alternative definitions for the operators defined in
+ * Folds. Most importantly, we are adding type annotations. We also
+ * define the Apalache-compatible behavior.
+ *
+ * These definitions are automatically rewired by the Apalache importer.
+ *
+ * Compare with the original definitions in Folds.tla:
+ *
+ * https://github.com/tlaplus/CommunityModules/blob/master/modules/Folds.tla
+ *)
+
+EXTENDS __apalache_internal
+
+
+(**
+ * Starting from base, apply op to f(x), for all x \in S, by choosing the set
+ * elements with `choose`. If there are multiple ways for choosing an element,
+ * op should be associative and commutative. Otherwise, the result may depend
+ * on the concrete implementation of `choose`.
+ *
+ * FoldSet, a simpler version for sets is contained in FiniteSetsEx.
+ * FoldFunction, a simpler version for functions is contained in Functions.
+ * FoldSeq, a simpler version for sequences is contained in SequencesExt.
+ *
+ * Apalache (the model checker) does not support MapThenFoldSet.
+ * However, we introduce this definition for the type checker.
+ *
+ * @type: ((a, b) => b, b, c => a, Set(c) => c, Set(c)) => b;
+ *)
+MapThenFoldSet(op(_, _), base, f(_), choose(_), S) ==
+  __NotSupportedByModelChecker("MapThenFoldSet. Use FoldSet, FoldSeq, FoldFunction.")
+
+=============================================================================

test/tla/TestFolds.tla

@@ -0,0 +1,26 @@
+------------------------ MODULE TestFolds -------------------------------------
+(**
+ * A test for the community module Folds.
+ * Since our implementation calls __NotSupportedByModelChecker,
+ * it is only useful to test it with a type checker.
+ *)
+
+EXTENDS Folds
+
+Init == TRUE
+
+Next == TRUE
+
+Test1 ==
+    LET \* @type: Seq(Set(Str));
+        seq == <<{"a"}, {"b"}, {"c"}>>
+    IN
+    LET F(i) == seq[i] IN
+    LET unite(S, T) == S \union T IN
+    LET choose(S) == CHOOSE x \in S: TRUE IN
+    MapThenFoldSet(unite, {}, F, choose, { 2, 3 }) = { "b", "c" }
+
+AllTests ==
+    Test1
+
+===============================================================================

test/tla/cli-integration-tests.md

@@ -1896,6 +1896,16 @@ $ apalache-mc check --length=0 --inv=AllTests TestBagsExt.tla | sed 's/[IEW]@.*/
 EXITCODE: OK
 ```
 
+### check TestFolds.tla reports no error
+
+```sh
+$ apalache-mc check --length=0 --inv=AllTests TestFolds.tla | sed 's/[IEW]@.*//'
+...
+TestFolds.tla:21:5-21:50: unsupported expression: Not supported: MapThenFoldSet. Use FoldSet, FoldSeq, FoldFunction.
+...
+EXITCODE: ERROR (12)
+```
+
 ### check Test1343.tla reports no error
 
 Regression test for #1343
@@ -2485,6 +2495,16 @@ $ apalache-mc typecheck MC_LamportMutexTyped.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### typecheck TestFolds.tla
+
+Typecheck the test for Folds.tla.
+
+```sh
+$ apalache-mc typecheck TestFolds.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ## configuring the output manager
 
 ### output manager: set out-dir by CLI flag

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

@@ -87,6 +87,7 @@ object StandardLibrary {
         "Functions.tla" -> "__rewire_functions_in_apalache.tla",
         "FiniteSetsExt.tla" -> "__rewire_finite_sets_ext_in_apalache.tla",
         "SequencesExt.tla" -> "__rewire_sequences_ext_in_apalache.tla",
+        "Folds.tla" -> "__rewire_folds_in_apalache.tla",
     ) ////
 
   /**