Refactor of Reduce / Fold operators #38
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemmy
reviewed
Mar 30, 2021
lemmy
reviewed
Mar 30, 2021
modules/FiniteSetsExt.tla
Outdated
| (* where `x` s the current value of the iterator. *) | ||
| (* *) | ||
| (* Example: *) | ||
| (* FoldSet(LAMBA x,y : x + y, 0 .. 10, 0) = 55 *) |
There was a problem hiding this comment.
Mismatch: Example mentions FoldSet but operator name is MapThenFoldSet.
There was a problem hiding this comment.
Isn't this in the definition of FoldSet by MapThenFoldSet ?
lemmy
reviewed
Mar 30, 2021
lemmy
reviewed
Mar 30, 2021
quicquid
force-pushed
the
wip-recursion-operators
branch
from
08a128e to
fc824da
Compare
lemmy
reviewed
Mar 30, 2021
quicquid
force-pushed
the
wip-recursion-operators
branch
2 times, most recently
from
f6f0342 to
1dc1c47
Compare
konnov
reviewed
Mar 31, 2021
modules/FiniteSetsExt.tla
Outdated
| (* Fold op over the elements of set using base as starting value. *) | ||
| (* *) | ||
| (* Example: *) | ||
| (* FoldSet(LAMBA x,y : x + y, 0 .. 10, 0) = 55 *) |
There was a problem hiding this comment.
Suggested change
| (* FoldSet(LAMBA x,y : x + y, 0 .. 10, 0) = 55 *) | |
| (* FoldSet(LAMBA x,y : x + y, 0, 0 .. 10) = 55 *) |
| (* An alias for FoldSet. ReduceSet was used instead of FoldSet in *) | ||
| (* earlier versions of the community modules. *) | ||
| (*************************************************************************) | ||
| FoldSet(op, set, acc) |
There was a problem hiding this comment.
Suggested change
| FoldSet(op, set, acc) | |
| FoldSet(op, acc, set) |
| (* Example: *) | ||
| (* Product(1 .. 3) = 6 *) | ||
| (*************************************************************************) | ||
| FoldSet(LAMBDA x, y: x * y, set, 1) |
There was a problem hiding this comment.
Suggested change
| FoldSet(LAMBDA x, y: x * y, set, 1) | |
| FoldSet(LAMBDA x, y: x * y, 1, set) |
| (* Example: *) | ||
| (* Sum(0 .. 10) = 55 *) | ||
| (*************************************************************************) | ||
| FoldSet(LAMBDA x, y: x + y, set, 0) |
There was a problem hiding this comment.
Suggested change
| FoldSet(LAMBDA x, y: x + y, set, 0) | |
| FoldSet(LAMBDA x, y: x + y, 0, set) |
Comment on lines
+42
to
+51
| FlattenSet(S) == | ||
| (******************************************************************************) | ||
| (* Starting from base, apply op to f(x), for all x \in S, in an arbitrary *) | ||
| (* order. It is assumed that op is associative and commutative. *) | ||
| (* *) | ||
| (* Example: *) | ||
| (* *) | ||
| (* FlattenSet({{1},{2}}) = {1,2} *) | ||
| (******************************************************************************) | ||
| FoldSet(LAMBDA x,y: x \cup y, {}, S) |
| (***************************************************************************) | ||
| ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc) | ||
| MapThenFoldSet(op, base, LAMBDA i : seq[i], LAMBDA x,y: TRUE, DOMAIN seq) | ||
| FoldLeft(op(_, _), base, seq) == |
There was a problem hiding this comment.
Suggested change
| FoldLeft(op(_, _), base, seq) == | |
| FoldSeqLeft(op(_, _), base, seq) == |
modules/SequencesExt.tla
Outdated
| (* FoldSeq folds op on all elements of seq from left to right. *) | ||
| (***************************************************************************) | ||
| MapThenFoldSet(op, base, LAMBDA i : seq[i], LAMBDA x,y: x < y, DOMAIN seq) | ||
| FoldRight(op(_, _), base, seq) == |
There was a problem hiding this comment.
Suggested change
| FoldRight(op(_, _), base, seq) == | |
| FoldSeqRight(op(_, _), base, seq) == |
…to appropriate modules (Functions, FiniteSequencesEx)
quicquid
force-pushed
the
wip-recursion-operators
branch
from
75790aa to
6a3dd90
Compare
muenchnerkindl
approved these changes
Apr 28, 2021
|
@quicquid Can you please add a note to https://github.com/tlaplus/CommunityModules/blob/master/README.md#contributing about the line-number business in tests? |
|
Merged with (squashed) commit 0b5fcd4 |
|
CommunityModules/modules/SequencesExt.tla Line 180 in fa811ce { f[x] : x \in DOMAIN f } that is even part of Functions!Range(s).
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.