Allow an arbitrary-type to take type parameters

7 files changed, 184 insertions, 34 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 36ffd3ec..227884f2 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1067,6 +1067,19 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class OpaqueType_AsParameter : TypeParameter

+  {

+    public readonly List<TypeParameter> TypeArgs;

+    public OpaqueType_AsParameter(IToken tok, string name, EqualitySupportValue equalitySupport, List<TypeParameter> typeArgs)

+      : base(tok, name, equalitySupport)

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(typeArgs != null);

+      TypeArgs = typeArgs;

+    }

+  }

+

   public class TypeParameter : Declaration {

     public interface ParentType {

       string FullName {

@@ -1935,7 +1948,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(name != null);

       Contract.Requires(module != null);

       Contract.Requires(typeArgs != null);

-      TheType = new TypeParameter(tok, name, equalitySupport);

+      TheType = new OpaqueType_AsParameter(tok, name, equalitySupport, TypeArgs);

     }

   }

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e681ce51..4b775017 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2577,19 +2577,26 @@ namespace Microsoft.Dafny
 

         } else if (type is UserDefinedType) {

           var udt = (UserDefinedType)type;

+          List<TypeParameter> formalTypeArgs = null;

           if (udt.ResolvedClass != null) {

-            Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);

+            formalTypeArgs = udt.ResolvedClass.TypeArgs;

+          } else if (udt.ResolvedParam is OpaqueType_AsParameter) {

+            var t = (OpaqueType_AsParameter)udt.ResolvedParam;

+            formalTypeArgs = t.TypeArgs;

+          }

+          if (formalTypeArgs == null) {

+            Contract.Assert(udt.TypeArgs.Count == 0);

+          } else {

+            Contract.Assert(formalTypeArgs.Count == udt.TypeArgs.Count);

             var i = 0;

             foreach (var argType in udt.TypeArgs) {

-              var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+              var formalTypeArg = formalTypeArgs[i];

               if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {

                 Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));

               }

               CheckEqualityTypes_Type(tok, argType);

               i++;

             }

-          } else {

-            Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

           }

 

         } else {

@@ -2707,17 +2714,25 @@ namespace Microsoft.Dafny
         return InferRequiredEqualitySupport(tp, sq.Arg);

       } else if (type is UserDefinedType) {

         var udt = (UserDefinedType)type;

+        List<TypeParameter> formalTypeArgs = null;

         if (udt.ResolvedClass != null) {

+          formalTypeArgs = udt.ResolvedClass.TypeArgs;

+        } else if (udt.ResolvedParam is OpaqueType_AsParameter) {

+          var t = (OpaqueType_AsParameter)udt.ResolvedParam;

+          formalTypeArgs = t.TypeArgs;

+        }

+        if (formalTypeArgs == null) {

+          Contract.Assert(udt.TypeArgs.Count == 0);

+        } else {

+          Contract.Assert(formalTypeArgs.Count == udt.TypeArgs.Count);

           var i = 0;

           foreach (var argType in udt.TypeArgs) {

-            var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+            var formalTypeArg = formalTypeArgs[i];

             if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {

               return true;

             }

             i++;

           }

-        } else {

-          Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

         }

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

@@ -3793,11 +3808,16 @@ namespace Microsoft.Dafny
             // error has been reported above

           } else if (d is AmbiguousTopLevelDecl) {

             Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());

-          } else if (d is ArbitraryTypeDecl) {

-            t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve like a type parameter

           } else {

-            // d is a class or datatype, and it may have type parameters

-            t.ResolvedClass = d;

+            string what;

+            if (d is ArbitraryTypeDecl) {

+              what = "arbitrary type";

+              t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType;  // resolve like a type parameter, and it may have type parameters if it's an arbitrary-type

+            } else {

+              // d is a class or datatype, and it may have type parameters

+              what = "class/datatype";

+              t.ResolvedClass = d;

+            }

             if (option.Opt == ResolveTypeOptionEnum.DontInfer) {

               // don't add anything

             } else if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) {

@@ -3805,7 +3825,7 @@ namespace Microsoft.Dafny
             }

             // defaults and auto have been applied; check if we now have the right number of arguments

             if (d.TypeArgs.Count != t.TypeArgs.Count) {

-              Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

+              Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", t.TypeArgs.Count, d.TypeArgs.Count, what, t.Name);

             }

           }

         }

@@ -3914,9 +3934,18 @@ namespace Microsoft.Dafny
           }

           return successSoFar;

         } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {

-          // these are both resolved type parameters

-          Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);

-          return true;

+          // type parameters

+          if (aa.TypeArgs.Count != bb.TypeArgs.Count) {

+            return false;

+          } else {

+            bool successSoFar = true;

+            for (int i = 0; i < aa.TypeArgs.Count; i++) {

+              if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) {

+                successSoFar = false;

+              }

+            }

+            return successSoFar;

+          }

         } else {

           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify

           return false;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e5812955..2c987b62 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -427,15 +427,24 @@ namespace Microsoft.Dafny {
     }

 

     void AddTypeDecl(ArbitraryTypeDecl td) {

+      Contract.Requires(td != null);

       string nm = nameTypeParam(td.TheType);

       if (abstractTypes.Contains(nm)) {

-        // do nothing!

-      } else {

+        // nothing to do; has already been added

+        return;

+      }

+      if (td.TypeArgs.Count == 0) {

         sink.TopLevelDeclarations.Add(

           new Bpl.Constant(td.tok,

             new TypedIdent(td.tok, nm, predef.Ty), false /* not unique */));

-        abstractTypes.Add(nm);

+      } else {

+        // Note, the function produced is NOT necessarily injective, because the type may be replaced

+        // in a refinement module in such a way that the type arguments do not matter.

+        var args = new List<Bpl.Variable>(td.TypeArgs.ConvertAll(a => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)));

+        var func = new Bpl.Function(td.tok, nm, args, BplFormalVar(null, predef.Ty, false));

+        sink.TopLevelDeclarations.Add(func);

       }

+      abstractTypes.Add(nm);

     }

 

     void AddDatatype(DatatypeDecl dt) {

@@ -3081,7 +3090,7 @@ namespace Microsoft.Dafny {
       {

         var args = new List<Bpl.Expr>();

         foreach (var p in GetTypeParams(f)) {

-          args.Add(trTypeParam(p));

+          args.Add(trTypeParam(p, null));

         }

         if (f.IsRecursive) {

           args.Add(etran.LayerN(1));

@@ -3116,7 +3125,7 @@ namespace Microsoft.Dafny {
         Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));

         List<Bpl.Expr> args = new List<Bpl.Expr>();

         foreach (var p in GetTypeParams(f)) {

-          args.Add(trTypeParam(p));

+          args.Add(trTypeParam(p, null));

         }

         if (f.IsRecursive) {

           args.Add(etran.LayerN(1));

@@ -7272,7 +7281,9 @@ namespace Microsoft.Dafny {
       }

     }

 

-    // Translates an AST Type to a Boogie expression of type Ty.

+    /// <summary>

+    /// Translates an AST Type to a Boogie expression of type Ty.

+    /// </summary>

     Bpl.Expr TypeToTy(Type type) {

       Contract.Requires(type != null);

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

@@ -7299,20 +7310,16 @@ namespace Microsoft.Dafny {
       } else if (type is IntType) {

         return new Bpl.IdentifierExpr(Token.NoToken, "TInt", predef.Ty);

       } else if (type.IsTypeParameter) {

-        return trTypeParam(type.AsTypeParameter);              

+        var args = type.TypeArgs.ConvertAll(TypeToTy);

+        return trTypeParam(type.AsTypeParameter, args);

       } else if (type is ObjectType) {

         return ClassTyCon(program.BuiltIns.ObjectDecl, new List<Bpl.Expr>());

       } else if (type is UserDefinedType) {

         // Classes, (co-)datatypes

-        List<Bpl.Expr> args = new List<Bpl.Expr> { };

-        foreach (Type ch in type.TypeArgs) {

-          var tr_ty = TypeToTy(ch);

-          Contract.Assert(tr_ty != null);

-          args.Add(TypeToTy(ch));

-        }

+        var args = type.TypeArgs.ConvertAll(TypeToTy);

         return ClassTyCon(((UserDefinedType)type), args);      

       } else if (type is ParamTypeProxy) {

-        return trTypeParam(((ParamTypeProxy)type).orig);

+        return trTypeParam(((ParamTypeProxy)type).orig, null);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

@@ -7328,9 +7335,16 @@ namespace Microsoft.Dafny {
       }

     }

    

-    Bpl.Expr trTypeParam(TypeParameter x) {

+    Bpl.Expr trTypeParam(TypeParameter x, List<Bpl.Expr> tyArguments) {

       Contract.Requires(x != null);

-      return new Bpl.IdentifierExpr(x.tok, nameTypeParam(x), predef.Ty);      

+      var nm = nameTypeParam(x);

+      var opaqueType = x as OpaqueType_AsParameter;

+      if (tyArguments != null && tyArguments.Count != 0) {

+        return FunctionCall(x.tok, nm, predef.Ty, tyArguments);

+      } else {

+        // return an identifier denoting a constant

+        return new Bpl.IdentifierExpr(x.tok, nm, predef.Ty);

+      }

     }

 

     public List<TypeParameter> GetTypeParams(IMethodCodeContext cc) {

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index e5f039b3..30c3eefd 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -157,3 +157,36 @@ class DatatypeInduction<T> {
     assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n;  // error reported

   }

 }

+

+// --- opaque types with type parameters ---

+

+abstract module OpaqueTypesWithParameters {

+  type P<A>

+

+  method M<B>(p: P<B>) returns (q: P<B>)

+  {

+    q := p;

+    var a := new P<int>[500];

+  }

+

+  method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)

+    requires a != null && b != null;

+    // If P were a known type, then it would also be known that P<int> and P<bool>

+    // would be different types, and then the types of 'a' and 'b' would be different,

+    // which would imply that the following postcondition would hold.

+    // However, it is NOT necessarily the case that the type parameters of an opaque

+    // type actually make the opaque type different.  For example, see the refinement

+    // module CaseInPoint below.

+    ensures a != b;  // error

+  {

+  }

+}

+

+module CaseInPoint refines OpaqueTypesWithParameters {

+  type P<A> = real  // note, the type parameter is not used

+  method Client() {

+    var x := new real[100];

+    DifferentTypes(x, x);

+    assert false;  // this is provable here, since DifferentTypes has a bogus postcondition

+  }

+}

diff --git a/Test/dafny0/DTypes.dfy.expect b/Test/dafny0/DTypes.dfy.expect
index d7a3a029..fccf1c9a 100644
--- a/Test/dafny0/DTypes.dfy.expect
+++ b/Test/dafny0/DTypes.dfy.expect
@@ -1,3 +1,7 @@
+DTypes.dfy(181,3): Error BP5003: A postcondition might not hold on this return path.

+DTypes.dfy(180,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

 DTypes.dfy(18,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -24,4 +28,4 @@ Execution trace:
     (0,0): anon6_Then

     (0,0): anon4

 

-Dafny program verifier finished with 27 verified, 6 errors

+Dafny program verifier finished with 36 verified, 7 errors

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 823fbe29..520b2e38 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1042,3 +1042,51 @@ type {:myAttribute x} Synonym = int  // error: x does not refer to anything
 

 module {:myAttribute x} Modulette {  // error: x does not refer to anything

 }

+

+// --- opaque types with type parameters ---

+

+module OpaqueTypes0 {

+  type P<AA>

+  method M<B>(p: P<B>) returns (q: P<B,B>)  // error: wrong param count

+  {

+    q := p;

+  }

+}

+

+module OpaqueTypes1 {

+  type P<A>

+

+  method M0<B>(p: P<B>) returns (q: P<B>)

+  {

+    q := p;

+    var m: P<BX>;  // error: BX undefined

+  }

+

+  method M1<B>(p: P<B>) returns (q: P)  // type parameter of q's type inferred

+  {

+    q := p;

+  }

+

+  method M2(p: P<int>) returns (q: P<bool>)

+  {

+    q := p;  // error: cannot assign P<bool> to P<int>

+  }

+

+  method M3<A,B>(p: P<A>) returns (q: P<B>)

+  {

+    q := p;  // error: cannot assign P<A> to P<B>

+  }

+

+  method M4<A>() returns (p: P<A>, q: P<int>)

+  {

+    q := p;  // error: cannot assign P<A> to P<int>

+    p := q;  // error: cannot assign P<int> to P<A>

+  }

+

+  method EqualityTests<X>(p: P<int>, q: P<bool>, r: P<X>)

+  {

+    assert p != r;  // error: types must be the same in order to do compare

+    assert q != r;  // error: types must be the same in order to do compare

+    assert p != q;  // error: types must be the same in order to do compare

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 820465db..38393b02 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -66,6 +66,15 @@ ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
 ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A

 ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A

 ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x

+ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to arbitrary type: P

+ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)

+ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)

+ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)

+ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)

+ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)

+ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)

+ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)

+ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)

 ResolutionErrors.dfy(429,2): Error: More than one default constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

@@ -162,4 +171,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
 ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)

 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

-164 resolution/type errors detected in ResolutionErrors.dfy

+173 resolution/type errors detected in ResolutionErrors.dfy