Update test output due to changed cryptol prelude.

This commit is contained in:
Brian Huffman 2021-05-06 13:38:43 -07:00
parent 9b7e60b9f4
commit 52c91817d9
8 changed files with 22 additions and 20 deletions

View File

@ -4,15 +4,15 @@ Loading module Main
[error] at T146.cry:1:18--6:10:
The type ?a is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`751
It cannot depend on quantified variables: fv`812
When checking type of field 'v0'
where
?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
fv`751 is signature variable 'fv' at T146.cry:11:10--11:12
fv`812 is signature variable 'fv' at T146.cry:11:10--11:12
[error] at T146.cry:5:19--5:24:
The type ?b is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`751
It cannot depend on quantified variables: fv`812
When checking signature variable 'fv'
where
?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
fv`751 is signature variable 'fv' at T146.cry:11:10--11:12
fv`812 is signature variable 'fv' at T146.cry:11:10--11:12

View File

@ -8,20 +8,20 @@ Loading module Main
[warning] at issue1024a.cry:4:34--4:39 Unused name: g
[error] at issue1024a.cry:1:6--1:11:
Illegal kind assigned to type variable: f`748
Illegal kind assigned to type variable: f`809
Unexpected: # -> *
where
f`748 is signature variable 'f' at issue1024a.cry:1:12--1:24
f`809 is signature variable 'f' at issue1024a.cry:1:12--1:24
[error] at issue1024a.cry:2:6--2:13:
Illegal kind assigned to type variable: f`749
Illegal kind assigned to type variable: f`810
Unexpected: Prop
where
f`749 is signature variable 'f' at issue1024a.cry:2:14--2:24
f`810 is signature variable 'f' at issue1024a.cry:2:14--2:24
[error] at issue1024a.cry:4:13--4:49:
Illegal kind assigned to type variable: f`751
Illegal kind assigned to type variable: f`812
Unexpected: # -> *
where
f`751 is signature variable 'f' at issue1024a.cry:4:22--4:32
f`812 is signature variable 'f' at issue1024a.cry:4:22--4:32
Loading module Cryptol
Loading module Main
0xffff

View File

@ -2,7 +2,7 @@ Loading module Cryptol
Run-time error: undefined
-- Backtrace --
Cryptol::error called at Cryptol:965:13--965:18
Cryptol::error called at Cryptol:990:13--990:18
Cryptol::undefined called at issue103.icry:1:9--1:18
Using exhaustive testing.
Testing... ERROR for the following inputs:

View File

@ -184,6 +184,8 @@ Symbols
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a
sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
split :
{parts, each, a} (fin each) => [parts * each]a -> [parts][each]a
splitAt :

View File

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

View File

@ -10,9 +10,9 @@ Loading module Main
assuming
• fin k
the following constraints hold:
• k == n`748
• k == n`809
arising from
matching types
at issue723.cry:7:17--7:19
where
n`748 is signature variable 'n' at issue723.cry:1:6--1:7
n`809 is signature variable 'n' at issue723.cry:1:6--1:7

View File

@ -3,7 +3,7 @@ Counterexample
(\x -> assert x "asdf" "asdf") False ~> ERROR
Run-time error: asdf
-- Backtrace --
Cryptol::error called at Cryptol:973:41--973:46
Cryptol::error called at Cryptol:998:41--998:46
Cryptol::assert called at safety.icry:3:14--3:20
<interactive>::it called at safety.icry:3:7--3:37
Counterexample

View File

@ -83,19 +83,19 @@ Loading module Main
[error] at tc-errors-5.cry:2:5--2:7:
Inferred type is not sufficiently polymorphic.
Quantified variable: a`748
Quantified variable: a`809
cannot match type: [0]?a
When checking the type of 'Main::f'
where
?a is type of sequence member at tc-errors-5.cry:2:5--2:7
a`748 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
a`809 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
Loading module Cryptol
Loading module Main
[error] at tc-errors-6.cry:4:7--4:8:
The type ?a is not sufficiently polymorphic.
It cannot depend on quantified variables: b`752
It cannot depend on quantified variables: b`813
When checking the type of 'g'
where
?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
b`752 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
b`813 is signature variable 'b' at tc-errors-6.cry:3:8--3:9