Added .Trunc field to real-based types

Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer

8 files changed, 129 insertions, 44 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 3d5bf111..bf9ef568 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -432,8 +432,7 @@ axiom (forall o: ref :: 0 <= _System.array.Length(o));
 // -- Reals ------------------------------------------------------

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

 

-function _System.Real.RealToInt(h: Heap, x: real): int { int(x) }

-function _System.Real.IntToReal(h: Heap, x: int): real { real(x) }

+function {:inline true} _System.real.Trunc(x: real): int { int(x) }

 

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

 // -- The heap ---------------------------------------------------

@@ -868,17 +867,6 @@ axiom (forall<T> s, t: Seq T ::
 function Seq#FromArray(h: Heap, a: ref): Seq Box;

 axiom (forall h: Heap, a: ref ::

   { Seq#Length(Seq#FromArray(h,a)) }

-  /*

-<<<<<<< local

-    Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

-axiom (forall h: Heap, a: ref :: { Seq#FromArray(h,a): Seq Box }

-   (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

-axiom (forall<alpha> h: Heap, o: ref, f: Field alpha, v: alpha, a: ref ::

-  { Seq#FromArray(update(h, o, f, v), a) }

-    o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );

-axiom (forall h: Heap, i: int, v: Box, a: ref ::

-=======

-*/

   Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

 axiom (forall h: Heap, a: ref, i: int ::

   { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index dd600e18..dbfdf846 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -141,6 +141,12 @@ namespace Microsoft.Dafny
     readonly Dictionary<ClassDecl, Dictionary<string, MemberDecl>> classMembers = new Dictionary<ClassDecl, Dictionary<string, MemberDecl>>();

     readonly Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>> datatypeMembers = new Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>>();

     readonly Dictionary<DatatypeDecl, Dictionary<string, DatatypeCtor>> datatypeCtors = new Dictionary<DatatypeDecl, Dictionary<string, DatatypeCtor>>();

+    enum BasicTypeVariety { Bool = 0, Int, Real, None }  // note, these are ordered, so they can be used as indices into basicTypeMembers

+    readonly Dictionary<string, MemberDecl>[] basicTypeMembers = new Dictionary<string, MemberDecl>[] {

+      new Dictionary<string, MemberDecl>(),

+      new Dictionary<string, MemberDecl>(),

+      new Dictionary<string, MemberDecl>()

+    };

     readonly Graph<ModuleDecl> dependencies = new Graph<ModuleDecl>();

     private ModuleSignature systemNameInfo = null;

     private bool useCompileSignatures = false;

@@ -149,6 +155,9 @@ namespace Microsoft.Dafny
     public Resolver(Program prog) {

       Contract.Requires(prog != null);

       builtIns = prog.BuiltIns;

+      // Populate the members of the basic types

+      var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null);

+      basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc);

     }

 

     [ContractInvariantMethod]

@@ -6072,6 +6081,16 @@ namespace Microsoft.Dafny
 

       nptype = null;  // prepare for the worst

       receiverType = receiverType.NormalizeExpand();

+      var opProxy = receiverType as OperationTypeProxy;

+      if (opProxy != null) {

+        if (opProxy.JustInts) {

+          // close enough to do member lookups for int-based types

+          receiverType = Type.Int;

+        } else if (opProxy.JustReals) {

+          // close enough to do member lookups for real-based types

+          receiverType = Type.Real;

+        }

+      }

       if (receiverType is TypeProxy) {

         Error(tok, "type of the receiver is not fully determined at this program point", receiverType);

         return null;

@@ -6110,6 +6129,24 @@ namespace Microsoft.Dafny
         }

       }

 

+      BasicTypeVariety basic;

+      if (receiverType.IsBoolType) {

+        basic = BasicTypeVariety.Bool;

+      } else if (receiverType.IsNumericBased(Type.NumericPersuation.Int)) {

+        basic = BasicTypeVariety.Int;

+      } else if (receiverType.IsNumericBased(Type.NumericPersuation.Real)) {

+        basic = BasicTypeVariety.Real;

+      } else {

+        basic = BasicTypeVariety.None;

+      }

+      if (basic != BasicTypeVariety.None) {

+        MemberDecl member;

+        if (basicTypeMembers[(int)basic].TryGetValue(memberName, out member)) {

+          nptype = (NonProxyType)receiverType;

+          return member;

+        }

+      }

+

       Error(tok, "type {0} does not have a member {1}", receiverType, memberName);

       return null;

     }

@@ -6470,18 +6507,22 @@ namespace Microsoft.Dafny
         Contract.Assert(e.Obj.Type != null);  // follows from postcondition of ResolveExpression

         NonProxyType nptype;

         MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.MemberName, out nptype);

-#if !NO_WORK_TO_BE_DONE

-        UserDefinedType ctype = nptype as UserDefinedType;

-#endif

         if (member == null) {

           // error has already been reported by ResolveMember

         } else if (member is Function) {

           var fn = member as Function;

           e.Member = fn;

           // build the type substitution map

-          var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs);

-          // instantiate all type arguments from the functions. no polymorphic application

-          e.TypeApplication = new List<Type>(ctype.TypeArgs);

+          e.TypeApplication = new List<Type>();

+          Dictionary<TypeParameter, Type> subst;

+          var ctype = nptype as UserDefinedType;

+          if (ctype == null) {

+            subst = new Dictionary<TypeParameter, Type>();

+          } else {

+            subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs);

+            // instantiate all type arguments from the functions. no polymorphic application

+            e.TypeApplication.AddRange(ctype.TypeArgs);

+          }

           foreach (var tp in fn.TypeArgs) {

             Type prox = new InferredTypeProxy();

             subst[tp] = prox; 

@@ -6489,20 +6530,23 @@ namespace Microsoft.Dafny
           }

           e.Type = SubstType(fn.Type, subst);

           AddCallGraphEdge(e, opts.codeContext, fn);

-        } else if (!(member is Field)) {

-          Error(expr, "member {0} in type {1} does not refer to a field or a function", e.MemberName,

-            cce.NonNull(ctype).Name);

-        } else {

-          Contract.Assert(member is Field);

-          Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember

+        } else if (member is Field) {

           var field = (Field)member;

           e.Member = field;

           if (e.Obj is StaticReceiverExpr) {

             Error(expr, "a field must be selected via an object, not just a class name");

           }

-          // build the type substitution map

-          var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs);

-          e.Type = SubstType(field.Type, subst);

+          var ctype = nptype as UserDefinedType;

+          if (ctype == null) {

+            e.Type = field.Type;

+          } else {

+            Contract.Assert(ctype.ResolvedClass != null); // follows from postcondition of ResolveMember

+            // build the type substitution map

+            var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs);

+            e.Type = SubstType(field.Type, subst);

+          }

+        } else {

+          Error(expr, "member {0} in type {1} does not refer to a field or a function", e.MemberName, nptype);

         }

 

       } else if (expr is SeqSelectExpr) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 1036d539..a261f396 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -60,6 +60,7 @@ namespace Microsoft.Dafny {
       private readonly Bpl.TypeSynonymDecl multiSetTypeCtor;

       private readonly Bpl.TypeCtorDecl mapTypeCtor;

       public readonly Bpl.Function ArrayLength;

+      public readonly Bpl.Function RealTrunc;

       private readonly Bpl.TypeCtorDecl seqTypeCtor;

       readonly Bpl.TypeCtorDecl fieldName;

       public readonly Bpl.Type HeapType;

@@ -82,6 +83,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(setTypeCtor != null);

         Contract.Invariant(multiSetTypeCtor != null);

         Contract.Invariant(ArrayLength != null);

+        Contract.Invariant(RealTrunc != null);

         Contract.Invariant(seqTypeCtor != null);

         Contract.Invariant(fieldName != null);

         Contract.Invariant(HeapVarName != null);

@@ -143,7 +145,8 @@ namespace Microsoft.Dafny {
       }

 

       public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,

-                             Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

+                             Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor,

+                             Bpl.Function arrayLength, Bpl.Function realTrunc, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

                              Bpl.TypeCtorDecl tyType, Bpl.TypeCtorDecl tyTagType,

                              Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,

                              Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl handleType, Bpl.TypeCtorDecl layerType, Bpl.TypeCtorDecl dtCtorId,

@@ -156,6 +159,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(multiSetTypeCtor != null);

         Contract.Requires(mapTypeCtor != null);

         Contract.Requires(arrayLength != null);

+        Contract.Requires(realTrunc != null);

         Contract.Requires(seqTypeCtor != null);

         Contract.Requires(fieldNameType != null);

         Contract.Requires(heap != null);

@@ -176,6 +180,7 @@ namespace Microsoft.Dafny {
         this.multiSetTypeCtor = multiSetTypeCtor;

         this.mapTypeCtor = mapTypeCtor;

         this.ArrayLength = arrayLength;

+        this.RealTrunc = realTrunc;

         this.seqTypeCtor = seqTypeCtor;

         this.fieldName = fieldNameType;

         this.HeapType = heap.TypedIdent.Type;

@@ -204,6 +209,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeSynonymDecl setTypeCtor = null;

       Bpl.TypeSynonymDecl multiSetTypeCtor = null;

       Bpl.Function arrayLength = null;

+      Bpl.Function realTrunc = null;

       Bpl.TypeCtorDecl seqTypeCtor = null;

       Bpl.TypeCtorDecl fieldNameType = null;

       Bpl.TypeCtorDecl classNameType = null;

@@ -271,8 +277,11 @@ namespace Microsoft.Dafny {
           }

         } else if (d is Bpl.Function) {

           var f = (Bpl.Function)d;

-          if (f.Name == "_System.array.Length")

+          if (f.Name == "_System.array.Length") {

             arrayLength = f;

+          } else if (f.Name == "_System.real.Trunc") {

+            realTrunc = f;

+          }

         }

       }

       if (seqTypeCtor == null) {

@@ -285,6 +294,8 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of type Map");

       } else if (arrayLength == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length");

+      } else if (realTrunc == null) {

+        Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Trunc");

       } else if (fieldNameType == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");

       } else if (classNameType == null) {

@@ -315,7 +326,11 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");

       } else {

         return new PredefinedDecls(refType, boxType, tickType,

-                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, tyType, tyTagType, heap, classNameType, nameFamilyType, datatypeType, handleType, layerType, dtCtorId,

+                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor,

+                                   arrayLength, realTrunc, seqTypeCtor, fieldNameType,

+                                   tyType, tyTagType,

+                                   heap, classNameType, nameFamilyType,

+                                   datatypeType, handleType, layerType, dtCtorId,

                                    allocField);

       }

       return null;

@@ -4657,6 +4672,18 @@ namespace Microsoft.Dafny {
       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         CheckWellformed(e.E, options, locals, builder, etran);

+        if (e is ConversionExpr) {

+          var ee = (ConversionExpr)e;

+          if (ee.ToType is IntType && ee.E.Type.IsNumericBased(Type.NumericPersuation.Real)) {

+            // this operation is well-formed only if the real-based number represents an integer

+            // assert ToReal(ToInt(e.E)) == e.E

+            var arg = etran.TrExpr(e.E);

+            Bpl.Expr isAnInt = new Bpl.NAryExpr(e.tok, new ArithmeticCoercion(e.tok, ArithmeticCoercion.CoercionType.ToInt), new List<Expr> { arg });

+            isAnInt = new Bpl.NAryExpr(e.tok, new ArithmeticCoercion(e.tok, ArithmeticCoercion.CoercionType.ToReal), new List<Expr> { isAnInt });

+            isAnInt = Bpl.Expr.Binary(e.tok, BinaryOperator.Opcode.Eq, isAnInt, arg);

+            builder.Add(Assert(expr.tok, isAnInt, "the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number)"));

+          }

+        }

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         CheckWellformed(e.E0, options, locals, builder, etran);

@@ -5525,7 +5552,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(f != null && !f.IsMutable);

       Contract.Requires(sink != null && predef != null);

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

-

       

       Bpl.Function ff;

       if (fieldFunctions.TryGetValue(f, out ff)) {        

@@ -5534,6 +5560,9 @@ namespace Microsoft.Dafny {
         if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude.

           fieldFunctions.Add(f, predef.ArrayLength);

           return predef.ArrayLength;

+        } else if (f.EnclosingClass == null && f.Name == "Trunc") { // link directly to the function in the prelude.

+          fieldFunctions.Add(f, predef.RealTrunc);

+          return predef.RealTrunc;

         }

         // function f(Ref): ty;

         Bpl.Type ty = TrType(f.Type);

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index ef9b7dae..127a3b08 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -11,6 +11,7 @@ method M()
   var s: set<int32>;

   var x: posReal;

   var y: posReal;

+  var yOrig := y;

   var z: int32;

   x := 5.3;

   z := 12;

@@ -35,4 +36,11 @@ method M()
   y := 60.0;

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

   assert dr == 32.0;

+

+  if yOrig == 0.3 {

+    var truncated := r0.Trunc + x.Trunc;

+    assert truncated == 5 + 5;

+    var rounded := (r0 + 0.5).Trunc;

+    assert rounded == 6;

+  }

 }

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index c3a02eeb..29f6e859 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -61,5 +61,8 @@ module Goodies {
     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];

+

+    var truncated := r0.Trunc + x.Trunc;

+    var rounded := (r0 + 0.5).Trunc;

   }

 }

diff --git a/Test/dafny0/RealCompare.dfy b/Test/dafny0/RealCompare.dfy
index b1dae47d..f5256d6f 100644
--- a/Test/dafny0/RealCompare.dfy
+++ b/Test/dafny0/RealCompare.dfy
@@ -145,7 +145,7 @@ method Test_AbsInt1()
 {

   var a, i := 0.3, 0.0;

   while i < 10.0

-    invariant i <= 10.0 && i == real(int(i));

+    invariant i <= 10.0 && i == real(i.Trunc);

     invariant a == 0.3 + 0.5 * i;

   {

     a, i := a + 0.5, i + 1.0;

diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy
index e51b76ad..76ac9d93 100644
--- a/Test/dafny0/RealTypes.dfy
+++ b/Test/dafny0/RealTypes.dfy
@@ -4,8 +4,15 @@
 method R1(ghost x: real, ghost y: real, i: int) {

   assert x + y == y + x;

   assert int(real(i)) == i;

-  assert real(int(x)) <= x;

-  assert real(int(x)) >= x; // error

+  assert real(x.Trunc) <= x;

+  if {

+    case real(x.Trunc) >= x =>

+      assert x.Trunc == int(x);  // the cast to int is allowed here

+    case true =>

+      var t := int(x);  // error: x may be a non-integer

+    case true =>

+      assert real(x.Trunc) >= x; // error

+  }

 }

 

 method R2(ghost x: real, ghost y: real) {

@@ -31,6 +38,7 @@ function R4(x:int, r:real) : int
 

 method RoundingDirection()

 {

-  assert int(51.500277) == 51;

-  assert int(-0.194771) == -1;

+  assert 51.500277.Trunc == 51;

+  assert (-0.194771).Trunc == -1;

+  assert -0.194771.Trunc == 0;

 }

diff --git a/Test/dafny0/RealTypes.dfy.expect b/Test/dafny0/RealTypes.dfy.expect
index 1f4d22a8..0d132948 100644
--- a/Test/dafny0/RealTypes.dfy.expect
+++ b/Test/dafny0/RealTypes.dfy.expect
@@ -1,18 +1,23 @@
-RealTypes.dfy(8,23): Error: assertion violation

+RealTypes.dfy(12,16): Error: the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number)

 Execution trace:

     (0,0): anon0

-RealTypes.dfy(14,12): Error: possible division by zero

+    (0,0): anon6_Then

+RealTypes.dfy(14,28): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    RealTypes.dfy(13,23): anon3_Else

+    (0,0): anon7_Then

+RealTypes.dfy(21,12): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    RealTypes.dfy(20,23): anon3_Else

     (0,0): anon2

-RealTypes.dfy(14,20): Error: assertion violation

+RealTypes.dfy(21,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    RealTypes.dfy(13,23): anon3_Else

+    RealTypes.dfy(20,23): anon3_Else

     (0,0): anon2

-RealTypes.dfy(22,12): Error: assertion violation

+RealTypes.dfy(29,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 6 verified, 4 errors

+Dafny program verifier finished with 6 verified, 5 errors