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, 3 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 9501caed..9cad2bb1 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -690,6 +690,8 @@ namespace Microsoft.Dafny
             bool isCoPredicate = f is CoPredicate;

             if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {

               reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name);

+            } else if (f.IsProtected != ((Function)member).IsProtected) {

+              reporter.Error(f, "a {0} in a refinement module must be declared 'protected' if and only if the refined {0} is", f.WhatKind);

             } else {

               var prevFunction = (Function)member;

               if (f.Req.Count != 0) {

@@ -726,10 +728,14 @@ namespace Microsoft.Dafny
               Expression replacementBody = null;

               if (prevFunction.Body == null) {

                 replacementBody = f.Body;

-              } else if (isPredicate) {

-                moreBody = f.Body;

               } else if (f.Body != null) {

-                reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

+                if (isPredicate && f.IsProtected) {

+                  moreBody = f.Body;

+                } else if (isPredicate) {

+                  reporter.Error(nwMember, "a refining predicate is not allowed to extend/change the body unless it is declared 'protected'");

+                } else {

+                  reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

+                }

               }

               var newF = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody, prevFunction.Body == null, f.Attributes);

               newF.RefinementBase = member;