Use dafny: Uris for standard library files

Source/DafnyCore/DafnyFile.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
+using System.Linq;
 using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
@@ -23,6 +24,13 @@ public class DafnyFile {
 
   public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
     DafnyOptions options, Uri uri, IToken origin) {
+
+    if (uri.Scheme == "doo") {
+      var uriString = uri.ToString();
+      var dots = uriString.Substring("doo://".Length).Split(".");
+      uri = new Uri(dots[0] + "://" + string.Join('.', dots.Skip(1)));
+    }
+
     var filePath = uri.LocalPath;
 
     origin ??= Token.NoToken;
@@ -98,10 +106,12 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
         dooFile = DooFile.Read(filePath);
       }
 
-      if (!dooFile.Validate(reporter, filePathForErrors, options, options.CurrentCommand, origin)) {
+      if (!dooFile.Validate(reporter, filePathForErrors, options, origin)) {
         return null;
       }
 
+      uri = new Uri("doo://" + uri.ToString().Replace("://", "."));
+
       // For now it's simpler to let the rest of the pipeline parse the
       // program text back into the AST representation.
       // At some point we'll likely want to serialize a program

Source/DafnyCore/DafnyOptions.cs

@@ -42,7 +42,6 @@ public class DafnyOptions : Bpl.CommandLineOptions {
     public IList<Uri> CliRootSourceUris = new List<Uri>();
 
     public DafnyProject DafnyProject { get; set; }
-    public Command CurrentCommand { get; set; }
 
     public static void ParseDefaultFunctionOpacity(Option<CommonOptionBag.DefaultFunctionOpacityOptions> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
       if (ps.ConfirmArgumentCount(1)) {

Source/DafnyCore/DooFile.cs

@@ -116,11 +116,10 @@ public DooFile(Program dafnyProgram) {
   private DooFile() {
   }
 
-  public bool Validate(ErrorReporter reporter, string filePath, DafnyOptions options, Command currentCommand,
-    IToken origin) {
-    if (currentCommand == null) {
+  public bool Validate(ErrorReporter reporter, string filePath, DafnyOptions options, IToken origin) {
+    if (!options.UsingNewCli) {
       reporter.Error(MessageSource.Project, origin,
-        $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
+        $"cannot load {filePath}: .doo files cannot be used with the legacy CLI");
       return false;
     }
 
@@ -131,7 +130,7 @@ public bool Validate(ErrorReporter reporter, string filePath, DafnyOptions optio
     }
 
     var success = true;
-    var relevantOptions = currentCommand.Options.ToHashSet();
+    var relevantOptions = options.Options.OptionArguments.Keys.ToHashSet();
     foreach (var (option, check) in OptionChecks) {
       // It's important to only look at the options the current command uses,
       // because other options won't be initialized to the correct default value.

Source/DafnyCore/Generic/Reporting.cs

@@ -68,7 +68,7 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri
 
         Options.OutputWriter.Write(errorLine);
 
-        if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok != Token.NoToken) {
+        if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok.Uri != null) {
           TextWriter tw = new StringWriter();
           new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
           Options.OutputWriter.Write(tw.ToString());

Source/DafnyDriver/Commands/DafnyCli.cs

@@ -198,7 +198,6 @@ async Task Handle(InvocationContext context) {
         }
       }
 
-      dafnyOptions.CurrentCommand = command;
       dafnyOptions.ApplyDefaultOptionsWithoutSettingsDefault();
       dafnyOptions.UsingNewCli = true;
       context.ExitCode = await continuation(dafnyOptions, context);

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -27,6 +27,7 @@
   <ItemGroup>
     <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
+    <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -106,7 +106,8 @@ private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions
       var dafnyOptions = DafnyOptions.Create(output);
       dafnyOptions.Set(ProjectManager.UpdateThrottling, 0);
       modifyOptions?.Invoke(dafnyOptions);
-      Microsoft.Dafny.LanguageServer.LanguageServer.ConfigureDafnyOptionsForServer(dafnyOptions);
+      dafnyOptions.UsingNewCli = true;
+      LanguageServer.ConfigureDafnyOptionsForServer(dafnyOptions);
       ApplyDefaultOptionValues(dafnyOptions);
       return options => {
         options.WithDafnyLanguageServer(() => { });

Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs

@@ -104,24 +104,6 @@ requires Err?
       await AssertPositionsLineUpWithRanges(source);
     }
 
-    /// <summary>
-    /// Given <paramref name="source"/> with N positions, for each K from 0 to N exclusive,
-    /// assert that a RequestDefinition at position K
-    /// returns either the Kth range, or the range with key K (as a string).
-    /// </summary>
-    private async Task AssertPositionsLineUpWithRanges(string source) {
-      MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource,
-        out var positions, out var ranges);
-
-      var documentItem = await CreateOpenAndWaitForResolve(cleanSource);
-      for (var index = 0; index < positions.Count; index++) {
-        var position = positions[index];
-        var range = ranges.ContainsKey(string.Empty) ? ranges[string.Empty][index] : ranges[index.ToString()].Single();
-        var result = (await RequestDefinition(documentItem, position)).Single();
-        Assert.Equal(range, result.Location!.Range);
-      }
-    }
-
     [Fact]
     public async Task StaticFunctionCall() {
       var source = @"

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -425,4 +425,22 @@ protected async Task<TextDocumentItem> GetDocumentItem(string source, string fil
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
     return documentItem;
   }
+
+  /// <summary>
+  /// Given <paramref name="source"/> with N positions, for each K from 0 to N exclusive,
+  /// assert that a RequestDefinition at position K
+  /// returns either the Kth range, or the range with key K (as a string).
+  /// </summary>
+  protected async Task AssertPositionsLineUpWithRanges(string source, string filePath = null) {
+    MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource,
+      out var positions, out var ranges);
+
+    var documentItem = await CreateOpenAndWaitForResolve(cleanSource, filePath);
+    for (var index = 0; index < positions.Count; index++) {
+      var position = positions[index];
+      var range = ranges.ContainsKey(string.Empty) ? ranges[string.Empty][index] : ranges[index.ToString()].Single();
+      var result = (await RequestDefinition(documentItem, position)).Single();
+      Assert.Equal(range, result.Location!.Range);
+    }
+  }
 }

Source/DafnyLanguageServer.Test/Various/StandardLibraryTest.cs

@@ -0,0 +1,70 @@
+using System;
+using System.IO;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
+
+public class StandardLibraryTest : ClientBasedLanguageServerTest {
+  [Fact]
+  public async Task CanUseWrappers() {
+    var source = @"
+import opened DafnyStdLibs.Wrappers
+
+const triggerSemicolonWarning := 3;
+
+method Foo() returns (s: Option<int>) { 
+  return Some(3); 
+}".TrimStart();
+
+    var projectSource = @"
+[options]
+standard-libraries = true";
+
+    var withoutStandardLibraries = CreateAndOpenTestDocument(source);
+    var diagnostics1 = await GetLastDiagnostics(withoutStandardLibraries, DiagnosticSeverity.Error);
+    Assert.Single(diagnostics1);
+
+    var directory = Path.GetTempFileName();
+    CreateAndOpenTestDocument(projectSource, Path.Combine(directory, DafnyProject.FileName));
+    var document = CreateAndOpenTestDocument(source, Path.Combine(directory, "document.dfy"));
+    var diagnostics2 = await GetLastDiagnostics(document);
+    Assert.Single(diagnostics2);
+    Assert.Equal(DiagnosticSeverity.Warning, diagnostics2[0].Severity);
+  }
+
+  [Fact]
+  public async Task GotoDefinition() {
+    var source = @"
+import opened DafnyStdLibs.Wrappers
+
+method Foo() returns (s: ><Option<int>) { 
+  return Some(3); 
+}".TrimStart();
+
+    var projectSource = @"
+[options]
+standard-libraries = true";
+
+    var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+    Directory.CreateDirectory(directory);
+    await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectSource);
+
+    MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource,
+      out var positions, out var ranges);
+
+    var filePath = Path.Combine(directory, "StandardLibraryGotoDefinition.dfy");
+    var documentItem = CreateAndOpenTestDocument(cleanSource, filePath);
+    await AssertNoDiagnosticsAreComing(CancellationToken);
+    var result = await RequestDefinition(documentItem, positions[0]);
+    Assert.Equal(new Uri("doo://dllresource.dafnypipeline/DafnyStandardLibraries.doo"), result.Single().Location.Uri);
+  }
+
+  public StandardLibraryTest(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) {
+  }
+}

Source/DafnyLanguageServer/Language/DafnyLangParser.cs

@@ -39,20 +39,7 @@ public Program Parse(Compilation compilation, CancellationToken cancellationToke
 
       var beforeParsing = DateTime.Now;
       try {
-        var rootFiles = compilation.RootFiles!;
-        List<DafnyFile> dafnyFiles = new();
-        foreach (var rootFile in rootFiles) {
-          try {
-            dafnyFiles.Add(rootFile);
-            if (logger.IsEnabled(LogLevel.Trace)) {
-              logger.LogTrace($"Parsing file with uri {rootFile.Uri} and content\n{rootFile.GetContent().ReadToEnd()}");
-            }
-          } catch (IOException) {
-            logger.LogError($"Tried to parse file {rootFile} that could not be found");
-          }
-        }
-
-        return programParser.ParseFiles(compilation.Project.ProjectName, dafnyFiles, compilation.Reporter, cancellationToken);
+        return programParser.ParseFiles(compilation.Project.ProjectName, compilation.RootFiles, compilation.Reporter, cancellationToken);
       }
       finally {
         telemetryPublisher.PublishTime("Parse", compilation.Project.Uri.ToString(), DateTime.Now - beforeParsing);

Source/DafnyLanguageServer/LanguageServer.cs

@@ -47,7 +47,6 @@ related locations
 
     public static void ConfigureDafnyOptionsForServer(DafnyOptions dafnyOptions) {
       dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, true);
-
       dafnyOptions.PrintIncludesMode = DafnyOptions.IncludesModes.None;
 
       // TODO This may be subject to change. See Microsoft.Boogie.Counterexample