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

Logic (Float e p) should be unsolvable #839

Closed
brianhuffman opened this issue Jul 28, 2020 · 1 comment · Fixed by #844
Closed

Logic (Float e p) should be unsolvable #839

brianhuffman opened this issue Jul 28, 2020 · 1 comment · Fixed by #844

Comments

@brianhuffman
Copy link
Contributor

Trying to use a Logic-class function like complement on a floating point type should be a type error, as we don't have a Logic instance for floats. But here's what you get now:

Cryptol> :m Float
Float> :t complement`{Float _ _}
complement`{Float _ _} : {n, m} (ValidFloat n m,
                                 Logic Float n m) =>
                           Float n m -> Float n m

(Note that Logic (Float n m) is incorrectly printed without parens due to #835.)

@brianhuffman
Copy link
Contributor Author

Similarly:

  • Logic should fail for Z n
  • Field should fail for Z n, [n]a, a -> b, and all tuple and record types
  • Round should fail for Z n, [n]a, a -> b, and all tuple and record types

The following constraints currently show as Unsolved, but should be upgraded to Unsolvable:

  • Logic Integer
  • Logic Rational
  • Field Bit
  • Field Integer
  • Round Bit
  • Round Integer
  • SignedCmp Bit
  • SignedCmp Integer
  • SignedCmp Rational

For example:

Cryptol> :t complement`{Integer}

[error] at <interactive>:1:1--1:11:
  Unsolved constraints:
    • Logic Integer
        arising from
        use of expression complement
        at <interactive>:1:1--1:11

brianhuffman pushed a commit that referenced this issue Jul 28, 2020
Also make the explanations/error messages a bit more uniform.
Fixes #839.
@brianhuffman brianhuffman mentioned this issue Jul 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant