Use dafny: Uris for standard library files

Source/DafnyCore/DafnyFile.cs

@@ -1,6 +1,8 @@
 using System;
 using System.Collections.Generic;
+using System.Diagnostics;
 using System.IO;
+using System.Linq;
 using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
@@ -16,13 +18,30 @@ public class DafnyFile {
   public string BaseName { get; private set; }
   public bool IsPreverified { get; set; }
   public bool IsPrecompiled { get; set; }
-  public bool IsPrerefined { get; private set; }
   public Func<TextReader> GetContent { get; set; }
-  public Uri Uri { get; }
+  public Uri Uri { get; private set; }
   [CanBeNull] public IToken Origin { get; }
 
+  private static readonly Dictionary<Uri, Uri> ExternallyVisibleEmbeddedFiles = new();
+
+  public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
+    var externalUri = new Uri("dafny:" + externalName);
+    ExternallyVisibleEmbeddedFiles[externalUri] = internalUri;
+    return externalUri;
+  }
+
   public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
     DafnyOptions options, Uri uri, IToken origin) {
+
+    var embeddedFile = ExternallyVisibleEmbeddedFiles.GetValueOrDefault(uri);
+    if (embeddedFile != null) {
+      var result = CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin);
+      if (result != null) {
+        result.Uri = uri;
+      }
+      return result;
+    }
+
     var filePath = uri.LocalPath;
 
     origin ??= Token.NoToken;
@@ -32,7 +51,6 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
     Func<TextReader> getContent = null;
     bool isPreverified;
     bool isPrecompiled;
-    var isPrerefined = false;
     var extension = ".dfy";
     if (uri.IsFile) {
       extension = Path.GetExtension(uri.LocalPath).ToLower();
@@ -98,7 +116,7 @@ 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;
       }
 
@@ -109,7 +127,6 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
       // the DooFile class should encapsulate the serialization logic better
       // and expose a Program instead of the program text.
       getContent = () => new StringReader(dooFile.ProgramText);
-      isPrerefined = true;
     } else if (extension == ".dll") {
       isPreverified = true;
       // Technically only for C#, this is for backwards compatability
@@ -127,7 +144,6 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
     return new DafnyFile(extension, canonicalPath, baseName, getContent, uri, origin) {
       IsPrecompiled = isPrecompiled,
       IsPreverified = isPreverified,
-      IsPrerefined = isPrerefined
     };
   }
 

Source/DafnyCore/DafnyMain.cs

@@ -22,9 +22,18 @@
 namespace Microsoft.Dafny {
 
   public class DafnyMain {
-    public static readonly string StandardLibrariesDooUriBase = "dllresource://DafnyPipeline/DafnyStandardLibraries";
-    public static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
-    public static readonly Uri StandardLibrariesArithmeticDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo");
+    public static readonly Dictionary<string, Uri> standardLibrariesDooUriTarget = new();
+    public static readonly Uri StandardLibrariesDooUri = DafnyFile.ExposeInternalUri("DafnyStandardLibraries.dfy",
+      new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo"));
+    public static readonly Uri StandardLibrariesArithmeticDooUri = DafnyFile.ExposeInternalUri("DafnyStandardLibraries-arithmetic.dfy",
+      new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo"));
+
+    static DafnyMain() {
+      foreach (var target in new[] { "cs", "java", "go", "py", "js", "notarget" }) {
+        standardLibrariesDooUriTarget[target] = DafnyFile.ExposeInternalUri($"DafnyStandardLibraries-{target}.dfy",
+          new($"dllresource://DafnyPipeline/DafnyStandardLibraries-{target}.doo"));
+      }
+    }
 
     public static void MaybePrintProgram(Program program, string filename, bool afterResolver) {
       if (filename == null) {

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/DafnyCore/Rewriters/PrecedenceLinter.cs

@@ -5,21 +5,18 @@
 // SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
-using System.Collections.Generic;
+
 using System.Linq;
-using System;
-using System.Diagnostics.Contracts;
-using JetBrains.Annotations;
 using Microsoft.Boogie;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny {
 
   public class PrecedenceLinter : IRewriter {
-    private CompilationData compilation;
+    private readonly CompilationData compilation;
     // Don't perform linting on doo files in general, since the source has already been processed.
     internal override void PostResolve(ModuleDefinition moduleDefinition) {
-      if (moduleDefinition.tok.Uri != null && moduleDefinition.tok.Uri.LocalPath.EndsWith(".doo")) {
+      if (moduleDefinition.tok.Uri != null && !moduleDefinition.ShouldVerify(compilation)) {
         return;
       }
       foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {

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);
@@ -490,7 +489,7 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
       var reporter = new ConsoleErrorReporter(options);
       if (options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = options.CompilerName ?? "notarget";
-        var stdlibDooUri = new Uri($"{DafnyMain.StandardLibrariesDooUriBase}-{targetName}.doo");
+        var stdlibDooUri = DafnyMain.standardLibrariesDooUriTarget[targetName];
         options.CliRootSourceUris.Add(stdlibDooUri);
         dafnyFiles.Add(DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, stdlibDooUri, Token.Cli));
       }

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("dafny:DafnyStandardLibraries.dfy"), 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

Source/DafnyLanguageServer/Workspace/Compilation.cs

@@ -132,7 +132,7 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
     if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
       if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = Options.CompilerName ?? "notarget";
-        var stdlibDooUri = new Uri($"{DafnyMain.StandardLibrariesDooUriBase}-{targetName}.doo");
+        var stdlibDooUri = DafnyMain.standardLibrariesDooUriTarget[targetName];
         Options.CliRootSourceUris.Add(stdlibDooUri);
         result.Add(DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken));
       }