GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-04 13:54:09 +03:00
Code Issues Projects Releases Wiki Activity

Tweak names and order of type variables on Cryptol prelude functions.

Browse Source 
Also update test output for new type variable names.

See #517.
This commit is contained in:
Brian Huffman 2018-06-28 14:14:11 -07:00
parent 75b56e251e
commit 836771aded
15 changed files with 134 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

102
lib/Cryptol.cry
View File

@ -280,7 +280,7 @@ primitive zero : {a} (Zero a) => a
/**
* Converts a bitvector to a non-negative integer in the range 0 to 2^^n-1.
*/
primitive toInteger : {a} (fin a) => [a] -> Integer
primitive toInteger : {bits} (fin bits) => [bits] -> Integer
/**
* Converts an unbounded integer to another arithmetic type. When converting
@ -297,25 +297,25 @@ primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
* Left shift. The first argument is the sequence to shift, the second is the
* number of positions to shift by.
*/
primitive (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
primitive (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
/**
* Right shift. The first argument is the sequence to shift, the second is the
* number of positions to shift by.
*/
primitive (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
primitive (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
/**
* Left rotate. The first argument is the sequence to rotate, the second is the
* number of positions to rotate by.
*/
primitive (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
primitive (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
/**
* Right rotate. The first argument is the sequence to rotate, the second is
* the number of positions to rotate by.
*/
primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
primitive (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
/**
* 2's complement signed (arithmetic) right shift. The first argument
@ -323,7 +323,7 @@ primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
* the second argument is the number of positions to shift
* by (considered as an unsigned value).
*/
primitive (>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
primitive (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
@ -358,24 +358,25 @@ primitive split : {parts, each, a} (fin each) => [parts * each]a
/**
* Reverses the elements in a sequence.
*/
primitive reverse : {a, b} (fin a) => [a]b -> [a]b
primitive reverse : {n, a} (fin n) => [n]a -> [n]a
/**
* Transposes an [a][b] matrix into a [b][a] matrix.
* Transposes a matrix.
* Satisfies the property 'transpose m @ i @ j == m @ j @ i'.
*/
primitive transpose : {a, b, c} [a][b]c -> [b][a]c
primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
/**
* Index operator. The first argument is a sequence. The second argument is
* the zero-based index of the element to select from the sequence.
*/
primitive (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
primitive (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
/**
* Bulk index operator. The first argument is a sequence. The second argument
* is a sequence of the zero-based indices of the elements to select.
*/
(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
xs @@ is = [ xs @ i | i <- is ]
/**
@ -383,14 +384,14 @@ xs @@ is = [ xs @ i | i <- is ]
* argument is the zero-based index of the element to select, starting from the
* end of the sequence.
*/
primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
primitive (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
/**
* Bulk reverse index operator. The first argument is a finite sequence. The
* second argument is a sequence of the zero-based indices of the elements to
* select, starting from the end of the sequence.
*/
(!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
xs !! is = [ xs ! i | i <- is ]
/**
@ -400,7 +401,7 @@ xs !! is = [ xs ! i | i <- is ]
* The third argument is the new element. The return value is the
* initial sequence updated so that the indicated index has the given value.
*/
primitive update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
primitive update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
/**
* Update the given sequence with new value at the given index position.
@ -409,7 +410,7 @@ primitive update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
* The third argument is the new element. The return value is the
* initial sequence updated so that the indicated index has the given value.
*/
primitive updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
primitive updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
/**
* Perform a series of updates to a sequence. The first argument is
@ -418,7 +419,7 @@ primitive updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
* This function applies the 'update' function in sequence with the
* given update pairs.
*/
updates : {a,b,c,d} (fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
updates : {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
updates xs0 idxs vals = xss!0
where
xss = [ xs0 ] #
@ -435,7 +436,7 @@ updates xs0 idxs vals = xss!0
* This function applies the 'updateEnd' function in sequence with the
* given update pairs.
*/
updatesEnd : {a,b,c,d} (fin a, fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
updatesEnd : {n, k, ix, a} (fin n, fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
updatesEnd xs0 idxs vals = xss!0
where
xss = [ xs0 ] #
@ -488,13 +489,13 @@ primitive infFrom : {a} (Arith a) => a -> [inf]a
*/
primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a
primitive error : {at, len} (fin len) => [len][8] -> at
primitive error : {a, len} (fin len) => [len][8] -> a
/**
* Performs multiplication of polynomials over GF(2).
*/
pmult : {a, b} (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + a + b]
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pmult x y = last zs
where
zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]
@ -502,33 +503,33 @@ pmult x y = last zs
/**
* Performs division of polynomials over GF(2).
*/
pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pdiv x y = [ z ! degree | z <- zs ]
where
degree : [width b]
degree = last (ds : [1 + b]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..b] | d <- ds ]
degree : [width v]
degree = last (ds : [1 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [b] -> [b]
reduce : [v] -> [v]
reduce u = if u ! degree then u ^ y else u
zs : [a][b]
zs : [u][v]
zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]
/**
* Performs modulus of polynomials over GF(2).
*/
pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
pmod x y = if y == 0 then 0/0 else last zs
where
degree : [width b]
degree = last (ds : [2 + b]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..b] | d <- ds ]
degree : [width v]
degree = last (ds : [2 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [1 + b] -> [1 + b]
reduce : [1 + v] -> [1 + v]
reduce u = if u ! degree then u ^ y else u
powers : [inf][1 + b]
powers : [inf][1 + v]
powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
@ -543,35 +544,34 @@ type String n = [n][8]
type Word n = [n]
type Char = [8]
take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem
take : {front, back, a} (fin front) => [front + back]a -> [front]a
take (x # _) = x
drop : {front,back,elem} (fin front) => [front + back] elem -> [back] elem
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
drop ((_ : [front] _) # y) = y
tail : {a, b} [1 + a]b -> [a]b
tail : {n, a} [1 + n]a -> [n]a
tail xs = drop`{1} xs
/**
* Return the left-most element of a sequence.
*/
head : {a, b} [1 + a]b -> b
head : {n, a} [1 + n]a -> a
head xs = xs @ 0
/**
* Return the right-most element of a sequence.
*/
last : {a, b} (fin a) => [1 + a]b -> b
last : {n, a} (fin n) => [1 + n]a -> a
last xs = xs ! 0
width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]
width _ = `len
width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
width _ = `n
undefined : {a} a
undefined = error "undefined"
groupBy : {each,parts,elem} (fin each) =>
[parts * each] elem -> [parts][each]elem
groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
groupBy = split`{parts=parts}
/**
@ -623,19 +623,19 @@ or xs = zero != xs
/**
* Conjunction after applying a predicate to all elements.
*/
all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
all f xs = and (map f xs)
/**
* Disjunction after applying a predicate to all elements.
*/
any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
any f xs = or (map f xs)
/**
* Map a function over a sequence.
*/
map : {a, b, n} (a -> b) -> [n]a -> [n]b
map : {n, a, b} (a -> b) -> [n]a -> [n]b
map f xs = [f x | x <- xs]
/**
@ -643,7 +643,7 @@ map f xs = [f x | x <- xs]
*
* foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
*/
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl f acc xs = ys ! 0
where ys = [acc] # [f a x | a <- ys | x <- xs]
@ -652,27 +652,27 @@ foldl f acc xs = ys ! 0
*
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
*/
foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foldr f acc xs = ys ! 0
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
/**
* Compute the sum of the values in the sequence.
*/
sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
sum xs = foldl (+) zero xs
sum : {n, a} (fin n, Arith a) => [n]a -> a
sum xs = foldl (+) (fromInteger 0) xs
/**
* Scan left is like a foldl that also emits the intermediate values.
*/
scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [n+1]b
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [n+1]b
scanl f acc xs = ys
where ys = [acc] # [f a x | a <- ys | x <- xs]
/**
* Scan right is like a foldr that also emits the intermediate values.
*/
scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr f acc xs = reverse ys
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
@ -691,13 +691,13 @@ elem a xs = any (\x -> x == a) xs
/**
* Create a list of tuples from two lists.
*/
zip : {a,b,n} [n]a -> [n]b -> [n](a,b)
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
zip xs ys = [(x,y) | x <- xs | y <- ys]
/**
* Create a list by applying the function to each pair of elements in the input.
*/
zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
zipWith f xs ys = [f x y | x <- xs | y <- ys]
/**

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

@ -3,12 +3,12 @@ Loading module Cryptol
Loading module Main
[error] at ./T146.cry:1:18--6:10:
The type ?q33 is not sufficiently polymorphic.
It cannot depend on quantified variables: a`858
where
?q33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
[error] at ./T146.cry:5:19--5:24:
The type ?s33 is not sufficiently polymorphic.
It cannot depend on quantified variables: a`858
It cannot depend on quantified variables: a`860
where
?s33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
?s33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
[error] at ./T146.cry:5:19--5:24:
The type ?u33 is not sufficiently polymorphic.
It cannot depend on quantified variables: a`860
where
?u33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24

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

@ -33,11 +33,11 @@ Symbols
(#) :
{front, back, a} (fin front) =>
[front]a -> [back]a -> [front + back]a
(<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
(<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
(>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
(>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
(<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
(>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
(>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
(>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
(+) : {a} (Arith a) => a -> a -> a
(-) : {a} (Arith a) => a -> a -> a
(%) : {a} (Arith a) => a -> a -> a
@ -46,24 +46,23 @@ Symbols
(/) : {a} (Arith a) => a -> a -> a
(/$) : {a} (Arith a) => a -> a -> a
(^^) : {a} (Arith a) => a -> a -> a
(!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
(!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
(@) : {a, b, c} (fin c) => [a]b -> [c] -> b
(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
all : {a, n} (fin n) => (a -> Bit) -> [n]a -> Bit
(!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
(@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
and : {n} (fin n) => [n] -> Bit
any : {a, n} (fin n) => (a -> Bit) -> [n]a -> Bit
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
carry : {n} (fin n) => [n] -> [n] -> Bit
complement : {a} (Logic a) => a -> a
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
demote : {val, rep} (Literal val rep) => rep
drop :
{front, back, elem} (fin front) => [front + back]elem -> [back]elem
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
error : {at, len} (fin len) => [len][8] -> at
error : {a, len} (fin len) => [len][8] -> a
False : Bit
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldr : {a, b, n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foo : {a} a -> a
fromInteger : {a} (Arith a) => Integer -> a
fromThen :
@ -81,31 +80,30 @@ Symbols
[1 + (last - first)]a
fromZ : {n} (fin n, n >= 1) => Z n -> Integer
groupBy :
{each, parts, elem} (fin each) =>
[each * parts]elem -> [parts][each]elem
head : {a, b} [1 + a]b -> b
{each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
head : {n, a} [1 + n]a -> a
infFrom : {a} (Arith a) => a -> [inf]a
infFromThen : {a} (Arith a) => a -> a -> [inf]a
iterate : {a} (a -> a) -> a -> [inf]a
join :
{parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
last : {a, b} (fin a) => [1 + a]b -> b
last : {n, a} (fin n) => [1 + n]a -> a
lg2 : {a} (Arith a) => a -> a
map : {a, b, n} (a -> b) -> [n]a -> [n]b
map : {n, a, b} (a -> b) -> [n]a -> [n]b
max : {a} (Cmp a) => a -> a -> a
min : {a} (Cmp a) => a -> a -> a
negate : {a} (Arith a) => a -> a
or : {n} (fin n) => [n] -> Bit
pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
pmult :
{a, b} (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + (a + b)]
{u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)]
random : {a} [256] -> a
repeat : {n, a} a -> [n]a
reverse : {a, b} (fin a) => [a]b -> [a]b
reverse : {n, a} (fin n) => [n]a -> [n]a
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [1 + n]b
scanr : {a, b, n} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
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]
split :
@ -113,30 +111,27 @@ Symbols
splitAt :
{front, back, a} (fin front) =>
[front + back]a -> ([front]a, [back]a)
sum : {a, n} (fin n, Zero a, Arith a) => [n]a -> a
sum : {n, a} (fin n, Arith a) => [n]a -> a
True : Bit
tail : {a, b} [1 + a]b -> [a]b
take :
{front, back, elem} (fin front) =>
[front + back]elem -> [front]elem
toInteger : {a} (fin a) => [a] -> Integer
tail : {n, a} [1 + n]a -> [n]a
take : {front, back, a} (fin front) => [front + back]a -> [front]a
toInteger : {bits} (fin bits) => [bits] -> Integer
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
traceVal : {n, a} (fin n) => [n][8] -> a -> a
transpose : {a, b, c} [a][b]c -> [b][a]c
transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
undefined : {a} a
update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
updates :
{a, b, c, d} (fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
{n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
updatesEnd :
{a, b, c, d} (fin a, fin c, fin d) =>
[a]b -> [d][c] -> [d]b -> [a]b
{n, k, ix, a} (fin n, fin ix, fin k) =>
[n]a -> [k][ix] -> [k]a -> [n]a
width :
{bits, len, elem} (fin len, fin bits, bits >= width len) =>
[len]elem -> [bits]
{bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
zero : {a} (Zero a) => a
zext : {m, n} (fin m, m >= n) => [n] -> [m]
zip : {a, b, n} [n]a -> [n]b -> [n](a, b)
zipWith : {a, b, c, n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c

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

@ -4,7 +4,7 @@ Loading module Main
[error] at ./issue290v2.cry:2:1--2:19:
Unsolved constraints:
a`855 == 1
a`857 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at ./issue290v2.cry:2:8--2:11

8
tests/regression/AES.icry.stdout
View File

@ -2,13 +2,13 @@ Loading module Cryptol
Loading module Cryptol
Loading module AES
[warning] at ./AES.cry:86:21--86:40:
Defaulting type argument 'b' of '(<<<)' to 2
Defaulting type argument 'ix' of '(<<<)' to 2
[warning] at ./AES.cry:91:24--91:43:
Defaulting type argument 'b' of '(>>>)' to 2
Defaulting type argument 'ix' of '(>>>)' to 2
[warning] at ./AES.cry:147:28--147:51:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
[warning] at ./AES.cry:147:53--147:63:
Defaulting type argument 'c' of '(@)' to 4
Defaulting type argument 'ix' of '(@)' to 4
[warning] at ./AES.cry:127:32--127:33:
Defaulting type argument 'rep' of 'demote' to [3]
True

2
tests/regression/check01.icry.stdout
View File

@ -2,6 +2,6 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check01.cry:2:5--2:27:
Defaulting type argument 'd' of '(@@)' to 5
Defaulting type argument 'ix' of '(@@)' to 5
[0x00000007, 0x00000014]
True

2
tests/regression/check02.icry.stdout
View File

@ -4,7 +4,7 @@ Loading module Main
[warning] at ./check02.cry:3:24--3:25:
Defaulting type argument 'rep' of 'demote' to [1]
[warning] at <interactive>:1:1--1:18:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:
* Using 'Integer' for 1st type argument of 'Main::ones'
[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]

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

@ -2,12 +2,12 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at <interactive>:1:1--1:22:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
[0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000004,
0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000009,
0x0000000a]
[warning] at <interactive>:1:1--1:23:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
[0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e, 0x0000000f,
0x00000010, 0x00000011, 0x00000012, 0x00000013, 0x00000014,
0x00000015]

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

@ -2,11 +2,11 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check04.cry:4:10--4:45:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check04.cry:4:43--4:44:
Defaulting type argument 'rep' of 'demote' to [2]
[warning] at <interactive>:1:1--1:21:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:
* Using 'Integer' for 1st type argument of 'Main::onetwos'
[1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1]

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

@ -2,11 +2,11 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check05.cry:4:10--4:45:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check05.cry:4:43--4:44:
Defaulting type argument 'rep' of 'demote' to [2]
[warning] at <interactive>:1:1--1:21:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:
* Using 'Integer' for 1st type argument of 'Main::twoones'
[2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2]

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

@ -2,11 +2,11 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check06.cry:5:10--5:70:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check06.cry:5:66--5:67:
Defaulting type argument 'rep' of 'demote' to [2]
[warning] at <interactive>:1:1--1:24:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:
* Using 'Integer' for 1st type argument of 'Main::onesytwosy'
[[1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1],

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

@ -2,21 +2,21 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check07.cry:7:16--7:35:
Defaulting type argument 'b' of '(<<)' to 6
Defaulting type argument 'ix' of '(<<)' to 6
[warning] at ./check07.cry:13:11--13:22:
Defaulting type argument 'a' of '(<<)' to 1
Defaulting type argument 'n' of '(<<)' to 1
[warning] at ./check07.cry:11:11--11:51:
Defaulting type argument 'd' of '(@@)' to 4
Defaulting type argument 'ix' of '(@@)' to 4
[warning] at ./check07.cry:5:14--5:29:
Defaulting type argument 'b' of '(>>)' to 7
Defaulting type argument 'ix' of '(>>)' to 7
[warning] at ./check07.cry:4:14--4:29:
Defaulting type argument 'b' of '(>>)' to 6
Defaulting type argument 'ix' of '(>>)' to 6
[warning] at ./check07.cry:3:14--3:29:
Defaulting type argument 'b' of '(<<)' to 32
Defaulting type argument 'ix' of '(<<)' to 32
[warning] at ./check07.cry:2:14--2:29:
Defaulting type argument 'b' of '(<<)' to 7
Defaulting type argument 'ix' of '(<<)' to 7
[warning] at ./check07.cry:1:14--1:29:
Defaulting type argument 'b' of '(<<)' to 6
Defaulting type argument 'ix' of '(<<)' to 6
[0b00010010001101000101011001111000,
0b00100100011010001010110011110000,
0b01001000110100010101100111100000,

6
tests/regression/check08.icry.stdout
View File

@ -2,11 +2,11 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check08.cry:9:19--9:54:
Defaulting type argument 'd' of '(@@)' to 3
Defaulting type argument 'ix' of '(@@)' to 3
[warning] at ./check08.cry:7:10--7:45:
Defaulting type argument 'd' of '(@@)' to 3
Defaulting type argument 'ix' of '(@@)' to 3
[warning] at <interactive>:1:1--1:15:
Defaulting type argument 'd' of '(@@)' to 3
Defaulting type argument 'ix' of '(@@)' to 3
[0x00000001, 0x00000002, 0x00000005, 0x0000000c, 0x0000001b]
True
Q.E.D.

10
tests/regression/check09.icry.stdout
View File

@ -14,16 +14,16 @@ Loading module Main
This binding for ss shadows the existing binding from
(at ./check09.cry:5:1--5:3, ss)
[warning] at ./check09.cry:17:12--17:28:
Defaulting type argument 'd' of '(@@)' to 3
Defaulting type argument 'ix' of '(@@)' to 3
[warning] at ./check09.cry:13:12--13:80:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check09.cry:14:12--14:80:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at <interactive>:1:1--1:15:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[0x00000008, 0x00004080, 0x00068c00, 0x00a22800]
[warning] at <interactive>:1:1--1:15:
Defaulting type argument 'd' of '(@@)' to 2
Defaulting type argument 'ix' of '(@@)' to 2
[0x00000800, 0x00005080, 0x00072d00, 0x00b08200]
[0x00000008, 0x131b638b, 0x4fdd24a2, 0xb9094711, 0xa9cc106f,
0x52c445fb, 0xec66ea8b]

2
tests/regression/check11.icry.stdout
View File

@ -2,7 +2,7 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check11.cry:5:10--5:25:
Defaulting type argument 'd' of '(@@)' to 7
Defaulting type argument 'ix' of '(@@)' to 7
[warning] at ./check11.cry:3:10--3:19:
Defaulting type argument 'a' of 'fromTo' to [7]
True