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

Sort function #1193

Merged
merged 3 commits into from
May 10, 2021
Merged

Sort function #1193

merged 3 commits into from
May 10, 2021

Conversation

brianhuffman
Copy link
Contributor

Add sort and sortBy functions to the Cryptol prelude.

I decided to make the helper function insertBy into a local definition, because I didn't think we really needed it as a prelude function.

@brianhuffman
Copy link
Contributor Author

Oh, I apparently need to update a bunch of expected test output files, since I added two new declarations to the prelude and now all the fresh-type-variable auto-generated names have different numbers on them.

Copy link
Member

@yav yav left a comment

Choose a reason for hiding this comment

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

I am a bit concerned with this code as I think people look at the Cryptol library for examples of how to write Cryptol, and I really wouldn't encourage people to write in this style. I know that you have to do this sort of hackery with the tools we have at the moment, though.

I am fine with committing it, if you think it is useful, but also think that perhaps this should be delegated a primitive, where we can actually implement it efficiently, and if one day we are generating code, we can generate reasonable code for it.

@brianhuffman brianhuffman merged commit 4a4673e into master May 10, 2021
@RyanGlScott RyanGlScott deleted the sort-function branch March 22, 2024 14:48
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.

> Here's an insertion sort that I believe to be stable: Sorting primitives
2 participants