Java override for FoldBag

Author: muenchnerkindl

modules/BagsExt.tla

@@ -27,24 +27,59 @@ BagRemove(B,x) ==
         ELSE [e \in DOMAIN B |-> IF e=x THEN B[e]-1 ELSE B[e]]
    ELSE B
 
+BagRemoveAll(B,x) ==
+   (************************************************************************)
+   (* Remove all copies of an element x from bag B.                        *)
+   (************************************************************************)
+   [e \in DOMAIN B \ {x} |-> B[e]]
+ 
+ MapThenFoldBag(op(_,_), base, f(_), choose(_), B) ==
+    (***********************************************************************)
+    (* Fold operation op over the images through f of all elements of bag  *)
+    (* B, starting from base. The parameter choose indicates the order in  *)
+    (* which elements of the bag are processed; all replicas of an element *)
+    (* are processed consecutively.                                        *)
+    (*                                                                     *)
+    (* Examples:                                                           *)
+    (*    MapThenFoldBag(LAMBDA x,y : x+y,                                 *)
+    (*                   0,                                                *)
+    (*                   LAMBDA x: 1,                                      *)
+    (*                   LAMBDA B : CHOOSE x \in DOMAIN B : TRUE,          *)
+    (*                   (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 6             *)
+    (*                                                                     *)
+    (*    MapThenFoldBag(LAMBDA x,y : x \o y,                              *)
+    (*                   << >>,                                            *)
+    (*                   LAMBDA x: << x >>,                                *)
+    (*                   LAMBDA S: CHOOSE x \in S : \A y \in S : x <= y,   *)
+    (*                   (1 :> 2) @@ (2 :> 1) @@ (3 :> 3))                 *)
+    (*                 = <<1,1,2,3,3,3>>                                   *)
+    (*                                                                     *)
+    (*    The fifth argument represents the bag {| 1, 1, 2, 3, 3, 3 |}.    *)
+    (*    The first example counts the elements of the bag.                *)
+    (*    The second example computes a sorted sequence of all elements    *)
+    (*    of the bag. It is brittle because concatenation of sequences is  *)
+    (*    non-commutative, and the result therefore relies on the          *)
+    (*    definition of MapThenFoldSet.                                    *)
+    (***********************************************************************)
+    LET handle(x) ==  \* handle all occurrences of x in B
+        LET pow[n \in Nat \ {0}] ==
+            op(IF n=1 THEN base ELSE pow[n-1], f(x))
+        IN  pow[B[x]]
+    IN  MapThenFoldSet(op, base, handle,
+                       LAMBDA S : CHOOSE x \in S : TRUE,
+                       DOMAIN B)
+
 FoldBag(op(_,_), base, B) ==
    (************************************************************************)
    (* Fold op over all elements of bag B, starting with value base.        *)
    (*                                                                      *)
    (* Example:                                                             *)
    (*    FoldBag(LAMBDA x,y : x+y,                                         *)
    (*            0,                                                        *)
-   (*            (1 :> 2) @@ (2 :> 1) @@ (3 :> 2)) = 10                    *)
-   (*    The third argument represents the bag {| 1, 1, 2, 3, 3 |}.        *)
-   (************************************************************************)
-   LET repl(x) ==
-         (* replicate operation op for all occurrences of x in B *)
-       LET it[n \in Nat \ {0}] ==
-           IF n = 1 THEN x ELSE op(x, it[n-1])
-       IN  it[B[x]]
-   IN  MapThenFoldSet(op, base, repl, 
-                      LAMBDA S : CHOOSE x \in S : TRUE,
-                      DOMAIN B)
+   (*            (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 13                    *)
+   (*    The third argument represents the bag {| 1, 1, 2, 3, 3, 3 |}.     *)
+   (************************************************************************)
+   MapThenFoldBag(op, base, LAMBDA x: x, LAMBDA S : CHOOSE x \in S : TRUE, B)
 
 SumBag(B) ==
    (************************************************************************)

modules/tlc2/overrides/BagsExt.java

@@ -0,0 +1,84 @@
+/*******************************************************************************
+ * Copyright (c) 2022 Inria. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Stephan Merz - initial implementation
+ ******************************************************************************/
+package tlc2.overrides;
+
+import java.util.Arrays;
+
+import tlc2.module.Bags;
+import tlc2.output.EC;
+import tlc2.tool.EvalControl;
+import tlc2.tool.EvalException;
+import tlc2.value.Values;
+// import tlc2.value.impl.Applicable;
+// import tlc2.value.impl.BoolValue;
+// import tlc2.value.impl.Enumerable;
+import tlc2.value.impl.FcnRcdValue;
+import tlc2.value.impl.OpValue;
+// import tlc2.value.impl.SetOfRcdsValue;
+// import tlc2.value.impl.TupleValue;
+import tlc2.value.impl.Value;
+import tlc2.value.impl.IntValue;
+// import tlc2.value.impl.ValueEnumeration;
+
+public final class BagsExt {
+	
+	private BagsExt() {
+		// no-instantiation!
+	}
+	
+	@TLAPlusOperator(identifier = "FoldBag", module = "BagsExt", warn = false)
+	public static Value foldBag(final OpValue op, final Value base, final Value bag) {
+		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
+		// make sure that the first parameter is a binary operator.
+
+            FcnRcdValue bfcn = (FcnRcdValue) bag.toFcnRcd();
+            if (bfcn == null) {
+                throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+                                        new String[] { "third", "FoldBag", "bag",
+                                                       Values.ppr(bag.toString()) });
+            }
+
+            final Value[] domain = bfcn.getDomainAsValues();
+            final Value[] values = bfcn.values;
+            final Value acc[] = new Value[2];
+            acc[0] = base;
+
+            for (int i=0; i < domain.length; i++) {
+                acc[1] = domain[i];
+                if (!(values[i] instanceof IntValue) || (((IntValue)values[i]).val <= 0)) {
+                    throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE,
+                                            new String[] { "third", "FoldBag", "bag",
+                                                           Values.ppr(bag.toString()) });
+                }
+                for (int j=0; j < ((IntValue)values[i]).val; j++) {
+                    acc[0] = op.apply(acc, EvalControl.Clear);
+                }
+            }
+
+            return acc[0];
+        }
+}
+

modules/tlc2/overrides/TLCOverrides.java

@@ -44,14 +44,14 @@ public Class[] get() {
                         // Remove `Json.resolves();` call when this Class is moved to `TLC`.
 			Json.resolves();
 			return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class,
-					FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class };
+                                             FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class };
 		} catch (NoClassDefFoundError e) {
                         // Remove this catch when this Class is moved to `TLC`.
 			System.out.println(
 					"gson dependencies of Json overrides not found, Json module won't work unless "
 					+ "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.");
 		}
 		return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class,
-				FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class };
+                                     FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class };
 	}
 }

tests/BagsExtTests.tla

@@ -16,16 +16,56 @@ ASSUME LET B == SetToBag({1,2}) IN BagRemove(B,2) = B (-) SetToBag({2})
 ASSUME LET B == SetToBag({1,2}) IN 
            /\ BagRemove(B,3) = B (-) SetToBag({3})
            /\ BagRemove(B,3) = B
+ASSUME LET B == (1 :> 2) @@ (2 :> 1) IN BagRemoveAll(B,1) = SetToBag({2})
 
 -----------------------------------------------------------------------------
 
-ASSUME FoldBag(LAMBDA x,y : x+y, 0, (1:>2) @@ (2:>1) @@ (3:>2)) = 10
+ASSUME LET B == (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)
+       IN  MapThenFoldBag(LAMBDA x,y : x \cup y,
+                          {},
+                          LAMBDA x : {x},
+                          LAMBDA S : CHOOSE x \in S : TRUE,
+                          B)
+         = BagToSet(B)
+
+(***************************************************************************)
+(* This operator is a copy of FoldBag in module BagsExt. It serves for     *)
+(* testing the Java override of the FoldBag operator. Note that the        *)
+(* operator MapThenFoldBag does not have a Java override.                  *)
+(***************************************************************************)
+TLAFoldBag(op(_,_), base, B) ==
+   (************************************************************************)
+   (* Fold op over all elements of bag B, starting with value base.        *)
+   (*                                                                      *)
+   (* Example:                                                             *)
+   (*    FoldBag(LAMBDA x,y : x+y,                                         *)
+   (*            0,                                                        *)
+   (*            (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 13                    *)
+   (*    The third argument represents the bag {| 1, 1, 2, 3, 3, 3 |}.     *)
+   (************************************************************************)
+   MapThenFoldBag(op, base, LAMBDA x: x, LAMBDA S : CHOOSE x \in S : TRUE, B)
+
+ASSUME LET B == (1:>2) @@ (2:>1) @@ (3:>3)
+       IN  FoldBag(LAMBDA x,y : x+y, 0, B)
+         = TLAFoldBag(LAMBDA x,y : x+y, 0, B)
+ASSUME LET B == ({1}:>2) @@ ({-2}:>1) @@ ({3}:>3)
+       IN  FoldBag(LAMBDA x,y : x \union y, {}, B)
+         = TLAFoldBag(LAMBDA x,y : x \union y, {}, B)
+
+ASSUME FoldBag(LAMBDA x,y : x+y, 0, (1:>2) @@ (2:>1) @@ (3:>3)) = 13
 ASSUME FoldBag(LAMBDA x,y : x+y, 0, (1:>2) @@ (-2:>1)) = 0
 
 ASSUME SumBag((1:>2) @@ (2:>1) @@ (3:>2)) = 10
 ASSUME SumBag((1:>2) @@ (-2:>1)) = 0
 
 ASSUME ProductBag((1:>2) @@ (-2:>1)) = -2
-ASSUME ProductBag((1:>2) @@ (0:>1) @@ (10000:>1)) = 0
+
+(***************************************************************************)
+(* The two following tests fail without the Java override for FoldBag.     *)
+(***************************************************************************)
+ASSUME LET B == (1 :> 1000) @@ (-2 :> 500)
+       IN FoldBag(LAMBDA x,y : x+y, 0, B) = 0 
+
+ASSUME ProductBag((0 :> 1) @@ (10000 :> 1000)) = 0
 
 =============================================================================