Start of derived types (aka "new types")

Fixed bug in type checking for integer division.

1 files changed, 8 insertions, 7 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index ac44375d..b6ebe5dc 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -60,12 +60,12 @@ ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: Bad
 ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List

 ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)

 ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-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(1000,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> A

+ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (derived types, 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(1019,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

+ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A

 ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x

 ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P

 ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)

@@ -142,7 +142,7 @@ ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specificat
 ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool)

+ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)

 ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)

 ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)

@@ -175,4 +175,5 @@ ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from
 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)

 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

-177 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

+178 resolution/type errors detected in ResolutionErrors.dfy