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

Issue839 #844

Merged
merged 3 commits into from
Jul 28, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
130 changes: 121 additions & 9 deletions src/Cryptol/TypeCheck/Solver/Class.hs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,26 @@ solveLogicInst ty = case tNoUser ty of
-- Logic Bit
TCon (TC TCBit) [] -> SolvedIf []

-- Logic Integer fails
TCon (TC TCInteger) [] ->
Unsolvable $
TCErrorMessage "Type 'Integer' does not support logical operations."

-- Logic (Z n) fails
TCon (TC TCIntMod) [_] ->
Unsolvable $
TCErrorMessage "Type 'Z' does not support logical operations."

-- Logic Rational fails
TCon (TC TCRational) [] ->
Unsolvable $
TCErrorMessage "Type 'Rational' does not support logical operations."

-- Logic (Float e p) fails
TCon (TC TCFloat) [_, _] ->
Unsolvable $
TCErrorMessage "Type 'Float' does not support logical operations."

-- Logic a => Logic [n]a
TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]

Expand Down Expand Up @@ -144,7 +164,7 @@ solveRingInst ty = case tNoUser ty of

-- Ring Bit fails
TCon (TC TCBit) [] ->
Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
Unsolvable $ TCErrorMessage "Type 'Bit' does not support ring operations."

-- Ring Integer
TCon (TC TCInteger) [] -> SolvedIf []
Expand Down Expand Up @@ -193,7 +213,7 @@ solveIntegralInst ty = case tNoUser ty of

-- Integral Bit fails
TCon (TC TCBit) [] ->
Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
Unsolvable $ TCErrorMessage "Type 'Bit' is not an integral type."

-- Integral Integer
TCon (TC TCInteger) [] -> SolvedIf []
Expand All @@ -219,16 +239,50 @@ solveFieldInst ty = case tNoUser ty of
-- Field Error -> fails
TCon (TError _ e) _ -> Unsolvable e

-- Field Bit fails
TCon (TC TCBit) [] ->
Unsolvable $
TCErrorMessage "Type 'Bit' does not support field operations."

-- Field Integer fails
TCon (TC TCInteger) [] ->
Unsolvable $
TCErrorMessage "Type 'Integer' does not support field operations."

-- Field Rational
TCon (TC TCRational) [] -> SolvedIf []

-- ValidFloat e p => Field (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]

-- Field Real
-- Field (Z n)

-- Field (Z n) fails for now (to be added later with a 'prime n' requirement)
TCon (TC TCIntMod) [_] ->
Unsolvable $
TCErrorMessage "Type 'Z' does not support field operations."
-- TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne, pPrime n ]

-- Field ([n]a) fails
TCon (TC TCSeq) [_, _] ->
Unsolvable $
TCErrorMessage "Sequence types do not support field operations."

-- Field (a -> b) fails
TCon (TC TCFun) [_, _] ->
Unsolvable $
TCErrorMessage "Function types do not support field operations."

-- Field (a, b, ...) fails
TCon (TC (TCTuple _)) _ ->
Unsolvable $
TCErrorMessage "Tuple types do not support field operations."

-- Field {x : a, y : b, ...} fails
TRec _ ->
Unsolvable $
TCErrorMessage "Record types do not support field operations."

_ -> Unsolved


Expand All @@ -239,6 +293,21 @@ solveRoundInst ty = case tNoUser ty of
-- Round Error -> fails
TCon (TError _ e) _ -> Unsolvable e

-- Round Bit fails
TCon (TC TCBit) [] ->
Unsolvable $
TCErrorMessage "Type 'Bit' does not support rounding operations."

-- Round Integer fails
TCon (TC TCInteger) [] ->
Unsolvable $
TCErrorMessage "Type 'Integer' does not support rounding operations."

-- Round (Z n) fails
TCon (TC TCIntMod) [_] ->
Unsolvable $
TCErrorMessage "Type 'Z' does not support rounding operations."

-- Round Rational
TCon (TC TCRational) [] -> SolvedIf []

Expand All @@ -247,6 +316,26 @@ solveRoundInst ty = case tNoUser ty of

-- Round Real

-- Round ([n]a) fails
TCon (TC TCSeq) [_, _] ->
Unsolvable $
TCErrorMessage "Sequence types do not support rounding operations."

-- Round (a -> b) fails
TCon (TC TCFun) [_, _] ->
Unsolvable $
TCErrorMessage "Function types do not support rounding operations."

-- Round (a, b, ...) fails
TCon (TC (TCTuple _)) _ ->
Unsolvable $
TCErrorMessage "Tuple types do not support rounding operations."

-- Round {x : a, y : b, ...} fails
TRec _ ->
Unsolvable $
TCErrorMessage "Record types do not support rounding operations."

_ -> Unsolved


Expand Down Expand Up @@ -281,7 +370,7 @@ solveEqInst ty = case tNoUser ty of

-- Eq (a -> b) fails
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
Unsolvable $ TCErrorMessage "Function types do not support comparisons."

-- (Eq a, Eq b) => Eq { x:a, y:b }
TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ]
Expand All @@ -307,7 +396,7 @@ solveCmpInst ty = case tNoUser ty of

-- Cmp (Z n) fails
TCon (TC TCIntMod) [_] ->
Unsolvable $ TCErrorMessage "Values of Z_n type cannot be compared for order"
Unsolvable $ TCErrorMessage "Type 'Z' does not support order comparisons."

-- ValidFloat e p => Cmp (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
Expand All @@ -320,7 +409,7 @@ solveCmpInst ty = case tNoUser ty of

-- Cmp (a -> b) fails
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
Unsolvable $ TCErrorMessage "Function types do not support order comparisons."

-- (Cmp a, Cmp b) => Cmp { x:a, y:b }
TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ]
Expand Down Expand Up @@ -350,8 +439,30 @@ solveSignedCmpInst ty = case tNoUser ty of
-- SignedCmp Error -> fails
TCon (TError _ e) _ -> Unsolvable e

-- SignedCmp Bit
TCon (TC TCBit) [] -> Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on bits"
-- SignedCmp Bit fails
TCon (TC TCBit) [] ->
Unsolvable $
TCErrorMessage "Type 'Bit' does not support signed comparisons."

-- SignedCmp Integer fails
TCon (TC TCInteger) [] ->
Unsolvable $
TCErrorMessage "Type 'Integer' does not support signed comparisons."

-- SignedCmp (Z n) fails
TCon (TC TCIntMod) [_] ->
Unsolvable $
TCErrorMessage "Type 'Z' does not support signed comparisons."

-- SignedCmp Rational fails
TCon (TC TCRational) [] ->
Unsolvable $
TCErrorMessage "Type 'Rational' does not support signed comparisons."

-- SignedCmp (Float e p) fails
TCon (TC TCFloat) [_, _] ->
Unsolvable $
TCErrorMessage "Type 'Float' does not support signed comparisons."

-- SignedCmp for sequences
TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a
Expand All @@ -361,7 +472,8 @@ solveSignedCmpInst ty = case tNoUser ty of

-- SignedCmp (a -> b) fails
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on functions."
Unsolvable $
TCErrorMessage "Function types do not support signed comparisons."

-- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ]
Expand Down
3 changes: 2 additions & 1 deletion tests/issues/issue835.icry.stdout
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,9 @@ Loading module Cryptol
Loading module Float

[error] at <interactive>:1:1--1:28:
Unsolved constraints:
Unsolvable constraints:
• SignedCmp (Float 5 11)
arising from
use of expression (<$)
at <interactive>:1:1--1:28
• Reason: Type 'Float' does not support signed comparisons.
Loading