Various resolution fixes and improvements

Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms.
Added IDE tool tips in newtype constraints.

5 files changed, 146 insertions, 41 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a9da389a..48486698 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7430,7 +7430,7 @@ namespace Microsoft.Dafny
         subst.Add(dt.TypeArgs[i], t);

       }

       // Construct a resolved type directly, as we know the declaration is dt.

-      dtv.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, dt, gt);

+      dtv.Type = new UserDefinedType(dtv.tok, dt.Name, dt, gt);

 

       DatatypeCtor ctor;

       if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

@@ -7655,8 +7655,26 @@ namespace Microsoft.Dafny
     /// If you are calling a field that could be a function, creates an ApplyExpr, otherwise an ordinary FunctionCallExpr.

     /// </summary>

     private Expression NewFunctionCallExpr(IToken tok, string fn, Expression receiver, IToken openParen, List<Expression> args) {

-      NonProxyType nptype;

-      MemberDecl member = ResolveMember(tok, receiver.Type, fn, out nptype);

+      Contract.Requires(tok != null);

+      Contract.Requires(fn != null);

+      Contract.Requires(receiver != null && receiver.Type != null);

+      // We're going to look for a field of a class or a destructor of a datatype, but rather than calling

+      // ResolveMember (which would report an error if the member is not found), we do it ourselves.

+      MemberDecl member;

+      UserDefinedType ctype = UserDefinedType.DenotesClass(receiver.Type);

+      if (ctype != null) {

+        var cd = (ClassDecl)ctype.ResolvedClass;  // correctness of cast follows from postcondition of DenotesClass

+        if (!classMembers[cd].TryGetValue(fn, out member)) {

+          member = null;

+        }

+      } else if (receiver.Type.IsDatatype) {

+        var dtd = receiver.Type.AsDatatype;

+        if (!datatypeMembers[dtd].TryGetValue(fn, out member)) {

+          member = null;

+        }

+      } else {

+        member = null;

+      }

       var field = member as Field;

       if (field != null) {

         if (field.Type is ArrowType || field.Type.IsTypeParameter) {

@@ -7830,11 +7848,6 @@ namespace Microsoft.Dafny
               ResolveExpression(arg, opts);

             }

           }

-        } else if (decl is ClassDecl) {

-          // ----- root is a class

-          var cd = (ClassDecl)decl;

-          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, opts, allowMethodCall, out call);

-

         } else if (decl is ModuleDecl) {

           // ----- root is a submodule

           if (!(1 < e.Tokens.Count)) {

@@ -7842,13 +7855,25 @@ namespace Microsoft.Dafny
           }

           call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);

         } else {

-          // ----- root is a datatype

-          var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

-          var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();

-          r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

-          ResolveExpression(r, opts);

-          if (e.Tokens.Count != 2) {

-            r = ResolveSuffix(r, e, 2, opts, allowMethodCall, out call);

+          // expand any synonyms

+          var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());

+          var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs).NormalizeExpand();

+          if (ty.IsRefType) {

+            // ----- root is a class

+            var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;

+            r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, opts, allowMethodCall, out call);

+          } else if (ty.IsDatatype) {

+            // ----- root is a datatype

+            var dt = ty.AsDatatype;

+            var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();

+            var dtv = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

+            ResolveDatatypeValue(opts, dtv, dt);

+            r = dtv;

+            if (e.Tokens.Count != 2) {

+              r = ResolveSuffix(r, e, 2, opts, allowMethodCall, out call);

+            }

+          } else {

+            Error(id, "name of type ('{0}') is used as a variable", id.val);

           }

         }

 

@@ -7940,28 +7965,34 @@ namespace Microsoft.Dafny
             Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);

           }

           call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);

-        } else if (decl is TypeSynonymDecl) {

-          // ----- root apparently refers to a type synonym

-          Error(e.tok, "type synonym {0} cannot be used here", id.val);  // todo: this is a bit of a cop-out; perhaps something better could be done

-        } else if (decl is ClassDecl) {

-          // ----- root is a class

-          var cd = (ClassDecl)decl;

-          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, opts, allowMethodCall, out call);

-        } else if (decl is DatatypeDecl) {

-          // ----- root is a datatype

-          var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

-          var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();

-          r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);

-          ResolveDatatypeValue(opts, (DatatypeValue)r, dt);

-          if (e.Tokens.Count != p + 2) {

-            r = ResolveSuffix(r, e, p + 2, opts, allowMethodCall, out call);

-          }

         } else {

-          Error(id, "unresolved identifier: {0}", id.val);

-          // resolve arguments, if any

-          if (e.Arguments != null) {

-            foreach (var arg in e.Arguments) {

-              ResolveExpression(arg, opts);

+          // expand any synonyms

+          var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());

+          var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs).NormalizeExpand();

+          if (ty.IsRefType) {

+            // ----- root is a class

+            var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;

+            r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, opts, allowMethodCall, out call);

+          } else if (ty.IsDatatype) {

+            // ----- root is a datatype

+            var dt = ty.AsDatatype;

+            var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();

+            r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);

+            ResolveDatatypeValue(opts, (DatatypeValue)r, dt);

+            if (e.Tokens.Count != p + 2) {

+              r = ResolveSuffix(r, e, p + 2, opts, allowMethodCall, out call);

+            }

+          } else {

+            if (p == e.Tokens.Count - 1 && e.Arguments != null) {

+              Error(id, "name of type ('{0}') is used as a function", id.val);

+            } else {

+              Error(id, "name of type ('{0}') is used as a variable", id.val);

+            }

+            // resolve arguments, if any

+            if (e.Arguments != null) {

+              foreach (var arg in e.Arguments) {

+                ResolveExpression(arg, opts);

+              }

             }

           }

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 8beadb51..893b72fc 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -500,7 +500,7 @@ namespace Microsoft.Dafny {
             ie.Var = oVarDafny; ie.Type = ie.Var.Type;  // resolve ie here

             var constraint = etran.TrExpr(Substitute(dd.Constraint, dd.Var, ie));

             var heap = new Bpl.BoundVariable(dd.tok, new Bpl.TypedIdent(dd.tok, predef.HeapVarName, predef.HeapType));

-            var ex = new Bpl.ExistsExpr(dd.tok, new List<Variable> { heap }, constraint);

+            var ex = new Bpl.ExistsExpr(dd.tok, new List<Variable> { heap }, BplAnd(FunctionCall(dd.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr), constraint));

             rhs = BplAnd(rhs, ex);

           }

           body = BplIff(is_o, rhs);

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index beab8303..3bb8f01c 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -213,6 +213,12 @@ namespace DafnyLanguage
                 IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);

               }

             }

+          } else if (d is NewtypeDecl) {

+            var dd = (NewtypeDecl)d;

+            if (dd.Var != null) {

+              IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module);

+              ExprRegions(dd.Constraint, newRegions, module);

+            }

           }

         }

       }

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index 51f42994..0fe36eec 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -140,3 +140,66 @@ module InferredType {
     j := a;  // error: AnotherInt not assignable to Int

   }

 }

+

+module SynonymsAndModules {

+  module M {

+    type Syn = int

+    type Y = Klass

+    class Klass {

+      static method H()

+    }

+  }

+

+  method P()

+  {

+    var x: M.Syn;

+    x := B;  // error: bad use of B

+    x := M.Syn;  // error: bad use of M.Syn

+    C.D();

+    X.D();

+    M.Klass.H();

+    M.Y.H();

+    M.Y.U();  // error: non-existent member U

+  }

+

+  type B = int

+  type X = C

+  class C {

+    static method D()

+  }

+}

+

+module MoreSynonyms {

+  import SynonymLibrary

+

+  type Syn<T> = Syn'<T,T>

+  type Syn'<A,B> = C<B>

+  class C<alpha> {

+    static method MyMethod<beta>(b: beta, a: alpha)

+  }

+  method M() {

+    var a, b;

+    Syn.MyMethod(b, a);

+    a, b := 25, true;

+  }

+  method P() {

+    var d := SynonymLibrary.S.Cons(50, SynonymLibrary.Dt.Nil);

+    var e := SynonymLibrary.Dt.Cons(true, SynonymLibrary.S.Cons(40, d));

+    var f := SynonymLibrary.S.Cons(50, SynonymLibrary.S.Cons(true, d));  // error: 'true' argument is expected to be an integer

+  }

+}

+

+module SynonymLibrary {

+  type S = Dt<int>

+  datatype Dt<T> = Nil | Cons(T, S)

+}

+

+module QualifiedDatatypeCtor {

+  type S = Dt<int>

+  datatype Dt<T> = Nil | Cons(T, S)

+

+  method P() {

+    var d: S;

+    var f := S.Cons(50, S.Nil);

+  }

+}

diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 1746b37e..091ca523 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -1,5 +1,5 @@
-DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (derived types, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

-DerivedTypesResolution.dfy(12,10): Error: derived types must be based on some numeric type (got List<int>)

+DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym

+DerivedTypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)

 DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)

 DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)

 DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)

@@ -14,7 +14,12 @@ DerivedTypesResolution.dfy(91,31): Error: old expressions are not allowed in thi
 DerivedTypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

 DerivedTypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

 DerivedTypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

-DerivedTypesResolution.dfy(120,21): Error: unresolved identifier: N9

+DerivedTypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

 DerivedTypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

 DerivedTypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

-19 resolution/type errors detected in DerivedTypesResolution.dfy

+DerivedTypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

+DerivedTypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

+DerivedTypesResolution.dfy(162,8): Error: member U does not exist in class Klass

+DerivedTypesResolution.dfy(162,4): Error: expected method call, found expression

+DerivedTypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

+24 resolution/type errors detected in DerivedTypesResolution.dfy