fixed bugs related to identifying newtypes as types of integers and reals.

2 files changed, 46 insertions, 35 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 600f7473..116b9004 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5223,7 +5223,9 @@ namespace Microsoft.Dafny {
     public static Expression CreateAdd(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

       Contract.Ensures(Contract.Result<Expression>() != null);

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;  // resolve here

@@ -5265,8 +5267,12 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateSubtract(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

+      Contract.Requires(e0.Type != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(e1.Type != null);

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

       Contract.Ensures(Contract.Result<Expression>() != null);

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here

@@ -5279,7 +5285,8 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateIncrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.IsIntegerType);

+      Contract.Requires(e.Type != null);

+      Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int));

       Contract.Requires(0 <= n);

       Contract.Ensures(Contract.Result<Expression>() != null);

       if (n == 0) {

@@ -5294,7 +5301,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateDecrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.IsIntegerType);

+      Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int));

       Contract.Requires(0 <= n);

       Contract.Ensures(Contract.Result<Expression>() != null);

       if (n == 0) {

@@ -5353,7 +5360,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateLess(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type.IsIntegerType && e1.Type.IsIntegerType);

+      Contract.Requires(e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int));

       Contract.Ensures(Contract.Result<Expression>() != null);

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt;  // resolve here

@@ -5367,7 +5374,9 @@ namespace Microsoft.Dafny {
     public static Expression CreateAtMost(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

       Contract.Ensures(Contract.Result<Expression>() != null);

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a2ae401a..210cd4ac 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7305,41 +7305,43 @@ namespace Microsoft.Dafny
             }

             eIter = ei.Seq;

           }

-          var e0 = eIter;

-

-          // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"

-          // Wrapping it in a let expr avoids exponential growth in the size of the expression

-          // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to

-          //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"

-

-          // Create a unique name for d', the variable we introduce in the let expression

-          string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);

-          IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName);

-          BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type);

-

-          // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

-          List<Expression> ctor_args = new List<Expression>();

-          foreach (Formal d in ctor.Formals) {

-            Expression v = null;

-            foreach (var dvPair in IndexToValue.Values) {

-              var destructor = dvPair.Item1;

-              if (d == destructor.CorrespondingFormal) {

-                Contract.Assert(v == null);

-                v = dvPair.Item2;

+          if (ctor != null) {

+            var e0 = eIter;

+

+            // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"

+            // Wrapping it in a let expr avoids exponential growth in the size of the expression

+            // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to

+            //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"

+

+            // Create a unique name for d', the variable we introduce in the let expression

+            string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);

+            IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName);

+            BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type);

+

+            // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

+            List<Expression> ctor_args = new List<Expression>();

+            foreach (Formal d in ctor.Formals) {

+              Expression v = null;

+              foreach (var dvPair in IndexToValue.Values) {

+                var destructor = dvPair.Item1;

+                if (d == destructor.CorrespondingFormal) {

+                  Contract.Assert(v == null);

+                  v = dvPair.Item2;

+                }

               }

+              ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null));

             }

-            ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null));

-          }

 

-          DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

+            DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

 

-          CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv);

-          LetExpr let = new LetExpr(e0.tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { e0 }, ctor_call, true);

+            CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv);

+            LetExpr let = new LetExpr(e0.tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { e0 }, ctor_call, true);

 

-          ResolveExpression(let, opts);

-          e.ResolvedUpdateExpr = let;

+            ResolveExpression(let, opts);

+            e.ResolvedUpdateExpr = let;

 

-          expr.Type = e0.Type;

+            expr.Type = e0.Type;

+          }

         } else {

           reporter.Error(MessageSource.Resolver, expr, "update requires a sequence, map, or datatype (got {0})", e.Seq.Type);

         }