This changeset changes the default visibility of a function/predicate body outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.

Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules

1 files changed, 9 insertions, 2 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f5a9f6b0..12b5adfc 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -386,11 +386,14 @@ namespace Microsoft.Dafny
   /// specifically asks to see it via the reveal_foo() lemma

   /// </summary>

   public class OpaqueFunctionRewriter : IRewriter {

+    readonly ResolutionErrorReporter reporter;

     protected Dictionary<Function, Function> fullVersion; // Given an opaque function, retrieve the full

     protected Dictionary<Function, Function> original;    // Given a full version of an opaque function, find the original opaque version

     protected Dictionary<Lemma, Function> revealOriginal; // Map reveal_* lemmas back to their original functions

 

-    public OpaqueFunctionRewriter() : base() {

+    public OpaqueFunctionRewriter(ResolutionErrorReporter reporter)

+      : base() {

+      this.reporter = reporter;

       fullVersion = new Dictionary<Function, Function>();

       original = new Dictionary<Function, Function>();

       revealOriginal = new Dictionary<Lemma, Function>();

@@ -471,7 +474,11 @@ namespace Microsoft.Dafny
         if (member is Function) {

           var f = (Function)member;

 

-          if (Attributes.Contains(f.Attributes, "opaque") && !RefinementToken.IsInherited(f.tok, c.Module)) {

+          if (!Attributes.Contains(f.Attributes, "opaque")) {

+            // Nothing to do

+          } else if (f.IsProtected) {

+            reporter.Error(f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");

+          } else if (!RefinementToken.IsInherited(f.tok, c.Module)) {

             // Create a copy, which will be the internal version with a full body

             // which will allow us to verify that the ensures are true

             var cloner = new Cloner();