Allow revealing using a static receiver

Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs

@@ -96,7 +96,7 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex
           if (effectiveExpr is NameSegment) {
             resolver.ResolveNameSegment((NameSegment)effectiveExpr, true, null, resolutionContext, true);
           } else {
-            resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, null, resolutionContext, true);
+            resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, true, null, resolutionContext, true);
           }
           var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)effectiveExpr).ResolvedExpression;
           if (callee == null) {
@@ -110,7 +110,7 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex
                 if (exprClone is NameSegment) {
                   resolver.ResolveNameSegment((NameSegment)exprClone, true, null, revealResolutionContext, true);
                 } else {
-                  resolver.ResolveDotSuffix((ExprDotName)exprClone, true, null, revealResolutionContext, true);
+                  resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true);
                 }
 
                 var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression);

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -187,7 +187,7 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte
           }
         case ExprDotName name: {
             var e = name;
-            ResolveDotSuffix(e, true, null, resolutionContext, false);
+            ResolveDotSuffix(e, false, true, null, resolutionContext, false);
             if (e.PreType is PreTypePlaceholderModule) {
               ReportError(e.tok, "name of module ({0}) is used as a variable", e.SuffixName);
               ResetTypeAssignment(e);  // the rest of type checking assumes actual types
@@ -1446,7 +1446,7 @@ private bool ResolveDatatypeConstructor(NameSegment expr, List<ActualBinding>/*?
     /// <param name="resolutionContext"></param>
     /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
     /// a Resolver_MethodCall.</param>
-    public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
+    public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
       Contract.Requires(resolutionContext != null);
@@ -1458,7 +1458,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, Lis
       if (expr.Lhs is NameSegment) {
         ResolveNameSegment((NameSegment)expr.Lhs, false, null, nonRevealOpts, false);
       } else if (expr.Lhs is ExprDotName) {
-        ResolveDotSuffix((ExprDotName)expr.Lhs, false, null, nonRevealOpts, false);
+        ResolveDotSuffix((ExprDotName)expr.Lhs, false, false, null, nonRevealOpts, false);
       } else {
         ResolveExpression(expr.Lhs, nonRevealOpts);
       }
@@ -1561,7 +1561,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, Lis
             if (!resolver.VisibleInScope(member)) {
               ReportError(expr.tok, $"member '{name}' has not been imported in this scope and cannot be accessed here");
             }
-            if (!member.IsStatic) {
+            if (!member.IsStatic && !allowStaticReferenceToInstance) {
               ReportError(expr.tok, $"accessing member '{name}' requires an instance expression"); //TODO Unify with similar error messages
               // nevertheless, continue creating an expression that approximates a correct one
             }
@@ -1720,7 +1720,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
         r = ResolveNameSegment((NameSegment)e.Lhs, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall);
         // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args
       } else if (e.Lhs is ExprDotName) {
-        r = ResolveDotSuffix((ExprDotName)e.Lhs, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall);
+        r = ResolveDotSuffix((ExprDotName)e.Lhs, false, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall);
         // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args
       } else {
         ResolveExpression(e.Lhs, resolutionContext);

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -1202,7 +1202,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut
               PreType = rr.PreType
             };
             var callLhs = new ExprDotName(((UserDefinedType)rr.EType).tok, lhs, initCallName, ret?.LastComponent.OptTypeArguments);
-            ResolveDotSuffix(callLhs, true, rr.Bindings.ArgumentBindings, resolutionContext, true);
+            ResolveDotSuffix(callLhs, false, true, rr.Bindings.ArgumentBindings, resolutionContext, true);
             if (prevErrorCount == ErrorCount) {
               Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr);  // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
               var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy

@@ -0,0 +1,39 @@
+// RUN: %resolve --type-system-refresh --allow-axioms %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+module Prod {
+  class Foo {
+    function P(x: int): bool {
+      true
+    }
+
+    static function Q(x: int): bool {
+      true
+    }
+  }
+
+  method StaticRevealWorks() {
+    hide *;
+
+    reveal Foo.P;
+    reveal Foo.Q;
+  }
+
+  method InstanceRevealWorks(foo: Foo) {
+    hide *;
+
+    reveal foo.P;
+    reveal foo.Q;
+  }
+}
+
+module Cons {
+  import Prod
+
+  method StaticRevealWorks() {
+    hide *;
+
+    reveal Prod.Foo.P;
+    reveal Prod.Foo.Q;
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier did not attempt verification

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect

@@ -13,11 +13,10 @@ git-issue-5017b.dfy(135,13): Error: only functions and constants can be revealed
 git-issue-5017b.dfy(136,13): Error: only functions and constants can be revealed
 git-issue-5017b.dfy(140,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A'
 git-issue-5017b.dfy(141,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A'
-git-issue-5017b.dfy(145,13): Error: accessing member 'WithBody' requires an instance expression
 git-issue-5017b.dfy(117,13): Error: unresolved identifier: UnknownFunction
 git-issue-5017b.dfy(118,13): Error: unresolved identifier: UnknownFunction
 git-issue-5017b.dfy(119,13): Error: only functions and constants can be revealed
 git-issue-5017b.dfy(120,13): Error: only functions and constants can be revealed
 git-issue-5017b.dfy(124,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid'
 git-issue-5017b.dfy(125,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid'
-22 resolution/type errors detected in git-issue-5017b.dfy
+21 resolution/type errors detected in git-issue-5017b.dfy

docs/dev/news/5760.fix

@@ -0,0 +1 @@
+The new resolver (accessible using `--type-system-refresh`) can now handle revealing instance functions using a static receiver, as it is the case for the current resolver