Implement 'extern' declaration modifier.

The 'extern' declaration modifier provides a more convenient
way of interfacing Dafny code with C# source files and
.Net DLLs.

We support an 'extern' keyword on a module, class, function method,
or method (cannot extern ghost). We check the CompileNames of
all modules to make sure there are no duplicate names.

Every Dafny-generated C# class is marked partial, so it can
potentially be extended.

The extern keyword could be accompanied by an optional string naming
the corresponding C# method/class to connect to. If not given
the name of the method/class is used.

An 'extern' keyword implies an {:axiom} attribute for functions
and methods, so their ensures clauses are assumed to be true
without proof.

In addition to the .dfy files, the user may supply
C# files (.cs) and dynamic linked libraries (.dll) on
command line. These will be passed onto the C# compiler,
the .cs files as sources, and the .dll files as references.

As part of this change the grammar was refactored some.
New productions are

- TopDecls - a list of top-level declarations.
- TopDecl - a single top-level declaration
- DeclModifiers - a list of declaration modifiers which are
  either 'abstract', 'ghost', 'static', 'protected', or 'extern'.
  They can be in any order and we diagnose duplicates.
  In addition, since they are not all allowed in all contexts,
  we check and give diagnostics if an DeclModifier appears
  where it is not allowed.

1 files changed, 29 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 4d900a1b..eb82df72 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -197,6 +197,33 @@ namespace Microsoft.Dafny
       Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));

     }

 

+    /// <summary>

+    /// Check that now two modules that are being compiled have the same CompileName.

+    /// 

+    /// This could happen if they are given the same name using the 'extern' declaration modifier.

+    /// </summary>

+    /// <param name="prog">The Dafny program being compiled.</param>

+    void CheckDupModuleNames(Program prog)

+    {

+      // Check that none of the modules have the same CompileName.

+      Dictionary<string, ModuleDefinition> compileNameMap = new Dictionary<string, ModuleDefinition>();

+      foreach (ModuleDefinition m in prog.CompileModules) {

+        if (m.IsAbstract) {

+          // the purpose of an abstract module is to skip compilation

+          continue;

+        }

+        string compileName = m.CompileName;

+        ModuleDefinition priorModDef;

+        if (compileNameMap.TryGetValue(compileName, out priorModDef)) {

+          reporter.Error(MessageSource.Resolver, m.tok, 

+            "Modules '{0}' and '{1}' both have CompileName '{2}'.",

+            priorModDef.tok.val, m.tok.val, compileName);

+        }

+        else {

+          compileNameMap.Add(compileName, m);

+        }

+      }

+    }

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       var origErrorCount = reporter.Count(ErrorLevel.Error); //TODO: This is used further below, but not in the >0 comparisons in the next few lines. Is that right?

@@ -459,6 +486,8 @@ namespace Microsoft.Dafny
           }

         }

       }

+

+      CheckDupModuleNames(prog);

     }

 

     void FillInDefaultDecreasesClauses(Program prog)