Fixed an encoding bug for newtypes (this fixes Issue #50)

7 files changed, 83 insertions, 13 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 734f328f..4f44d154 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -747,6 +747,16 @@ namespace Microsoft.Dafny {
       ResolvedClass = systemModule.TopLevelDecls.Find(d => d.Name == Name);

       Contract.Assume(ResolvedClass != null);

     }

+    /// <summary>

+    /// Constructs and returns a resolved arrow type.

+    /// </summary>

+    public ArrowType(IToken tok, ArrowTypeDecl atd, List<Type> typeArgsAndResult)

+      : base(tok, ArrowTypeName(atd.Arity), atd, typeArgsAndResult) {

+      Contract.Requires(tok != null);

+      Contract.Requires(atd != null);

+      Contract.Requires(typeArgsAndResult != null);

+      Contract.Requires(typeArgsAndResult.Count == atd.Arity + 1);

+    }

 

     public const string Arrow_FullCompileName = "Func";  // this is the same for all arities

     public override string FullCompileName {

@@ -1004,6 +1014,24 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Constructs a Type (in particular, a UserDefinedType) from a TopLevelDecl denoting a type declaration.  If

+    /// the given declaration takes type parameters, these are filled as references to the formal type parameters

+    /// themselves.  (Usually, this method is called when the type parameters in the result don't matter, other

+    /// than that they need to be filled in, so as to make a properly resolved UserDefinedType.)

+    /// </summary>

+    public static UserDefinedType FromTopLevelDecl(IToken tok, TopLevelDecl cd) {

+      Contract.Requires(tok != null);

+      Contract.Requires(cd != null);

+      Contract.Assert((cd is ArrowTypeDecl) == ArrowType.IsArrowTypeName(cd.Name));

+      var args =  cd.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp));

+      if (cd is ArrowTypeDecl) {

+        return new ArrowType(tok, (ArrowTypeDecl)cd, args);

+      } else {

+        return new UserDefinedType(tok, cd.Name, cd, args);

+      }

+    }

+

+    /// <summary>

     /// This constructor constructs a resolved class/datatype/iterator type

     /// </summary>

     public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List<Type> typeArgs) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 6067ed50..3772d3c0 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -177,7 +177,7 @@ namespace Microsoft.Dafny
                   } else {

                     // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

                     // taken place, so we defer it until the PostResolve phase.

-                    var udt = new UserDefinedType(nw.tok, nw.Name, nw, nw.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)));

+                    var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw);

                     postTasks.Enqueue(() => {

                       if (!udt.SupportsEquality) {

                         reporter.Error(udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index fe219dbc..eab4fd08 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6256,11 +6256,7 @@ namespace Microsoft.Dafny
       Contract.Requires(cl != null);

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

 

-      List<Type> args = new List<Type>();

-      foreach (TypeParameter tp in cl.TypeArgs) {

-        args.Add(new UserDefinedType(tok, tp));

-      }

-      return new UserDefinedType(tok, cl.Name, cl, args);

+      return UserDefinedType.FromTopLevelDecl(tok, cl);

     }

 

     /// <summary>

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f8f4b218..f5a9f6b0 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -182,7 +182,7 @@ namespace Microsoft.Dafny
       Contract.Assert(ReprField != null);  // we expect there to be a "Repr" field, since we added one in PreResolve

 

       Boogie.IToken clTok = new AutoGeneratedToken(cl.tok);

-      Type ty = new UserDefinedType(clTok, cl.Name, cl, cl.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)));

+      Type ty = UserDefinedType.FromTopLevelDecl(clTok, cl);

       var self = new ThisExpr(clTok);

       self.Type = ty;

       var implicitSelf = new ImplicitThisExpr(clTok);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d5b7020b..7878d46e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5292,7 +5292,6 @@ namespace Microsoft.Dafny {
     // Note: Prefer to call ClassTyCon or TypeToTy instead.

     private string GetClassTyCon(TopLevelDecl dl) {

       Contract.Requires(dl != null);

-      int n = dl.TypeArgs.Count; // arity

       string name;

       if (classConstants.TryGetValue(dl, out name)) {

         Contract.Assert(name != null);

@@ -5692,10 +5691,8 @@ namespace Microsoft.Dafny {
 

     private string AddTyAxioms(TopLevelDecl td) {

       IToken tok = td.tok;

-      var ty_repr =

-        td is ArrowTypeDecl ? predef.HandleType :

-        td is DatatypeDecl ? predef.DatatypeType :

-        predef.RefType;

+

+      var ty_repr = TrType(UserDefinedType.FromTopLevelDecl(td.tok, td));

       var arity = td.TypeArgs.Count;

       var inner_name = GetClass(td).TypedIdent.Name;

       string name = "T" + inner_name;

diff --git a/Test/dafny0/Newtypes.dfy b/Test/dafny0/Newtypes.dfy
index 93caa7ab..b941e0bf 100644
--- a/Test/dafny0/Newtypes.dfy
+++ b/Test/dafny0/Newtypes.dfy
@@ -309,3 +309,52 @@ module Guessing_Termination_Metrics {
     }

   }

 }

+

+// ----------- test $Is predicates ----------------------------

+

+module SeqTests {

+  newtype byte = i:int | 0 <= i < 0x100

+

+  method M0(many_bytes: seq<byte>, one_byte: byte)

+    requires |many_bytes| == 1;

+  {

+    assert 0 <= int(one_byte) < 0x100;

+    assert 0 <= int(many_bytes[0]) < 0x100;

+  }

+

+  method M1(many_bytes: seq<byte>, many_ints: seq<int>) 

+    requires |many_bytes| == 1;

+    requires |many_ints| == 1;

+  {

+    assert many_bytes[0] in many_bytes;

+    assert many_ints[0] in many_ints;    

+  }

+

+  lemma Lemma2<T>(elt: T, s: seq<T>, index: nat)

+    requires index < |s|;

+    requires elt == s[index];

+    ensures elt in s;

+  {}

+

+  method M2(many_bytes: seq<byte>, many_ints: seq<int>) 

+    requires |many_bytes| == 1;

+    requires |many_ints| == 1;

+  {

+    Lemma2(many_bytes[0], many_bytes, 0);

+    Lemma2(many_ints[0], many_ints, 0);

+    assert many_bytes[0] in many_bytes;

+    assert many_ints[0] in many_ints;    

+  }

+

+  lemma Lemma3_ints(data: seq<int>)

+    requires |data| > 25;

+    ensures  data[0..25] == [data[0]] + data[1..25];

+  {

+  }

+

+  lemma Lemma3_bytes(data: seq<byte>)

+    requires |data| > 25;

+    ensures  data[0..25] == [data[0]] + data[1..25];

+  {

+  }

+}

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 3ca77f1d..8e6ff4c5 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -55,4 +55,4 @@ Execution trace:
     (0,0): anon9_LoopBody

     (0,0): anon10_Then

 

-Dafny program verifier finished with 47 verified, 13 errors

+Dafny program verifier finished with 60 verified, 13 errors