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

join primitive used at type [inf][0] -> [0] crashes REPL #395

Closed
brianhuffman opened this issue Jan 27, 2017 · 0 comments
Closed

join primitive used at type [inf][0] -> [0] crashes REPL #395

brianhuffman opened this issue Jan 27, 2017 · 0 comments
Assignees
Labels
bug Something not working correctly

Comments

@brianhuffman
Copy link
Contributor

I found this problem while exploring some corner cases of Cryptol's evaluation semantics. For example:

Cryptol> :t join (zero : [inf][0])
join (zero : [inf][0]) : [0]
Cryptol> join (zero : [inf][0])
cryptol: divide by zero

Instead of returning to the REPL prompt, cryptol then exits to the command line.

A related result:

Cryptol> :t join (zero : [inf][0]) == []
(join (zero : [inf][0]) == []) : Bit
Cryptol> join (zero : [inf][0]) == []
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/galoisinc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  e48f430b3074c59eec6eec3f9d9fcd1d7bfddfe8
  Branch:    master (non-committed files present during build)
  Location:  [Eval] fromVWord
  Message:   not a word
             compareLeft
%< --------------------------------------------------- 

also:

Cryptol> :prove join (zero : [inf][0]) == []
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/galoisinc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  e48f430b3074c59eec6eec3f9d9fcd1d7bfddfe8
  Branch:    master (non-committed files present during build)
  Location:  Cryptol.Symbolic.Prims.cmpValue
  Message:   type mismatch
%< --------------------------------------------------- 
@brianhuffman brianhuffman added the bug Something not working correctly label Feb 3, 2017
@robdockins robdockins self-assigned this May 9, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly
Projects
None yet
Development

No branches or pull requests

2 participants