From ae578ae92040975fed005d045110679e4e858c31 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 2 Aug 2014 01:05:17 -0700 Subject: Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator --- Test/dafny0/EqualityTypes.dfy.expect | 2 +- Test/dafny0/ResolutionErrors.dfy | 8 ++++---- Test/dafny0/ResolutionErrors.dfy.expect | 3 ++- Test/dafny0/TypeSynonyms.dfy | 7 +++++++ Test/dafny0/TypeSynonyms.dfy.expect | 2 +- Test/dafny0/TypeTests.dfy.expect | 4 ++-- 6 files changed, 17 insertions(+), 9 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index 410e4507..70e46ff0 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) -EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) +EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D) diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 520b2e38..aaf1291c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1007,20 +1007,20 @@ module CycleError2 { type A = B // error: cycle: A -> B -> A type B = set } -module Good0 { +module CycleErrors3 { type A = (B, D) type B = C class C { var a: A; // this is fine } - datatype D = Make(A, B, C) // this is fine, too + datatype D = Make(A, B, C) // error: cannot construct a D } -module CycleError3 { +module CycleError4 { type A = B // error: cycle: A -> B -> A type B = C class C { } } -module CycleError4 { +module CycleError5 { type A = B // error: cycle: A -> B -> A type B = Dt datatype Dt = Make(T) diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 49cfe650..d5d12eb9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -63,6 +63,7 @@ ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x @@ -171,4 +172,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real) ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int) ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat) -173 resolution/type errors detected in ResolutionErrors.dfy +174 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy index 4bec5253..85beb340 100644 --- a/Test/dafny0/TypeSynonyms.dfy +++ b/Test/dafny0/TypeSynonyms.dfy @@ -44,3 +44,10 @@ function Skip(s: Synonym3): Synonym0 case Nil => Nil case Cons(_, tail) => tail } + +type MyMap = map> + +predicate MyMapProperty(m: MyMap, x: int) +{ + x in m && real(x) in m[x] && m[x][real(x)] +} diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect index 4ef2de53..76f19e0d 100644 --- a/Test/dafny0/TypeSynonyms.dfy.expect +++ b/Test/dafny0/TypeSynonyms.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 6 verified, 0 errors +Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 62e41019..5d78fe16 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -25,8 +25,8 @@ TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement) TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type +TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type +TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context -- cgit v1.2.3