mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
commit
4a4673eec4
@ -897,6 +897,31 @@ generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
|
||||
generate f = [ f i | i <- [0 .. <n] ]
|
||||
|
||||
|
||||
/**
|
||||
* Sort a sequence of elements. Equivalent to 'sortBy (<=)'.
|
||||
*/
|
||||
sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a
|
||||
sort = sortBy (<=)
|
||||
|
||||
/**
|
||||
* Sort a sequence according to the given less-than-or-equal relation.
|
||||
* The sorting is stable, so it preserves the relative position of any
|
||||
* pair of elements that are equivalent according to the order relation.
|
||||
*/
|
||||
sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
|
||||
sortBy le vs =
|
||||
if `n == (0 : Integer) then vs
|
||||
else drop`{1 - min 1 n} (insertBy (vs@0) (sortBy le (drop`{min 1 n} vs)))
|
||||
where
|
||||
insertBy : {k} (fin k) => a -> [k]a -> [k+1]a
|
||||
insertBy x0 ys = xys.0 # [last xs]
|
||||
where
|
||||
xs : [k+1]a
|
||||
xs = [x0] # xys.1
|
||||
xys : [k](a, a)
|
||||
xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]
|
||||
|
||||
|
||||
// GF_2^n polynomial computations -------------------------------------------
|
||||
|
||||
/**
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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:
|
||||
|
@ -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 :
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
4
tests/regression/sort.icry
Normal file
4
tests/regression/sort.icry
Normal file
@ -0,0 +1,4 @@
|
||||
sortBy (\x y -> x.0 ==> y.0) [(True, 0x1), (False, 0x2), (True, 0x3), (False, 0x4)]
|
||||
[ ((n * n) % 23 : Integer, n) | n <- [0..22] ]
|
||||
sortBy (\x y -> x.0 <= y.0) it
|
||||
sortBy (\x y -> x.1 >= y.1) it
|
14
tests/regression/sort.icry.stdout
Normal file
14
tests/regression/sort.icry.stdout
Normal file
@ -0,0 +1,14 @@
|
||||
Loading module Cryptol
|
||||
[(False, 0x2), (False, 0x4), (True, 0x1), (True, 0x3)]
|
||||
[(0, 0), (1, 1), (4, 2), (9, 3), (16, 4), (2, 5), (13, 6), (3, 7),
|
||||
(18, 8), (12, 9), (8, 10), (6, 11), (6, 12), (8, 13), (12, 14),
|
||||
(18, 15), (3, 16), (13, 17), (2, 18), (16, 19), (9, 20), (4, 21),
|
||||
(1, 22)]
|
||||
[(0, 0), (1, 1), (1, 22), (2, 5), (2, 18), (3, 7), (3, 16), (4, 2),
|
||||
(4, 21), (6, 11), (6, 12), (8, 10), (8, 13), (9, 3), (9, 20),
|
||||
(12, 9), (12, 14), (13, 6), (13, 17), (16, 4), (16, 19), (18, 8),
|
||||
(18, 15)]
|
||||
[(1, 22), (4, 21), (9, 20), (16, 19), (2, 18), (13, 17), (3, 16),
|
||||
(18, 15), (12, 14), (8, 13), (6, 12), (6, 11), (8, 10), (12, 9),
|
||||
(18, 8), (3, 7), (13, 6), (2, 5), (16, 4), (9, 3), (4, 2), (1, 1),
|
||||
(0, 0)]
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user