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.

Sign up for GitHub

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

Jump to bottom

Merge Cryptol::Extras into Prelude #427

Closed
TomMD opened this issue Jun 22, 2017 · 5 comments
Closed

Merge Cryptol::Extras into Prelude #427

TomMD opened this issue Jun 22, 2017 · 5 comments
Labels
low-hanging fruit For issues that should be easy to fix
Milestone
Cryptol 2.6

Comments

@TomMD
Copy link
Contributor

TomMD commented Jun 22, 2017

Now that issue #302 is closed, what are the thoughts on merging Cryptol::Extras into Prelude?

Advantages:

  • Easy access to folds, scan, zip, not, and, or, map, any, sum, extend, repeat, iterate...
  • Encourages use of higher level operations.

Disadvantages:

  • Users might feel the language has changed.
  • Code might diverge into the "traditional cryptol" and "functional cryptol" styles.
  • Little evidence of how well the resulting SMT (or crucible core) is handled.
@robdockins
Copy link
Contributor

Personally, I'm in favor of merging Extras into Prelude. Sometimes you really just want a fold, instead of having to remember the slightly strange way to encode it as a sequence comprehension.

@atomb
Copy link
Contributor

atomb commented Jul 26, 2017

Now that it's pretty fast to load, I think it's probably worth doing.

@atomb atomb added this to the Cryptol 2.6 milestone Feb 5, 2018
@atomb atomb added the low-hanging fruit For issues that should be easy to fix label Feb 8, 2018
@atomb atomb closed this as completed in 99f3fdb May 24, 2018
@brianhuffman
Copy link
Contributor

We now have some redundant functions in the prelude:

  • not is identical to primitive complement
  • extend and extendSigned are duplicates of zext and sext (added in 2b9e5a2)

Which names should we get rid of, and which should we keep?

@TomMD
Copy link
Contributor Author

TomMD commented May 24, 2018

I think we should get rid of the new names, deleting not, extend, and extendSigned. Keeping complement, zext, and sext. Why? Well, why would we want to create churn and breakage? I'm not convinced the new function names are sufficiently better to justify the breakage.

@atomb
Copy link
Contributor

atomb commented May 24, 2018

Seems reasonable to me.

brianhuffman pushed a commit that referenced this issue May 24, 2018
Remove redundant prelude functions not, extend, and extendSigned.
ab00098 
These were recently moved here from Cryptol::Extras. They are duplicates
of existing functions `complement`, `zext`, and `sext`.

See #427.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
low-hanging fruit For issues that should be easy to fix
Projects
None yet
Milestone
Cryptol 2.6
Development

No branches or pull requests
4 participants
@atomb @TomMD @brianhuffman @robdockins