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

laziness of conditionals #419

Closed
msaaltink opened this issue May 13, 2017 · 2 comments
Closed

laziness of conditionals #419

msaaltink opened this issue May 13, 2017 · 2 comments
Assignees
Labels
semantics Issues related to the dynamic semantics of Cryptol.

Comments

@msaaltink
Copy link
Contributor

The reference evaluator and REPL evaluator disagree again:

Cryptol> if error "boo" then () else ()

Run-time error: boo
Cryptol> :eval if error "boo" then () else ()
()

Similarly with infinite recursion:

Cryptol> if b then () else () where b = b

<<loop>> while evaluating (at <interactive>:1:28--1:29, <interactive>::b)
Cryptol> :eval if b then () else () where b = b
()
@robdockins
Copy link
Contributor

robdockins commented May 19, 2017

This seems like essentially the same problem as #422. Basically, we should only demand the value of the conditional test if the caller is going to demand at least one bit of the output... and there are no bits of output at the unit type.

@robdockins robdockins self-assigned this May 19, 2017
@atomb atomb added this to the Cryptol 2.6 milestone Feb 5, 2018
@atomb atomb removed this from the Cryptol 2.6 milestone May 17, 2018
@brianhuffman brianhuffman added the semantics Issues related to the dynamic semantics of Cryptol. label Jun 21, 2019
@brianhuffman
Copy link
Contributor

Duplicate of #422.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
semantics Issues related to the dynamic semantics of Cryptol.
Projects
None yet
Development

No branches or pull requests

4 participants