|
| 1 | +------------------------------ MODULE BagsExt ------------------------------ |
| 2 | +(***************************************************************************) |
| 3 | +(* Additional operators on bags (multisets). *) |
| 4 | +(***************************************************************************) |
| 5 | + |
| 6 | +LOCAL INSTANCE Bags |
| 7 | +LOCAL INSTANCE Integers |
| 8 | +LOCAL INSTANCE Folds |
| 9 | + |
| 10 | +BagAdd(B, x) == |
| 11 | + (************************************************************************) |
| 12 | + (* Add an element x to bag B. *) |
| 13 | + (* Same as B (+) SetToBag({x}). *) |
| 14 | + (************************************************************************) |
| 15 | + IF x \in DOMAIN B |
| 16 | + THEN [e \in DOMAIN B |-> IF e=x THEN B[e]+1 ELSE B[e]] |
| 17 | + ELSE [e \in DOMAIN B \union {x} |-> IF e=x THEN 1 ELSE B[e]] |
| 18 | + |
| 19 | +BagRemove(B,x) == |
| 20 | + (************************************************************************) |
| 21 | + (* Remove an element x from bag B. *) |
| 22 | + (* Same as B (-) SetToBag({x}). *) |
| 23 | + (************************************************************************) |
| 24 | + IF x \in DOMAIN B |
| 25 | + THEN IF B[x] = 1 |
| 26 | + THEN [e \in DOMAIN B \ {x} |-> B[e]] |
| 27 | + ELSE [e \in DOMAIN B |-> IF e=x THEN B[e]-1 ELSE B[e]] |
| 28 | + ELSE B |
| 29 | + |
| 30 | +FoldBag(op(_,_), base, B) == |
| 31 | + (************************************************************************) |
| 32 | + (* Fold op over all elements of bag B, starting with value base. *) |
| 33 | + (* *) |
| 34 | + (* Example: *) |
| 35 | + (* FoldBag(LAMBDA x,y : x+y, *) |
| 36 | + (* 0, *) |
| 37 | + (* (1 :> 2) @@ (2 :> 1) @@ (3 :> 2)) = 10 *) |
| 38 | + (* The third argument represents the bag {| 1, 1, 2, 3, 3 |}. *) |
| 39 | + (************************************************************************) |
| 40 | + LET repl(x) == |
| 41 | + (* replicate operation op for all occurrences of x in B *) |
| 42 | + LET it[n \in Nat \ {0}] == |
| 43 | + IF n = 1 THEN x ELSE op(x, it[n-1]) |
| 44 | + IN it[B[x]] |
| 45 | + IN MapThenFoldSet(op, base, repl, |
| 46 | + LAMBDA S : CHOOSE x \in S : TRUE, |
| 47 | + DOMAIN B) |
| 48 | + |
| 49 | +SumBag(B) == |
| 50 | + (************************************************************************) |
| 51 | + (* Compute the sum of the elements of B. *) |
| 52 | + (************************************************************************) |
| 53 | + FoldBag(LAMBDA x,y : x+y, 0, B) |
| 54 | + |
| 55 | +ProductBag(B) == |
| 56 | + (************************************************************************) |
| 57 | + (* Compute the product of the elements of B. *) |
| 58 | + (************************************************************************) |
| 59 | + FoldBag(LAMBDA x,y : x*y, 1, B) |
| 60 | + |
| 61 | +============================================================================= |
0 commit comments