Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added defs that extract values of a map as a set and as a list #1282

Merged
merged 4 commits into from
Dec 7, 2023

Conversation

ivan-gavran
Copy link
Contributor

@ivan-gavran ivan-gavran commented Dec 1, 2023

This PR adds to spells (added to commonSpells):

  • extracting a set of all values from a map (mapValuesSet)
  • extracting a list of all values from map (mapValuesList)
  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

@ivan-gavran ivan-gavran requested a review from konnov December 1, 2023 16:17
Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for expanding out the common spells!

We are lagging a bit in processing these vital PRs, but I'll aim to get them resolved this coming week.

/// - @param __map a map from type a to type b
/// - @returns the list of all values in the map
pure def mapValuesList(__map: a -> b): List[b] = {
__map.keys().fold([], (__list, __k) => __list.append(__map.get(__k)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have two thoughts here:

Similar to the discussion at #1107 (comment), a snag with operators that take sets to lists is that fold's behavior is undefined for non-commutative operations (like append), due to sets being unordered.

Perhaps it would suffice if we have the toList method from #1107 (fixed as described in the liked comment) together with the mapValusSet added here. Then mapValuesList would be available just as the composition m.mapValuesSet().toList(f) (where f is the ordering function needed to ensure well defined behavior), without needing another named operator.

WDYT?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I totally agree with Shon here. It would be much better to isolate the potentially problematic behavior of fold in one place

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! In that case, I'll plan to make the needed change to the previous pr, and help see these through.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I understand the concern, @shonfeder ! However, the problem with using m.mapValuesSet().toList() in place of mapValuesList is that it removes duplicates.

Think about values of the mapping being shares, and we wanted to get the sum of all of them. What would be a preferred way to achieve that? (That was the original use-case, and I perhaps jumped too quickly to a solution.)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I see! I didn't think about that :)

We could implement this taking the comparator then. Alternatively, we could provide a foldMap : (acc, (key, value)) => acc => acc if the intermediate representation as a list is not really essential.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe what would be best here is to have the inverse of setToMap: mapToSet : Map[a, b] -> Set[(a, b)]. Then one could fold over this as needed. We may need some warning about only using this on maps with a finite domain, but I think it would likely be useful. WDYT, @konnov?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe what would be best here is to have the inverse of setToMap: mapToSet : Map[a, b] -> Set[(a, b)]. Then one could fold over this as needed. We may need some warning about only using this on maps with a finite domain, but I think it would likely be useful. WDYT, @konnov?

Yes, this makes sense to me. This would simply convert a map to a relation. I thought that we already had something like that in Apalache, but we only have it in the opposite direction.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've made the discussed change. @ivan-gavran, do you think this would be suitable for the motivating usecase?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Absolutely. Thanks :)

@shonfeder shonfeder self-assigned this Dec 6, 2023
@shonfeder shonfeder requested a review from bugarela December 6, 2023 22:10
Copy link
Collaborator

@bugarela bugarela left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

examples/spells/commonSpells.qnt Outdated Show resolved Hide resolved
@shonfeder
Copy link
Contributor

Thanks for the contribution and for flagging the need for this, @ivan-gavran!

@shonfeder shonfeder merged commit cf1f612 into main Dec 7, 2023
15 checks passed
@shonfeder shonfeder deleted the ivan/mapValuesSpells branch December 7, 2023 17:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants