From ad9fed296a58beb452bd83e5817a1dbf86733b48 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 11 Aug 2020 16:05:29 -0700 Subject: [PATCH 1/3] Remove 8-bit type constraint for character/string literals. This makes it possible to use wider character types to represent Unicode code points beyond the first 256. See #863. --- src/Cryptol/TypeCheck/Infer.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index ba783a2ba..a653077c2 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -133,12 +133,10 @@ desugarLiteral lit = in P.EAppT fracPrim [ arg numerator, arg denominator, rnd ] P.ECChar c -> - number [ ("val", P.TNum (toInteger (fromEnum c))) - , ("rep", tBits (8 :: Integer)) ] + number [ ("val", P.TNum (toInteger (fromEnum c))) ] P.ECString s -> - P.ETyped (P.EList [ P.ELit (P.ECChar c) | c <- s ]) - (P.TSeq P.TWild (P.TSeq (P.TNum 8) P.TBit)) + P.EList [ P.ELit (P.ECChar c) | c <- s ] From 41438b78bed91575a71d6a9ea757f0440375fa29 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 11 Aug 2020 16:07:05 -0700 Subject: [PATCH 2/3] Update test output with changed type variable names/numbers. --- tests/issues/T146.icry.stdout | 16 +-- tests/issues/issue290v2.icry.stdout | 4 +- tests/issues/issue723.icry.stdout | 4 +- tests/regression/instance.icry.stdout | 180 +++++++++++++------------- 4 files changed, 102 insertions(+), 102 deletions(-) diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 8234d6252..c16fd5825 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,14 +3,14 @@ Loading module Cryptol Loading module Main [error] at T146.cry:1:18--6:10: - The type ?fv`958 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`942 + The type ?fv`968 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`952 where - ?fv`958 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`942 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`968 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 + fv`952 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: - The type ?fv`960 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`942 + The type ?fv`970 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`952 where - ?fv`960 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`942 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`970 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 + fv`952 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 80d491320..f5fcea938 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`939 == 1 + • n`949 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`939 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`949 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index 808bee838..562f45e95 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`939 + • k == n`949 arising from matching types at issue723.cry:7:17--7:19 where - n`939 is signature variable 'n' at issue723.cry:1:6--1:7 + n`949 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index c2a52ada1..385b3a00e 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`1179) + • Logic (Z ?n`1189) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1179 is type wildcard (_) at :1:15--1:16 + ?n`1189 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`1193 ?n`1194) + • Logic (Float ?n`1203 ?n`1204) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1193 is type wildcard (_) at :1:19--1:20 - ?n`1194 is type wildcard (_) at :1:21--1:22 + ?n`1203 is type wildcard (_) at :1:19--1:20 + ?n`1204 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`1217) + • Integral (Z ?n`1227) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1217' is not an integral type. + • Reason: Type 'Z ?n`1227' is not an integral type. where - ?n`1217 is type wildcard (_) at :1:8--1:9 + ?n`1227 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`1220 -> ?a`1221) + • Integral (?a`1230 -> ?a`1231) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1220 -> ?a`1221' is not an integral type. + • Reason: Type '?a`1230 -> ?a`1231' is not an integral type. where - ?a`1220 is type wildcard (_) at :1:7--1:8 - ?a`1221 is type wildcard (_) at :1:12--1:13 + ?a`1230 is type wildcard (_) at :1:7--1:8 + ?a`1231 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`1220, ?a`1221) + • Integral (?a`1230, ?a`1231) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1220, ?a`1221)' is not an integral type. + • Reason: Type '(?a`1230, ?a`1231)' is not an integral type. where - ?a`1220 is type wildcard (_) at :1:7--1:8 - ?a`1221 is type wildcard (_) at :1:10--1:11 + ?a`1230 is type wildcard (_) at :1:7--1:8 + ?a`1231 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`1220, y : ?a`1221} + • Integral {x : ?a`1230, y : ?a`1231} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1220, y : ?a`1221}' is not an integral type. + • Reason: Type '{x : ?a`1230, y : ?a`1231}' is not an integral type. where - ?a`1220 is type wildcard (_) at :1:11--1:12 - ?a`1221 is type wildcard (_) at :1:18--1:19 + ?a`1230 is type wildcard (_) at :1:11--1:12 + ?a`1231 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1220 ?n`1221) + • Integral (Float ?n`1230 ?n`1231) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1220 ?n`1221' is not an integral type. + • Reason: Type 'Float ?n`1230 ?n`1231' is not an integral type. where - ?n`1220 is type wildcard (_) at :1:12--1:13 - ?n`1221 is type wildcard (_) at :1:14--1:15 + ?n`1230 is type wildcard (_) at :1:12--1:13 + ?n`1231 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`1221) + • Field (Z ?n`1231) arising from use of expression recip at :1:1--1:6 • Reason: Type 'Z' does not support field operations. where - ?n`1221 is type wildcard (_) at :1:10--1:11 + ?n`1231 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Field ([?n`1221]?a`1222) + • Field ([?n`1231]?a`1232) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1221 is type wildcard (_) at :1:9--1:10 - ?a`1222 is type wildcard (_) at :1:11--1:12 + ?n`1231 is type wildcard (_) at :1:9--1:10 + ?a`1232 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1221 -> ?a`1222) + • Field (?a`1231 -> ?a`1232) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1221 is type wildcard (_) at :1:9--1:10 - ?a`1222 is type wildcard (_) at :1:14--1:15 + ?a`1231 is type wildcard (_) at :1:9--1:10 + ?a`1232 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`1221, ?a`1222) + • Field (?a`1231, ?a`1232) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1221 is type wildcard (_) at :1:9--1:10 - ?a`1222 is type wildcard (_) at :1:12--1:13 + ?a`1231 is type wildcard (_) at :1:9--1:10 + ?a`1232 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`1221, y : ?a`1222} + • Field {x : ?a`1231, y : ?a`1232} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1221 is type wildcard (_) at :1:13--1:14 - ?a`1222 is type wildcard (_) at :1:20--1:21 + ?a`1231 is type wildcard (_) at :1:13--1:14 + ?a`1232 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`1225) + • Round (Z ?n`1235) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1225 is type wildcard (_) at :1:10--1:11 + ?n`1235 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1225]?a`1226) + • Round ([?n`1235]?a`1236) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1225 is type wildcard (_) at :1:9--1:10 - ?a`1226 is type wildcard (_) at :1:11--1:12 + ?n`1235 is type wildcard (_) at :1:9--1:10 + ?a`1236 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1225 -> ?a`1226) + • Round (?a`1235 -> ?a`1236) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1225 is type wildcard (_) at :1:9--1:10 - ?a`1226 is type wildcard (_) at :1:14--1:15 + ?a`1235 is type wildcard (_) at :1:9--1:10 + ?a`1236 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`1225, ?a`1226) + • Round (?a`1235, ?a`1236) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1225 is type wildcard (_) at :1:9--1:10 - ?a`1226 is type wildcard (_) at :1:12--1:13 + ?a`1235 is type wildcard (_) at :1:9--1:10 + ?a`1236 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`1225, y : ?a`1226} + • Round {x : ?a`1235, y : ?a`1236} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1225 is type wildcard (_) at :1:13--1:14 - ?a`1226 is type wildcard (_) at :1:20--1:21 + ?a`1235 is type wildcard (_) at :1:13--1:14 + ?a`1236 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`1236 -> ?a`1237) + • Eq (?a`1246 -> ?a`1247) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1236 is type wildcard (_) at :1:8--1:9 - ?a`1237 is type wildcard (_) at :1:13--1:14 + ?a`1246 is type wildcard (_) at :1:8--1:9 + ?a`1247 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`1250) + • Cmp (Z ?n`1260) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1250 is type wildcard (_) at :1:8--1:9 + ?n`1260 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`1253 -> ?a`1254) + • Cmp (?a`1263 -> ?a`1264) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1253 is type wildcard (_) at :1:7--1:8 - ?a`1254 is type wildcard (_) at :1:12--1:13 + ?a`1263 is type wildcard (_) at :1:7--1:8 + ?a`1264 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`1264) + • SignedCmp (Z ?n`1274) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1264 is type wildcard (_) at :1:9--1:10 + ?n`1274 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`1267 -> ?a`1268) + • SignedCmp (?a`1277 -> ?a`1278) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1267 is type wildcard (_) at :1:8--1:9 - ?a`1268 is type wildcard (_) at :1:13--1:14 + ?a`1277 is type wildcard (_) at :1:8--1:9 + ?a`1278 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,24 +454,24 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1275 ?n`1276) + • SignedCmp (Float ?n`1285 ?n`1286) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1275 is type wildcard (_) at :1:13--1:14 - ?n`1276 is type wildcard (_) at :1:15--1:16 + ?n`1285 is type wildcard (_) at :1:13--1:14 + ?n`1286 is type wildcard (_) at :1:15--1:16 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1275 Bit + • Literal ?val`1285 Bit arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type 'Bit' does not support integer literals. where - ?val`1275 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1285 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Ambiguous numeric type: type argument 'val' of 'number' @@ -484,60 +484,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1282 (?a`1283 -> ?a`1284) + • Literal ?val`1292 (?a`1293 -> ?a`1294) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1283 -> ?a`1284' does not support integer literals. + • Reason: Type '?a`1293 -> ?a`1294' does not support integer literals. where - ?val`1282 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1283 is type wildcard (_) at :1:15--1:16 - ?a`1284 is type wildcard (_) at :1:20--1:21 + ?val`1292 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1293 is type wildcard (_) at :1:15--1:16 + ?a`1294 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1282 () + • Literal ?val`1292 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1282 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1292 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1282 (?a`1283, ?a`1284) + • Literal ?val`1292 (?a`1293, ?a`1294) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1283, ?a`1284)' does not support integer literals. + • Reason: Type '(?a`1293, ?a`1294)' does not support integer literals. where - ?val`1282 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1283 is type wildcard (_) at :1:16--1:17 - ?a`1284 is type wildcard (_) at :1:19--1:20 + ?val`1292 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1293 is type wildcard (_) at :1:16--1:17 + ?a`1294 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1282 {} + • Literal ?val`1292 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1282 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1292 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1282 {x : ?a`1283, y : ?a`1284} + • Literal ?val`1292 {x : ?a`1293, y : ?a`1294} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1283, - y : ?a`1284}' does not support integer literals. + • Reason: Type '{x : ?a`1293, + y : ?a`1294}' does not support integer literals. where - ?val`1282 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1283 is type wildcard (_) at :1:20--1:21 - ?a`1284 is type wildcard (_) at :1:27--1:28 + ?val`1292 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1293 is type wildcard (_) at :1:20--1:21 + ?a`1294 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 From 1df2bd8efa4f0aaff7d1280fd5e66d3239d6d546 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 11 Aug 2020 16:19:03 -0700 Subject: [PATCH 3/3] Add type constraints to strings in some regression tests. --- tests/issues/issue138.icry | 2 +- tests/issues/issue389.icry | 4 ++-- tests/issues/issue474.icry | 2 +- tests/issues/issue474.icry.stdout | 2 +- tests/regression/check17.cry | 2 +- tests/regression/r04.icry | 2 +- tests/regression/safety.icry | 4 ++-- tests/regression/safety.icry.stdout | 2 +- 8 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/issues/issue138.icry b/tests/issues/issue138.icry index 517399f00..f4722bdf4 100644 --- a/tests/issues/issue138.icry +++ b/tests/issues/issue138.icry @@ -1,4 +1,4 @@ :l issue138.cry down down' -take_some`{4,3} "abcd" +take_some`{4,3,[8]} "abcd" diff --git a/tests/issues/issue389.icry b/tests/issues/issue389.icry index 6681105a5..c9c23a12c 100644 --- a/tests/issues/issue389.icry +++ b/tests/issues/issue389.icry @@ -1,3 +1,3 @@ :l issue389.cry -pad (join "a") -test (join "a") +pad (join "a" : [8]) +test (join "a" : [8]) diff --git a/tests/issues/issue474.icry b/tests/issues/issue474.icry index d25191836..072aa4e04 100644 --- a/tests/issues/issue474.icry +++ b/tests/issues/issue474.icry @@ -1,3 +1,3 @@ let mapping = ['A' .. 'Z'] <<< 13 let mapped c = if (('A' <= c) && (c <= 'Z')) then (mapping @ (c - 'A')) else c -:sat \x -> mapped x == 'N' +:sat \(x : [8]) -> mapped x == 'N' diff --git a/tests/issues/issue474.icry.stdout b/tests/issues/issue474.icry.stdout index 50c8b5e9f..041f535e4 100644 --- a/tests/issues/issue474.icry.stdout +++ b/tests/issues/issue474.icry.stdout @@ -1,3 +1,3 @@ Loading module Cryptol Satisfiable -(\x -> mapped x == 'N') 0x41 = True +(\(x : [8]) -> mapped x == 'N') 0x41 = True diff --git a/tests/regression/check17.cry b/tests/regression/check17.cry index 67616e55a..280acb15d 100644 --- a/tests/regression/check17.cry +++ b/tests/regression/check17.cry @@ -1 +1 @@ -check17 = "" == [] +check17 = ("" : [0][8]) == [] diff --git a/tests/regression/r04.icry b/tests/regression/r04.icry index d540ba086..3aab0d430 100644 --- a/tests/regression/r04.icry +++ b/tests/regression/r04.icry @@ -1,2 +1,2 @@ :set ascii=on -if 1 <= 9 /\ 9 >= 1 /\ 1 < 9 /\ 9 > 1 /\ 1 == 1 then "comparisons good" else "comparisons bad " +if 1 <= 9 /\ 9 >= 1 /\ 1 < 9 /\ 9 > 1 /\ 1 == 1 then "comparisons good" else "comparisons bad " : [_][8] diff --git a/tests/regression/safety.icry b/tests/regression/safety.icry index a23735752..3e5e02d9c 100644 --- a/tests/regression/safety.icry +++ b/tests/regression/safety.icry @@ -1,9 +1,9 @@ :set prover-stats = no -:safe (\x -> assert x "asdf" "asdf") +:safe (\x -> assert x "asdf" "asdf" : [_][8]) :safe (\(x:[4]) -> [0..14]@x == x) :safe (\y -> (10:Integer) / y) -:safe (\x -> if x then "OK!!" else assert (~x) "not OK!" "asdf") +:safe (\x -> if x then "OK!!" else assert (~x) "not OK!" "asdf" : [_][8]) :safe (\(x:[4]) -> [0..15]@x == x) :safe (\y -> if y == 0 then 42 else (10:Integer) / y) diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout index a5e02ff6e..2d9047c37 100644 --- a/tests/regression/safety.icry.stdout +++ b/tests/regression/safety.icry.stdout @@ -1,6 +1,6 @@ Loading module Cryptol Counterexample -(\x -> assert x "asdf" "asdf") False ~> ERROR +(\x -> assert x "asdf" "asdf" : [_][8]) False ~> ERROR Counterexample (\(x : [4]) -> [0 .. 14] @ x == x) 0xf ~> ERROR Counterexample