Merge branch 'master' of https://github.com/dafny-lang/dafny into std…

…lib-cleanup

# Conflicts:
#	Source/DafnyStandardLibraries/README.md
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo

.github/workflows/publish-release-reusable.yml

@@ -35,7 +35,7 @@ env:
 jobs:
 
   publish-release:
-    runs-on: ubuntu-20.04
+    runs-on: macos-latest   # Put back 'ubuntu-20.04' if macos-latest fails in any way
     steps:
     - name: Print version
       run: echo ${{ inputs.name }}

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -2690,6 +2690,8 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
           wr.Write("var ");
           PrintCasePattern(e.Lhs);
           wr.Write(" :- ");
+        } else {
+          wr.Write(":- ");
         }
         PrintExpression(e.Rhs, true);
         wr.Write("; ");

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,19 +5,20 @@
 // 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.ShouldVerify(compilation)) {
+        return;
+      }
       foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var callable in topLevelDecl.Members.OfType<ICallable>()) {
           var visitor = new PrecedenceLinterVisitor(compilation, Reporter);
@@ -107,27 +108,27 @@ protected override bool VisitOneExpr(Expression expr, ref LeftMargin st) {
       // that is, we inspect line and column information.
 
       if (expr is BinaryExpr bin && (bin.Op == BinaryExpr.Opcode.Imp || bin.Op == BinaryExpr.Opcode.Exp || bin.Op == BinaryExpr.Opcode.Iff)) {
+        // For
+        //   a)  LHS ==> RHS
+        //   b)  LHS ==>
+        //         RHS-somewhere-on-this-line
+        // use LHS.StartToken as the left margin.
+        // For
+        //   c)  LHS0 &&
+        //       LHS1 ==> RHS
+        // use expr.tok (that is, the location of ==>) as the left margin. This is bound to generate a warning.
+        // For
+        //   d)  LHS0 &&
+        //       LHS1 ==>
+        //         RHS-somewhere-on-this-line
+        //   e)  LHS0 &&
+        //       LHS1
+        //       ==>
+        //         RHS-somewhere-on-this-line
+        // use LHS.StartToken as the left margin.
         VisitLhsComponent(expr.tok, bin.E0,
-          // For
-          //   a)  LHS ==> RHS
-          //   b)  LHS ==>
-          //         RHS-somewhere-on-this-line
-          // use LHS.StartToken as the left margin.
           bin.E0.StartToken.line == expr.tok.line ? bin.E0.StartToken.col :
-          // For
-          //   c)  LHS0 &&
-          //       LHS1 ==> RHS
-          // use expr.tok (that is, the location of ==>) as the left margin. This is bound to generate a warning.
           bin.E1.StartToken.line == expr.tok.line ? expr.tok.col :
-          // For
-          //   d)  LHS0 &&
-          //       LHS1 ==>
-          //         RHS-somewhere-on-this-line
-          //   e)  LHS0 &&
-          //       LHS1
-          //       ==>
-          //         RHS-somewhere-on-this-line
-          // use LHS.StartToken as the left margin.
           bin.E0.StartToken.col,
           "left-hand operand of " + BinaryExpr.OpcodeString(bin.Op));
         VisitRhsComponent(expr.tok, bin.E1, "right-hand operand of " + BinaryExpr.OpcodeString(bin.Op));

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);
+    }
+  }
 }