1 files changed, 27 insertions, 9 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c328f7b7..b3994f40 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -604,7 +604,7 @@ namespace Microsoft.Dafny {
       return "int";

     }

     public override bool Equals(Type that) {

-      return that.NormalizeExpand() is IntType;

+      return that.IsIntegerType;

     }

   }

 

@@ -622,7 +622,7 @@ namespace Microsoft.Dafny {
       return "real";

     }

     public override bool Equals(Type that) {

-      return that.NormalizeExpand() is RealType;

+      return that.IsRealType;

     }

   }

 

@@ -4745,7 +4745,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateAdd(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));

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

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

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

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

@@ -4754,15 +4754,33 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Create a resolved expression of the form "e0 - e1"

+    /// Create a resolved expression of the form "CVT(e0) - CVT(e1)", where "CVT" is either "int" (if

+    /// e0.Type is an integer-based numeric type) or "real" (if e0.Type is a real-based numeric type).

     /// </summary>

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

+    public static Expression CreateSubtract_TypeConvert(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != 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);

+

+      Type toType = e0.Type.IsNumericBased(Type.NumericPersuation.Int) ? (Type)Type.Int : Type.Real;

+      e0 = new ConversionExpr(e0.tok, e0, toType);

+      e0.Type = toType;

+      e1 = new ConversionExpr(e1.tok, e1, toType);

+      e1.Type = toType;

+      return CreateSubtract(e0, e1);

+    }

+

+    /// <summary>

+    /// Create a resolved expression of the form "e0 - e1"

+    /// </summary>

+    public static Expression CreateSubtract(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.Ensures(Contract.Result<Expression>() != null);

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

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

       s.Type = e0.Type;  // resolve here

@@ -4774,7 +4792,7 @@ namespace Microsoft.Dafny {
     /// </summary>

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

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.NormalizeExpand() is IntType);

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

       Contract.Requires(0 <= n);

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

       if (n == 0) {

@@ -4789,7 +4807,7 @@ namespace Microsoft.Dafny {
     /// </summary>

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

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.NormalizeExpand() is IntType);

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

       Contract.Requires(0 <= n);

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

       if (n == 0) {

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

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType);

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

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

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

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

@@ -4862,7 +4880,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateAtMost(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));

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

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

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

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