Update tests for changes to inference

The changes didn't alter the behavior of the typechecker, only the
warning/error output, and the order of some variables when generalizing.
This commit is contained in:
Trevor Elliott 2014-12-30 10:43:38 -08:00
parent 12e0d8605c
commit 41ca73ffaa
27 changed files with 204 additions and 204 deletions

View File

@ -1,4 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
maxSeq' : {a, b} (fin b) => [a][b] -> [1 + a][b]
maxSeq' : {a, b} (fin a) => [b][a] -> [1 + b][a]

View File

@ -4,16 +4,16 @@ Loading module Main
[warning] at simon.cry2:83:1--92:15:
Defaulting type parameter 'bits'
of literal or demoted expression
at simon.cry2:87:28--87:30
to max (width a`431) 3
at simon.cry2:87:34--87:35
to max (width a`450) 3
[warning] at simon.cry2:83:1--92:15:
Defaulting 3rd type parameter
of expression (@)
at simon.cry2:90:27--90:28
to width a`433
Defaulting type parameter 'bits'
of literal or demoted expression
at simon.cry2:90:29--90:31
to width a`452
[warning] at simon.cry2:83:1--92:15:
Defaulting 3rd type parameter
of expression (@)
at simon.cry2:89:29--89:30
to max (width (a`432 - 1)) (max (width a`431) 6)
Defaulting type parameter 'bits'
of literal or demoted expression
at simon.cry2:89:36--89:38
to max (width (a`451 - 1)) (max (width a`450) 6)
True

View File

@ -4,16 +4,16 @@ Loading module test01
module test01
import Cryptol
/* Not recursive */
test01::a : {a, b} (fin b) => [b]a -> [2 * b]a
test01::a = \{a, b} (fin b) ->
(\ (x : [b]a) ->
f b x
test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
test01::a = \{a, b} (fin a) ->
(\ (x : [a]b) ->
f a x
where
/* Not recursive */
f : {c} [c]a -> [b + c]a
f = \{c} (y : [c]a) -> (#) b c a <> x y
f : {c} [c]b -> [a + c]b
f = \{c} (y : [c]b) -> (#) a c b <> x y
) : [b]a -> [2 * b]a
) : [a]b -> [2 * a]b
Loading module Cryptol
Loading module test01

View File

@ -21,15 +21,15 @@ Loading module test02
module test02
import Cryptol
/* Not recursive */
test02::test : {a, b} a -> b
test02::test = \{a, b} (a : a) ->
test02::test : {a, b} b -> a
test02::test = \{a, b} (a : b) ->
f a
where
/* Recursive */
f : a -> b
f = \ (x : a) -> g a
g : a -> b
g = \ (x : a) -> f x
f : b -> a
f = \ (x : b) -> g a
g : b -> a
g = \ (x : b) -> f x

View File

@ -22,11 +22,11 @@ Loading module test04
at test04.cry:3:19--3:21
to 4
[error] at test04.cry:3:17--3:21:
[error] at test04.cry:3:19--3:21:
Type mismatch:
Expected type: [?b3]
Inferred type: ()
Expected type: ()
Inferred type: [?k3]
where
?b3 is type parameter 'bits'
?k3 is type parameter 'bits'
of literal or demoted expression
at test04.cry:3:19--3:21

View File

@ -2,29 +2,29 @@ Loading module Cryptol
Loading module Cryptol
Loading module AES
[warning] at AES.cry:147:1--150:39:
Defaulting 4th type parameter
of expression (@@)
at AES.cry:147:33--147:35
Defaulting type parameter 'bits'
of finite enumeration
at AES.cry:147:36--147:51
to 4
[warning] at AES.cry:147:1--150:39:
Defaulting 3rd type parameter
of expression (@)
at AES.cry:147:58--147:59
Defaulting type parameter 'bits'
of literal or demoted expression
at AES.cry:147:60--147:63
to 4
[warning] at AES.cry:124:1--124:9:
Defaulting type parameter 'bits'
of literal or demoted expression
at AES.cry:127:26--127:29
at AES.cry:127:32--127:33
to 3
[warning] at AES.cry:91:1--93:23:
Defaulting 2nd type parameter
of expression (>>>)
at AES.cry:91:28--91:31
Defaulting type parameter 'bits'
of finite enumeration
at AES.cry:92:61--92:69
to 2
[warning] at AES.cry:86:1--88:20:
Defaulting 2nd type parameter
of expression (<<<)
at AES.cry:86:25--86:28
Defaulting type parameter 'bits'
of finite enumeration
at AES.cry:87:58--87:66
to 2
True
True

View File

@ -2,9 +2,9 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at check01.cry:2:1--2:27:
Defaulting 4th type parameter
of expression (@@)
at check01.cry:2:17--2:19
Defaulting type parameter 'bits'
of literal or demoted expression
at check01.cry:2:24--2:26
to 5
[0x00000007, 0x00000014]
True

View File

@ -2,14 +2,14 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--3:25:
Defaulting 1st type parameter
of expression Main::ones
at check02.cry:3:10--3:14
Defaulting type parameter 'bits'
of literal or demoted expression
at check02.cry:3:24--3:25
to 1
[warning] at <interactive>:1:1--1:18:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:6--1:8
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:9--1:18
to 4
Assuming a = 1
[0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1]

View File

@ -2,17 +2,17 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at <interactive>:1:1--1:22:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:8--1:10
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:11--1:22
to 4
[0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000004,
0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000009,
0x0000000a]
[warning] at <interactive>:1:1--1:23:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:9--1:11
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:12--1:23
to 4
[0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e, 0x0000000f,
0x00000010, 0x00000011, 0x00000012, 0x00000013, 0x00000014,

View File

@ -2,19 +2,19 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--4:45:
Defaulting 1st type parameter
of expression Main::onetwos
at check04.cry:4:10--4:17
Defaulting type parameter 'bits'
of finite enumeration
at check04.cry:4:21--4:29
to 2
[warning] at :1:1--4:45:
Defaulting 4th type parameter
of expression (@@)
at check04.cry:4:18--4:20
Defaulting type parameter 'bits'
of literal or demoted expression
at check04.cry:4:43--4:44
to 2
[warning] at <interactive>:1:1--1:21:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:9--1:11
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:12--1:21
to 4
Assuming a = 2
[0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1]

View File

@ -2,19 +2,19 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--4:45:
Defaulting 1st type parameter
of expression Main::twoones
at check05.cry:4:10--4:17
Defaulting type parameter 'bits'
of finite enumeration
at check05.cry:4:21--4:29
to 2
[warning] at :1:1--4:45:
Defaulting 4th type parameter
of expression (@@)
at check05.cry:4:18--4:20
Defaulting type parameter 'bits'
of literal or demoted expression
at check05.cry:4:43--4:44
to 2
[warning] at <interactive>:1:1--1:21:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:9--1:11
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:12--1:21
to 4
Assuming a = 2
[0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2]

View File

@ -2,19 +2,19 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--5:70:
Defaulting 1st type parameter
of expression Main::onesytwosy
at check06.cry:5:10--5:20
Defaulting type parameter 'bits'
of finite enumeration
at check06.cry:5:24--5:32
to 2
[warning] at :1:1--5:70:
Defaulting 4th type parameter
of expression (@@)
at check06.cry:5:21--5:23
Defaulting type parameter 'bits'
of literal or demoted expression
at check06.cry:5:66--5:67
to 2
[warning] at <interactive>:1:1--1:24:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:12--1:14
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:15--1:24
to 4
Assuming a = 2
[[0x1, 0x2], [0x2, 0x1], [0x1, 0x2], [0x2, 0x1], [0x1, 0x2],

View File

@ -2,44 +2,44 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--14:39:
Defaulting 1st type parameter
of expression (<<)
at check07.cry:13:13--13:15
Defaulting type parameter 'bits'
of literal or demoted expression
at check07.cry:13:21--13:22
to 1
[warning] at :1:1--14:39:
Defaulting 4th type parameter
of expression (@@)
at check07.cry:11:36--11:38
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:11:39--11:51
to 4
[warning] at check07.cry:7:1--7:56:
Defaulting 2nd type parameter
of expression (<<)
at check07.cry:7:31--7:33
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:7:43--7:54
to 6
[warning] at :1:1--14:39:
Defaulting 2nd type parameter
of expression (>>)
at check07.cry:5:25--5:27
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:5:37--5:49
to 7
[warning] at :1:1--14:39:
Defaulting 2nd type parameter
of expression (>>)
at check07.cry:4:25--4:27
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:4:37--4:48
to 6
[warning] at :1:1--14:39:
Defaulting 2nd type parameter
of expression (<<)
at check07.cry:3:25--3:27
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:3:37--3:65
to 32
[warning] at :1:1--14:39:
Defaulting 2nd type parameter
of expression (<<)
at check07.cry:2:25--2:27
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:2:37--2:49
to 7
[warning] at :1:1--14:39:
Defaulting 2nd type parameter
of expression (<<)
at check07.cry:1:25--1:27
Defaulting type parameter 'bits'
of finite enumeration
at check07.cry:1:37--1:48
to 6
[0b00010010001101000101011001111000,
0b00100100011010001010110011110000,

View File

@ -2,19 +2,19 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--7:45:
Defaulting 4th type parameter
of expression (@@)
at check08.cry:9:22--9:24
Defaulting type parameter 'bits'
of finite enumeration
at check08.cry:9:25--9:33
to 3
[warning] at :1:1--7:45:
Defaulting 4th type parameter
of expression (@@)
at check08.cry:7:13--7:15
Defaulting type parameter 'bits'
of finite enumeration
at check08.cry:7:16--7:24
to 3
[warning] at <interactive>:1:1--1:15:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:4--1:6
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:7--1:15
to 3
[0x00000001, 0x00000002, 0x00000005, 0x0000000c, 0x0000001b]
True

View File

@ -14,30 +14,30 @@ Loading module Main
This binding for ss shadows the existing binding from
(at check09.cry:5:1--5:3, Main::ss)
[warning] at check09.cry:17:1--30:54:
Defaulting 4th type parameter
of expression (@@)
at check09.cry:17:15--17:17
Defaulting type parameter 'bits'
of finite enumeration
at check09.cry:17:18--17:28
to 3
[warning] at :1:1--37:28:
Defaulting 4th type parameter
of expression (@@)
at check09.cry:14:15--14:17
Defaulting type parameter 'bits'
of finite enumeration
at check09.cry:13:18--13:26
to 2
[warning] at :1:1--37:28:
Defaulting 4th type parameter
of expression (@@)
at check09.cry:13:15--13:17
Defaulting type parameter 'bits'
of finite enumeration
at check09.cry:14:18--14:26
to 2
[warning] at <interactive>:1:1--1:15:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:4--1:6
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:7--1:15
to 2
[0x00000008, 0x00004080, 0x00068c00, 0x00a22800]
[warning] at <interactive>:1:1--1:15:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:4--1:6
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:7--1:15
to 2
[0x00000800, 0x00005080, 0x00072d00, 0x00b08200]
[0x00000008, 0x131b638b, 0x4fdd24a2, 0xb9094711, 0xa9cc106f,

View File

@ -7,8 +7,8 @@ Loading module Main
at check11.cry:3:10--3:19
to 7
[warning] at :1:1--5:25:
Defaulting 4th type parameter
of expression (@@)
at check11.cry:5:13--5:15
Defaulting type parameter 'bits'
of finite enumeration
at check11.cry:5:16--5:25
to 7
True

View File

@ -4,7 +4,7 @@ Loading module Main
[warning] at :1:1--5:76:
Defaulting type parameter 'bits'
of literal or demoted expression
at check14.cry:5:41--5:42
at check14.cry:5:73--5:74
to 3
Assuming a = 3
[[0x3, 0x2, 0x1, 0x0], [0x7, 0x6, 0x5, 0x4]]

View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--4:17:
Defaulting 1st type parameter
of expression Cryptol::width
at check16-tab.cry:1:11--1:16
Defaulting type parameter 'bits'
of literal or demoted expression
at check16-tab.cry:1:22--1:23
to 4
True

View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--4:13:
Defaulting 1st type parameter
of expression Cryptol::width
at check16.cry:1:11--1:16
Defaulting type parameter 'bits'
of literal or demoted expression
at check16.cry:1:22--1:23
to 4
True

View File

@ -4,6 +4,6 @@ Loading module Main
[warning] at :1:1--3:39:
Defaulting type parameter 'bits'
of literal or demoted expression
at check20.cry:1:30--1:31
at check20.cry:3:31--3:33
to 4
True

View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--7:63:
Defaulting 3rd type parameter
of expression (!)
at check21.cry:4:18--4:19
Defaulting type parameter 'bits'
of literal or demoted expression
at check21.cry:4:31--4:32
to 4
True

View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--12:70:
Defaulting 3rd type parameter
of expression (!)
at check22.cry:3:18--3:19
Defaulting type parameter 'bits'
of literal or demoted expression
at check22.cry:3:31--3:32
to 4
True

View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--4:82:
Defaulting 1st type parameter
of expression Main::xor
at check24.cry:4:13--4:16
Defaulting type parameter 'bits'
of finite enumeration
at check24.cry:4:60--4:71
to 4
True

View File

@ -5,9 +5,9 @@ Loading module check25
This binding for tz shadows the existing binding from
(at check25.cry:3:1--3:3, check25::tz)
[warning] at check25.cry:1:1--8:19:
Defaulting 1st type parameter
of expression check25::tx
at check25.cry:8:11--8:13
Defaulting type parameter 'bits'
of literal or demoted expression
at check25.cry:8:17--8:19
to 4
[warning] at check25.cry:1:1--8:19:
Defaulting type parameter 'bits'

View File

@ -2,59 +2,34 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at :1:1--13:43:
Defaulting 1st type parameter
Defaulting 2nd type parameter
of expression Main::xys
at check26.cry:11:42--11:45
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xys
at check26.cry:8:31--8:34
to 3
[warning] at :1:1--13:43:
Defaulting type parameter 'bits'
of finite enumeration
at check26.cry:9:23--9:34
to 4
[warning] at :1:1--13:43:
Defaulting type parameter 'bits'
of finite enumeration
at check26.cry:9:41--9:51
to 3
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xys
at check26.cry:8:31--8:34
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xys
at check26.cry:8:31--8:34
to 3
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:5:35--5:37
at check26.cry:4:17--4:19
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xy
at check26.cry:5:35--5:37
to 5
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:5:17--5:19
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xy
at check26.cry:5:17--5:19
to 5
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:4:43--4:45
to 4
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:4:37--4:39
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xy
at check26.cry:4:37--4:39
at check26.cry:4:17--4:19
to 5
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
@ -64,11 +39,36 @@ Loading module Main
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:4:17--4:19
at check26.cry:4:37--4:39
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xy
at check26.cry:4:17--4:19
at check26.cry:4:37--4:39
to 5
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:4:43--4:45
to 4
[warning] at :1:1--13:43:
Defaulting 2nd type parameter
of expression Main::xy
at check26.cry:5:17--5:19
to 5
[warning] at :1:1--13:43:
Defaulting type parameter 'bits'
of literal or demoted expression
at check26.cry:5:23--5:25
to 4
[warning] at :1:1--13:43:
Defaulting 1st type parameter
of expression Main::xy
at check26.cry:5:35--5:37
to 4
[warning] at :1:1--13:43:
Defaulting type parameter 'bits'
of literal or demoted expression
at check26.cry:5:41--5:43
to 5
True

View File

@ -3,25 +3,25 @@ Loading module Cryptol
Loading module Main
[warning] at <interactive>:1:1--1:42:
Defaulting type parameter 'bits'
of literal or demoted expression
at <interactive>:1:40--1:42
of finite enumeration
at <interactive>:1:11--1:19
to 4
True
[warning] at <interactive>:1:1--1:43:
Defaulting type parameter 'bits'
of literal or demoted expression
at <interactive>:1:41--1:43
of finite enumeration
at <interactive>:1:11--1:20
to 4
False
[warning] at <interactive>:1:1--1:48:
Defaulting type parameter 'bits'
of literal or demoted expression
at <interactive>:1:46--1:48
of finite enumeration
at <interactive>:1:11--1:25
to 7
False
[warning] at <interactive>:1:1--1:47:
Defaulting type parameter 'bits'
of literal or demoted expression
at <interactive>:1:45--1:47
of finite enumeration
at <interactive>:1:11--1:24
to 7
True

View File

@ -3,7 +3,7 @@ Assuming a = 4
[0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb]
[warning] at <interactive>:1:1--1:68:
Defaulting type parameter 'bits'
of finite enumeration
at <interactive>:1:1--1:10
of literal or demoted expression
at <interactive>:1:65--1:67
to 4
True