Skip to content

Commit a80a246

Browse files
lemmylemmy
committed
Refactor all operator descriptions/comments into what SANY considers proper pre-comments.
## Old parse tree ``` | | N_OperatorDefinition *ReplaceAllSubSeqs #heirs: 3 kind: 389 | | | N_IdentLHS #heirs: 8 kind: 366 | | | | ReplaceAllSubSeqs #heirs: 0 kind: 292 | | | | ( #heirs: 0 kind: 94 | | | | N_IdentDecl #heirs: 1 kind: 363 | | | | | r #heirs: 0 kind: 292 | | | | , #heirs: 0 kind: 88 | | | | N_IdentDecl #heirs: 1 kind: 363 | | | | | s #heirs: 0 kind: 292 | | | | , #heirs: 0 kind: 88 | | | | N_IdentDecl #heirs: 1 kind: 363 | | | | | t #heirs: 0 kind: 292 | | | | ) #heirs: 0 kind: 95 | | | == #heirs: 0 kind: 93 | | | N_Case #heirs: 10 kind: 336 | | | | CASE #heirs: 0 kind: 42 preComment: 0 (**************************************************************************) 1 (* The sequence t with all subsequences s replaced by the sequence r *) 2 (* Overlapping replacements are disambiguated by choosing the occurrence *) 3 (* closer to the beginning of the sequence. *) 4 (* *) 5 (* Examples: *) 6 (* *) 7 (* ReplaceAllSubSeqs(<<>>,<<>>,<<>>) = <<>> *) 8 (* ReplaceAllSubSeqs(<<4>>,<<>>,<<>>) = <<4>> *) 9 (* ReplaceAllSubSeqs(<<2>>,<<3>>,<<1,3>>) = <<1,2>> *) 10 (* ReplaceAllSubSeqs(<<2,2>>,<<1,1>>,<<1,1,1>>) = <<2,2,1>> *) 11 (**************************************************************************) ``` ## New parse tree ``` | | N_OperatorDefinition *ReplaceAllSubSeqs #heirs: 3 kind: 389 | | | N_IdentLHS #heirs: 8 kind: 366 | | | | ReplaceAllSubSeqs #heirs: 0 kind: 292 preComment: 0 (**************************************************************************) 1 (* The sequence t with all subsequences s replaced by the sequence r *) 2 (* Overlapping replacements are disambiguated by choosing the occurrence *) 3 (* closer to the beginning of the sequence. *) 4 (* *) 5 (* Examples: *) 6 (* *) 7 (* ReplaceAllSubSeqs(<<>>,<<>>,<<>>) = <<>> *) 8 (* ReplaceAllSubSeqs(<<4>>,<<>>,<<>>) = <<4>> *) 9 (* ReplaceAllSubSeqs(<<2>>,<<3>>,<<1,3>>) = <<1,2>> *) 10 (* ReplaceAllSubSeqs(<<2,2>>,<<1,1>>,<<1,1,1>>) = <<2,2,1>> *) 11 (**************************************************************************) ``` [Refactor] Signed-off-by: Markus Alexander Kuppe <[email protected]>
1 parent c4ea8d5 commit a80a246

9 files changed

+562
-562
lines changed

‎modules/BagsExt.tla

Lines changed: 53 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -7,60 +7,60 @@ LOCAL INSTANCE Bags
77
LOCAL INSTANCE Integers
88
LOCAL INSTANCE Folds
99

10+
(************************************************************************)
11+
(* Add an element x to bag B. *)
12+
(* Same as B (+) SetToBag({x}). *)
13+
(************************************************************************)
1014
BagAdd(B, x) ==
11-
(************************************************************************)
12-
(* Add an element x to bag B. *)
13-
(* Same as B (+) SetToBag({x}). *)
14-
(************************************************************************)
1515
IF x \in DOMAIN B
1616
THEN [e \in DOMAIN B |-> IF e=x THEN B[e]+1 ELSE B[e]]
1717
ELSE [e \in DOMAIN B \union {x} |-> IF e=x THEN 1 ELSE B[e]]
1818

19+
(************************************************************************)
20+
(* Remove an element x from bag B. *)
21+
(* Same as B (-) SetToBag({x}). *)
22+
(************************************************************************)
1923
BagRemove(B,x) ==
20-
(************************************************************************)
21-
(* Remove an element x from bag B. *)
22-
(* Same as B (-) SetToBag({x}). *)
23-
(************************************************************************)
2424
IF x \in DOMAIN B
2525
THEN IF B[x] = 1
2626
THEN [e \in DOMAIN B \ {x} |-> B[e]]
2727
ELSE [e \in DOMAIN B |-> IF e=x THEN B[e]-1 ELSE B[e]]
2828
ELSE B
2929

30+
(************************************************************************)
31+
(* Remove all copies of an element x from bag B. *)
32+
(************************************************************************)
3033
BagRemoveAll(B,x) ==
31-
(************************************************************************)
32-
(* Remove all copies of an element x from bag B. *)
33-
(************************************************************************)
3434
[e \in DOMAIN B \ {x} |-> B[e]]
3535

36+
(***********************************************************************)
37+
(* Fold operation op over the images through f of all elements of bag *)
38+
(* B, starting from base. The parameter choose indicates the order in *)
39+
(* which elements of the bag are processed; all replicas of an element *)
40+
(* are processed consecutively. *)
41+
(* *)
42+
(* Examples: *)
43+
(* MapThenFoldBag(LAMBDA x,y : x+y, *)
44+
(* 0, *)
45+
(* LAMBDA x: 1, *)
46+
(* LAMBDA B : CHOOSE x \in DOMAIN B : TRUE, *)
47+
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 6 *)
48+
(* *)
49+
(* MapThenFoldBag(LAMBDA x,y : x \o y, *)
50+
(* << >>, *)
51+
(* LAMBDA x: << x >>, *)
52+
(* LAMBDA S: CHOOSE x \in S : \A y \in S : x <= y, *)
53+
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) *)
54+
(* = <<1,1,2,3,3,3>> *)
55+
(* *)
56+
(* The fifth argument represents the bag {| 1, 1, 2, 3, 3, 3 |}. *)
57+
(* The first example counts the elements of the bag. *)
58+
(* The second example computes a sorted sequence of all elements *)
59+
(* of the bag. It is brittle because concatenation of sequences is *)
60+
(* non-commutative, and the result therefore relies on the *)
61+
(* definition of MapThenFoldSet. *)
62+
(***********************************************************************)
3663
MapThenFoldBag(op(_,_), base, f(_), choose(_), B) ==
37-
(***********************************************************************)
38-
(* Fold operation op over the images through f of all elements of bag *)
39-
(* B, starting from base. The parameter choose indicates the order in *)
40-
(* which elements of the bag are processed; all replicas of an element *)
41-
(* are processed consecutively. *)
42-
(* *)
43-
(* Examples: *)
44-
(* MapThenFoldBag(LAMBDA x,y : x+y, *)
45-
(* 0, *)
46-
(* LAMBDA x: 1, *)
47-
(* LAMBDA B : CHOOSE x \in DOMAIN B : TRUE, *)
48-
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 6 *)
49-
(* *)
50-
(* MapThenFoldBag(LAMBDA x,y : x \o y, *)
51-
(* << >>, *)
52-
(* LAMBDA x: << x >>, *)
53-
(* LAMBDA S: CHOOSE x \in S : \A y \in S : x <= y, *)
54-
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) *)
55-
(* = <<1,1,2,3,3,3>> *)
56-
(* *)
57-
(* The fifth argument represents the bag {| 1, 1, 2, 3, 3, 3 |}. *)
58-
(* The first example counts the elements of the bag. *)
59-
(* The second example computes a sorted sequence of all elements *)
60-
(* of the bag. It is brittle because concatenation of sequences is *)
61-
(* non-commutative, and the result therefore relies on the *)
62-
(* definition of MapThenFoldSet. *)
63-
(***********************************************************************)
6464
LET handle(x) == \* handle all occurrences of x in B
6565
LET pow[n \in Nat \ {0}] ==
6666
op(IF n=1 THEN base ELSE pow[n-1], f(x))
@@ -69,28 +69,28 @@ BagRemoveAll(B,x) ==
6969
LAMBDA S : CHOOSE x \in S : TRUE,
7070
DOMAIN B)
7171

72+
(************************************************************************)
73+
(* Fold op over all elements of bag B, starting with value base. *)
74+
(* *)
75+
(* Example: *)
76+
(* FoldBag(LAMBDA x,y : x+y, *)
77+
(* 0, *)
78+
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 13 *)
79+
(* The third argument represents the bag {| 1, 1, 2, 3, 3, 3 |}. *)
80+
(************************************************************************)
7281
FoldBag(op(_,_), base, B) ==
73-
(************************************************************************)
74-
(* Fold op over all elements of bag B, starting with value base. *)
75-
(* *)
76-
(* Example: *)
77-
(* FoldBag(LAMBDA x,y : x+y, *)
78-
(* 0, *)
79-
(* (1 :> 2) @@ (2 :> 1) @@ (3 :> 3)) = 13 *)
80-
(* The third argument represents the bag {| 1, 1, 2, 3, 3, 3 |}. *)
81-
(************************************************************************)
8282
MapThenFoldBag(op, base, LAMBDA x: x, LAMBDA S : CHOOSE x \in S : TRUE, B)
8383

84+
(************************************************************************)
85+
(* Compute the sum of the elements of B. *)
86+
(************************************************************************)
8487
SumBag(B) ==
85-
(************************************************************************)
86-
(* Compute the sum of the elements of B. *)
87-
(************************************************************************)
8888
FoldBag(LAMBDA x,y : x+y, 0, B)
8989

90+
(************************************************************************)
91+
(* Compute the product of the elements of B. *)
92+
(************************************************************************)
9093
ProductBag(B) ==
91-
(************************************************************************)
92-
(* Compute the product of the elements of B. *)
93-
(************************************************************************)
9494
FoldBag(LAMBDA x,y : x*y, 1, B)
9595

9696
=============================================================================

‎modules/Bitwise.tla

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ LOCAL And(x,y,n,m) ==
1010
ELSE exp * ((x \div exp) % 2) * ((y \div exp) % 2)
1111
+ And(x,y,n+1,m \div 2)
1212

13+
(***************************************************************************)
14+
(* Bitwise AND of (non-negative) x and y (defined for Nat \cup {0}). *)
15+
(***************************************************************************)
1316
x & y ==
14-
(***************************************************************************)
15-
(* Bitwise AND of (non-negative) x and y (defined for Nat \cup {0}). *)
16-
(***************************************************************************)
1717
IF x >= y THEN And(x, y, 0, x) ELSE And(y, x, 0, y) \* Infix variant of And(x,y)
1818

1919
-------------------------------------------------------------------------------
@@ -28,10 +28,10 @@ LOCAL Or(x,y,n,m) ==
2828
ELSE exp * (((xdm + ydm) + (xdm * ydm)) % 2)
2929
+ Or(x,y,n+1,m \div 2)
3030

31+
(***************************************************************************)
32+
(* Bitwise OR of (non-negative) x and y (defined for Nat \cup {0}). *)
33+
(***************************************************************************)
3134
x | y ==
32-
(***************************************************************************)
33-
(* Bitwise OR of (non-negative) x and y (defined for Nat \cup {0}). *)
34-
(***************************************************************************)
3535
IF x >= y THEN Or(x, y, 0, x) ELSE Or(y, x, 0, y) \* Infix variant of Or(x,y)
3636

3737
-------------------------------------------------------------------------------
@@ -44,10 +44,10 @@ LOCAL Xor(x,y,n,m) ==
4444
ELSE exp * (((x \div exp) + (y \div exp)) % 2)
4545
+ Xor(x,y,n+1,m \div 2)
4646

47+
(***************************************************************************)
48+
(* Bitwise XOR of (non-negative) x and y (defined for Nat \cup {0}). *)
49+
(***************************************************************************)
4750
x ^^ y == \* single "^" already taken by Naturals.tla
48-
(***************************************************************************)
49-
(* Bitwise XOR of (non-negative) x and y (defined for Nat \cup {0}). *)
50-
(***************************************************************************)
5151
IF x >= y THEN Xor(x, y, 0, x) ELSE Xor(y, x, 0, y) \* Infix variant of Xor(x,y)
5252

5353
-------------------------------------------------------------------------------
@@ -61,20 +61,20 @@ LOCAL NotR(x,n,m) ==
6161
ELSE exp * ((xdm + 1) % 2)
6262
+ NotR(x,n+1,m \div 2)
6363

64+
(***************************************************************************)
65+
(* Bitwise NOT of (non-negative) x (defined for Nat \cup {0}). *)
66+
(***************************************************************************)
6467
Not(a) ==
65-
(***************************************************************************)
66-
(* Bitwise NOT of (non-negative) x (defined for Nat \cup {0}). *)
67-
(***************************************************************************)
6868
NotR(a,0,a)
6969

7070
-------------------------------------------------------------------------------
7171

72+
(***************************************************************************)
73+
(* Logical bit-shifting the (non-negative) n by pos positions to the right *)
74+
(* shifting zeros in from the left/MSB (defined for Nat \cup {0}). *)
75+
(***************************************************************************)
7276
RECURSIVE shiftR(_,_)
7377
shiftR(n,pos) ==
74-
(***************************************************************************)
75-
(* Logical bit-shifting the (non-negative) n by pos positions to the right *)
76-
(* shifting zeros in from the left/MSB (defined for Nat \cup {0}). *)
77-
(***************************************************************************)
7878
IF pos = 0
7979
THEN n
8080
ELSE LET odd(z) == z % 2 = 1

0 commit comments

Comments
 (0)