diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index f25cec699..1248f065c 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -49,6 +49,7 @@ import Cryptol.Utils.RecordMap mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym) mkLit sym ty i = case ty of + TVBit -> pure $ VBit (bitLit sym (i > 0)) TVInteger -> VInteger <$> integerLit sym i TVIntMod m | m == 0 -> evalPanic "mkLit" ["0 modulus not allowed"] diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index 48ecb75c6..8f5d2e5f9 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -531,6 +531,9 @@ solveLiteralInst val ty -- Literal n Error -> fails TCon (TError _ e) _ -> Unsolvable e + -- (1 >= val) => Literal val Bit + TCon (TC TCBit) [] -> SolvedIf [ tOne >== val ] + -- (fin val) => Literal val Integer TCon (TC TCInteger) [] -> SolvedIf [ pFin val ] diff --git a/tests/issues/issue913.icry b/tests/issues/issue913.icry new file mode 100644 index 000000000..955ab040e --- /dev/null +++ b/tests/issues/issue913.icry @@ -0,0 +1,5 @@ +or [0,1,0,1] +and [1,0,1,1] +[0,1,0,1,1,0,1,1:Bit] +:t number`{rep=Bit} +2 : Bit diff --git a/tests/issues/issue913.icry.stdout b/tests/issues/issue913.icry.stdout new file mode 100644 index 000000000..7472047c0 --- /dev/null +++ b/tests/issues/issue913.icry.stdout @@ -0,0 +1,13 @@ +Loading module Cryptol +True +False +0x5b +number`{rep = Bit} : {n} (1 >= n) => Bit + +[error] at :1:1--1:2: + Unsolvable constraints: + • 1 >= 2 + arising from + use of literal or demoted expression + at :1:1--1:2 + • Reason: It is not the case that 1 >= 2 diff --git a/tests/regression/instance.cry b/tests/regression/instance.cry index 9f3d0c1f2..331f3634d 100644 --- a/tests/regression/instance.cry +++ b/tests/regression/instance.cry @@ -348,6 +348,10 @@ signedCmpRecord = (<$) //////////////////////////////////////////////////////////////////////////////// // Literal +/** instance (1 >= val) => Literal val Bit */ +literalBit : {val} (1 >= val) => Bit +literalBit = `val + /** instance (fin val) => Literal val Integer */ literalInteger : {val} (fin val) => Integer literalInteger = `val diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index 33e7391b6..bba099f86 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Z ?n`1201) + • Logic (Z ?n`1203) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1201 is type wildcard (_) at :1:15--1:16 + ?n`1203 is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -50,14 +50,14 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Float ?n`1215 ?n`1216) + • Logic (Float ?n`1217 ?n`1218) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1215 is type wildcard (_) at :1:19--1:20 - ?n`1216 is type wildcard (_) at :1:21--1:22 + ?n`1217 is type wildcard (_) at :1:19--1:20 + ?n`1218 is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: Unsolvable constraints: @@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Z ?n`1239) + • Integral (Z ?n`1241) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1239' is not an integral type. + • Reason: Type 'Z ?n`1241' is not an integral type. where - ?n`1239 is type wildcard (_) at :1:8--1:9 + ?n`1241 is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1242 -> ?a`1243) + • Integral (?a`1244 -> ?a`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1242 -> ?a`1243' is not an integral type. + • Reason: Type '?a`1244 -> ?a`1245' is not an integral type. where - ?a`1242 is type wildcard (_) at :1:7--1:8 - ?a`1243 is type wildcard (_) at :1:12--1:13 + ?a`1244 is type wildcard (_) at :1:7--1:8 + ?a`1245 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: Unsolvable constraints: @@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1242, ?a`1243) + • Integral (?a`1244, ?a`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1242, ?a`1243)' is not an integral type. + • Reason: Type '(?a`1244, ?a`1245)' is not an integral type. where - ?a`1242 is type wildcard (_) at :1:7--1:8 - ?a`1243 is type wildcard (_) at :1:10--1:11 + ?a`1244 is type wildcard (_) at :1:7--1:8 + ?a`1245 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: Unsolvable constraints: @@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral {x : ?a`1242, y : ?a`1243} + • Integral {x : ?a`1244, y : ?a`1245} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1242, y : ?a`1243}' is not an integral type. + • Reason: Type '{x : ?a`1244, y : ?a`1245}' is not an integral type. where - ?a`1242 is type wildcard (_) at :1:11--1:12 - ?a`1243 is type wildcard (_) at :1:18--1:19 + ?a`1244 is type wildcard (_) at :1:11--1:12 + ?a`1245 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1242 ?n`1243) + • Integral (Float ?n`1244 ?n`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1242 ?n`1243' is not an integral type. + • Reason: Type 'Float ?n`1244 ?n`1245' is not an integral type. where - ?n`1242 is type wildcard (_) at :1:12--1:13 - ?n`1243 is type wildcard (_) at :1:14--1:15 + ?n`1244 is type wildcard (_) at :1:12--1:13 + ?n`1245 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -187,35 +187,35 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (Z ?n`1243) + • Field (Z ?n`1245) arising from use of expression recip at :1:1--1:6 • Reason: Type 'Z' does not support field operations. where - ?n`1243 is type wildcard (_) at :1:10--1:11 + ?n`1245 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Field ([?n`1243]?a`1244) + • Field ([?n`1245]?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1243 is type wildcard (_) at :1:9--1:10 - ?a`1244 is type wildcard (_) at :1:11--1:12 + ?n`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1243 -> ?a`1244) + • Field (?a`1245 -> ?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1243 is type wildcard (_) at :1:9--1:10 - ?a`1244 is type wildcard (_) at :1:14--1:15 + ?a`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -227,14 +227,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1243, ?a`1244) + • Field (?a`1245, ?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1243 is type wildcard (_) at :1:9--1:10 - ?a`1244 is type wildcard (_) at :1:12--1:13 + ?a`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -246,14 +246,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field {x : ?a`1243, y : ?a`1244} + • Field {x : ?a`1245, y : ?a`1246} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1243 is type wildcard (_) at :1:13--1:14 - ?a`1244 is type wildcard (_) at :1:20--1:21 + ?a`1245 is type wildcard (_) at :1:13--1:14 + ?a`1246 is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m @@ -276,35 +276,35 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (Z ?n`1247) + • Round (Z ?n`1249) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1247 is type wildcard (_) at :1:10--1:11 + ?n`1249 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1247]?a`1248) + • Round ([?n`1249]?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1247 is type wildcard (_) at :1:9--1:10 - ?a`1248 is type wildcard (_) at :1:11--1:12 + ?n`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1247 -> ?a`1248) + • Round (?a`1249 -> ?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1247 is type wildcard (_) at :1:9--1:10 - ?a`1248 is type wildcard (_) at :1:14--1:15 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -316,14 +316,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1247, ?a`1248) + • Round (?a`1249, ?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1247 is type wildcard (_) at :1:9--1:10 - ?a`1248 is type wildcard (_) at :1:12--1:13 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -335,14 +335,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round {x : ?a`1247, y : ?a`1248} + • Round {x : ?a`1249, y : ?a`1250} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1247 is type wildcard (_) at :1:13--1:14 - ?a`1248 is type wildcard (_) at :1:20--1:21 + ?a`1249 is type wildcard (_) at :1:13--1:14 + ?a`1250 is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -352,14 +352,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • Eq (?a`1258 -> ?a`1259) + • Eq (?a`1260 -> ?a`1261) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1258 is type wildcard (_) at :1:8--1:9 - ?a`1259 is type wildcard (_) at :1:13--1:14 + ?a`1260 is type wildcard (_) at :1:8--1:9 + ?a`1261 is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -373,25 +373,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (Z ?n`1272) + • Cmp (Z ?n`1274) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1272 is type wildcard (_) at :1:8--1:9 + ?n`1274 is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (?a`1275 -> ?a`1276) + • Cmp (?a`1277 -> ?a`1278) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1275 is type wildcard (_) at :1:7--1:8 - ?a`1276 is type wildcard (_) at :1:12--1:13 + ?a`1277 is type wildcard (_) at :1:7--1:8 + ?a`1278 is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -426,25 +426,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Z ?n`1286) + • SignedCmp (Z ?n`1288) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1286 is type wildcard (_) at :1:9--1:10 + ?n`1288 is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (?a`1289 -> ?a`1290) + • SignedCmp (?a`1291 -> ?a`1292) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1289 is type wildcard (_) at :1:8--1:9 - ?a`1290 is type wildcard (_) at :1:13--1:14 + ?a`1291 is type wildcard (_) at :1:8--1:9 + ?a`1292 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,24 +454,15 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1297 ?n`1298) + • SignedCmp (Float ?n`1299 ?n`1300) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1297 is type wildcard (_) at :1:13--1:14 - ?n`1298 is type wildcard (_) at :1:15--1:16 - -[error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1297 Bit - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type 'Bit' does not support integer literals. - where - ?val`1297 is type argument 'val' of 'number' at :1:1--1:7 + ?n`1299 is type wildcard (_) at :1:13--1:14 + ?n`1300 is type wildcard (_) at :1:15--1:16 +number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:7: Ambiguous numeric type: type argument 'val' of 'number' @@ -484,60 +475,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1304 (?a`1305 -> ?a`1306) + • Literal ?val`1308 (?a`1309 -> ?a`1310) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1305 -> ?a`1306' does not support integer literals. + • Reason: Type '?a`1309 -> ?a`1310' does not support integer literals. where - ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1305 is type wildcard (_) at :1:15--1:16 - ?a`1306 is type wildcard (_) at :1:20--1:21 + ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1309 is type wildcard (_) at :1:15--1:16 + ?a`1310 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1304 () + • Literal ?val`1308 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1304 (?a`1305, ?a`1306) + • Literal ?val`1308 (?a`1309, ?a`1310) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1305, ?a`1306)' does not support integer literals. + • Reason: Type '(?a`1309, ?a`1310)' does not support integer literals. where - ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1305 is type wildcard (_) at :1:16--1:17 - ?a`1306 is type wildcard (_) at :1:19--1:20 + ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1309 is type wildcard (_) at :1:16--1:17 + ?a`1310 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1304 {} + • Literal ?val`1308 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1304 {x : ?a`1305, y : ?a`1306} + • Literal ?val`1308 {x : ?a`1309, y : ?a`1310} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1305, - y : ?a`1306}' does not support integer literals. + • Reason: Type '{x : ?a`1309, + y : ?a`1310}' does not support integer literals. where - ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1305 is type wildcard (_) at :1:20--1:21 - ?a`1306 is type wildcard (_) at :1:27--1:28 + ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1309 is type wildcard (_) at :1:20--1:21 + ?a`1310 is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i