-
Notifications
You must be signed in to change notification settings - Fork 126
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
Newtypes #1015
Newtypes #1015
Conversation
298e2cc
to
0264ada
Compare
@pnwamk, @david-christiansen, There are some nontrivial questions about how to represent values of newtypes in the cryptol remote API, and I'd love you have your opinions about what we should do here. |
@yav, @brianhuffman, aside from the questions about the remote API, I think this PR is ready to go. |
Can we have a video chat about it in the first week of January? Just so there's time to go back and forth a bit about what the feature is used for and its history so we can pick the right trade-offs. |
Sure, I'll set something up. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I only looked at the diff on github
, so not in a lot of detail, but it looks reasonable to me.
In the longer run we may want to represent newtypes with a single field a bit more efficiently, but let's worry about that if it every comes up. I'd say merge it in, this way we'll get to test it by using it.
r = x.real * y.real - x.imag * y.imag | ||
i = x.real * y.imag + x.imag * y.real | ||
|
||
cplxEq : CplxQ -> CplxQ -> CplxQ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note to self : should be cplxEq : CplxQ -> CplxQ -> Bit
src/Cryptol/Eval/Reference.lhs
Outdated
|
||
At runtime, newtypes values are represented in exactly | ||
the same was as records. The constructor function for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
was -> way
the fields of the newtype body, and push newtypes into various parts of the evaluator, random testing, etc.
and use `TValue` instead of `Type` in more places.
in scope. Also, demote the `NewtypeEnv` to a type synonym, as the newtype was just annoying.
of `Type`. This allows us to directly carry the `Newtype` instead of having to look it up in a table at use sites.
functions. Newtype information is now propigated directly into types via the typechecker instead of being looked up separately.
make it responsive to the `show-examples` option.
by the newtype body.
We've had partial support for a while now for a
newtype
construct, but that support was never fully fleshed out. This PR is for completing the job, writing associated documentation, test cases, etc.CF #870