GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Update test suite

Browse Source
This commit is contained in:
Rob Dockins 2020-05-26 15:33:46 -07:00
parent fd13055eb6
commit e817f5c777
6 changed files with 22 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/contrib/MISTY1.cry
View File

@ -227,7 +227,7 @@ extend : {total, n} (fin total, fin n, total >= n) => [n] -> [total]
extend n = zero # n extend n = zero # n
isEven : {a} (fin a) => [a] -> Bool isEven : {a} (fin a) => [a] -> Bool
isEven n = ~(n ! zero) isEven n = ~(n ! 0)
// //
// Examples // Examples

16
tests/issues/T146.icry.stdout
View File

@ -3,14 +3,14 @@ Loading module Cryptol
Loading module Main Loading module Main
[error] at T146.cry:1:18--6:10: [error] at T146.cry:1:18--6:10:
The type ?fv`968 is not sufficiently polymorphic. The type ?fv`942 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`952 It cannot depend on quantified variables: fv`926
where where
?fv`968 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 ?fv`942 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 fv`926 is signature variable 'fv' at T146.cry:11:10--11:12
[error] at T146.cry:5:19--5:24: [error] at T146.cry:5:19--5:24:
The type ?fv`970 is not sufficiently polymorphic. The type ?fv`944 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`952 It cannot depend on quantified variables: fv`926
where where
?fv`970 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 ?fv`944 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 fv`926 is signature variable 'fv' at T146.cry:11:10--11:12

5
tests/issues/issue226.icry.stdout
View File

@ -106,7 +106,7 @@ Symbols
(*) : {a} (Ring a) => a -> a -> a (*) : {a} (Ring a) => a -> a -> a
(/) : {a} (Integral a) => a -> a -> a (/) : {a} (Integral a) => a -> a -> a
(/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
(^^) : {a, n} (Ring a, fin n) => a -> [n] -> a (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
(!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a
(!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a (!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a
(@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a
@ -134,7 +134,8 @@ Symbols
lengthFromThenTo first next last == len) => lengthFromThenTo first next last == len) =>
[len]a [len]a
fromTo : fromTo :
{first, last, a} (fin last, last >= first, Literal last a) => {first, last, a} (fin last, last >= first, Literal first a,
Literal last a) =>
[1 + (last - first)]a [1 + (last - first)]a
fromZ : {n} (fin n, n >= 1) => Z n -> Integer fromZ : {n} (fin n, n >= 1) => Z n -> Integer
generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a

4
tests/issues/issue290v2.icry.stdout
View File

@ -4,9 +4,9 @@ Loading module Main
[error] at issue290v2.cry:2:1--2:19: [error] at issue290v2.cry:2:1--2:19:
Unsolved constraints: Unsolved constraints:
• n`949 == 1 • n`923 == 1
arising from arising from
checking a pattern: type of 1st argument of Main::minMax checking a pattern: type of 1st argument of Main::minMax
at issue290v2.cry:2:8--2:11 at issue290v2.cry:2:8--2:11
where where
n`949 is signature variable 'n' at issue290v2.cry:1:11--1:12 n`923 is signature variable 'n' at issue290v2.cry:1:11--1:12

6
tests/issues/issue486.icry.stdout
View File

@ -1,4 +1,10 @@
Loading module Cryptol Loading module Cryptol
[warning] at <interactive>:1:17--1:28:
Defaulting type argument 'e' of '(^^)' to [0]
Q.E.D. Q.E.D.
[warning] at <interactive>:1:17--1:28:
Defaulting type argument 'e' of '(^^)' to [1]
Q.E.D. Q.E.D.
[warning] at <interactive>:1:17--1:44:
Defaulting type argument 'e' of '(^^)' to [3]
Q.E.D. Q.E.D.

4
tests/regression/check07.icry.stdout
View File

@ -1,8 +1,8 @@
Loading module Cryptol Loading module Cryptol
Loading module Cryptol Loading module Cryptol
Loading module Main Loading module Main
[warning] at check07.cry:9:17--9:38: [warning] at check07.cry:9:46--9:57:
Defaulting type argument 'n' of '(^^)' to 6 Defaulting type argument 'a' of 'fromTo' to [6]
[warning] at check07.cry:7:43--7:54: [warning] at check07.cry:7:43--7:54:
Defaulting type argument 'a' of 'fromTo' to [6] Defaulting type argument 'a' of 'fromTo' to [6]
[warning] at check07.cry:13:11--13:22: [warning] at check07.cry:13:11--13:22: