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

Support for newtypes #1256

Closed
robdockins opened this issue Jan 15, 2021 · 5 comments · Fixed by #1396
Closed

Support for newtypes #1256

robdockins opened this issue Jan 15, 2021 · 5 comments · Fixed by #1396
Assignees
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core

Comments

@robdockins
Copy link
Contributor

Following the merge of GaloisInc/cryptol#1015, we need to add support for newtypes to cryptol-saw-core.

As a first pass, we will simply erase newtypes. They don't satisfy any typeclass constraints, so that part of the translation should be easy.

@robdockins robdockins self-assigned this Jan 15, 2021
@brianhuffman brianhuffman transferred this issue from GaloisInc/saw-core Apr 27, 2021
@brianhuffman brianhuffman added the subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core label Apr 27, 2021
@robdockins
Copy link
Contributor Author

I think this has been done for some time now.

@atomb atomb reopened this Jul 21, 2021
@atomb
Copy link
Contributor

atomb commented Jul 21, 2021

We have an internal example where record selection to project from a newtype fails to translate.

@robdockins
Copy link
Contributor Author

Are you able to minimize the example?

@atomb
Copy link
Contributor

atomb commented Jul 21, 2021

Just finished doing that. Here you go.

Say you have the following in newtype_bug.cry:

newtype T n = { vec : [n] }

fromT : {n} T n -> [n]
fromT x = x.vec

Then running import "newtype_bug.cry" at the SAWScript REPL leads to a panic about an invalid record selector.

@robdockins
Copy link
Contributor Author

Ah, I see. The record selector code is type-driven and doesn't know what to do for newtypes. That shouldn't be too hard to fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants