Changed syntax of newtype

4 files changed, 72 insertions, 31 deletions

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index 09e43d32..77fbe75d 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -46,38 +46,38 @@ method M()
 }

 

 module Constraints {

-  newtype SmallInt = x: int where 0 <= x < 100

-  newtype LargeInt = y: int where 0 <= y < 100

+  newtype SmallInt = x: int | 0 <= x < 100

+  newtype LargeInt = y: int | 0 <= y < 100

 

-  newtype A = x: int where 0 <= x

-  newtype B = x: A where x < 100

+  newtype A = x: int | 0 <= x

+  newtype B = x: A | x < 100

   newtype C = B  // the constraints 0 <= x < 100 still apply

 

   static predicate IsEven(x: int)  // note that this is a ghost predicate

   {

     x % 2 == 0

   }

-  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

+  newtype G = x: int | IsEven(x)  // it's okay to use ghost constructs in type constraints

 

   newtype N = nat

 

-  newtype AssertType = s: int where

+  newtype AssertType = s: int |

     var k := s;

     assert k <= s;

     k < 10 || 10 <= s

 

-  newtype Te = x: int where 0 <= x < 3 && [5, 7, 8][x] % 2 != 0

+  newtype Te = x: int | 0 <= x < 3 && [5, 7, 8][x] % 2 != 0

 

-  newtype Ta = x: int where 0 <= x < 3

-  newtype Tb = y: Ta where [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

+  newtype Ta = x: int | 0 <= x < 3

+  newtype Tb = y: Ta | [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

 

-  newtype Odds = x: int where x % 2 == 1  // error: cannot find witness

+  newtype Odds = x: int | x % 2 == 1  // error: cannot find witness

 

-  newtype K = x: real where 10.0 <= x ==> 200.0 / (x - 20.0) < 30.0  // error: division by zero

+  newtype K = x: real | 10.0 <= x ==> 200.0 / (x - 20.0) < 30.0  // error: division by zero

 }

 

 module PredicateTests {

-  newtype char8 = x: int where 0 <= x < 256

+  newtype char8 = x: int | 0 <= x < 256

 

   method M() {

     var u: char8 := 85;

@@ -138,3 +138,20 @@ module DatatypeCtorResolution {
     q := Pair.Pair(10, 20);

   }

 }

+

+module X {

+  newtype Int = x | 0 <= x < 100

+  newtype Real = r | 0.0 <= r <= 100.0

+

+  method M() returns (i: Int, r: Real)

+  {

+    i := 4;

+    r := 4.0;

+  }

+

+  method N()

+  {

+    var x := var i := 3; i;

+    var y := var j := 3.0; j;

+  }

+}

diff --git a/Test/dafny0/DerivedTypes.dfy.expect b/Test/dafny0/DerivedTypes.dfy.expect
index 41c21410..0161a713 100644
--- a/Test/dafny0/DerivedTypes.dfy.expect
+++ b/Test/dafny0/DerivedTypes.dfy.expect
@@ -1,7 +1,7 @@
 DerivedTypes.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,49): Error: possible division by zero

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

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -20,4 +20,4 @@ DerivedTypes.dfy(104,16): Error: result of operation might violate newtype const
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 24 verified, 6 errors

+Dafny program verifier finished with 30 verified, 6 errors

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index b1407f10..51f42994 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -54,7 +54,7 @@ module Goodies {
 

     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

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

     z, x := di, dr;

 

     var sq := [23, 50];

@@ -68,38 +68,41 @@ module Goodies {
 }

 

 module Constraints {

-  newtype SmallInt = x: int where 0 <= x < 100

-  newtype LargeInt = y: int where 0 <= y < 100

+  newtype SmallInt = x: int | 0 <= x < 100

+  newtype LargeInt = y: int | 0 <= y < 100

 

   newtype BadConstraint = a: SmallInt

-    where a + a  // error: not a boolean

+    | a + a  // error: not a boolean

   newtype WotsDisVariable = u  :BadConstraint

-    where u + a < 50  // error: undeclared identifier 'a'

+    | u + a < 50  // error: undeclared identifier 'a'

 

-  newtype A = x: int where 0 <= x

-  newtype B = x: A where x < 100

+  newtype A = x: int | 0 <= x

+  newtype B = x: A | x < 100

   newtype C = B  // the constraints 0 <= x < 100 still apply

 

   static predicate IsEven(x: int)  // note that this is a ghost predicate

   {

     x % 2 == 0

   }

-  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

+  newtype G = x: int | IsEven(x)  // it's okay to use ghost constructs in type constraints

 

   newtype N = nat

 

-  newtype OldState = y: real where old(y) == y  // error: old is not allowed in constraint

+  newtype OldState = y: real | old(y) == y  // error: old is not allowed in constraint

 

-  newtype AssertType = s: int where

+  newtype AssertType = s: int |

     var k := s;

     assert k == s;

     k < 10 || 10 <= s

+}

 

+module WrongNumberOfArguments {

+  newtype N = nat

   method BadTypeArgs(n: N<int>)  // error: N takes no type arguments

 }

 

 module CyclicDependencies {

-  newtype Cycle = x: int where (BadLemma(); false)  // error: cycle

+  newtype Cycle = x: int | (BadLemma(); false)  // error: cycle

   static lemma BadLemma()

     ensures false;

   {

@@ -108,7 +111,7 @@ module CyclicDependencies {
 }

 

 module SelfCycleTest {

-  newtype SelfCycle = x: int where var s: SelfCycle := 4; s < 10  // error: cyclic dependency on itself

+  newtype SelfCycle = x: int | var s: SelfCycle := 4; s < 10  // error: cyclic dependency on itself

 }

 

 module Module0 {

@@ -121,3 +124,19 @@ module Module0 {
 module Module1 {

   newtype N9 = int

 }

+

+module InferredType {

+  newtype Int = x | 0 <= x < 100

+  newtype Real = r | 0.0 <= r <= 100.0

+  method M() returns (i: Int, r: Real)

+  {

+    i := 4;

+    r := 4.0;

+  }

+  newtype AnotherInt = int

+  method P(i: int, a: AnotherInt) returns (j: Int)

+  {

+    j := i;  // error: int not assignable to Int

+    j := a;  // error: AnotherInt not assignable to Int

+  }

+}

diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 2f5682ac..1746b37e 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -8,8 +8,13 @@ DerivedTypesResolution.dfy(52,13): Error: arguments to < must have the same type
 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(98,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

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

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

-DerivedTypesResolution.dfy(117,21): Error: unresolved identifier: N9

-14 resolution/type errors detected in DerivedTypesResolution.dfy

+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: unresolved identifier: N9

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

+19 resolution/type errors detected in DerivedTypesResolution.dfy