Refactored ArrowType's to be resolved with other types. ArrowTypeDecl's are now created by the parser into the system module.

5 files changed, 39 insertions, 47 deletions

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 1a06d8f2..e50dc797 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -8,13 +8,10 @@ Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass
 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

 Modules0.dfy(76,6): Error: expected method call, found expression

 Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

 Modules0.dfy(79,6): Error: expected method call, found expression

 Modules0.dfy(84,8): Error: type MyClassY does not have a member M

-Modules0.dfy(84,8): Error: type MyClassY does not have a member M

 Modules0.dfy(84,6): Error: expected method call, found expression

 Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

 Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

@@ -22,24 +19,19 @@ Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
 Modules0.dfy(233,13): Error: Undeclared type X in module B

 Modules0.dfy(243,13): Error: unresolved identifier: X

 Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X

 Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

 Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)

 Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(287,6): Error: expected method call, found expression

 Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(288,6): Error: expected method call, found expression

 Modules0.dfy(310,24): Error: module Q_Imp does not exist

 Modules0.dfy(102,6): Error: type MyClassY does not have a member M

-Modules0.dfy(102,6): Error: type MyClassY does not have a member M

 Modules0.dfy(102,4): Error: expected method call, found expression

 Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts

 Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts

 Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts

 Modules0.dfy(143,11): Error: unresolved identifier: allocated

 Modules0.dfy(146,19): Error: unresolved identifier: allocated

-44 resolution/type errors detected in Modules0.dfy

+36 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 0161a713..2678e526 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -1,22 +1,22 @@
-DerivedTypes.dfy(74,11): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)

+Newtypes.dfy(74,11): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)

 Execution trace:

     (0,0): anon0

-DerivedTypes.dfy(76,45): Error: possible division by zero

+Newtypes.dfy(76,45): Error: possible division by zero

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-DerivedTypes.dfy(87,14): Error: result of operation might violate newtype constraint

+Newtypes.dfy(87,14): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

-DerivedTypes.dfy(95,12): Error: result of operation might violate newtype constraint

+Newtypes.dfy(95,12): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-DerivedTypes.dfy(97,14): Error: result of operation might violate newtype constraint

+Newtypes.dfy(97,14): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-DerivedTypes.dfy(104,16): Error: result of operation might violate newtype constraint

+Newtypes.dfy(104,16): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect
index 091ca523..81c43d35 100644
--- a/Test/dafny0/NewtypesResolution.dfy.expect
+++ b/Test/dafny0/NewtypesResolution.dfy.expect
@@ -1,25 +1,25 @@
-DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

-DerivedTypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)

-DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

-DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

-DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

-DerivedTypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)

-DerivedTypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)

-DerivedTypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)

-DerivedTypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)

-DerivedTypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)

-DerivedTypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)

-DerivedTypesResolution.dfy(77,10): Error: unresolved identifier: a

-DerivedTypesResolution.dfy(91,31): Error: old expressions are not allowed in this context

-DerivedTypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

-DerivedTypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

-DerivedTypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

-DerivedTypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

-DerivedTypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

-DerivedTypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

-DerivedTypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

-DerivedTypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

-DerivedTypesResolution.dfy(162,8): Error: member U does not exist in class Klass

-DerivedTypesResolution.dfy(162,4): Error: expected method call, found expression

-DerivedTypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

-24 resolution/type errors detected in DerivedTypesResolution.dfy

+NewtypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

+NewtypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)

+NewtypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

+NewtypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

+NewtypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

+NewtypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)

+NewtypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)

+NewtypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)

+NewtypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)

+NewtypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)

+NewtypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)

+NewtypesResolution.dfy(77,10): Error: unresolved identifier: a

+NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this context

+NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

+NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

+NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

+NewtypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

+NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

+NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

+NewtypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

+NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

+NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass

+NewtypesResolution.dfy(162,4): Error: expected method call, found expression

+NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

+24 resolution/type errors detected in NewtypesResolution.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index cf1810e6..3f08e72a 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 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(1000,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A

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

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

+ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, 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?)

diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index 0cb9413c..994d78f2 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -2,8 +2,8 @@ ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand
 ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

 ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field

 ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)

-ResolveError.dfy(32,12): Error: cannot apply arguments with types int,int to expression with type int -> int

-ResolveError.dfy(33,12): Error: cannot apply arguments with types bool to expression with type int -> int

+ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)

+ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)

 ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)

 ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)

 ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)