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

Improvements to error messages

Browse Source
This commit is contained in:
Iavor Diatchki 2020-11-16 13:29:57 -08:00
parent 51910d7e8b
commit bfad11ba86
14 changed files with 421 additions and 461 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

102
src/Cryptol/TypeCheck/Error.hs
View File

@ -338,14 +338,7 @@ instance PP (WithNames Error) where
, "When checking" <+> pp src
]
UnsolvableGoals gs ->
addTVarsDescsAfter names err $
nested "Unsolvable constraints:" $
let unErr g = case tIsError (goal g) of
Just p -> g { goal = p }
Nothing -> g
in
bullets (map (ppWithNames names) (map unErr gs))
UnsolvableGoals gs -> explainUnsolvable names gs
UnsolvedGoals gs
| noUni ->
@ -451,6 +444,99 @@ instance PP (WithNames Error) where
explainUnsolvable :: NameMap -> [Goal] -> Doc
explainUnsolvable names gs =
addTVarsDescsAfter names gs (bullets (map explain gs))
where
bullets xs = vcat [ "•" <+> d | d <- xs ]
explain g =
let useCtr = "Unsolvable constraint:" $$
nest 2 (ppWithNames names g)
in
case tNoUser (goal g) of
TCon (PC pc) ts ->
let tys = [ backticks (ppWithNames names t) | t <- ts ]
doc1 : _ = tys
custom msg = msg $$
nest 2 (text "arising from" $$
pp (goalSource g) $$
text "at" <+> pp (goalRange g))
in
case pc of
PEqual -> useCtr
PNeq -> useCtr
PGeq -> useCtr
PFin -> useCtr
PPrime -> useCtr
PHas sel ->
custom ("Type" <+> doc1 <+> "does not have field" <+> f
<+> "of type" <+> (tys !! 1))
where f = case sel of
P.TupleSel n _ -> int n
P.RecordSel fl _ -> backticks (pp fl)
P.ListSel n _ -> int n
PZero ->
custom ("Type" <+> doc1 <+> "does not have `zero`")
PLogic ->
custom ("Type" <+> doc1 <+> "does not support logical operations.")
PRing ->
custom ("Type" <+> doc1 <+> "does not support ring operations.")
PIntegral ->
custom (doc1 <+> "is not an integral type.")
PField ->
custom ("Type" <+> doc1 <+> "does not support field operations.")
PRound ->
custom ("Type" <+> doc1 <+> "does not support rounding operations.")
PEq ->
custom ("Type" <+> doc1 <+> "does not support equality.")
PCmp ->
custom ("Type" <+> doc1 <+> "does not support comparisons.")
PSignedCmp ->
custom ("Type" <+> doc1 <+> "does not support signed comparisons.")
PLiteral ->
let doc2 = tys !! 1
in custom (doc1 <+> "is not a valid literal of type" <+> doc2)
PFLiteral ->
case ts of
~[m,n,_r,_a] ->
let frac = backticks (ppWithNamesPrec names 4 m <> "/" <>
ppWithNamesPrec names 4 n)
ty = tys !! 3
in custom (frac <+> "is not a valid literal of type" <+> ty)
PValidFloat ->
case ts of
~[e,p] ->
custom ("Unsupported floating point parameters:" $$
nest 2 ("exponent =" <+> ppWithNames names e $$
"precision =" <+> ppWithNames names p))
PAnd -> useCtr
PTrue -> useCtr
_ -> useCtr
-- | This picks the names to use when showing errors and warnings.
computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap
computeFreeVarNames warns errs =

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

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

20
tests/issues/T820.icry.stdout
View File

@ -4,15 +4,13 @@ Showing a specific instance of polymorphic result:
(ratio 1 2)
[error] at <interactive>:1:1--1:8:
Unsolvable constraints:
• Integral ?a`776
arising from
use of expression (/)
at <interactive>:1:1--1:8
• FLiteral 1 1 0 ?a`776
arising from
use of fractional literal
at <interactive>:1:1--1:8
• Reason: Mutually exclusive goals
• `?a` is not an integral type.
arising from
use of expression (/)
at <interactive>:1:1--1:8
• `1/1` is not a valid literal of type `?a`
arising from
use of fractional literal
at <interactive>:1:1--1:8
where
?a`776 is type argument 'a' of 'fraction' at <interactive>:1:1--1:8
?a is type argument 'a' of 'fraction' at <interactive>:1:1--1:8

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

@ -1,9 +1,8 @@
Loading module Cryptol
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• 0 >= 1
• Unsolvable constraint:
0 >= 1
arising from
use of partial type function (-)
at <interactive>:1:1--1:11
• Reason: It is not the case that 0 >= 1

30
tests/issues/issue582.icry.stdout
View File

@ -1,52 +1,46 @@
Loading module Cryptol
[error] at <interactive>:1:1--1:18:
Unsolvable constraints:
• fin inf
• Unsolvable constraint:
fin inf
arising from
use of partial type function (/^)
at <interactive>:1:1--1:18
• Reason: Expected a finite type, but found `inf`.
[error] at <interactive>:1:1--1:18:
Unsolvable constraints:
• fin inf
• Unsolvable constraint:
fin inf
arising from
use of partial type function (/^)
at <interactive>:1:1--1:18
• Reason: Expected a finite type, but found `inf`.
[error] at <interactive>:1:1--1:16:
Unsolvable constraints:
• 0 >= 1
• Unsolvable constraint:
0 >= 1
arising from
use of partial type function (/^)
at <interactive>:1:1--1:16
• Reason: It is not the case that 0 >= 1
[error] at <interactive>:1:1--1:18:
Unsolvable constraints:
• fin inf
• Unsolvable constraint:
fin inf
arising from
use of partial type function (%^)
at <interactive>:1:1--1:18
• Reason: Expected a finite type, but found `inf`.
[error] at <interactive>:1:1--1:18:
Unsolvable constraints:
• fin inf
• Unsolvable constraint:
fin inf
arising from
use of partial type function (%^)
at <interactive>:1:1--1:18
• Reason: Expected a finite type, but found `inf`.
[error] at <interactive>:1:1--1:16:
Unsolvable constraints:
• 0 >= 1
• Unsolvable constraint:
0 >= 1
arising from
use of partial type function (%^)
at <interactive>:1:1--1:16
• Reason: It is not the case that 0 >= 1
Loading module Cryptol
Loading module Main

10
tests/issues/issue835.icry.stdout
View File

@ -3,9 +3,7 @@ Loading module Cryptol
Loading module Float
[error] at <interactive>:1:1--1:28:
Unsolvable constraints:
• SignedCmp (Float 5 11)
arising from
use of expression (<$)
at <interactive>:1:1--1:28
• Reason: Type 'Float' does not support signed comparisons.
• Type `Float 5 11` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:28

50
tests/issues/issue845.icry.stdout
View File

@ -27,45 +27,35 @@ Loading module Main
(ratio 1 2)
[error] at <interactive>:1:1--1:9:
Unsolvable constraints:
• FLiteral 1 0 0 Rational
arising from
use of fractional literal
at <interactive>:1:1--1:9
• Reason: Fractions may not have 0 as the denominator.
• `1/0` is not a valid literal of type `Rational`
arising from
use of fractional literal
at <interactive>:1:1--1:9
[error] at <interactive>:1:1--1:9:
Unsolvable constraints:
• FLiteral inf 2 0 Rational
arising from
use of fractional literal
at <interactive>:1:1--1:9
• Reason: Fractions may not use `inf`
• `inf/2` is not a valid literal of type `Rational`
arising from
use of fractional literal
at <interactive>:1:1--1:9
Loading module Cryptol
Loading module Float
0x0.8
[error] at <interactive>:1:1--1:9:
Unsolvable constraints:
• FLiteral 1 0 0 Float64
arising from
use of fractional literal
at <interactive>:1:1--1:9
• Reason: Fractions may not have 0 as the denominator.
• `1/0` is not a valid literal of type `Float64`
arising from
use of fractional literal
at <interactive>:1:1--1:9
[error] at <interactive>:1:1--1:9:
Unsolvable constraints:
• FLiteral inf 2 0 Float64
arising from
use of fractional literal
at <interactive>:1:1--1:9
• Reason: Fractions may not use `inf`
• `inf/2` is not a valid literal of type `Float64`
arising from
use of fractional literal
at <interactive>:1:1--1:9
0x0.2
[error] at <interactive>:1:1--1:9:
Unsolvable constraints:
• FLiteral 1 10 1 (Float 3 2)
arising from
use of fractional literal
at <interactive>:1:1--1:9
• Reason: 1/10 cannot be represented in Float 3 2
• `1/10` is not a valid literal of type `Float 3 2`
arising from
use of fractional literal
at <interactive>:1:1--1:9

40
tests/issues/issue910.icry.stdout
View File

@ -1,29 +1,25 @@
Loading module Cryptol
[error] at <interactive>:1:1--1:21:
Unsolvable constraints:
• Integral ?a`778
arising from
use of expression (@)
at <interactive>:1:8--1:21
• Field ?a`778
arising from
use of expression (/.)
at <interactive>:1:14--1:20
• Reason: Mutually exclusive goals
• `?a` is not an integral type.
arising from
use of expression (@)
at <interactive>:1:8--1:21
• Type `?a` does not support field operations.
arising from
use of expression (/.)
at <interactive>:1:14--1:20
where
?a`778 is type argument 'a' of '(/.)' at <interactive>:1:14--1:20
?a is type argument 'a' of '(/.)' at <interactive>:1:14--1:20
[error] at <interactive>:1:1--1:16:
Unsolvable constraints:
• Integral ?a`776
arising from
use of expression (@)
at <interactive>:1:8--1:16
• FLiteral 6 5 0 ?a`776
arising from
use of fractional literal
at <interactive>:1:13--1:16
• Reason: Mutually exclusive goals
• `?a` is not an integral type.
arising from
use of expression (@)
at <interactive>:1:8--1:16
• `6/5` is not a valid literal of type `?a`
arising from
use of fractional literal
at <interactive>:1:13--1:16
where
?a`776 is type argument 'a' of 'fraction' at <interactive>:1:13--1:16
?a is type argument 'a' of 'fraction' at <interactive>:1:13--1:16

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

@ -5,9 +5,8 @@ False
number`{rep = Bit} : {n} (1 >= n) => Bit
[error] at <interactive>:1:1--1:2:
Unsolvable constraints:
• 1 >= 2
• Unsolvable constraint:
1 >= 2
arising from
use of literal or demoted expression
at <interactive>:1:1--1:2
• Reason: It is not the case that 1 >= 2

10
tests/mono-binds/test04.icry.stdout
View File

@ -18,9 +18,7 @@ Loading module Cryptol
Loading module test04
[error] at test04.cry:1:1--5:14:
Unsolvable constraints:
• Literal 10 ()
arising from
use of literal or demoted expression
at test04.cry:3:19--3:21
• Reason: Type '()' does not support integer literals.
• `10` is not a valid literal of type `()`
arising from
use of literal or demoted expression
at test04.cry:3:19--3:21

20
tests/regression/float.icry.stdout
View File

@ -71,24 +71,20 @@ IEEE-754 floating point numbers.
0x4.0p0
[error] at <interactive>:1:1--1:20:
Unsolvable constraints:
• FLiteral 5 1 1 Small
arising from
use of fractional literal
at <interactive>:1:1--1:6
• Reason: 5/1 cannot be represented in Float 3 2
• `5/1` is not a valid literal of type `Small`
arising from
use of fractional literal
at <interactive>:1:1--1:6
0x1.3p0
0x2.0p-4
0x2.0p-4
0x8.0p0
[error] at <interactive>:1:1--1:2:
Unsolvable constraints:
• Literal 7 Small
arising from
use of literal or demoted expression
at <interactive>:1:1--1:2
• Reason: 7 cannot be represented in Float 3 2
• `7` is not a valid literal of type `Small`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:2
"-- NaN------------------------------------------------------------------------"
fpNaN : {e, p} (ValidFloat e p) => Float e p

551
tests/regression/instance.icry.stdout
View File

@ -16,30 +16,24 @@ zero`{Float _ _} : {n, m} (ValidFloat n m) => Float n m
complement`{Bit} : Bit -> Bit
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic Integer
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Integer' does not support logical operations.
• Type `Integer` does not support logical operations.
arising from
use of expression complement
at <interactive>:1:1--1:11
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic Rational
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Rational' does not support logical operations.
• Type `Rational` does not support logical operations.
arising from
use of expression complement
at <interactive>:1:1--1:11
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic (Z ?n`1011)
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Z' does not support logical operations.
• Type `Z ?m` does not support logical operations.
arising from
use of expression complement
at <interactive>:1:1--1:11
where
?n`1011 is type wildcard (_) at <interactive>:1:15--1:16
?m is type wildcard (_) at <interactive>:1:15--1:16
complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a
complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b
complement`{()} : () -> ()
@ -49,23 +43,19 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) =>
{x : a, y : b} -> {x : a, y : b}
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic (Float ?n`1025 ?n`1026)
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Float' does not support logical operations.
• Type `Float ?m ?n` does not support logical operations.
arising from
use of expression complement
at <interactive>:1:1--1:11
where
?n`1025 is type wildcard (_) at <interactive>:1:19--1:20
?n`1026 is type wildcard (_) at <interactive>:1:21--1:22
?m is type wildcard (_) at <interactive>:1:19--1:20
?n is type wildcard (_) at <interactive>:1:21--1:22
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Ring Bit
arising from
use of expression negate
at <interactive>:1:1--1:7
• Reason: Type 'Bit' does not support ring operations.
• Type `Bit` does not support ring operations.
arising from
use of expression negate
at <interactive>:1:1--1:7
negate`{Integer} : Integer -> Integer
negate`{Rational} : Rational -> Rational
negate`{Z _} : {n} (n >= 1, fin n) => Z n -> Z n
@ -81,259 +71,207 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) =>
Float n m -> Float n m
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral Bit
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Bit' is not an integral type.
• `Bit` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
(%)`{Integer} : Integer -> Integer -> Integer
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral Rational
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Rational' is not an integral type.
• `Rational` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (Z ?n`1049)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Z ?n`1049' is not an integral type.
• `Z ?m` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
where
?n`1049 is type wildcard (_) at <interactive>:1:8--1:9
?m is type wildcard (_) at <interactive>:1:8--1:9
(%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (?a`1052 -> ?a`1053)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '?a`1052 -> ?a`1053' is not an integral type.
• `?a -> ?b` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
where
?a`1052 is type wildcard (_) at <interactive>:1:7--1:8
?a`1053 is type wildcard (_) at <interactive>:1:12--1:13
?a is type wildcard (_) at <interactive>:1:7--1:8
?b is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral ()
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '()' is not an integral type.
• `()` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (?a`1052, ?a`1053)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '(?a`1052, ?a`1053)' is not an integral type.
• `(?a, ?b)` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
where
?a`1052 is type wildcard (_) at <interactive>:1:7--1:8
?a`1053 is type wildcard (_) at <interactive>:1:10--1:11
?a is type wildcard (_) at <interactive>:1:7--1:8
?b is type wildcard (_) at <interactive>:1:10--1:11
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral {}
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '{}' is not an integral type.
• `{}` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral {x : ?a`1052, y : ?a`1053}
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '{x : ?a`1052, y : ?a`1053}' is not an integral type.
• `{x : ?a, y : ?b}` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
where
?a`1052 is type wildcard (_) at <interactive>:1:11--1:12
?a`1053 is type wildcard (_) at <interactive>:1:18--1:19
?a is type wildcard (_) at <interactive>:1:11--1:12
?b is type wildcard (_) at <interactive>:1:18--1:19
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (Float ?n`1052 ?n`1053)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Float ?n`1052 ?n`1053' is not an integral type.
• `Float ?m ?n` is not an integral type.
arising from
use of expression (%)
at <interactive>:1:1--1:4
where
?n`1052 is type wildcard (_) at <interactive>:1:12--1:13
?n`1053 is type wildcard (_) at <interactive>:1:14--1:15
?m is type wildcard (_) at <interactive>:1:12--1:13
?n is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field Bit
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Type 'Bit' does not support field operations.
• Type `Bit` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field Integer
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Type 'Integer' does not support field operations.
• Type `Integer` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
recip`{Rational} : Rational -> Rational
recip`{Z _} : {n} (prime n, n >= 1) => Z n -> Z n
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field ([?n`1055]?a`1056)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Sequence types do not support field operations.
• Type `[?m]?a` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
where
?n`1055 is type wildcard (_) at <interactive>:1:9--1:10
?a`1056 is type wildcard (_) at <interactive>:1:11--1:12
?m is type wildcard (_) at <interactive>:1:9--1:10
?a is type wildcard (_) at <interactive>:1:11--1:12
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field (?a`1055 -> ?a`1056)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Function types do not support field operations.
• Type `?a -> ?b` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
where
?a`1055 is type wildcard (_) at <interactive>:1:9--1:10
?a`1056 is type wildcard (_) at <interactive>:1:14--1:15
?a is type wildcard (_) at <interactive>:1:9--1:10
?b is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field ()
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Tuple types do not support field operations.
• Type `()` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field (?a`1055, ?a`1056)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Tuple types do not support field operations.
• Type `(?a, ?b)` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
where
?a`1055 is type wildcard (_) at <interactive>:1:9--1:10
?a`1056 is type wildcard (_) at <interactive>:1:12--1:13
?a is type wildcard (_) at <interactive>:1:9--1:10
?b is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field {}
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Record types do not support field operations.
• Type `{}` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field {x : ?a`1055, y : ?a`1056}
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Record types do not support field operations.
• Type `{x : ?a, y : ?b}` does not support field operations.
arising from
use of expression recip
at <interactive>:1:1--1:6
where
?a`1055 is type wildcard (_) at <interactive>:1:13--1:14
?a`1056 is type wildcard (_) at <interactive>:1:20--1:21
?a is type wildcard (_) at <interactive>:1:13--1:14
?b is type wildcard (_) at <interactive>:1:20--1:21
recip`{Float _ _} : {n, m} (ValidFloat n m) =>
Float n m -> Float n m
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round Bit
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Type 'Bit' does not support rounding operations.
• Type `Bit` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round Integer
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Type 'Integer' does not support rounding operations.
• Type `Integer` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
floor`{Rational} : Rational -> Integer
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (Z ?n`1059)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Type 'Z' does not support rounding operations.
• Type `Z ?m` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
where
?n`1059 is type wildcard (_) at <interactive>:1:10--1:11
?m is type wildcard (_) at <interactive>:1:10--1:11
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round ([?n`1059]?a`1060)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Sequence types do not support rounding operations.
• Type `[?m]?a` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
where
?n`1059 is type wildcard (_) at <interactive>:1:9--1:10
?a`1060 is type wildcard (_) at <interactive>:1:11--1:12
?m is type wildcard (_) at <interactive>:1:9--1:10
?a is type wildcard (_) at <interactive>:1:11--1:12
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (?a`1059 -> ?a`1060)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Function types do not support rounding operations.
• Type `?a -> ?b` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
where
?a`1059 is type wildcard (_) at <interactive>:1:9--1:10
?a`1060 is type wildcard (_) at <interactive>:1:14--1:15
?a is type wildcard (_) at <interactive>:1:9--1:10
?b is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round ()
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Tuple types do not support rounding operations.
• Type `()` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (?a`1059, ?a`1060)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Tuple types do not support rounding operations.
• Type `(?a, ?b)` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
where
?a`1059 is type wildcard (_) at <interactive>:1:9--1:10
?a`1060 is type wildcard (_) at <interactive>:1:12--1:13
?a is type wildcard (_) at <interactive>:1:9--1:10
?b is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round {}
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Record types do not support rounding operations.
• Type `{}` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round {x : ?a`1059, y : ?a`1060}
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Record types do not support rounding operations.
• Type `{x : ?a, y : ?b}` does not support rounding operations.
arising from
use of expression floor
at <interactive>:1:1--1:6
where
?a`1059 is type wildcard (_) at <interactive>:1:13--1:14
?a`1060 is type wildcard (_) at <interactive>:1:20--1:21
?a is type wildcard (_) at <interactive>:1:13--1:14
?b is type wildcard (_) at <interactive>:1:20--1:21
floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
(==)`{Bit} : Bit -> Bit -> Bit
(==)`{Integer} : Integer -> Integer -> Bit
@ -342,15 +280,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
(==)`{[_]_} : {n, a} (Eq a, fin n) => [n]a -> [n]a -> Bit
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• Eq (?a`1070 -> ?a`1071)
arising from
use of expression (==)
at <interactive>:1:1--1:5
• Reason: Function types do not support comparisons.
• Type `?a -> ?b` does not support equality.
arising from
use of expression (==)
at <interactive>:1:1--1:5
where
?a`1070 is type wildcard (_) at <interactive>:1:8--1:9
?a`1071 is type wildcard (_) at <interactive>:1:13--1:14
?a is type wildcard (_) at <interactive>:1:8--1:9
?b is type wildcard (_) at <interactive>:1:13--1:14
(==)`{()} : () -> () -> Bit
(==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit
(==)`{{}} : {} -> {} -> Bit
@ -363,26 +299,22 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
(<)`{Rational} : Rational -> Rational -> Bit
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Cmp (Z ?n`1084)
arising from
use of expression (<)
at <interactive>:1:1--1:4
• Reason: Type 'Z' does not support order comparisons.
• Type `Z ?m` does not support comparisons.
arising from
use of expression (<)
at <interactive>:1:1--1:4
where
?n`1084 is type wildcard (_) at <interactive>:1:8--1:9
?m is type wildcard (_) at <interactive>:1:8--1:9
(<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Cmp (?a`1087 -> ?a`1088)
arising from
use of expression (<)
at <interactive>:1:1--1:4
• Reason: Function types do not support order comparisons.
• Type `?a -> ?b` does not support comparisons.
arising from
use of expression (<)
at <interactive>:1:1--1:4
where
?a`1087 is type wildcard (_) at <interactive>:1:7--1:8
?a`1088 is type wildcard (_) at <interactive>:1:12--1:13
?a is type wildcard (_) at <interactive>:1:7--1:8
?b is type wildcard (_) at <interactive>:1:12--1:13
(<)`{()} : () -> () -> Bit
(<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit
(<)`{{}} : {} -> {} -> Bit
@ -392,50 +324,40 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
Float n m -> Float n m -> Bit
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp Bit
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Bit' does not support signed comparisons.
• Type `Bit` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp Integer
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Integer' does not support signed comparisons.
• Type `Integer` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp Rational
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Rational' does not support signed comparisons.
• Type `Rational` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (Z ?n`1098)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Z' does not support signed comparisons.
• Type `Z ?m` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
where
?n`1098 is type wildcard (_) at <interactive>:1:9--1:10
?m is type wildcard (_) at <interactive>:1:9--1:10
(<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (?a`1101 -> ?a`1102)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Function types do not support signed comparisons.
• Type `?a -> ?b` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
where
?a`1101 is type wildcard (_) at <interactive>:1:8--1:9
?a`1102 is type wildcard (_) at <interactive>:1:13--1:14
?a is type wildcard (_) at <interactive>:1:8--1:9
?b is type wildcard (_) at <interactive>:1:13--1:14
(<$)`{()} : () -> () -> Bit
(<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) =>
(a, b) -> (a, b) -> Bit
@ -444,15 +366,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
{x : a, y : b} -> {x : a, y : b} -> Bit
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (Float ?n`1109 ?n`1110)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Float' does not support signed comparisons.
• Type `Float ?m ?n` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:5
where
?n`1109 is type wildcard (_) at <interactive>:1:13--1:14
?n`1110 is type wildcard (_) at <interactive>:1:15--1:16
?m is type wildcard (_) at <interactive>:1:13--1:14
?n is type wildcard (_) at <interactive>:1:15--1:16
number`{rep = Bit} : {n} (1 >= n) => Bit
[error] at <interactive>:1:1--1:7:
@ -465,61 +385,50 @@ number`{rep = Z _} : {n, m} (m >= 1 + n, m >= 1, fin m, fin n) =>
number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m]
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1118 (?a`1119 -> ?a`1120)
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '?a`1119 -> ?a`1120' does not support integer literals.
• `?m` is not a valid literal of type `?a -> ?b`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
where
?val`1118 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1119 is type wildcard (_) at <interactive>:1:15--1:16
?a`1120 is type wildcard (_) at <interactive>:1:20--1:21
?m is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a is type wildcard (_) at <interactive>:1:15--1:16
?b is type wildcard (_) at <interactive>:1:20--1:21
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1118 ()
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '()' does not support integer literals.
• `?m` is not a valid literal of type `()`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
where
?val`1118 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?m is type argument 'val' of 'number' at <interactive>:1:1--1:7
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1118 (?a`1119, ?a`1120)
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '(?a`1119, ?a`1120)' does not support integer literals.
• `?m` is not a valid literal of type `(?a, ?b)`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
where
?val`1118 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1119 is type wildcard (_) at <interactive>:1:16--1:17
?a`1120 is type wildcard (_) at <interactive>:1:19--1:20
?m is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a is type wildcard (_) at <interactive>:1:16--1:17
?b is type wildcard (_) at <interactive>:1:19--1:20
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1118 {}
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '{}' does not support integer literals.
• `?m` is not a valid literal of type `{}`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
where
?val`1118 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?m is type argument 'val' of 'number' at <interactive>:1:1--1:7
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1118 {x : ?a`1119, y : ?a`1120}
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '{x : ?a`1119,
y : ?a`1120}' does not support integer literals.
• `?m` is not a valid literal of type `{x : ?a, y : ?b}`
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
where
?val`1118 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1119 is type wildcard (_) at <interactive>:1:20--1:21
?a`1120 is type wildcard (_) at <interactive>:1:27--1:28
?m is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a is type wildcard (_) at <interactive>:1:20--1:21
?b is type wildcard (_) at <interactive>:1:27--1:28
number`{rep = Float _ _} : {n, m, i} (ValidFloat m i,
Literal n (Float m i)) =>
Float m i

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

@ -49,20 +49,18 @@ Expected test coverage: 0.00% (100 of 2^^1042 values)
1
[error] at <interactive>:1:1--1:8:
Unsolvable constraints:
• prime 8
• Unsolvable constraint:
prime 8
arising from
use of expression z1prime
at <interactive>:1:1--1:8
• Reason: 8 is not a prime number
[error] at <interactive>:1:1--1:8:
Unsolvable constraints:
• prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129
• Unsolvable constraint:
prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129
arising from
use of expression z1prime
at <interactive>:1:1--1:8
• Reason: 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 is not a prime number
Q.E.D.
Q.E.D.
Q.E.D.

21
tests/regression/tc-errors.icry.stdout
View File

@ -16,20 +16,19 @@ Loading module Cryptol
[error] at <interactive>:1:9--1:10:
Matching would result in an infinite type.
The type: ?arg`771
occurs in: ?arg`771 -> ?res
The type: ?b
occurs in: ?b -> ?a
When checking type of function argument
where
?res is type of function result at <interactive>:1:1--1:10
?arg`771 is type of function argument at <interactive>:1:7--1:10
?a is type of function result at <interactive>:1:1--1:10
?b is type of function argument at <interactive>:1:7--1:10
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• fin inf
• Unsolvable constraint:
fin inf
arising from
use of expression take
at <interactive>:1:1--1:5
• Reason: Expected a finite type, but found `inf`.
Parse error at <interactive>:1:8,
unexpected: ,
@ -85,18 +84,18 @@ Loading module Main
[error] at tc-errors-5.cry:2:5--2:7:
Inferred type is not sufficiently polymorphic.
Quantified variable: a`767
cannot match type: [0]?a`769
cannot match type: [0]?a
When checking the type of 'Main::f'
where
?a`769 is type of sequence member at tc-errors-5.cry:2:5--2:7
?a is type of sequence member at tc-errors-5.cry:2:5--2:7
a`767 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 ?x`770 is not sufficiently polymorphic.
The type ?a is not sufficiently polymorphic.
It cannot depend on quantified variables: b`771
When checking the type of 'Main::g'
where
?x`770 is the type of 'x' at tc-errors-6.cry:1:3--1:4
?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
b`771 is signature variable 'b' at tc-errors-6.cry:3:8--3:9