Flattening a tuple of tuples

[Mitchell Hashimoto]

Hello,

I’m sure I’m missing something obvious relating to tuples being functions of Domain 1..Len(Tuple) here but I’m struggling to flatten a tuple of tuples.

i.e. Given T == << <<A>>, <<B>>, <<C>> >> I’m looking to make that <<A, B, C>>. I am able to assure that every element is a tuple, and that the nesting level is only one level deep.

Background on why: I’m validating that a certain traversal of a tree returns the elements in the correct order. I typically use sets, but I’m forced to use tuples since order matters in this specific specification.

I’m effectively looking for something like UNION for tuples.

Thank you!

Best,

Mitchell

[Hillel Wayne]

Hi,

From the community modules we have FoldLeft. Then we can write flatten as

Flatten(seq) == FoldLeft(LAMBDA x, y: x \o y, <<>>, seq)

H

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9363e689-106a-4055-aaa8-82955a9c1e8a%40Spark.

[Mitchell Hashimoto]

That's it. Perfect thank you.

[Markus Kuppe]

On 6/30/21 8:55 AM, Hillel Wayne wrote:
> From the community modules we have FoldLeft

> <https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla>.

> Then we can write flatten as
>
> Flatten(seq) == FoldLeft(LAMBDA x, y: x \o y, <<>>, seq)

As an old school, more readable recursive function:


EXTENDS Naturals, Sequences

Flatten(seq) ==
LET F[ i \in 0..Len(seq)] == \* 0 to handle seq=<<>>
IF i = 0
THEN <<>>
ELSE F[i-1] \o seq[i]
IN F[Len(seq)]



It's likely faster for TLC to evaluate until at least
Folds!MapThenFoldSet gets a module override.

M.

[Mitchell Hashimoto]

On Jun 30, 2021, 11:23 AM -0700, Markus Kuppe <tlaplus-go...@lemmster.de>, wrote:

On 6/30/21 8:55 AM, Hillel Wayne wrote:

From the community modules we have FoldLeft
<https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla>.
Then we can write flatten as

Flatten(seq) == FoldLeft(LAMBDA x, y: x \o y, <<>>, seq)

As an old school, more readable recursive function:


EXTENDS Naturals, Sequences

Flatten(seq) ==
LET F[ i \in 0..Len(seq)] == \* 0 to handle seq=<<>>
IF i = 0
THEN <<>>
ELSE F[i-1] \o seq[i]
IN F[Len(seq)]

Thank you Markus. This is a great example and I’m still not fully appreciating functions yet to naturally see this solution. This helps me study more and get closer to that.

Thanks,
Mitchell

It's likely faster for TLC to evaluate until at least
Folds!MapThenFoldSet gets a module override.

M.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/afgpTC5w7us/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/53c3adad-d1cf-8bae-8143-bd2840af0b78%40lemmster.de.