Add support for the "include" keyword, which accepts a (possibly relative) path

to another Dafny file.  That file's functions and methods are included but not checked.
This is intended to support incremental verification on a per-file basis.

4 files changed, 47 insertions, 26 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index c92caf4e..5a7aad6f 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -97,8 +97,10 @@ namespace DafnyLanguage
     bool ParseAndTypeCheck() {

       Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);

       Dafny.BuiltIns builtIns = new Dafny.BuiltIns();

-      int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, module, builtIns, new VSErrors(this));

-      if (errorCount != 0)

+      Dafny.Errors parseErrors = new VSErrors(this);

+      int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, module, builtIns, parseErrors);

+      string errString = Dafny.Main.ParseIncludes(module, builtIns, parseErrors);

+      if (errorCount != 0 || errString != null)

         return false;

       Dafny.Program program = new Dafny.Program(_filename, module, builtIns);

 

@@ -112,9 +114,9 @@ namespace DafnyLanguage
       return true;  // success

     }

 

-    void RecordError(int line, int col, ErrorCategory cat, string msg)

+    void RecordError(string filename, int line, int col, ErrorCategory cat, string msg)

     {

-      _errors.Add(new DafnyError(line, col, cat, msg, _snapshot));

+      _errors.Add(new DafnyError(filename, line, col, cat, msg, _snapshot, null, System.IO.Path.GetFullPath(this._filename) == filename));

     }

 

     class VSErrors : Dafny.Errors

@@ -124,15 +126,15 @@ namespace DafnyLanguage
         this.dd = dd;

       }

       public override void SynErr(string filename, int line, int col, string msg) {

-        dd.RecordError(line - 1, col - 1, ErrorCategory.ParseError, msg);

+        dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ParseError, msg);

         count++;

       }

       public override void SemErr(string filename, int line, int col, string msg) {

-        dd.RecordError(line - 1, col - 1, ErrorCategory.ResolveError, msg);

+        dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ResolveError, msg);

         count++;

       }

       public override void Warning(string filename, int line, int col, string msg) {

-        dd.RecordError(line - 1, col - 1, ErrorCategory.ParseWarning, msg);

+        dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ParseWarning, msg);

       }

     }

 

@@ -159,7 +161,7 @@ namespace DafnyLanguage
 

       public override void Error(Bpl.IToken tok, string msg, params object[] args) {

         string s = string.Format(msg, args);

-        dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);

+        dd.RecordError(tok.filename, tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);

         ErrorCount++;

       }

     }

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 5d26573e..f8afaf13 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -325,22 +325,22 @@ namespace DafnyLanguage
             if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))

             {

               var s = RequestIdToSnapshot[errorInfo.RequestId];

-              errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString()), errorInfo.ImplementationName, requestId);

+              errorListHolder.AddError(new DafnyError(errorInfo.Tok.filename, errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString(), System.IO.Path.GetFullPath(_document.FilePath) == errorInfo.Tok.filename), errorInfo.ImplementationName, requestId);

               foreach (var aux in errorInfo.Aux)

               {

-                errorListHolder.AddError(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s), errorInfo.ImplementationName, requestId);

+                errorListHolder.AddError(new DafnyError(aux.Tok.filename, aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s, null, System.IO.Path.GetFullPath(_document.FilePath) == aux.Tok.filename), errorInfo.ImplementationName, requestId);

               }

             }

           }

         });

         if (!success)

         {

-          errorListHolder.AddError(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error", snapshot), "$$program$$", requestId);

+          errorListHolder.AddError(new DafnyError("$$program$$", 0, 0, ErrorCategory.InternalError, "Verification process error", snapshot), "$$program$$", requestId);

         }

       }

       catch (Exception e)

       {

-        errorListHolder.AddError(new DafnyError(0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot), "$$program$$", requestId);

+        errorListHolder.AddError(new DafnyError("$$program$$", 0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot), "$$program$$", requestId);

       }

 

       lock (this) {

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 81346c77..df7878c4 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -271,7 +271,7 @@ namespace DafnyLanguage
       var currentSnapshot = spans[0].Snapshot;

       foreach (var err in AllErrors)

       {

-        if (err.Category != ErrorCategory.ProcessError)

+        if (err.Category != ErrorCategory.ProcessError && err.Filename == System.IO.Path.GetFullPath(_document.FilePath))

         {

           yield return new TagSpan<IDafnyResolverTag>(err.Span.GetSpan(currentSnapshot), new DafnyErrorResolverTag(err));

 

@@ -316,7 +316,8 @@ namespace DafnyLanguage
       if (snapshot == Snapshot)

         return;  // we've already done this snapshot

 

-      var driver = new DafnyDriver(snapshot, _document != null ? _document.FilePath : "<program>");

+      string filename = _document != null ? _document.FilePath : "<program>";

+      var driver = new DafnyDriver(snapshot, filename);

       List<DafnyError> newErrors;

       Dafny.Program program;

       try

@@ -326,7 +327,7 @@ namespace DafnyLanguage
       }

       catch (Exception e)

       {

-        newErrors = new List<DafnyError> { new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) };

+        newErrors = new List<DafnyError> { new DafnyError(filename, 0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) };

         program = null;

       }

 

@@ -359,11 +360,19 @@ namespace DafnyLanguage
           _errorProvider.SuspendRefresh();  // reduce flickering

           _errorProvider.Tasks.Clear();

           foreach (var err in AllErrors)

-          {

-            var span = err.Span.GetSpan(snapshot);

-            var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

-            var line = snapshot.GetLineFromPosition(span.Start.Position);

-            var columnNum = span.Start - line.Start;

+          { 

+            var lineNum = 0;

+            var columnNum = 0;

+            if (err.Span != null) {

+              var span = err.Span.GetSpan(snapshot);

+              lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

+              var line = snapshot.GetLineFromPosition(span.Start.Position);

+              columnNum = span.Start - line.Start;

+            } else {

+              lineNum = err.Line;

+              columnNum = err.Column;

+            }

+            

             ErrorTask task = new ErrorTask()

             {

               Category = TaskCategory.BuildCompile,

@@ -372,7 +381,10 @@ namespace DafnyLanguage
               Line = lineNum,

               Column = columnNum

             };

-            if (_document != null)

+            if (err.Filename != null) {

+              task.Document = err.Filename;

+            } 

+            else if (_document != null)

             {

               task.Document = _document.FilePath;

             }

@@ -470,6 +482,7 @@ namespace DafnyLanguage
 

   public class DafnyError

   {

+    public readonly string Filename;

     public readonly int Line;  // 0 based

     public readonly int Column;  // 0 based

     public readonly ErrorCategory Category;

@@ -562,17 +575,22 @@ namespace DafnyLanguage
     /// <summary>

     /// "line" and "col" are expected to be 0-based

     /// </summary>

-    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, string model = null)

+    public DafnyError(string filename, int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, string model = null, bool inCurrentDocument=true)

     {

+      Filename = filename;

       Line = Math.Max(0, line);

       Column = Math.Max(0, col);

       Category = cat;

       Message = msg;

       Snapshot = snapshot;

-      var sLine = snapshot.GetLineFromLineNumber(line);

-      Contract.Assert(Column <= sLine.Length);

-      var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

-      Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

+      if (inCurrentDocument) {

+        var sLine = snapshot.GetLineFromLineNumber(line);

+        Contract.Assert(Column <= sLine.Length);

+        var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

+        Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

+      } else {

+        Span = null;

+      }

       ModelText = model;

       _errorSelection = _errorSelectionSingleton;

       SelectedStateId = -1;

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index b019db0a..3999db1e 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -282,6 +282,7 @@ namespace DafnyLanguage
                 case "if":

                 case "import":

                 case "in":

+                case "include":

                 case "int":

                 case "invariant":

                 case "iterator":