Support for non-constrained derived types ("new types").

Arbitrary conversion from int/real to derived types not yet supported.
Changed rules about numeric type conversions to allow conversions from any numeric type.

9 files changed, 104 insertions, 20 deletions

diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 140aa890..196b3faa 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -19,6 +19,6 @@ CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only
 CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not determined

-CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not determined

+CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined

+CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined

 23 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
new file mode 100644
index 00000000..7a2249da
--- /dev/null
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -0,0 +1,38 @@
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+type int32 = new int

+type posReal = new real

+type int8 = new int32

+

+method M()

+{

+  var k8 := new int8[100];

+  var s: set<int32>;

+  var x: posReal;

+  var y: posReal;

+  var z: int32;

+  x := 5.3;

+  z := 12;

+  s := {};

+  s := {40,20};

+  x := x + y;

+  var r0 := real(x);

+  var r1: real := 2.0 * r0;

+  var i0 := int(z);

+  var i1: nat := 2 * i0;

+  assert i1 == 24;

+  assert y == 0.0 ==> r1 == 10.6;

+

+  assert real(x) == r0;

+  assert 2.0 * real(x) == real(2.0 * x);

+

+  assert real(int(z)) == real(i0);

+  assert 2 * int(z) == int(2 * z);

+

+  var di: int32 := z / 2 + 24 / z;

+  assert di == 8;

+  y := 60.0;

+  var dr: posReal := y / 2.0 + 120.0 / y;

+  assert dr == 32.0;

+}

diff --git a/Test/dafny0/DerivedTypes.dfy.expect b/Test/dafny0/DerivedTypes.dfy.expect
new file mode 100644
index 00000000..33214760
--- /dev/null
+++ b/Test/dafny0/DerivedTypes.dfy.expect
@@ -0,0 +1,3 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Compiled assembly into DerivedTypes.dll

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index 0c242db9..336a087a 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -23,5 +23,43 @@ module Goodies {
     var s: set<int32>;

     var x: posReal;

     var y: posReal;

+    var z: int32;

+    x := 5.3;

+    z := 12;

+    s := {};

+    s := {40,20};

+    x := x + y;

+    var r0 := real(x);

+    var r1: real := 2.0 * r0;

+    var i0 := int(z);

+    var i1: nat := 2 * i0;

+    assert i1 == 24;

+    assert r1 == 10.6;

+    if x == r0 {  // error: cannot compare posReal and real

+    } else if real(x) == r0 {

+    } else if i0 == int(x) {

+    } else if i0 == int(real(x)) {

+    } else if real(i0) == real(x) {

+    }

+    if z == i0 {  // error: cannot compare int32 and int

+    } else if int(z) == i0 {

+    } else if r0 == real(z) {

+    } else if r0 == real(int(z)) {

+    } else if int(r0) == int(z) {

+    }

+    assert x == z;  // error: cannot compare posReal and int32

+    assert x <= z;  // error: cannot compare posReal and int32

+    assert z < i0;  // error: cannot compare int32 and int

+    assert x > r1;  // error: cannot compare posReal and real

+

+    var di := z % 2 - z / 2 + if z == 0 then 3 else 100 / z + 100 % z;

+    var dr := x / 2.0 + if x == 0.0 then 3.0 else 100.0 / x;

+    dr := dr % 3.0 + 3.0 % dr;  // error: mod not supported for real-based types

+    z, x := di, dr;

+

+    var sq := [23, 50];

+    assert forall ii :: 0 <= ii < |sq| ==> sq[ii] == sq[ii];

+    var ms := multiset{23.0, 50.0};

+    assert forall rr :: 0.0 <= rr < 100.0  ==> ms[rr] == ms[rr];

   }

 }

diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 09b41101..4f86c813 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -1,3 +1,11 @@
 DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (derived types, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

 DerivedTypesResolution.dfy(12,7): Error: derived types must be based on some numeric type (got List<int>)

-2 resolution/type errors detected in DerivedTypesResolution.dfy

+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)

+10 resolution/type errors detected in DerivedTypesResolution.dfy

diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy.expect b/Test/dafny0/OpaqueFunctionsFail.dfy.expect
index 8c2638c3..a893c35e 100644
--- a/Test/dafny0/OpaqueFunctionsFail.dfy.expect
+++ b/Test/dafny0/OpaqueFunctionsFail.dfy.expect
@@ -1,4 +1,4 @@
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called.
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not determined
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called.
-3 resolution/type errors detected in OpaqueFunctionsFail.dfy
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.

+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not be determined

+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.

+3 resolution/type errors detected in OpaqueFunctionsFail.dfy

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 3c9156dd..38f2f9c2 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -957,9 +957,9 @@ method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real
 

   s := (2.0 / 1.7) + (r / s) - (--r) * -12.3;

 

-  s := real(s);  // error: cannot convert real->real

-  j := int(j);  // error: cannot convert int->int

-  j := int(n);  // error: cannot convert nat->int

+  s := real(s);  // fine (identity transform)

+  j := int(j);  // fine (identity transform)

+  j := int(n);  // fine (identity transform)

 }

 

 // --- filling in type arguments and checking that there aren't too many ---

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 4827dc07..cf1810e6 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -2,8 +2,8 @@ ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

-ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not determined

-ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not determined

+ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined

 ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements

@@ -171,11 +171,8 @@ ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#
 ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))

 ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)

 ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)

-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)

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

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

 ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-180 resolution/type errors detected in ResolutionErrors.dfy

+177 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect
index dfb4e978..04394d78 100644
--- a/Test/hofs/Underspecified.dfy.expect
+++ b/Test/hofs/Underspecified.dfy.expect
@@ -1,5 +1,5 @@
-Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not determined; please specify the type explicitly

-Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not determined; please specify the type explicitly

-Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not determined; please specify the type explicitly

-Underspecified.dfy(8,11): Error: type of bound variable 'a' could not determined; please specify the type explicitly

+Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly

+Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly

+Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly

+Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly

 4 resolution/type errors detected in Underspecified.dfy