Dafny: Allow < and > for comparisons of datatype values (which then compares their ranks)

3 files changed, 93 insertions, 33 deletions

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index cea08862..ef047c4d 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -288,17 +288,24 @@ namespace Microsoft.Dafny
   }

   

   /// <summary>

+  /// This proxy stands for any datatype.

+  /// </summary>  

+  public class DatatypeProxy : RestrictedTypeProxy {

+    public override int OrderID { get { return 0; } }

+  }

+  

+  /// <summary>

   /// This proxy stands for object or any class/array type.

   /// </summary>  

   public class ObjectTypeProxy : RestrictedTypeProxy {

-    public override int OrderID { get { return 0; } }

+    public override int OrderID { get { return 1; } }

   }

   

   /// <summary>

   /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.

   /// </summary>

   public class ObjectsTypeProxy : RestrictedTypeProxy {

-    public override int OrderID { get { return 1; } }

+    public override int OrderID { get { return 2; } }

   }

   

   /// <summary>

@@ -310,7 +317,7 @@ namespace Microsoft.Dafny
     public CollectionTypeProxy(Type! arg) {

       Arg = arg;

     }

-    public override int OrderID { get { return 2; } }

+    public override int OrderID { get { return 3; } }

   }

 

   /// <summary>

@@ -325,7 +332,7 @@ namespace Microsoft.Dafny
     public OperationTypeProxy(bool allowSeq) {

       AllowSeq = allowSeq;

     }

-    public override int OrderID { get { return 3; } }

+    public override int OrderID { get { return 4; } }

   }

   

   /// <summary>

@@ -337,7 +344,7 @@ namespace Microsoft.Dafny
     public IndexableTypeProxy(Type! arg) {

       Arg = arg;

     }

-    public override int OrderID { get { return 4; } }

+    public override int OrderID { get { return 5; } }

   }

 

   // ------------------------------------------------------------------------------------------------------

@@ -1203,7 +1210,9 @@ namespace Microsoft.Dafny
       SetEq, SetNeq, ProperSubset, Subset, Superset, ProperSuperset, Disjoint, InSet, NotInSet,

       Union, Intersection, SetDifference,

       // sequences

-      SeqEq, SeqNeq, ProperPrefix, Prefix, Concat, InSeq, NotInSeq

+      SeqEq, SeqNeq, ProperPrefix, Prefix, Concat, InSeq, NotInSeq,

+      // datatypes

+      RankLt, RankGt

     }

     public ResolvedOpcode ResolvedOp;  // filled in by resolution

                                  

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 6e16aff6..671469f3 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -701,6 +701,13 @@ namespace Microsoft.Dafny {
         }

       

       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy

+      } else if (proxy is DatatypeProxy) {

+        if (t.IsDatatype) {

+          // all is fine, proxy can be redirected to t

+        } else {

+          return false;

+        }

+      

       } else if (proxy is ObjectTypeProxy) {

         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is fine, proxy can be redirected to t

@@ -765,7 +772,15 @@ namespace Microsoft.Dafny {
       modifies a.T, b.T;

       ensures result ==> a.T != null || b.T != null;

     {

-      if (a is ObjectTypeProxy) {

+      if (a is DatatypeProxy) {

+        if (b is DatatypeProxy) {

+          // all is fine

+          a.T = b;

+          return true;

+        } else {

+          return false;

+        }

+      } else if (a is ObjectTypeProxy) {

         if (b is ObjectTypeProxy) {

           // all is fine

           a.T = b;

@@ -1778,19 +1793,29 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

             {

-              bool err = false;

-              if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {

-                Error(expr, "arguments to {0} must be int or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

-                err = true;

-              }

-              if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

-                Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

-                err = true;

-              }

-              if (e.Op != BinaryExpr.Opcode.Add) {

+              if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsDatatype) {

+                if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

+                  Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

+                }

+                if (!specContext) {

+                  Error(expr, "rank comparisons are allowed only in specification and ghost contexts");

+                }

                 expr.Type = Type.Bool;

-              } else if (!err) {

-                expr.Type = e.E0.Type;

+              } else {

+                bool err = false;

+                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {

+                  Error(expr, "arguments to {0} must be int or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

+                  err = true;

+                }

+                if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

+                  Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

+                  err = true;

+                }

+                if (e.Op != BinaryExpr.Opcode.Add) {

+                  expr.Type = Type.Bool;

+                } else if (!err) {

+                  expr.Type = e.E0.Type;

+                }

               }

             }

             break;

@@ -1800,19 +1825,29 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Gt:

           case BinaryExpr.Opcode.Ge:

             {

-              bool err = false;

-              if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {

-                Error(expr, "arguments to {0} must be int or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

-                err = true;

-              }

-              if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

-                Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

-                err = true;

-              }

-              if (e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge) {

+              if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsDatatype) {

+                if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

+                  Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

+                }

+                if (!specContext) {

+                  Error(expr, "rank comparisons are allowed only in specification and ghost contexts");

+                }

                 expr.Type = Type.Bool;

-              } else if (!err) {

-                expr.Type = e.E0.Type;

+              } else {

+                bool err = false;

+                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {

+                  Error(expr, "arguments to {0} must be int or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

+                  err = true;

+                }

+                if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

+                  Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

+                  err = true;

+                }

+                if (e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge) {

+                  expr.Type = Type.Bool;

+                } else if (!err) {

+                  expr.Type = e.E0.Type;

+                }

               }

             }

             break;

@@ -2061,7 +2096,9 @@ namespace Microsoft.Dafny {
           }

         case BinaryExpr.Opcode.Disjoint:  return BinaryExpr.ResolvedOpcode.Disjoint;

         case BinaryExpr.Opcode.Lt:

-          if (operandType is SetType) {

+          if (operandType.IsDatatype) {

+            return BinaryExpr.ResolvedOpcode.RankLt;

+          } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSubset;

           } else if (operandType is SeqType) {

             return BinaryExpr.ResolvedOpcode.ProperPrefix;

@@ -2097,7 +2134,9 @@ namespace Microsoft.Dafny {
             return BinaryExpr.ResolvedOpcode.Mul;

           }

         case BinaryExpr.Opcode.Gt:

-          if (operandType is SetType) {

+          if (operandType.IsDatatype) {

+            return BinaryExpr.ResolvedOpcode.RankGt;

+          } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSuperset;

           } else {

             return BinaryExpr.ResolvedOpcode.Gt;

@@ -2178,6 +2217,9 @@ namespace Microsoft.Dafny {
         return UsesSpecFeatures(e.E);

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

+        if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankLt || e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankGt) {

+          return true;

+        }

         return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);

       } else if (expr is QuantifierExpr) {

         return true;

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 778096e9..eea9d91b 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -3021,6 +3021,15 @@ namespace Microsoft.Dafny {
                        BoxIfNecessary(expr.tok, e0, (!)e.E0.Type));

               return Bpl.Expr.Not(arg);

 

+            case BinaryExpr.ResolvedOpcode.RankLt:

+              return Bpl.Expr.Lt(

+                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),

+                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));

+            case BinaryExpr.ResolvedOpcode.RankGt:

+              return Bpl.Expr.Gt(

+                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),

+                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));

+              

             default:

               assert false;  // unexpected binary expression

           }